Step * of Lemma real-vec-angle-lemma

n:ℕ. ∀x,z:ℝ^n.  (d(z;x) < d(z;r(-1)*x) ⇐⇒ r0 < x⋅z)
BY
(Intros
   THEN RepUR ``real-vec-dist real-vec-norm`` 0
   THEN (RWO "rsqrt-rless-iff<THENA Auto)
   THEN (RWW "dot-product-linearity1-sub.1 dot-product-linearity1-sub.2" 0⋅ THENA Auto)
   THEN (RWW "dot-product-linearity2.1 dot-product-linearity2.2" 0⋅ THENA Auto)
   THEN (Assert z⋅x⋅BY
               Auto)
   THEN (RWO "-1" THENA Auto)
   THEN nRNorm 0
   THEN Auto) }

1
1. : ℕ
2. : ℝ^n
3. : ℝ^n
4. z⋅x⋅z
5. (x⋅(r(-2) x⋅z) z⋅z) < (x⋅(r(2) x⋅z) z⋅z)
⊢ r0 < x⋅z

2
1. : ℕ
2. : ℝ^n
3. : ℝ^n
4. z⋅x⋅z
5. r0 < x⋅z
⊢ (x⋅(r(-2) x⋅z) z⋅z) < (x⋅(r(2) x⋅z) z⋅z)


Latex:


Latex:
\mforall{}n:\mBbbN{}.  \mforall{}x,z:\mBbbR{}\^{}n.    (d(z;x)  <  d(z;r(-1)*x)  \mLeftarrow{}{}\mRightarrow{}  r0  <  x\mcdot{}z)


By


Latex:
(Intros
  THEN  RepUR  ``real-vec-dist  real-vec-norm``  0
  THEN  (RWO  "rsqrt-rless-iff<"  0  THENA  Auto)
  THEN  (RWW  "dot-product-linearity1-sub.1  dot-product-linearity1-sub.2"  0\mcdot{}  THENA  Auto)
  THEN  (RWW  "dot-product-linearity2.1  dot-product-linearity2.2"  0\mcdot{}  THENA  Auto)
  THEN  (Assert  z\mcdot{}x  =  x\mcdot{}z  BY
                          Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  nRNorm  0
  THEN  Auto)




Home Index