---

Step * 1 1 1 of Lemma Euclid-Prop19-lemma2


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. f : Point
7. a # bc
8. cbd < abd
9. a=d=c
10. a-f-c
11. cbf ≅a abf
12. x : Point
13. bx ≅ bc
14. out(b ax)
15. b # xc
16. x1 : Point
17. x-x1-c
18. out(b fx1)
19. abf ≅a xbx1
20. cbf ≅a cbx1
21. x' : Point
22. x-x'-c
23. out(b dx')
24. abd ≅a xbx'
25. cbd ≅a cbx'
⊢ |af| < |cf|
BY
{ ((Assert xbx1 ≅a cbx1 BY
          ((InstLemma `geo-cong-angle-transitivity` [⌜e⌝;⌜x⌝;⌜b⌝;⌜x1⌝;⌜a⌝;⌜b⌝;⌜f⌝;⌜c⌝;⌜b⌝;⌜f⌝]⋅ THENA EAuto 1)
           THEN InstLemma `geo-cong-angle-transitivity` [⌜e⌝;⌜x⌝;⌜b⌝;⌜x1⌝;⌜c⌝;⌜b⌝;⌜f⌝;⌜c⌝;⌜b⌝;⌜x1⌝]⋅
           THEN EAuto 1))
   THEN InstLemma `Euclid-Prop19-lemma2_1` [⌜e⌝;⌜x⌝;⌜b⌝;⌜c⌝;⌜x1⌝;⌜x'⌝]⋅
   THEN Auto) }

1
.....antecedent..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. f : Point
7. a # bc
8. cbd < abd
9. a=d=c
10. a-f-c
11. cbf ≅a abf
12. x : Point
13. bx ≅ bc
14. out(b ax)
15. b # xc
16. x1 : Point
17. x-x1-c
18. out(b fx1)
19. abf ≅a xbx1
20. cbf ≅a cbx1
21. x' : Point
22. x-x'-c
23. out(b dx')
24. abd ≅a xbx'
25. cbd ≅a cbx'
26. xbx1 ≅a cbx1
⊢ x=x1=c

2
.....antecedent..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. f : Point
7. a # bc
8. cbd < abd
9. a=d=c
10. a-f-c
11. cbf ≅a abf
12. x : Point
13. bx ≅ bc
14. out(b ax)
15. b # xc
16. x1 : Point
17. x-x1-c
18. out(b fx1)
19. abf ≅a xbx1
20. cbf ≅a cbx1
21. x' : Point
22. x-x'-c
23. out(b dx')
24. abd ≅a xbx'
25. cbd ≅a cbx'
26. xbx1 ≅a cbx1
⊢ cbx' < xbx'

3
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. f : Point
7. a # bc
8. cbd < abd
9. a=d=c
10. a-f-c
11. cbf ≅a abf
12. x : Point
13. bx ≅ bc
14. out(b ax)
15. b # xc
16. x1 : Point
17. x-x1-c
18. out(b fx1)
19. abf ≅a xbx1
20. cbf ≅a cbx1
21. x' : Point
22. x-x'-c
23. out(b dx')
24. abd ≅a xbx'
25. cbd ≅a cbx'
26. xbx1 ≅a cbx1
27. xbx1 < xbx'
⊢ |af| < |cf|

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  f  :  Point
7.  a  \#  bc
8.  cbd  <  abd
9.  a=d=c
10.  a-f-c
11.  cbf  \mcong{}\msuba{}  abf
12.  x  :  Point
13.  bx  \mcong{}  bc
14.  out(b  ax)
15.  b  \#  xc
16.  x1  :  Point
17.  x-x1-c
18.  out(b  fx1)
19.  abf  \mcong{}\msuba{}  xbx1
20.  cbf  \mcong{}\msuba{}  cbx1
21.  x'  :  Point
22.  x-x'-c
23.  out(b  dx')
24.  abd  \mcong{}\msuba{}  xbx'
25.  cbd  \mcong{}\msuba{}  cbx'
\mvdash{}  |af|  <  |cf|


By

---

Latex:
((Assert  xbx1  \mcong{}\msuba{}  cbx1  BY
                ((InstLemma  `geo-cong-angle-transitivity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}
                    THENA  EAuto  1
                    )
                  THEN  InstLemma  `geo-cong-angle-transitivity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{}]\mcdot{}
                  THEN  EAuto  1))
  THEN  InstLemma  `Euclid-Prop19-lemma2\_1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index