---

Step * 1 1 1 1 1 1 2 of Lemma Euclid-prop16

.....antecedent..... 
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a # bc
7. b-c-d
8. x : {x:Point| b=x=c} 
9. y : {y:Point| a=x=y} 
10. abc ≅a ycb
11. b # x
12. x # c
13. a # x
14. x # y
15. g' : Point
16. a-c-g'
17. cg' ≅ OX
18. x # ac
19. g'-c-a
20. y-x-a
21. a # xc
22. a # yg'
23. out(a cg')
24. p : Point
25. g'-p-x
26. y-p-c
⊢ bcy < bcg'
BY
{ ((((InstLemma `Euclid-midpoint` [⌜g⌝;⌜p⌝;⌜g'⌝]⋅ THEN Auto) THEN ExRepD)
    THEN (Assert ¬out(c bg') BY
                ((Assert g' # cb BY
                        (InstLemma `out-preserves-lsep` [⌜g⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜b⌝;⌜g'⌝]⋅ THEN EAuto 1))
                 THEN InstLemma `out-preserves-lsep` [⌜g⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜b⌝;⌜g'⌝]⋅
                 THEN EAuto 1))
    )
   THEN (Unfold `geo-lt-angle` 0 THEN GenRepD)
   THEN InstConcl [⌜y⌝;⌜p⌝;⌜x⌝;⌜g'⌝]⋅
   THEN EAuto 1) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a # bc
7. b-c-d
8. x : {x:Point| b=x=c} 
9. y : {y:Point| a=x=y} 
10. abc ≅a ycb
11. b # x
12. x # c
13. a # x
14. x # y
15. g' : Point
16. a-c-g'
17. cg' ≅ OX
18. x # ac
19. g'-c-a
20. y-x-a
21. a # xc
22. a # yg'
23. out(a cg')
24. p : Point
25. g'-p-x
26. y-p-c
27. d1 : Point
28. p=d1=g'
29. ¬out(c bg')
30. bcy ≅a bcy
31. B(cpy)
⊢ out(c bx)

---

Latex:

---

Latex:
.....antecedent..... 
1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  a  \#  bc
7.  b-c-d
8.  x  :  \{x:Point|  b=x=c\} 
9.  y  :  \{y:Point|  a=x=y\} 
10.  abc  \mcong{}\msuba{}  ycb
11.  b  \#  x
12.  x  \#  c
13.  a  \#  x
14.  x  \#  y
15.  g'  :  Point
16.  a-c-g'
17.  cg'  \mcong{}  OX
18.  x  \#  ac
19.  g'-c-a
20.  y-x-a
21.  a  \#  xc
22.  a  \#  yg'
23.  out(a  cg')
24.  p  :  Point
25.  g'-p-x
26.  y-p-c
\mvdash{}  bcy  <  bcg'


By

---

Latex:
((((InstLemma  `Euclid-midpoint`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}g'\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  ExRepD)
    THEN  (Assert  \mneg{}out(c  bg')  BY
                            ((Assert  g'  \#  cb  BY
                                            (InstLemma  `out-preserves-lsep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}g'\mkleeneclose{}]\mcdot{}  THEN  EAuto  1))
                              THEN  InstLemma  `out-preserves-lsep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}g'\mkleeneclose{}]\mcdot{}
                              THEN  EAuto  1))
    )
  THEN  (Unfold  `geo-lt-angle`  0  THEN  GenRepD)
  THEN  InstConcl  [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}g'\mkleeneclose{}]\mcdot{}
  THEN  EAuto  1)

---

Home Index