Step
*
2
1
of Lemma
geo-ge_functionality
1. e : EuclideanPlaneStructure
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@0,f:Point. (ab>cd ⇒ cd ≥ e@0f ⇒ ab>e@0f)
6. ∀a,b,c,d,e@0,f:Point. (ab ≥ cd ⇒ cd>e@0f ⇒ ab>e@0f)
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. a1 : Point
16. a2 : Point
17. b1 : Point
18. b2 : Point
19. c1 : Point
20. c2 : Point
21. d1 : Point
22. d2 : Point
23. a1 ≡ a2
24. b1 ≡ b2
25. c1 ≡ c2
26. d1 ≡ d2
27. ∀a:Point. a ≡ a
28. ∀a,b:Point. ab ≅ ba
29. ∀a,b,c:Point. (a ≡ b ⇒ ac ≅ bc)
30. a2b2 ≥ c2d2
31. c1d1>a1b1
32. a1b1 ≥ a2b2
33. c1d1>a2b2
⊢ False
BY
{ (InstHyp [⌜c1⌝;⌜d1⌝;⌜a2⌝;⌜b2⌝;⌜c2⌝;⌜d2⌝] (6)⋅ THEN Auto) }
1
.....antecedent.....
1. e : EuclideanPlaneStructure
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@0,f:Point. (ab>cd ⇒ cd ≥ e@0f ⇒ ab>e@0f)
6. ∀a,b,c,d,e@0,f:Point. (ab ≥ cd ⇒ cd>e@0f ⇒ ab>e@0f)
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. a1 : Point
16. a2 : Point
17. b1 : Point
18. b2 : Point
19. c1 : Point
20. c2 : Point
21. d1 : Point
22. d2 : Point
23. a1 ≡ a2
24. b1 ≡ b2
25. c1 ≡ c2
26. d1 ≡ d2
27. ∀a:Point. a ≡ a
28. ∀a,b:Point. ab ≅ ba
29. ∀a,b,c:Point. (a ≡ b ⇒ ac ≅ bc)
30. a2b2 ≥ c2d2
31. c1d1>a1b1
32. a1b1 ≥ a2b2
33. c1d1>a2b2
⊢ a2b2>c2d2
2
1. e : EuclideanPlaneStructure
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@0,f:Point. (ab>cd ⇒ cd ≥ e@0f ⇒ ab>e@0f)
6. ∀a,b,c,d,e@0,f:Point. (ab ≥ cd ⇒ cd>e@0f ⇒ ab>e@0f)
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. a1 : Point
16. a2 : Point
17. b1 : Point
18. b2 : Point
19. c1 : Point
20. c2 : Point
21. d1 : Point
22. d2 : Point
23. a1 ≡ a2
24. b1 ≡ b2
25. c1 ≡ c2
26. d1 ≡ d2
27. ∀a:Point. a ≡ a
28. ∀a,b:Point. ab ≅ ba
29. ∀a,b,c:Point. (a ≡ b ⇒ ac ≅ bc)
30. a2b2 ≥ c2d2
31. c1d1>a1b1
32. a1b1 ≥ a2b2
33. c1d1>a2b2
34. c1d1>c2d2
⊢ False
Latex:
Latex:
1. e : EuclideanPlaneStructure
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@0,f:Point. (ab>cd {}\mRightarrow{} cd \mgeq{} e@0f {}\mRightarrow{} ab>e@0f)
6. \mforall{}a,b,c,d,e@0,f:Point. (ab \mgeq{} cd {}\mRightarrow{} cd>e@0f {}\mRightarrow{} ab>e@0f)
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. a1 : Point
16. a2 : Point
17. b1 : Point
18. b2 : Point
19. c1 : Point
20. c2 : Point
21. d1 : Point
22. d2 : Point
23. a1 \mequiv{} a2
24. b1 \mequiv{} b2
25. c1 \mequiv{} c2
26. d1 \mequiv{} d2
27. \mforall{}a:Point. a \mequiv{} a
28. \mforall{}a,b:Point. ab \mcong{} ba
29. \mforall{}a,b,c:Point. (a \mequiv{} b {}\mRightarrow{} ac \mcong{} bc)
30. a2b2 \mgeq{} c2d2
31. c1d1>a1b1
32. a1b1 \mgeq{} a2b2
33. c1d1>a2b2
\mvdash{} False
By
Latex:
(InstHyp [\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}d1\mkleeneclose{};\mkleeneopen{}a2\mkleeneclose{};\mkleeneopen{}b2\mkleeneclose{};\mkleeneopen{}c2\mkleeneclose{};\mkleeneopen{}d2\mkleeneclose{}] (6)\mcdot{} THEN Auto)
Home
Index