---

Step * 3 2 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'' : Point
21. c'' : Point
22. out(b' a'a'')
23. out(b' c'c'')
24. ba ≅ b'a''
25. bc ≅ b'c''
26. d'' : Point
27. out(b' d''p')
28. b' ≠ d''
29. b'd'' ≅ bd
30. ba ≅ b'a''
31. bc ≅ b'c''
32. bd ≅ b'd''
33. ad ≅ a''d''
34. dc ≅ d''c''
35. out(b' d''p')
⊢ a''_d''_c''
BY
{ ((gProperProlong ⌜a''⌝⌜d''⌝`C'⌜d⌝⌜c⌝⋅ THEN Auto)
   THEN (Assert bc ≅ b'C BY
               (InstLemma `geo-five-segment` [⌜e⌝;⌜a⌝;⌜d⌝;⌜c⌝;⌜b⌝;⌜a''⌝;⌜d''⌝;⌜C⌝;⌜b'⌝]⋅ THEN EAuto 1))
   ) }

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'' : Point
21. c'' : Point
22. out(b' a'a'')
23. out(b' c'c'')
24. ba ≅ b'a''
25. bc ≅ b'c''
26. d'' : Point
27. out(b' d''p')
28. b' ≠ d''
29. b'd'' ≅ bd
30. ba ≅ b'a''
31. bc ≅ b'c''
32. bd ≅ b'd''
33. ad ≅ a''d''
34. dc ≅ d''c''
35. out(b' d''p')
36. C : Point
37. a''-d''-C
38. d''C ≅ dc
39. bc ≅ b'C
⊢ 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.  a''  :  Point
21.  c''  :  Point
22.  out(b'  a'a'')
23.  out(b'  c'c'')
24.  ba  \mcong{}  b'a''
25.  bc  \mcong{}  b'c''
26.  d''  :  Point
27.  out(b'  d''p')
28.  b'  \mneq{}  d''
29.  b'd''  \mcong{}  bd
30.  ba  \mcong{}  b'a''
31.  bc  \mcong{}  b'c''
32.  bd  \mcong{}  b'd''
33.  ad  \mcong{}  a''d''
34.  dc  \mcong{}  d''c''
35.  out(b'  d''p')
\mvdash{}  a''\_d''\_c''


By

---

Latex:
((gProperProlong  \mkleeneopen{}a''\mkleeneclose{}\mkleeneopen{}d''\mkleeneclose{}`C'\mkleeneopen{}d\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (Assert  bc  \mcong{}  b'C  BY
                          (InstLemma  `geo-five-segment`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a''\mkleeneclose{};\mkleeneopen{}d''\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{}]\mcdot{}
                            THEN  EAuto  1
                            ))
  )

---

Home Index