---

Step * 3 of Lemma opp-side_half-plane-angle-congruence-lemma


1. e : EuclideanPlane
2. b : Point
3. p : Point
4. b' : Point
5. p' : Point
6. a : Point
7. c : Point
8. a' : Point
9. c' : Point
10. d : Point
11. a leftof bp
12. c leftof pb
13. a' leftof b'p'
14. c' leftof p'b'
15. abp ≅a a'b'p'
16. pbc ≅a p'b'c'
17. a-d-c
18. out(b dp)
19. b ≠ d
20. ∃a'',c'':Point. ((out(b' a'a'') ∧ out(b' c'c'')) ∧ ba ≅ b'a'' ∧ bc ≅ b'c'')
⊢ ∃a'',c'',d'':Point
   ((ba ≅ b'a'' ∧ (bc ≅ b'c'' ∧ bd ≅ b'd'') ∧ ad ≅ a''d'' ∧ dc ≅ d''c'' ∧ out(b' d''p')) ∧ a''_d''_c'')
BY
{ (Assert ∃d'':Point. ((out(b' d''p') ∧ b' ≠ d'') ∧ b'd'' ≅ bd) BY
         (((gProperProlong ⌜p'⌝⌜b'⌝`D'⌜a'⌝⌜b'⌝⋅ THENA Auto) THEN (gProperProlong ⌜D⌝⌜b'⌝`d\'\''⌜b⌝⌜d⌝⋅ THENA Auto))
          THEN InstConcl [⌜d''⌝]⋅
          THEN Auto)) }

1
1. e : EuclideanPlane
2. b : Point
3. p : Point
4. b' : Point
5. p' : Point
6. a : Point
7. c : Point
8. a' : Point
9. c' : Point
10. d : Point
11. a leftof bp
12. c leftof pb
13. a' leftof b'p'
14. c' leftof p'b'
15. abp ≅a a'b'p'
16. pbc ≅a p'b'c'
17. a-d-c
18. out(b dp)
19. b ≠ d
20. ∃a'',c'':Point. ((out(b' a'a'') ∧ out(b' c'c'')) ∧ ba ≅ b'a'' ∧ bc ≅ b'c'')
21. D : Point
22. p'-b'-D
23. b'D ≅ a'b'
24. d'' : Point
25. D-b'-d''
26. b'd'' ≅ bd
⊢ out(b' d''p')

2
1. e : EuclideanPlane
2. b : Point
3. p : Point
4. b' : Point
5. p' : Point
6. a : Point
7. c : Point
8. a' : Point
9. c' : Point
10. d : Point
11. a leftof bp
12. c leftof pb
13. a' leftof b'p'
14. c' leftof p'b'
15. abp ≅a a'b'p'
16. pbc ≅a p'b'c'
17. a-d-c
18. out(b dp)
19. b ≠ d
20. ∃a'',c'':Point. ((out(b' a'a'') ∧ out(b' c'c'')) ∧ ba ≅ b'a'' ∧ bc ≅ b'c'')
21. ∃d'':Point. ((out(b' d''p') ∧ b' ≠ d'') ∧ b'd'' ≅ bd)
⊢ ∃a'',c'',d'':Point
   ((ba ≅ b'a'' ∧ (bc ≅ b'c'' ∧ bd ≅ b'd'') ∧ ad ≅ a''d'' ∧ dc ≅ d''c'' ∧ out(b' d''p')) ∧ a''_d''_c'')

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  b  :  Point
3.  p  :  Point
4.  b'  :  Point
5.  p'  :  Point
6.  a  :  Point
7.  c  :  Point
8.  a'  :  Point
9.  c'  :  Point
10.  d  :  Point
11.  a  leftof  bp
12.  c  leftof  pb
13.  a'  leftof  b'p'
14.  c'  leftof  p'b'
15.  abp  \mcong{}\msuba{}  a'b'p'
16.  pbc  \mcong{}\msuba{}  p'b'c'
17.  a-d-c
18.  out(b  dp)
19.  b  \mneq{}  d
20.  \mexists{}a'',c'':Point.  ((out(b'  a'a'')  \mwedge{}  out(b'  c'c''))  \mwedge{}  ba  \mcong{}  b'a''  \mwedge{}  bc  \mcong{}  b'c'')
\mvdash{}  \mexists{}a'',c'',d'':Point
      ((ba  \mcong{}  b'a''  \mwedge{}  (bc  \mcong{}  b'c''  \mwedge{}  bd  \mcong{}  b'd'')  \mwedge{}  ad  \mcong{}  a''d''  \mwedge{}  dc  \mcong{}  d''c''  \mwedge{}  out(b'  d''p'))
      \mwedge{}  a''\_d''\_c'')


By

---

Latex:
(Assert  \mexists{}d'':Point.  ((out(b'  d''p')  \mwedge{}  b'  \mneq{}  d'')  \mwedge{}  b'd''  \mcong{}  bd)  BY
              (((gProperProlong  \mkleeneopen{}p'\mkleeneclose{}\mkleeneopen{}b'\mkleeneclose{}`D'\mkleeneopen{}a'\mkleeneclose{}\mkleeneopen{}b'\mkleeneclose{}\mcdot{}  THENA  Auto)
                  THEN  (gProperProlong  \mkleeneopen{}D\mkleeneclose{}\mkleeneopen{}b'\mkleeneclose{}`d\mbackslash{}'\mbackslash{}''\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}d\mkleeneclose{}\mcdot{}  THENA  Auto)
                  )
                THEN  InstConcl  [\mkleeneopen{}d''\mkleeneclose{}]\mcdot{}
                THEN  Auto))

---

Home Index