Step
*
1
1
1
1
of Lemma
hypotenuse-leg-congruence
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. Rabc
9. Rxyz
10. ac ≅ xz
11. ab ≅ xy
12. a ≠ b
13. x ≠ y
14. b ≠ c
15. y ≠ z
16. b1 : Point
17. a-b-b1
18. bb1 ≅ ab
19. y1 : Point
20. x-y-y1
21. yy1 ≅ xy
22. ac ≅ b1c
23. xz ≅ y1z
⊢ y1z ≅ b1c
BY
{ EAuto 1 }
Latex:
Latex:
1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  z  :  Point
8.  Rabc
9.  Rxyz
10.  ac  \mcong{}  xz
11.  ab  \mcong{}  xy
12.  a  \mneq{}  b
13.  x  \mneq{}  y
14.  b  \mneq{}  c
15.  y  \mneq{}  z
16.  b1  :  Point
17.  a-b-b1
18.  bb1  \mcong{}  ab
19.  y1  :  Point
20.  x-y-y1
21.  yy1  \mcong{}  xy
22.  ac  \mcong{}  b1c
23.  xz  \mcong{}  y1z
\mvdash{}  y1z  \mcong{}  b1c
By
Latex:
EAuto  1
Home
Index