---

Step * 1 1 of Lemma hypotenuse-leg-congruence

.....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
BY
{ (Assert ac ≅ b1c BY
         ((InstLemma  `adjacent-right-angles-supplementary` [⌜e⌝;⌜c⌝;⌜b⌝;⌜a⌝;⌜b1⌝]⋅ THENA Auto)
          THEN ((FLemma  `right-angle-symmetry` [8]  THEN Auto)
                THEN (InstLemma  `congruence-preserves-right-angle2` [⌜e⌝;⌜c⌝;⌜b⌝;⌜a⌝]⋅ THENA Auto)
                )
          THEN (InstHyp [⌜c⌝;⌜b⌝;⌜b1⌝] (-1)⋅ THEN Auto)
          THEN (FLemma  `right-angle-symmetry` [-1]  THEN Auto)
          THEN InstLemma  `right-angle-SAS` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜b1⌝;⌜b⌝;⌜c⌝]⋅
          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. 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
⊢ y1z ≅ b1c

---

Latex:

---

Latex:
.....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  \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{}  y1z  \mcong{}  b1c


By

---

Latex:
(Assert  ac  \mcong{}  b1c  BY
              ((InstLemma    `adjacent-right-angles-supplementary`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  ((FLemma    `right-angle-symmetry`  [8]    THEN  Auto)
                            THEN  (InstLemma    `congruence-preserves-right-angle2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            )
                THEN  (InstHyp  [\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
                THEN  (FLemma    `right-angle-symmetry`  [-1]    THEN  Auto)
                THEN  InstLemma    `right-angle-SAS`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}
                THEN  Auto))

---

Home Index