---

Step * 1 1 1 1 1 of Lemma Cauchy-Schwarz1-strict


1. n : ℕ
2. x : ℕn + 1 ⟶ ℝ
3. y : ℕn + 1 ⟶ ℝ
4. ∃i,j:ℕn + 1. x[j] * y[i] ≠ x[i] * y[j]
5. i : ℤ
6. 0 ≤ i
7. i ≤ n
8. i1 : ℤ
9. 0 ≤ i1
10. i1 ≤ n
⊢ ((((x[i] * x[i]) * y[i1] * y[i1]) + ((y[i] * y[i]) * x[i1] * x[i1])) - r(2) * (x[i] * y[i]) * x[i1] * y[i1])
= (x[i1] * y[i]) - x[i] * y[i1]^2
BY
{ (RWO "rnexp2" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  x  :  \mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}
3.  y  :  \mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}
4.  \mexists{}i,j:\mBbbN{}n  +  1.  x[j]  *  y[i]  \mneq{}  x[i]  *  y[j]
5.  i  :  \mBbbZ{}
6.  0  \mleq{}  i
7.  i  \mleq{}  n
8.  i1  :  \mBbbZ{}
9.  0  \mleq{}  i1
10.  i1  \mleq{}  n
\mvdash{}  ((((x[i]  *  x[i])  *  y[i1]  *  y[i1])  +  ((y[i]  *  y[i])  *  x[i1]  *  x[i1]))  -  r(2)
*  (x[i]  *  y[i])
*  x[i1]
*  y[i1])
=  (x[i1]  *  y[i])  -  x[i]  *  y[i1]\^{}2


By

---

Latex:
(RWO  "rnexp2"  0  THEN  Auto)

---

Home Index