Step
*
of Lemma
geo-axioms-imply
No Annotations
∀g:GeometryPrimitives
(BasicGeometryAxioms(g)
⇒ ((∀a:Point. (¬a # a))
∧ (∀a,b,x,y:Point. ((¬a # b) ⇒ B(xay) ⇒ B(xby)))
∧ (∀a,b,c:Point. ((¬a # b) ⇒ ac ≅ cb))
∧ (∀a,b,c,d:Point. ((¬¬(∃w:Point. (B(cwd) ∧ cw ≅ ab))) ⇒ a # b ⇒ c # d))
∧ (∀a,b,c:Point. ((¬a # b) ⇒ B(abc)))
∧ (∀a,b,c:Point. (B(abc) ⇒ B(cba)))
∧ (∀a,b,c,d:Point. (B(abd) ⇒ B(bcd) ⇒ B(abc)))
∧ (∀a,b:Point. aa ≅ bb)
∧ (∀a,b,p,q,r,s:Point. (ab ≅ pq ⇒ ab ≅ rs ⇒ pq ≅ rs))
∧ (∀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))
∧ (∀a,b,c,x,y:Point. (ax ≅ ay ⇒ bx ≅ by ⇒ cx ≅ cy ⇒ x # y ⇒ (¬a # bc)))))
BY
{ (RepeatFor 2 (Intro)
THEN (Assert ∀a,b,c,d,x,y:Point. (ab ≅ cd ⇒ cd>xy ⇒ ab>xy) BY
(Auto THEN InstLemma `basic-geo-cong-preserves-gt-prim` [⌜g⌝] ⋅ THEN Auto))
THEN (Assert ∀a:Point. (¬a # a) BY
(Auto THEN InstLemma `geo-sep-irreflexive` [⌜g⌝;⌜a⌝]⋅ THEN Auto))
THEN (Assert ∀a,b:Point. ba ≥ ab BY
(Auto THEN (InstLemma `geo-gt-prim-irreflexive` [⌜g⌝]⋅ THEN Auto) THEN Unfold `geo-ge` 0 THEN Auto))
THEN (D 2 THEN SplitAndHyps)
THEN (Assert ∀a,b,c,d:Point. (ab>cd ⇒ ba>cd) BY
Auto)
THEN (Assert ∀a,b,c,d:Point. (ab>cd ⇒ ab>dc) BY
Auto)
THEN SplitAndConcl
THEN Try (Trivial)
THEN Auto) }
1
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. B(xay)
⊢ B(xby)
2
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. c : Point
23. ¬a # b
⊢ ac ≅ cb
3
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. c : Point
23. d : Point
24. ¬¬(∃w:Point. (B(cwd) ∧ cw ≅ ab))
25. a # b
⊢ c # d
4
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. c : Point
23. ¬a # b
⊢ B(abc)
5
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. c : Point
23. B(abc)
⊢ B(cba)
6
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
⊢ aa ≅ bb
7
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. p : Point
23. q : Point
24. r : Point
25. s : Point
26. ab ≅ pq
27. ab ≅ rs
⊢ pq ≅ rs
Latex:
Latex:
No Annotations
\mforall{}g:GeometryPrimitives
(BasicGeometryAxioms(g)
{}\mRightarrow{} ((\mforall{}a:Point. (\mneg{}a \# a))
\mwedge{} (\mforall{}a,b,x,y:Point. ((\mneg{}a \# b) {}\mRightarrow{} B(xay) {}\mRightarrow{} B(xby)))
\mwedge{} (\mforall{}a,b,c:Point. ((\mneg{}a \# b) {}\mRightarrow{} ac \mcong{} cb))
\mwedge{} (\mforall{}a,b,c,d:Point. ((\mneg{}\mneg{}(\mexists{}w:Point. (B(cwd) \mwedge{} cw \mcong{} ab))) {}\mRightarrow{} a \# b {}\mRightarrow{} c \# d))
\mwedge{} (\mforall{}a,b,c:Point. ((\mneg{}a \# b) {}\mRightarrow{} B(abc)))
\mwedge{} (\mforall{}a,b,c:Point. (B(abc) {}\mRightarrow{} B(cba)))
\mwedge{} (\mforall{}a,b,c,d:Point. (B(abd) {}\mRightarrow{} B(bcd) {}\mRightarrow{} B(abc)))
\mwedge{} (\mforall{}a,b:Point. aa \mcong{} bb)
\mwedge{} (\mforall{}a,b,p,q,r,s:Point. (ab \mcong{} pq {}\mRightarrow{} ab \mcong{} rs {}\mRightarrow{} pq \mcong{} rs))
\mwedge{} (\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))
\mwedge{} (\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)))))
By
Latex:
(RepeatFor 2 (Intro)
THEN (Assert \mforall{}a,b,c,d,x,y:Point. (ab \mcong{} cd {}\mRightarrow{} cd>xy {}\mRightarrow{} ab>xy) BY
(Auto THEN InstLemma `basic-geo-cong-preserves-gt-prim` [\mkleeneopen{}g\mkleeneclose{}] \mcdot{} THEN Auto))
THEN (Assert \mforall{}a:Point. (\mneg{}a \# a) BY
(Auto THEN InstLemma `geo-sep-irreflexive` [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{} THEN Auto))
THEN (Assert \mforall{}a,b:Point. ba \mgeq{} ab BY
(Auto
THEN (InstLemma `geo-gt-prim-irreflexive` [\mkleeneopen{}g\mkleeneclose{}]\mcdot{} THEN Auto)
THEN Unfold `geo-ge` 0
THEN Auto))
THEN (D 2 THEN SplitAndHyps)
THEN (Assert \mforall{}a,b,c,d:Point. (ab>cd {}\mRightarrow{} ba>cd) BY
Auto)
THEN (Assert \mforall{}a,b,c,d:Point. (ab>cd {}\mRightarrow{} ab>dc) BY
Auto)
THEN SplitAndConcl
THEN Try (Trivial)
THEN Auto)
Home
Index