---

Step * of Lemma Cauchy-Schwarz-non-equality1

∀n:ℕ. ∀x,y:ℝ^n.  ((r0 < ||y||) ⇒ (∀a:ℝ. x ≠ a*y) ⇒ (|x⋅y| < (||x|| * ||y||)))
BY
{ (Auto
   THEN (RWO "Cauchy-Schwarz-strict<" 0 THENA Auto)
   THEN (FLemma `real-vec-norm-positive-iff` [4]⋅ THENA Auto)
   THEN ExRepD
   THEN RenameVar `j' (-2)) }

1
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)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}x,y:\mBbbR{}\^{}n.    ((r0  <  ||y||)  {}\mRightarrow{}  (\mforall{}a:\mBbbR{}.  x  \mneq{}  a*y)  {}\mRightarrow{}  (|x\mcdot{}y|  <  (||x||  *  ||y||)))


By

---

Latex:
(Auto
  THEN  (RWO  "Cauchy-Schwarz-strict<"  0  THENA  Auto)
  THEN  (FLemma  `real-vec-norm-positive-iff`  [4]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  RenameVar  `j'  (-2))

---

Home Index