---

Step * 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
⊢ bc ≅ yz
BY
{ (InstLemma  `geo-inner-five-segment` [⌜e⌝;⌜x⌝;⌜y⌝;⌜y1⌝;⌜z⌝;⌜a⌝;⌜b⌝;⌜b1⌝;⌜c⌝]⋅ THEN Auto) }

1
.....antecedent..... 
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
⊢ y1z ≅ b1c

---

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
\mvdash{}  bc  \mcong{}  yz


By

---

Latex:
(InstLemma    `geo-inner-five-segment`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}y1\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index