---

Step * 2 1 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 : 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)]
BY
{ ((InstLemma `Euclid-Prop1-left` [⌜e⌝;⌜d⌝;⌜d'⌝]⋅ THENA Auto)
   THEN D -1
   THEN RenameVar `p' (-2)
   THEN D 0 With ⌜p⌝ 
   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. qd ≅ d'd
15. qd' ≅ dd'
16. qd' ≅ qd
17. q leftof d'd
18. p : Point
19. pd' ≅ dd'
20. pd ≅ d'd
21. pd ≅ pd'
22. p leftof dd'
⊢ ab  ⊥c pc

2
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. qd ≅ d'd
15. qd' ≅ dd'
16. qd' ≅ qd
17. q leftof d'd
18. p : Point
19. pd' ≅ dd'
20. pd ≅ d'd
21. pd ≅ pd'
22. p leftof dd'
23. ab  ⊥c pc
⊢ ab  ⊥c qc

3
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. qd ≅ d'd
15. qd' ≅ dd'
16. qd' ≅ qd
17. q leftof d'd
18. p : Point
19. pd' ≅ dd'
20. pd ≅ d'd
21. pd ≅ pd'
22. p leftof dd'
23. ab  ⊥c pc
24. ab  ⊥c qc
25. 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.  d  :  Point
6.  d'  :  Point
7.  d  \mneq{}  c
8.  d\_c\_d'
9.  dc  \mcong{}  cd'
10.  Colinear(a;b;d)
11.  \mforall{}x:Point.  (x  leftof  ab  \mLeftarrow{}{}\mRightarrow{}  x  leftof  dd')
12.  d  \mneq{}  d'
13.  q  :  Point
14.  [\%14]  :  ((qd  \mcong{}  d'd  \mwedge{}  qd'  \mcong{}  dd')  \mwedge{}  qd'  \mcong{}  qd)  \mwedge{}  q  leftof  d'd
\mvdash{}  \mexists{}p:Point  [(ab    \mbot{}c  pc  \mwedge{}  ab    \mbot{}c  qc  \mwedge{}  p  leftof  ab  \mwedge{}  q  leftof  ba)]


By

---

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

---

Home Index