---

Step * 1 1 2 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 ∈ ℤ
10. (-(x 1)/||x||) ≠ r0
11. i1 : ℤ
12. i1 = 1 ∈ ℤ
⊢ (y 1) = ((y 0/(-(x 1)/||x||)) * (x 0/||x||))
BY
{ (MoveToConcl (-3)
   THEN (GenConclTerm ⌜(-(x 1)/||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 1)/||x||)
9. i = 0 ∈ ℤ
10. i1 : ℤ
11. i1 = 1 ∈ ℤ
12. v : ℝ
13. (-(x 1)/||x||) = v ∈ ℝ
14. v ≠ r0
⊢ -((x 1) * (y 1)) = ((x 0) * (y 0))

---

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


By

---

Latex:
(MoveToConcl  (-3)
  THEN  (GenConclTerm  \mkleeneopen{}(-(x  1)/||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