Step
*
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 ∧ bC ≅ OX
23. c'' : Point
24. C-b-c'' ∧ bc'' ≅ ba
25. out(b cc'')
26. ∃z:Point. (((cbx' ≅a c''bz ∧ abx' ≅a abz) ∧ out(b x'z)) ∧ a-z-c'')
27. ∃z':Point. (((cbx ≅a c''bz' ∧ abx ≅a abz') ∧ out(b xz')) ∧ a-z'-c'')
⊢ out(b xy) ∧ abx ≅a a'by
BY
{ (ExRepD
   THEN (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⌝;⌜a'⌝;⌜b⌝;⌜y⌝;⌜a⌝;⌜b⌝;⌜x'⌝;⌜a⌝;⌜b⌝;⌜z⌝]⋅ THENA Auto)
                      THEN (InstLemma `geo-cong-angle-transitivity` [⌜e⌝;⌜c'⌝;⌜b⌝;⌜y⌝;⌜c⌝;⌜b⌝;⌜x'⌝;⌜c''⌝;⌜b⌝;⌜z⌝]⋅
                            THENA Auto
                            )
                      )
                THEN (InstLemma `geo-cong-angle-transitivity` [⌜e⌝;⌜c'⌝;⌜b⌝;⌜y⌝;⌜a'⌝;⌜b⌝;⌜y⌝;⌜a⌝;⌜b⌝;⌜z⌝]⋅ THEN EAuto 1)
                THEN InstLemma `geo-cong-angle-transitivity` [⌜e⌝;⌜c''⌝;⌜b⌝;⌜z⌝;⌜c'⌝;⌜b⌝;⌜y⌝;⌜a⌝;⌜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''
⊢ 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  \mwedge{}  bC  \mcong{}  OX
23.  c''  :  Point
24.  C-b-c''  \mwedge{}  bc''  \mcong{}  ba
25.  out(b  cc'')
26.  \mexists{}z:Point.  (((cbx'  \mcong{}\msuba{}  c''bz  \mwedge{}  abx'  \mcong{}\msuba{}  abz)  \mwedge{}  out(b  x'z))  \mwedge{}  a-z-c'')
27.  \mexists{}z':Point.  (((cbx  \mcong{}\msuba{}  c''bz'  \mwedge{}  abx  \mcong{}\msuba{}  abz')  \mwedge{}  out(b  xz'))  \mwedge{}  a-z'-c'')
\mvdash{}  out(b  xy)  \mwedge{}  abx  \mcong{}\msuba{}  a'by
By
Latex:
(ExRepD
  THEN  (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{}a'\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};
                                          \mkleeneopen{}z\mkleeneclose{}]\mcdot{}
                                          THENA  Auto
                                          )
                                        THEN  (InstLemma  `geo-cong-angle-transitivity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};
                                                    \mkleeneopen{}c''\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}
                                                    THENA  Auto
                                                    )
                                        )
                            THEN  (InstLemma  `geo-cong-angle-transitivity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};
                                        \mkleeneopen{}z\mkleeneclose{}]\mcdot{}
                                        THEN  EAuto  1
                                        )
                            THEN  InstLemma  `geo-cong-angle-transitivity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c''\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};
                            \mkleeneopen{}z\mkleeneclose{}]\mcdot{}
                            THEN  EAuto  1))
  )
Home
Index