---

Step * 1 2 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 0/||x||)
9. i = 1 ∈ ℤ
10. (x 0/||x||) ≠ r0
11. i1 : ℤ
12. i1 = 0 ∈ ℤ
⊢ (y 0) = ((y 1/(x 0/||x||)) * (-(x 1)/||x||))
BY
{ (MoveToConcl (-3)
   THEN (GenConclTerm ⌜(x 0/||x||)⌝⋅ THEN Auto)
   THEN nRMul ⌜v⌝ 0⋅
   THEN (RWO "-2<" 0 THENA Auto)
   THEN nRMul ⌜||x||⌝ 0⋅
   THEN Auto) }

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

---

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  0/||x||)
9.  i  =  1
10.  (x  0/||x||)  \mneq{}  r0
11.  i1  :  \mBbbZ{}
12.  i1  =  0
\mvdash{}  (y  0)  =  ((y  1/(x  0/||x||))  *  (-(x  1)/||x||))


By

---

Latex:
(MoveToConcl  (-3)
  THEN  (GenConclTerm  \mkleeneopen{}(x  0/||x||)\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  nRMul  \mkleeneopen{}v\mkleeneclose{}  0\mcdot{}
  THEN  (RWO  "-2<"  0  THENA  Auto)
  THEN  nRMul  \mkleeneopen{}||x||\mkleeneclose{}  0\mcdot{}
  THEN  Auto)

---

Home Index