---

Step * of Lemma r2-straightedge-compass-ext

∀c,d,a:ℝ^2. ∀b:{b:ℝ^2| b ≠ a ∧ c_b_d} .
  ∃u:{u:ℝ^2| cu=cd ∧ a_b_u} 
   (∃v:ℝ^2 [(cv=cd ∧ v_b_u ∧ (¬((¬a_b_v) ∧ (¬b_v_a) ∧ (¬v_a_b))) ∧ (b ≠ d ⇒ (v ≠ u ∧ u ≠ b ∧ v ≠ b)))])
BY
{ (Intros
   THEN UseWitness ⌜let t = d(λi.if (i =z 0) then |d(c;d) + d(c;b)| + r1 else r0 fi ;λi.r0) in
                     let p = (d(b;a) + t/d(b;a))*a + (-(t)/d(b;a))*b in
                     let u,v = rvlinecircle0(2;c;d;b;p) 
                     in <v, u>⌝⋅
   ) }

1
1. c : ℝ^2
2. d : ℝ^2
3. a : ℝ^2
4. b : {b:ℝ^2| b ≠ a ∧ c_b_d} 
⊢ let t = d(λi.if (i =z 0) then |d(c;d) + d(c;b)| + r1 else r0 fi ;λi.r0) in
   let p = (d(b;a) + t/d(b;a))*a + (-(t)/d(b;a))*b in
   let u,v = rvlinecircle0(2;c;d;b;p) 
   in <v, u> ∈ ∃u:{u:ℝ^2| cu=cd ∧ a_b_u} 
                (∃v:ℝ^2 [(cv=cd ∧ v_b_u ∧ (¬((¬a_b_v) ∧ (¬b_v_a) ∧ (¬v_a_b))) ∧ (b ≠ d ⇒ (v ≠ u ∧ u ≠ b ∧ v ≠ b)))])

---

Latex:

---

Latex:
\mforall{}c,d,a:\mBbbR{}\^{}2.  \mforall{}b:\{b:\mBbbR{}\^{}2|  b  \mneq{}  a  \mwedge{}  c\_b\_d\}  .
    \mexists{}u:\{u:\mBbbR{}\^{}2|  cu=cd  \mwedge{}  a\_b\_u\} 
      (\mexists{}v:\mBbbR{}\^{}2  [(cv=cd
                      \mwedge{}  v\_b\_u
                      \mwedge{}  (\mneg{}((\mneg{}a\_b\_v)  \mwedge{}  (\mneg{}b\_v\_a)  \mwedge{}  (\mneg{}v\_a\_b)))
                      \mwedge{}  (b  \mneq{}  d  {}\mRightarrow{}  (v  \mneq{}  u  \mwedge{}  u  \mneq{}  b  \mwedge{}  v  \mneq{}  b)))])


By

---

Latex:
(Intros
  THEN  UseWitness  \mkleeneopen{}let  t  =  d(\mlambda{}i.if  (i  =\msubz{}  0)  then  |d(c;d)  +  d(c;b)|  +  r1  else  r0  fi  ;\mlambda{}i.r0)  in
                                      let  p  =  (d(b;a)  +  t/d(b;a))*a  +  (-(t)/d(b;a))*b  in
                                      let  u,v  =  rvlinecircle0(2;c;d;b;p) 
                                      in  <v,  u>\mkleeneclose{}\mcdot{}
  )

---

Home Index