---

Step * 1 1 of Lemma circle-param-onto


1. p : ℝ^2
2. r(-1) < (p 0)
3. r2-unit-circle(p)
4. r0 < ((p 0) + r1)
⊢ req-vec(2;circle-param((p 1/(p 0) + r1));p)
BY
{ (MoveToConcl (-1) THEN (GenConcl ⌜((p 0) + r1) = x1 ∈ ℝ⌝⋅ THENA Auto)) }

1
1. p : ℝ^2
2. r(-1) < (p 0)
3. r2-unit-circle(p)
4. x1 : ℝ
5. ((p 0) + r1) = x1 ∈ ℝ
⊢ (r0 < x1) ⇒ req-vec(2;circle-param((p 1/x1));p)

---

Latex:

---

Latex:

1.  p  :  \mBbbR{}\^{}2
2.  r(-1)  <  (p  0)
3.  r2-unit-circle(p)
4.  r0  <  ((p  0)  +  r1)
\mvdash{}  req-vec(2;circle-param((p  1/(p  0)  +  r1));p)


By

---

Latex:
(MoveToConcl  (-1)  THEN  (GenConcl  \mkleeneopen{}((p  0)  +  r1)  =  x1\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index