---

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


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 ))
BY
{ ((Assert (-(x 1)/||x||) ≠ r0 BY
          (D -2 THEN Auto))
   THEN D 0 With ⌜(y 0/(-(x 1)/||x||))⌝ 
   THEN Auto
   THEN IntSegCases (-1)
   THEN Reduce 0) }

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 ∈ ℤ
10. (-(x 1)/||x||) ≠ r0
11. i1 : ℤ
12. i1 = 0 ∈ ℤ
⊢ (y 0) = ((y 0/(-(x 1)/||x||)) * (-(x 1)/||x||))

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 1)/||x||)
9. i = 0 ∈ ℤ
10. (-(x 1)/||x||) ≠ r0
11. i1 : ℤ
12. i1 = 1 ∈ ℤ
⊢ (y 1) = ((y 0/(-(x 1)/||x||)) * (x 0/||x||))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}\^{}2
2.  r0  <  ||x||
3.  y  :  \mBbbR{}\^{}2
4.  y\mcdot{}x  =  r0
5.  ||r2-perp(x)||  =  r1
6.  r0  <  ||r2-perp(x)||
7.  i  :  \mBbbZ{}
8.  r0  \mneq{}  (-(x  1)/||x||)
9.  i  =  0
\mvdash{}  \mexists{}t:\mBbbR{}.  \mforall{}i:\mBbbN{}2.  ((y  i)  =  (t  *  if  (i  =\msubz{}  0)  then  (-(x  1)/||x||)  else  (x  0/||x||)  fi  ))


By

---

Latex:
((Assert  (-(x  1)/||x||)  \mneq{}  r0  BY
                (D  -2  THEN  Auto))
  THEN  D  0  With  \mkleeneopen{}(y  0/(-(x  1)/||x||))\mkleeneclose{} 
  THEN  Auto
  THEN  IntSegCases  (-1)
  THEN  Reduce  0)

---

Home Index