Step
*
1
1
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''
39. a=z'=c''
40. z' ≡ z
⊢ out(b xy)
BY
{ (EliminatePoint (-1) THEN Auto) }
1
1. e : EuclideanPlane
2. z : Point
3. a : Point
4. b : Point
5. c : Point
6. a' : Point
7. c' : Point
8. x : Point
9. y : Point
10. a # bc
11. out(b aa')
12. out(b cc')
13. a-x-c
14. a'-y-c'
15. abx ≅a cbx
16. a'by ≅a c'by
17. x' : Point
18. a-x'-c
19. out(b yx')
20. a'by ≅a abx'
21. c'by ≅a cbx'
22. C : Point
23. c-b-C
24. bC ≅ OX
25. c'' : Point
26. C-b-c''
27. bc'' ≅ ba
28. out(b cc'')
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''
40. z' ≡ z
⊢ out(b xy)
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''
39. a=z'=c''
40. z' \mequiv{} z
\mvdash{} out(b xy)
By
Latex:
(EliminatePoint (-1) THEN Auto)
Home
Index