---

Step * 1 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
18. acb + acd ≅ bcd
⊢ ijk < a1a2a3
BY
{ (InstLemma  `hp-angle-sum-subst4` [⌜g⌝;⌜a⌝;⌜c⌝;⌜b⌝;⌜a⌝;⌜c⌝;⌜d⌝;⌜b⌝;⌜c⌝;⌜d⌝;⌜a1⌝;⌜a2⌝;⌜a3⌝]⋅ THENA Auto) }

1
.....antecedent..... 
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
⊢ bcd ≅a a1a2a3

2
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
19. acb + acd ≅ a1a2a3
⊢ 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
18.  acb  +  acd  \mcong{}  bcd
\mvdash{}  ijk  <  a1a2a3


By

---

Latex:
(InstLemma    `hp-angle-sum-subst4`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}a2\mkleeneclose{};\mkleeneopen{}a3\mkleeneclose{}]\mcdot{}
  THENA  Auto
  )

---

Home Index