Step
*
1
1
2
1
of Lemma
geo-axioms-imply
1. g : GeometryPrimitives
2. ∀a,b,c,d:Point. (ab>cd ⇒ ab ≥ cd)
3. ∀a,b,c:Point. (ba>ac ⇒ b # c)
4. ∀a,b,c:Point. bc ≥ aa
5. ∀a,b,c,d,e,f:Point. (ab>cd ⇒ cd ≥ ef ⇒ ab>ef)
6. ∀a,b,c,d,e,f:Point. (ab ≥ cd ⇒ cd>ef ⇒ ab>ef)
7. ∀a,b,c:Point. (B(abc) ⇒ b # c ⇒ ac>ab)
8. ∀a,b,c:Point. (a leftof bc ⇒ b leftof ca)
9. ∀a,b,c:Point. (a leftof bc ⇒ b # c)
10. ∀a,b,c,d:Point. (B(abd) ⇒ B(bcd) ⇒ B(abc))
11. ∀a,b,c,d,A,B,C,D:Point. (a # b ⇒ B(abc) ⇒ B(ABC) ⇒ ab ≅ AB ⇒ bc ≅ BC ⇒ ad ≅ AD ⇒ bd ≅ BD ⇒ cd ≅ CD)
12. ∀a,b,c,x,y:Point. (ax ≅ ay ⇒ bx ≅ by ⇒ cx ≅ cy ⇒ x # y ⇒ (¬a # bc))
13. ∀a,b,x,y,z:Point. (x leftof ab ⇒ y leftof ab ⇒ B(xzy) ⇒ z leftof ab)
14. ∀a,b,c,y:Point. (a # bc ⇒ y # b ⇒ (¬y # ab) ⇒ y # bc)
15. ∀a,b,c,d,x,y:Point. (ab ≅ cd ⇒ cd>xy ⇒ ab>xy)
16. ∀a:Point. (¬a # a)
17. ∀a,b:Point. ba ≥ ab
18. ∀a,b,c,d:Point. (ab>cd ⇒ ba>cd)
19. ∀a,b,c,d:Point. (ab>cd ⇒ ab>dc)
20. a : Point
21. b : Point
22. x : Point
23. y : Point
24. ¬a # b
25. ¬x # ay
26. ¬xa>xy
27. ¬ay>xy
28. ∀a,b:Point. (b # a ⇒ a # b)
29. ∀a,b,x,y:Point. ((¬a # b) ⇒ a leftof xy ⇒ b leftof xy)
30. ¬b # a
31. ∀a,b,c,d,e,f:Point. (ab ≥ cd ⇒ cd ≥ ef ⇒ ab ≥ ef)
32. ya ≥ by
33. ay ≥ ya
⊢ ¬by>xy
BY
{ ((Assert xy ≥ ya BY Auto) THEN Auto) }
1
.....aux.....
1. g : GeometryPrimitives
2. ∀a,b,c,d:Point. (ab>cd ⇒ ab ≥ cd)
3. ∀a,b,c:Point. (ba>ac ⇒ b # c)
4. ∀a,b,c:Point. bc ≥ aa
5. ∀a,b,c,d,e,f:Point. (ab>cd ⇒ cd ≥ ef ⇒ ab>ef)
6. ∀a,b,c,d,e,f:Point. (ab ≥ cd ⇒ cd>ef ⇒ ab>ef)
7. ∀a,b,c:Point. (B(abc) ⇒ b # c ⇒ ac>ab)
8. ∀a,b,c:Point. (a leftof bc ⇒ b leftof ca)
9. ∀a,b,c:Point. (a leftof bc ⇒ b # c)
10. ∀a,b,c,d:Point. (B(abd) ⇒ B(bcd) ⇒ B(abc))
11. ∀a,b,c,d,A,B,C,D:Point. (a # b ⇒ B(abc) ⇒ B(ABC) ⇒ ab ≅ AB ⇒ bc ≅ BC ⇒ ad ≅ AD ⇒ bd ≅ BD ⇒ cd ≅ CD)
12. ∀a,b,c,x,y:Point. (ax ≅ ay ⇒ bx ≅ by ⇒ cx ≅ cy ⇒ x # y ⇒ (¬a # bc))
13. ∀a,b,x,y,z:Point. (x leftof ab ⇒ y leftof ab ⇒ B(xzy) ⇒ z leftof ab)
14. ∀a,b,c,y:Point. (a # bc ⇒ y # b ⇒ (¬y # ab) ⇒ y # bc)
15. ∀a,b,c,d,x,y:Point. (ab ≅ cd ⇒ cd>xy ⇒ ab>xy)
16. ∀a:Point. (¬a # a)
17. ∀a,b:Point. ba ≥ ab
18. ∀a,b,c,d:Point. (ab>cd ⇒ ba>cd)
19. ∀a,b,c,d:Point. (ab>cd ⇒ ab>dc)
20. a : Point
21. b : Point
22. x : Point
23. y : Point
24. ¬a # b
25. ¬x # ay
26. ¬xa>xy
27. ¬ay>xy
28. ∀a,b:Point. (b # a ⇒ a # b)
29. ∀a,b,x,y:Point. ((¬a # b) ⇒ a leftof xy ⇒ b leftof xy)
30. ¬b # a
31. ∀a,b,c,d,e,f:Point. (ab ≥ cd ⇒ cd ≥ ef ⇒ ab ≥ ef)
32. ya ≥ by
33. ay ≥ ya
⊢ xy ≥ ya
Latex:
Latex:
1. g : GeometryPrimitives
2. \mforall{}a,b,c,d:Point. (ab>cd {}\mRightarrow{} ab \mgeq{} cd)
3. \mforall{}a,b,c:Point. (ba>ac {}\mRightarrow{} b \# c)
4. \mforall{}a,b,c:Point. bc \mgeq{} aa
5. \mforall{}a,b,c,d,e,f:Point. (ab>cd {}\mRightarrow{} cd \mgeq{} ef {}\mRightarrow{} ab>ef)
6. \mforall{}a,b,c,d,e,f:Point. (ab \mgeq{} cd {}\mRightarrow{} cd>ef {}\mRightarrow{} ab>ef)
7. \mforall{}a,b,c:Point. (B(abc) {}\mRightarrow{} b \# c {}\mRightarrow{} ac>ab)
8. \mforall{}a,b,c:Point. (a leftof bc {}\mRightarrow{} b leftof ca)
9. \mforall{}a,b,c:Point. (a leftof bc {}\mRightarrow{} b \# c)
10. \mforall{}a,b,c,d:Point. (B(abd) {}\mRightarrow{} B(bcd) {}\mRightarrow{} B(abc))
11. \mforall{}a,b,c,d,A,B,C,D:Point.
(a \# b {}\mRightarrow{} B(abc) {}\mRightarrow{} B(ABC) {}\mRightarrow{} ab \mcong{} AB {}\mRightarrow{} bc \mcong{} BC {}\mRightarrow{} ad \mcong{} AD {}\mRightarrow{} bd \mcong{} BD {}\mRightarrow{} cd \mcong{} CD)
12. \mforall{}a,b,c,x,y:Point. (ax \mcong{} ay {}\mRightarrow{} bx \mcong{} by {}\mRightarrow{} cx \mcong{} cy {}\mRightarrow{} x \# y {}\mRightarrow{} (\mneg{}a \# bc))
13. \mforall{}a,b,x,y,z:Point. (x leftof ab {}\mRightarrow{} y leftof ab {}\mRightarrow{} B(xzy) {}\mRightarrow{} z leftof ab)
14. \mforall{}a,b,c,y:Point. (a \# bc {}\mRightarrow{} y \# b {}\mRightarrow{} (\mneg{}y \# ab) {}\mRightarrow{} y \# bc)
15. \mforall{}a,b,c,d,x,y:Point. (ab \mcong{} cd {}\mRightarrow{} cd>xy {}\mRightarrow{} ab>xy)
16. \mforall{}a:Point. (\mneg{}a \# a)
17. \mforall{}a,b:Point. ba \mgeq{} ab
18. \mforall{}a,b,c,d:Point. (ab>cd {}\mRightarrow{} ba>cd)
19. \mforall{}a,b,c,d:Point. (ab>cd {}\mRightarrow{} ab>dc)
20. a : Point
21. b : Point
22. x : Point
23. y : Point
24. \mneg{}a \# b
25. \mneg{}x \# ay
26. \mneg{}xa>xy
27. \mneg{}ay>xy
28. \mforall{}a,b:Point. (b \# a {}\mRightarrow{} a \# b)
29. \mforall{}a,b,x,y:Point. ((\mneg{}a \# b) {}\mRightarrow{} a leftof xy {}\mRightarrow{} b leftof xy)
30. \mneg{}b \# a
31. \mforall{}a,b,c,d,e,f:Point. (ab \mgeq{} cd {}\mRightarrow{} cd \mgeq{} ef {}\mRightarrow{} ab \mgeq{} ef)
32. ya \mgeq{} by
33. ay \mgeq{} ya
\mvdash{} \mneg{}by>xy
By
Latex:
((Assert xy \mgeq{} ya BY Auto) THEN Auto)
Home
Index