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


1. : ℕ
2. : ℝ^n
3. : ℝ^n
4. r0 < ||y||
5. ∀a:ℝx ≠ a*y
6. : ℕn
7. r0 ≠ j
⊢ ∃i,j:ℕn. (x j) (y i) ≠ (x i) (y j)
BY
((Assert 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 -1) }

1
1. : ℕ
2. : ℝ^n
3. : ℝ^n
4. r0 < ||y||
5. ∀a:ℝx ≠ a*y
6. : ℕn
7. r0 ≠ j
8. j ≠ r0
9. x ≠ (x j/y j)*y
10. : ℕ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