---

Step * 1 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 < (|y j| * |-((x j/y j)*y i) + (x i)|)
⊢ r0 < |((x i) * (y j)) - (x j) * (y i)|
BY
{ ((RWO "rabs-rmul<" (-1) THENA Auto) THEN RepUR ``real-vec-mul`` -1 THEN (nRNorm (-1) THENA Auto)) }

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) * (y j)) + -((x j) * (y 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  <  (|y  j|  *  |-((x  j/y  j)*y  i)  +  (x  i)|)
\mvdash{}  r0  <  |((x  i)  *  (y  j))  -  (x  j)  *  (y  i)|


By

---

Latex:
((RWO  "rabs-rmul<"  (-1)  THENA  Auto)  THEN  RepUR  ``real-vec-mul``  -1  THEN  (nRNorm  (-1)  THENA  Auto))

---

Home Index