---

Step * 1 1 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
8. y j ≠ r0
9. x ≠ (x j/y j)*y
10. i : ℕn
11. r0 < |(x i) - (x j/y j)*y i|
⊢ r0 < |((x i) * (y j)) - (x j) * (y i)|
BY
{ (nRMul ⌜|y j|⌝ (-1)⋅ THENA EAuto 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 < (|y j| * |-((x j/y j)*y i) + (x i)|)
⊢ r0 < |((x i) * (y j)) - (x j) * (y i)|

---

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
8.  y  j  \mneq{}  r0
9.  x  \mneq{}  (x  j/y  j)*y
10.  i  :  \mBbbN{}n
11.  r0  <  |(x  i)  -  (x  j/y  j)*y  i|
\mvdash{}  r0  <  |((x  i)  *  (y  j))  -  (x  j)  *  (y  i)|


By

---

Latex:
(nRMul  \mkleeneopen{}|y  j|\mkleeneclose{}  (-1)\mcdot{}  THENA  EAuto  1)

---

Home Index