---

Step * 1 of Lemma r2-dot-product-eq-0-iff-perp


1. x : ℝ^2
2. r0 < ||x||
3. y : ℝ^2
4. y⋅x = r0
⊢ ∃t:ℝ. req-vec(2;y;t*r2-perp(x))
BY
{ ((Assert ||r2-perp(x)|| = r1 BY
          (GenConclTerm ⌜r2-perp(x)⌝⋅ THEN Auto))
   THEN (Assert r0 < ||r2-perp(x)|| BY
               (RWO "-1" 0 THEN Auto))
   THEN (FLemma `real-vec-norm-positive-iff` [-1]⋅ THENA Auto)
   THEN D -1
   THEN IntSegCases (-2)
   THEN HypSubst' (-1) (-2)
   THEN RepUR ``req-vec r2-perp real-vec-mul`` 0
   THEN RepUR ``r2-perp`` -2) }

1
1. x : ℝ^2
2. r0 < ||x||
3. y : ℝ^2
4. y⋅x = r0
5. ||r2-perp(x)|| = r1
6. r0 < ||r2-perp(x)||
7. i : ℤ
8. r0 ≠ (-(x 1)/||x||)
9. i = 0 ∈ ℤ
⊢ ∃t:ℝ. ∀i:ℕ2. ((y i) = (t * if (i =z 0) then (-(x 1)/||x||) else (x 0/||x||) fi ))

2
1. x : ℝ^2
2. r0 < ||x||
3. y : ℝ^2
4. y⋅x = r0
5. ||r2-perp(x)|| = r1
6. r0 < ||r2-perp(x)||
7. i : ℤ
8. r0 ≠ (x 0/||x||)
9. i = 1 ∈ ℤ
⊢ ∃t:ℝ. ∀i:ℕ2. ((y i) = (t * if (i =z 0) then (-(x 1)/||x||) else (x 0/||x||) fi ))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}\^{}2
2.  r0  <  ||x||
3.  y  :  \mBbbR{}\^{}2
4.  y\mcdot{}x  =  r0
\mvdash{}  \mexists{}t:\mBbbR{}.  req-vec(2;y;t*r2-perp(x))


By

---

Latex:
((Assert  ||r2-perp(x)||  =  r1  BY
                (GenConclTerm  \mkleeneopen{}r2-perp(x)\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  r0  <  ||r2-perp(x)||  BY
                          (RWO  "-1"  0  THEN  Auto))
  THEN  (FLemma  `real-vec-norm-positive-iff`  [-1]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  IntSegCases  (-2)
  THEN  HypSubst'  (-1)  (-2)
  THEN  RepUR  ``req-vec  r2-perp  real-vec-mul``  0
  THEN  RepUR  ``r2-perp``  -2)

---

Home Index