---

Step * 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)
⊢ ac ≅ xz
BY
{ (Assert cc' ≅ zz' BY
         (((Assert B(zyz') BY EAuto 1) THEN (Assert B(cbc') BY EAuto 1))
          THEN (FLemma `geo-add-length-between` [38]⋅ THENA Auto)
          THEN FLemma
          `geo-add-length-between` [39]⋅
          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'
⊢ 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)
\mvdash{}  ac  \mcong{}  xz


By

---

Latex:
(Assert  cc'  \mcong{}  zz'  BY
              (((Assert  B(zyz')  BY  EAuto  1)  THEN  (Assert  B(cbc')  BY  EAuto  1))
                THEN  (FLemma  `geo-add-length-between`  [38]\mcdot{}  THENA  Auto)
                THEN  FLemma
                `geo-add-length-between`  [39]\mcdot{}
                THEN  Auto))

---

Home Index