---

Step * 1 1 1 1 1 of Lemma right-angle-SAS


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. ∀c':Point. (c'=b=c ⇒ ac ≅ ac')
9. a # b
10. b # c
11. ∀c':Point. (c'=y=z ⇒ xz ≅ xc')
12. x # y
13. y # z
14. ab ≅ xy
15. bc ≅ yz
16. c' : Point
17. c-b-c'
18. bc' ≅ cb
19. z' : Point
20. z-y-z'
21. yz' ≅ zy
22. Rabc
23. Rxyz
24. ac ≅ ac'
25. xz ≅ xz'
26. t : Point
27. tc ≅ c'c
28. tc' ≅ cc'
29. tc' ≅ tc
30. t # cc'
31. c1 : Point
32. c1z ≅ z'z
33. c1z' ≅ zz'
34. c1z' ≅ c1z
35. c1 # zz'
36. Colinear(x;c1;y)
37. Colinear(a;t;b)
38. cc' ≅ zz'
⊢ ac ≅ xz
BY
{ ((gProperProlong ⌜a⌝⌜b⌝`a\''⌜a⌝⌜b⌝⋅ THEN Auto) THEN gProperProlong ⌜x⌝⌜y⌝`x\''⌜x⌝⌜y⌝⋅ THEN Auto) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. ∀c':Point. (c'=b=c ⇒ ac ≅ ac')
9. a # b
10. b # c
11. ∀c':Point. (c'=y=z ⇒ xz ≅ xc')
12. x # y
13. y # z
14. ab ≅ xy
15. bc ≅ yz
16. c' : Point
17. c-b-c'
18. bc' ≅ cb
19. z' : Point
20. z-y-z'
21. yz' ≅ zy
22. Rabc
23. Rxyz
24. ac ≅ ac'
25. xz ≅ xz'
26. t : Point
27. tc ≅ c'c
28. tc' ≅ cc'
29. tc' ≅ tc
30. t # cc'
31. c1 : Point
32. c1z ≅ z'z
33. c1z' ≅ zz'
34. c1z' ≅ c1z
35. c1 # zz'
36. Colinear(x;c1;y)
37. Colinear(a;t;b)
38. cc' ≅ zz'
39. a' : Point
40. a-b-a'
41. ba' ≅ ab
42. x' : Point
43. x-y-x'
44. yx' ≅ xy
⊢ ac ≅ xz

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  z  :  Point
8.  \mforall{}c':Point.  (c'=b=c  {}\mRightarrow{}  ac  \mcong{}  ac')
9.  a  \#  b
10.  b  \#  c
11.  \mforall{}c':Point.  (c'=y=z  {}\mRightarrow{}  xz  \mcong{}  xc')
12.  x  \#  y
13.  y  \#  z
14.  ab  \mcong{}  xy
15.  bc  \mcong{}  yz
16.  c'  :  Point
17.  c-b-c'
18.  bc'  \mcong{}  cb
19.  z'  :  Point
20.  z-y-z'
21.  yz'  \mcong{}  zy
22.  Rabc
23.  Rxyz
24.  ac  \mcong{}  ac'
25.  xz  \mcong{}  xz'
26.  t  :  Point
27.  tc  \mcong{}  c'c
28.  tc'  \mcong{}  cc'
29.  tc'  \mcong{}  tc
30.  t  \#  cc'
31.  c1  :  Point
32.  c1z  \mcong{}  z'z
33.  c1z'  \mcong{}  zz'
34.  c1z'  \mcong{}  c1z
35.  c1  \#  zz'
36.  Colinear(x;c1;y)
37.  Colinear(a;t;b)
38.  cc'  \mcong{}  zz'
\mvdash{}  ac  \mcong{}  xz


By

---

Latex:
((gProperProlong  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}`a\mbackslash{}''\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  gProperProlong  \mkleeneopen{}x\mkleeneclose{}\mkleeneopen{}y\mkleeneclose{}`x\mbackslash{}''\mkleeneopen{}x\mkleeneclose{}\mkleeneopen{}y\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index