---

Step * 1 of Lemma Euclid-Prop17


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. i : Point
6. j : Point
7. k : Point
8. a # bc
9. acb + abc ≅ ijk
10. a1 : Point
11. a2 : Point
12. a3 : Point
13. a1-a2-a3
14. d : Point
15. b-c-d
16. cd ≅ OX
17. abc < acd
⊢ ijk < a1a2a3
BY
{ (Assert acb + acd ≅ bcd BY
         (InstLemma  `Euclid-prop13` [⌜g⌝;⌜a⌝;⌜c⌝;⌜b⌝;⌜d⌝]⋅ THEN Auto)) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. i : Point
6. j : Point
7. k : Point
8. a # bc
9. acb + abc ≅ ijk
10. a1 : Point
11. a2 : Point
12. a3 : Point
13. a1-a2-a3
14. d : Point
15. b-c-d
16. cd ≅ OX
17. abc < acd
18. acb + acd ≅ bcd
⊢ ijk < a1a2a3

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  i  :  Point
6.  j  :  Point
7.  k  :  Point
8.  a  \#  bc
9.  acb  +  abc  \mcong{}  ijk
10.  a1  :  Point
11.  a2  :  Point
12.  a3  :  Point
13.  a1-a2-a3
14.  d  :  Point
15.  b-c-d
16.  cd  \mcong{}  OX
17.  abc  <  acd
\mvdash{}  ijk  <  a1a2a3


By

---

Latex:
(Assert  acb  +  acd  \mcong{}  bcd  BY
              (InstLemma    `Euclid-prop13`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THEN  Auto))

---

Home Index