---

Step * 1 1 1 of Lemma angle-bisector-unique


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. c' : Point
7. x : Point
8. y : Point
9. a # bc
10. out(b aa')
11. out(b cc')
12. a-x-c
13. a'-y-c'
14. abx ≅a cbx
15. a'by ≅a c'by
16. x' : Point
17. a-x'-c
18. out(b yx')
19. a'by ≅a abx'
20. c'by ≅a cbx'
21. C : Point
22. c-b-C
23. bC ≅ OX
24. c'' : Point
25. C-b-c''
26. bc'' ≅ ba
27. out(b cc'')
28. z : Point
29. cbx' ≅a c''bz
30. abx' ≅a abz
31. out(b x'z)
32. a-z-c''
33. z' : Point
34. cbx ≅a c''bz'
35. abx ≅a abz'
36. out(b xz')
37. a-z'-c''
38. a=z=c''
⊢ out(b xy) ∧ abx ≅a a'by
BY
{ (Assert a=z'=c'' BY
         ((D 0 THEN Auto)
          THEN (InstLemma `geo-sas2` [⌜e⌝;⌜b⌝;⌜a⌝;⌜z'⌝;⌜b⌝;⌜c''⌝;⌜z'⌝]⋅ THEN EAuto 1)
          THEN (InstLemma `geo-cong-angle-transitivity` [⌜e⌝;⌜c⌝;⌜b⌝;⌜x⌝;⌜a⌝;⌜b⌝;⌜x⌝;⌜a⌝;⌜b⌝;⌜z'⌝]⋅ THENA EAuto 1)
          THEN InstLemma `geo-cong-angle-transitivity` [⌜e⌝;⌜a⌝;⌜b⌝;⌜z'⌝;⌜c⌝;⌜b⌝;⌜x⌝;⌜c''⌝;⌜b⌝;⌜z'⌝]⋅
          THEN EAuto 1)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. c' : Point
7. x : Point
8. y : Point
9. a # bc
10. out(b aa')
11. out(b cc')
12. a-x-c
13. a'-y-c'
14. abx ≅a cbx
15. a'by ≅a c'by
16. x' : Point
17. a-x'-c
18. out(b yx')
19. a'by ≅a abx'
20. c'by ≅a cbx'
21. C : Point
22. c-b-C
23. bC ≅ OX
24. c'' : Point
25. C-b-c''
26. bc'' ≅ ba
27. out(b cc'')
28. z : Point
29. cbx' ≅a c''bz
30. abx' ≅a abz
31. out(b x'z)
32. a-z-c''
33. z' : Point
34. cbx ≅a c''bz'
35. abx ≅a abz'
36. out(b xz')
37. a-z'-c''
38. a=z=c''
39. a=z'=c''
⊢ out(b xy) ∧ abx ≅a a'by

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a'  :  Point
6.  c'  :  Point
7.  x  :  Point
8.  y  :  Point
9.  a  \#  bc
10.  out(b  aa')
11.  out(b  cc')
12.  a-x-c
13.  a'-y-c'
14.  abx  \mcong{}\msuba{}  cbx
15.  a'by  \mcong{}\msuba{}  c'by
16.  x'  :  Point
17.  a-x'-c
18.  out(b  yx')
19.  a'by  \mcong{}\msuba{}  abx'
20.  c'by  \mcong{}\msuba{}  cbx'
21.  C  :  Point
22.  c-b-C
23.  bC  \mcong{}  OX
24.  c''  :  Point
25.  C-b-c''
26.  bc''  \mcong{}  ba
27.  out(b  cc'')
28.  z  :  Point
29.  cbx'  \mcong{}\msuba{}  c''bz
30.  abx'  \mcong{}\msuba{}  abz
31.  out(b  x'z)
32.  a-z-c''
33.  z'  :  Point
34.  cbx  \mcong{}\msuba{}  c''bz'
35.  abx  \mcong{}\msuba{}  abz'
36.  out(b  xz')
37.  a-z'-c''
38.  a=z=c''
\mvdash{}  out(b  xy)  \mwedge{}  abx  \mcong{}\msuba{}  a'by


By

---

Latex:
(Assert  a=z'=c''  BY
              ((D  0  THEN  Auto)
                THEN  (InstLemma  `geo-sas2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c''\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)
                THEN  (InstLemma  `geo-cong-angle-transitivity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{}]\mcdot{}
                            THENA  EAuto  1
                            )
                THEN  InstLemma  `geo-cong-angle-transitivity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}c''\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{}]\mcdot{}
                THEN  EAuto  1))

---

Home Index