---

Step * 1 1 1 7 1 1 1 1 of Lemma rectangle-sides-cong


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. e # ac
9. f # eb
10. ac  ⊥b be
11. df  ⊥e eb
12. d-e-f
13. a-b-c
14. ab ≅ eb
15. bc ≅ eb
16. de ≅ eb
17. ef ≅ eb
18. ae ≅ ce
19. db ≅ fb
20. db ≅ ae
21. feb ≅a deb
22. abe ≅a cbe
23. a leftof eb
24. f leftof eb
25. d leftof be
26. x : Point
27. Colinear(e;b;x)
28. a-x-d
29. B(exb)
30. e # b
31. x # b
32. x # e
33. axb ≅a dxe
34. Reba
35. Rbed
36. xba ≅a xed
37. bx ≅ ex ∧ xa ≅ xd ∧ xab ≅a xde
⊢ ad ≅ fc ∧ dc ≅ fa
BY
{ ((Assert fex ≅a dex BY
          ((InstLemma  `out-preserves-angle-cong_1` [⌜g⌝;⌜f⌝;⌜e⌝;⌜b⌝;⌜d⌝;⌜e⌝;⌜b⌝;⌜f⌝;⌜x⌝;⌜d⌝;⌜x⌝]⋅ THEN EAuto 1)
           THEN D 0
           THEN Auto))
   THEN (Assert x # fd BY
               Auto)
   THEN (Assert fx ≅ dx BY
               ((InstLemma  `geo-sas` [⌜g⌝;⌜e⌝;⌜f⌝;⌜x⌝;⌜e⌝;⌜d⌝;⌜x⌝]⋅ THEN Auto) THEN D 0 THEN Auto))
   THEN (Assert cbx ≅a abx BY
               ((InstLemma  `out-preserves-angle-cong_1` [⌜g⌝;⌜c⌝;⌜b⌝;⌜e⌝;⌜a⌝;⌜b⌝;⌜e⌝;⌜c⌝;⌜x⌝;⌜a⌝;⌜x⌝]⋅ THEN EAuto 1)
                THEN D 0
                THEN Auto))
   THEN (Assert x # ac BY
               Auto)
   THEN (Assert cx ≅ ax BY
               ((InstLemma  `geo-sas` [⌜g⌝;⌜b⌝;⌜c⌝;⌜x⌝;⌜b⌝;⌜a⌝;⌜x⌝]⋅ THEN Auto) THEN D 0 THEN Auto))) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. e # ac
9. f # eb
10. ac  ⊥b be
11. df  ⊥e eb
12. d-e-f
13. a-b-c
14. ab ≅ eb
15. bc ≅ eb
16. de ≅ eb
17. ef ≅ eb
18. ae ≅ ce
19. db ≅ fb
20. db ≅ ae
21. feb ≅a deb
22. abe ≅a cbe
23. a leftof eb
24. f leftof eb
25. d leftof be
26. x : Point
27. Colinear(e;b;x)
28. a-x-d
29. B(exb)
30. e # b
31. x # b
32. x # e
33. axb ≅a dxe
34. Reba
35. Rbed
36. xba ≅a xed
37. bx ≅ ex ∧ xa ≅ xd ∧ xab ≅a xde
38. fex ≅a dex
39. x # fd
40. fx ≅ dx
41. cbx ≅a abx
42. x # ac
43. cx ≅ ax
⊢ ad ≅ fc ∧ dc ≅ fa

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  e  :  Point
7.  f  :  Point
8.  e  \#  ac
9.  f  \#  eb
10.  ac    \mbot{}b  be
11.  df    \mbot{}e  eb
12.  d-e-f
13.  a-b-c
14.  ab  \mcong{}  eb
15.  bc  \mcong{}  eb
16.  de  \mcong{}  eb
17.  ef  \mcong{}  eb
18.  ae  \mcong{}  ce
19.  db  \mcong{}  fb
20.  db  \mcong{}  ae
21.  feb  \mcong{}\msuba{}  deb
22.  abe  \mcong{}\msuba{}  cbe
23.  a  leftof  eb
24.  f  leftof  eb
25.  d  leftof  be
26.  x  :  Point
27.  Colinear(e;b;x)
28.  a-x-d
29.  B(exb)
30.  e  \#  b
31.  x  \#  b
32.  x  \#  e
33.  axb  \mcong{}\msuba{}  dxe
34.  Reba
35.  Rbed
36.  xba  \mcong{}\msuba{}  xed
37.  bx  \mcong{}  ex  \mwedge{}  xa  \mcong{}  xd  \mwedge{}  xab  \mcong{}\msuba{}  xde
\mvdash{}  ad  \mcong{}  fc  \mwedge{}  dc  \mcong{}  fa


By

---

Latex:
((Assert  fex  \mcong{}\msuba{}  dex  BY
                ((InstLemma    `out-preserves-angle-cong\_1`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
                    THEN  EAuto  1
                    )
                  THEN  D  0
                  THEN  Auto))
  THEN  (Assert  x  \#  fd  BY
                          Auto)
  THEN  (Assert  fx  \mcong{}  dx  BY
                          ((InstLemma    `geo-sas`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  D  0  THEN  Auto))
  THEN  (Assert  cbx  \mcong{}\msuba{}  abx  BY
                          ((InstLemma    `out-preserves-angle-cong\_1`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]
                              \mcdot{}
                              THEN  EAuto  1
                              )
                            THEN  D  0
                            THEN  Auto))
  THEN  (Assert  x  \#  ac  BY
                          Auto)
  THEN  (Assert  cx  \mcong{}  ax  BY
                          ((InstLemma    `geo-sas`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  D  0  THEN  Auto)))

---

Home Index