Proof of Nuprl Lemma : euclidean-plane-axioms

Step * 1 1 of Lemma euclidean-plane-axioms

1. g : EuclideanPlane
2. BasicGeometryAxioms(g) ∧ (∀a,b,c:Point.  (a # bc ⇒ (¬Colinear(a;b;c))))
3. SqStable(geo-left-axioms(g))
4. (∀a:Point. a ≡ a) ∧ (∀a,b:Point.  ab ≅ ba) ∧ (∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc))
5. ∀a,b:Point.  (a # b ⇒ b # a)
⊢ ((∀a,b:Point.  (a # b ⇒ b # a))
  ∧ (∀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:Point.  (a ≡ b ⇒ ac ≅ bc)))
  ∧ (∀a,b,c,d:Point.  (cd ≥ 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.  ab ≅ ba)
  ∧ (∀a,b,p,q,r,s:Point.  (ab ≅ pq ⇒ ab ≅ rs ⇒ pq ≅ rs))
  ∧ (∀a,b:Point.  aa ≅ bb)
  ∧ (∀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:Point.  (¬a # bc ⇐⇒ Colinear(a;b;c)))
∧ (∀a,b,c:Point.  (a leftof bc ⇒ b leftof ca))
∧ (∀a,b,c:Point.  (a leftof bc ⇒ b # c))
∧ (∀a,b,x,y,z:Point.  (x leftof ab ⇒ y leftof ab ⇒ B(xzy) ⇒ z # ab))
∧ (∀a,b,c,y:Point.  (a # bc ⇒ y # b ⇒ Colinear(y;a;b) ⇒ y # bc))
BY
{ (RepeatFor 2 (D 2) THEN SplitAndHyps THEN SplitAndConcl THEN Try (Hypothesis) THEN Auto) }

1
1. g : EuclideanPlane
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:Point.  (a # bc ⇒ (¬Colinear(a;b;c)))
16. SqStable(geo-left-axioms(g))
17. ∀a:Point. a ≡ a
18. ∀a,b:Point.  ab ≅ ba
19. ∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc)
20. ∀a,b:Point.  (a # b ⇒ b # a)
21. a : Point
22. b : Point
23. x : Point
24. y : Point
25. a ≡ b
26. B(xay)
⊢ B(xby)

2
1. g : EuclideanPlane
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:Point.  (a # bc ⇒ (¬Colinear(a;b;c)))
16. SqStable(geo-left-axioms(g))
17. ∀a:Point. a ≡ a
18. ∀a,b:Point.  ab ≅ ba
19. ∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc)
20. ∀a,b:Point.  (a # b ⇒ b # a)
21. a : Point
22. b : Point
23. c : Point
24. a ≡ b
⊢ ac ≅ cb

3
1. g : EuclideanPlane
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:Point.  (a # bc ⇒ (¬Colinear(a;b;c)))
16. SqStable(geo-left-axioms(g))
17. ∀a:Point. a ≡ a
18. ∀a,b:Point.  ab ≅ ba
19. ∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc)
20. ∀a,b:Point.  (a # b ⇒ b # a)
21. a : Point
22. b : Point
23. c : Point
24. d : Point
25. cd ≥ ab
26. a # b
⊢ c # d

4
1. g : EuclideanPlane
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:Point.  (a # bc ⇒ (¬Colinear(a;b;c)))
16. SqStable(geo-left-axioms(g))
17. ∀a:Point. a ≡ a
18. ∀a,b:Point.  ab ≅ ba
19. ∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc)
20. ∀a,b:Point.  (a # b ⇒ b # a)
21. a : Point
22. b : Point
23. c : Point
24. a ≡ b
⊢ B(abc)

5
1. g : EuclideanPlane
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:Point.  (a # bc ⇒ (¬Colinear(a;b;c)))
16. SqStable(geo-left-axioms(g))
17. ∀a:Point. a ≡ a
18. ∀a,b:Point.  ab ≅ ba
19. ∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc)
20. ∀a,b:Point.  (a # b ⇒ b # a)
21. a : Point
22. b : Point
23. c : Point
24. B(abc)
⊢ B(cba)

6
1. g : EuclideanPlane
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:Point.  (a # bc ⇒ (¬Colinear(a;b;c)))
16. SqStable(geo-left-axioms(g))
17. ∀a:Point. a ≡ a
18. ∀a,b:Point.  ab ≅ ba
19. ∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc)
20. ∀a,b:Point.  (a # b ⇒ b # a)
21. a : Point
22. b : Point
23. p : Point
24. q : Point
25. r : Point
26. s : Point
27. ab ≅ pq
28. ab ≅ rs
⊢ pq ≅ rs

7
1. g : EuclideanPlane
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:Point.  (a # bc ⇒ (¬Colinear(a;b;c)))
16. SqStable(geo-left-axioms(g))
17. ∀a:Point. a ≡ a
18. ∀a,b:Point.  ab ≅ ba
19. ∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc)
20. ∀a,b:Point.  (a # b ⇒ b # a)
21. a : Point
22. b : Point
⊢ aa ≅ bb

8
1. g : EuclideanPlane
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:Point.  (a # bc ⇒ (¬Colinear(a;b;c)))
16. SqStable(geo-left-axioms(g))
17. ∀a:Point. a ≡ a
18. ∀a,b:Point.  ab ≅ ba
19. ∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc)
20. ∀a,b:Point.  (a # b ⇒ b # a)
21. a : Point
22. b : Point
23. x : Point
24. y : Point
25. z : Point
26. x leftof ab
27. y leftof ab
28. B(xzy)
⊢ z # ab

Latex:

Latex:
1. g : EuclideanPlane 2. BasicGeometryAxioms(g) \mwedge{} (\mforall{}a,b,c:Point. (a \# bc {}\mRightarrow{} (\mneg{}Colinear(a;b;c)))) 3. SqStable(geo-left-axioms(g)) 4. (\mforall{}a:Point. a \mequiv{} a) \mwedge{} (\mforall{}a,b:Point. ab \mcong{} ba) \mwedge{} (\mforall{}a,b,c:Point. (a \mequiv{} b {}\mRightarrow{} ac \mcong{} bc)) 5. \mforall{}a,b:Point. (a \# b {}\mRightarrow{} b \# a) \mvdash{} ((\mforall{}a,b:Point. (a \# b {}\mRightarrow{} b \# a)) \mwedge{} (\mforall{}a:Point. (\mneg{}a \# a)) \mwedge{} (\mforall{}a,b,x,y:Point. (a \mequiv{} b {}\mRightarrow{} B(xay) {}\mRightarrow{} B(xby))) \mwedge{} ((\mforall{}a,b,c:Point. (a \mequiv{} b {}\mRightarrow{} ac \mcong{} cb)) \mwedge{} (\mforall{}a,b,c:Point. (a \mequiv{} b {}\mRightarrow{} ac \mcong{} bc))) \mwedge{} (\mforall{}a,b,c,d:Point. (cd \mgeq{} ab {}\mRightarrow{} a \# b {}\mRightarrow{} c \# d)) \mwedge{} (\mforall{}a,b,c:Point. (a \mequiv{} 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. ab \mcong{} ba) \mwedge{} (\mforall{}a,b,p,q,r,s:Point. (ab \mcong{} pq {}\mRightarrow{} ab \mcong{} rs {}\mRightarrow{} pq \mcong{} rs)) \mwedge{} (\mforall{}a,b:Point. aa \mcong{} bb) \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:Point. (\mneg{}a \# bc \mLeftarrow{}{}\mRightarrow{} Colinear(a;b;c))) \mwedge{} (\mforall{}a,b,c:Point. (a leftof bc {}\mRightarrow{} b leftof ca)) \mwedge{} (\mforall{}a,b,c:Point. (a leftof bc {}\mRightarrow{} b \# c)) \mwedge{} (\mforall{}a,b,x,y,z:Point. (x leftof ab {}\mRightarrow{} y leftof ab {}\mRightarrow{} B(xzy) {}\mRightarrow{} z \# ab)) \mwedge{} (\mforall{}a,b,c,y:Point. (a \# bc {}\mRightarrow{} y \# b {}\mRightarrow{} Colinear(y;a;b) {}\mRightarrow{} y \# bc)) By Latex: (RepeatFor 2 (D 2) THEN SplitAndHyps THEN SplitAndConcl THEN Try (Hypothesis) THEN Auto) Home Index