---

Step * of Lemma r2-straightedge-compass-simple1

No Annotations
∀c,d,a:ℝ^2. ∀b:{b:ℝ^2| b ≠ a ∧ c_b_d} .  (∃u:ℝ^2 [(cu=cd ∧ a_b_u ∧ (b ≠ d ⇒ b ≠ u))])
BY
{ (InstLemma `r2-straightedge-compass-ext` [] THEN RepeatFor 4 (ParallelLast')) }

1
1. c : ℝ^2
2. d : ℝ^2
3. a : ℝ^2
4. b : {b:ℝ^2| b ≠ a ∧ c_b_d} 
5. ∃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)))])
⊢ ∃u:ℝ^2 [(cu=cd ∧ a_b_u ∧ (b ≠ d ⇒ b ≠ u))]

---

Latex:

---

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


By

---

Latex:
(InstLemma  `r2-straightedge-compass-ext`  []  THEN  RepeatFor  4  (ParallelLast'))

---

Home Index