---

Step * 2 of Lemma Euclid-erect-2perp


1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a ≠ b} 
4. c : {c:Point| Colinear(a;b;c)} 
5. ∃d,d':Point. (d ≠ c ∧ d=c=d' ∧ Colinear(a;b;d) ∧ (∀x:Point. (x leftof ab ⇐⇒ x leftof dd')))
⊢ ∃q:Point. (∃p:Point [(ab  ⊥c pc ∧ ab  ⊥c qc ∧ p leftof ab ∧ q leftof ba)])
BY
{ (ExRepD
   THEN D -3
   THEN (Assert d ≠ d' BY
               Auto)
   THEN (InstLemma `Euclid-Prop1-left` [⌜e⌝;⌜d'⌝;⌜d⌝]⋅ THENA Auto)
   THEN D -1
   THEN RenameVar `q' (-2)
   THEN D 0 With ⌜q⌝ 
   THEN Auto) }

1
1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a ≠ b} 
4. c : {c:Point| Colinear(a;b;c)} 
5. d : Point
6. d' : Point
7. d ≠ c
8. d_c_d'
9. dc ≅ cd'
10. Colinear(a;b;d)
11. ∀x:Point. (x leftof ab ⇐⇒ x leftof dd')
12. d ≠ d'
13. q : Point
14. [%14] : ((qd ≅ d'd ∧ qd' ≅ dd') ∧ qd' ≅ qd) ∧ q leftof d'd
⊢ ∃p:Point [(ab  ⊥c pc ∧ ab  ⊥c qc ∧ p leftof ab ∧ q leftof ba)]

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  \{b:Point|  a  \mneq{}  b\} 
4.  c  :  \{c:Point|  Colinear(a;b;c)\} 
5.  \mexists{}d,d':Point.  (d  \mneq{}  c  \mwedge{}  d=c=d'  \mwedge{}  Colinear(a;b;d)  \mwedge{}  (\mforall{}x:Point.  (x  leftof  ab  \mLeftarrow{}{}\mRightarrow{}  x  leftof  dd')))
\mvdash{}  \mexists{}q:Point.  (\mexists{}p:Point  [(ab    \mbot{}c  pc  \mwedge{}  ab    \mbot{}c  qc  \mwedge{}  p  leftof  ab  \mwedge{}  q  leftof  ba)])


By

---

Latex:
(ExRepD
  THEN  D  -3
  THEN  (Assert  d  \mneq{}  d'  BY
                          Auto)
  THEN  (InstLemma  `Euclid-Prop1-left`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  RenameVar  `q'  (-2)
  THEN  D  0  With  \mkleeneopen{}q\mkleeneclose{} 
  THEN  Auto)

---

Home Index