---

Step * 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'')
⊢ out(b xy) ∧ abx ≅a a'by
BY
{ ((Assert ∃z:Point. (((cbx' ≅a c''bz ∧ abx' ≅a abz) ∧ out(b x'z)) ∧ a-z-c'') BY
          ((InstLemma `geo-out-interior-point-exists` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜a⌝;⌜c''⌝;⌜x'⌝]⋅ THENA EAuto 1)
           THEN ExRepD
           THEN D 0 With ⌜x'@0⌝ 
           THEN Auto))
   THEN (Assert ∃z':Point. (((cbx ≅a c''bz' ∧ abx ≅a abz') ∧ out(b xz')) ∧ a-z'-c'') BY
               ((InstLemma `geo-out-interior-point-exists` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜a⌝;⌜c''⌝;⌜x⌝]⋅ THENA EAuto 1)
                THEN ExRepD
                THEN D 0 With ⌜x1⌝ 
                THEN Auto))
   ) }

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 ∧ 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

---

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'')
\mvdash{}  out(b  xy)  \mwedge{}  abx  \mcong{}\msuba{}  a'by


By

---

Latex:
((Assert  \mexists{}z:Point.  (((cbx'  \mcong{}\msuba{}  c''bz  \mwedge{}  abx'  \mcong{}\msuba{}  abz)  \mwedge{}  out(b  x'z))  \mwedge{}  a-z-c'')  BY
                ((InstLemma  `geo-out-interior-point-exists`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c''\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{}]\mcdot{}  THENA  EAuto  1)
                  THEN  ExRepD
                  THEN  D  0  With  \mkleeneopen{}x'@0\mkleeneclose{} 
                  THEN  Auto))
  THEN  (Assert  \mexists{}z':Point.  (((cbx  \mcong{}\msuba{}  c''bz'  \mwedge{}  abx  \mcong{}\msuba{}  abz')  \mwedge{}  out(b  xz'))  \mwedge{}  a-z'-c'')  BY
                          ((InstLemma  `geo-out-interior-point-exists`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c''\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
                              THENA  EAuto  1
                              )
                            THEN  ExRepD
                            THEN  D  0  With  \mkleeneopen{}x1\mkleeneclose{} 
                            THEN  Auto))
  )

---

Home Index