---

Step * 1 of Lemma Cauchy-Schwarz-non-equality1


1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
4. r0 < ||y||
5. ∀a:ℝ. x ≠ a*y
6. j : ℕn
7. r0 ≠ y j
⊢ ∃i,j:ℕn. (x j) * (y i) ≠ (x i) * (y j)
BY
{ ((Assert y j ≠ r0 BY
          (BLemma `rneq-symmetry` THEN Auto))
   THEN (InstHyp [⌜(x j/y j)⌝] 5⋅ THENA Auto)
   THEN (FLemma `real-vec-sep-iff` [-1] THENA Auto)
   THEN D -1) }

1
1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
4. r0 < ||y||
5. ∀a:ℝ. x ≠ a*y
6. j : ℕn
7. r0 ≠ y j
8. y j ≠ r0
9. x ≠ (x j/y j)*y
10. i : ℕn
11. r0 < |(x i) - (x j/y j)*y i|
⊢ ∃i,j:ℕn. (x j) * (y i) ≠ (x i) * (y j)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  x  :  \mBbbR{}\^{}n
3.  y  :  \mBbbR{}\^{}n
4.  r0  <  ||y||
5.  \mforall{}a:\mBbbR{}.  x  \mneq{}  a*y
6.  j  :  \mBbbN{}n
7.  r0  \mneq{}  y  j
\mvdash{}  \mexists{}i,j:\mBbbN{}n.  (x  j)  *  (y  i)  \mneq{}  (x  i)  *  (y  j)


By

---

Latex:
((Assert  y  j  \mneq{}  r0  BY
                (BLemma  `rneq-symmetry`  THEN  Auto))
  THEN  (InstHyp  [\mkleeneopen{}(x  j/y  j)\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  (FLemma  `real-vec-sep-iff`  [-1]  THENA  Auto)
  THEN  D  -1)

---

Home Index