Step
*
1
1
1
1
1
of Lemma
implies-geo-between_functionality
.....antecedent.....
1. e : EuclideanPlaneStructure
2. ∀a,b:Point. (a # b ⇒ b # a)
3. ∀a,b,c,d:Point. (ab>cd ⇒ ab ≥ cd)
4. ∀a,b,c:Point. (ba>ac ⇒ b # c)
5. ∀a,b,c:Point. bc ≥ aa
6. ∀a,b,c,d,e@0,f:Point. (ab>cd ⇒ cd ≥ e@0f ⇒ ab>e@0f)
7. ∀a,b,c,d,e@0,f:Point. (ab ≥ cd ⇒ cd>e@0f ⇒ ab>e@0f)
8. ∀a,b,c:Point. (B(abc) ⇒ b # c ⇒ ac>ab)
9. ∀a,b,c:Point. (a leftof bc ⇒ b leftof ca)
10. ∀a,b,c:Point. (a leftof bc ⇒ b # c)
11. ∀a,b,c,d:Point. (B(abd) ⇒ B(bcd) ⇒ B(abc))
12. ∀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)
13. ∀a,b,c,x,y:Point. (ax ≅ ay ⇒ bx ≅ by ⇒ cx ≅ cy ⇒ x # y ⇒ (¬a # bc))
14. ∀a,b,x,y,z:Point. (x leftof ab ⇒ y leftof ab ⇒ B(xzy) ⇒ z leftof ab)
15. ∀a,b,c,y:Point. (a # bc ⇒ y # b ⇒ (¬y # ab) ⇒ y # bc)
16. ∀a,b1,b2,c:Point. (b1 ≡ b2 ⇒ B(ab1c) ⇒ B(ab2c))
17. ∀a1,a2,b,c:Point. (a1 ≡ a2 ⇒ B(a1bc) ⇒ B(a2bc))
18. ∀a:Point. a ≡ a
19. ∀a,b:Point. ab ≅ ba
20. ∀a,b,c:Point. (a ≡ b ⇒ ac ≅ bc)
21. ∀a,b:Point. (a # b ⇒ b # a)
22. ∀x,y:Point. (x ≡ y ⇒ y ≡ x)
23. ∀x:Point. x ≡ x
24. ∀a,b,c,d:Point. (B(abd) ⇒ B(bcd) ⇒ B(abc))
25. a : Point
26. b : Point
27. c1 : Point
28. c2 : Point
29. c1 ≡ c2
30. B(abc1)
⊢ B(bc2c1)
BY
{ ((Assert ∀a,b,x,y:Point. ((¬ab>aa) ⇒ a leftof xy ⇒ b leftof xy) BY
(Auto
THEN (Assert B(a1b1a1) BY
(Unfold `geo-between` 0
THEN Auto
THEN (D 0 THEN Auto)
THEN Unfold `geo-lsep` -1
THEN D -1
THEN Auto))
THEN InstHyp [⌜x⌝;⌜y⌝;⌜a1⌝;⌜a1⌝;⌜b1⌝] (14)⋅
THEN Auto))
THEN (Assert ∀a,b,c,d,e1,f:Point. (ab ≥ cd ⇒ cd ≥ e1f ⇒ ab ≥ e1f) BY
(Intros THEN RepeatFor 2 (ParallelLast) THEN Auto))
) }
1
1. e : EuclideanPlaneStructure
2. ∀a,b:Point. (a # b ⇒ b # a)
3. ∀a,b,c,d:Point. (ab>cd ⇒ ab ≥ cd)
4. ∀a,b,c:Point. (ba>ac ⇒ b # c)
5. ∀a,b,c:Point. bc ≥ aa
6. ∀a,b,c,d,e@0,f:Point. (ab>cd ⇒ cd ≥ e@0f ⇒ ab>e@0f)
7. ∀a,b,c,d,e@0,f:Point. (ab ≥ cd ⇒ cd>e@0f ⇒ ab>e@0f)
8. ∀a,b,c:Point. (B(abc) ⇒ b # c ⇒ ac>ab)
9. ∀a,b,c:Point. (a leftof bc ⇒ b leftof ca)
10. ∀a,b,c:Point. (a leftof bc ⇒ b # c)
11. ∀a,b,c,d:Point. (B(abd) ⇒ B(bcd) ⇒ B(abc))
12. ∀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)
13. ∀a,b,c,x,y:Point. (ax ≅ ay ⇒ bx ≅ by ⇒ cx ≅ cy ⇒ x # y ⇒ (¬a # bc))
14. ∀a,b,x,y,z:Point. (x leftof ab ⇒ y leftof ab ⇒ B(xzy) ⇒ z leftof ab)
15. ∀a,b,c,y:Point. (a # bc ⇒ y # b ⇒ (¬y # ab) ⇒ y # bc)
16. ∀a,b1,b2,c:Point. (b1 ≡ b2 ⇒ B(ab1c) ⇒ B(ab2c))
17. ∀a1,a2,b,c:Point. (a1 ≡ a2 ⇒ B(a1bc) ⇒ B(a2bc))
18. ∀a:Point. a ≡ a
19. ∀a,b:Point. ab ≅ ba
20. ∀a,b,c:Point. (a ≡ b ⇒ ac ≅ bc)
21. ∀a,b:Point. (a # b ⇒ b # a)
22. ∀x,y:Point. (x ≡ y ⇒ y ≡ x)
23. ∀x:Point. x ≡ x
24. ∀a,b,c,d:Point. (B(abd) ⇒ B(bcd) ⇒ B(abc))
25. a : Point
26. b : Point
27. c1 : Point
28. c2 : Point
29. c1 ≡ c2
30. B(abc1)
31. ∀a,b,x,y:Point. ((¬ab>aa) ⇒ a leftof xy ⇒ b leftof xy)
32. ∀a,b,c,d,e1,f:Point. (ab ≥ cd ⇒ cd ≥ e1f ⇒ ab ≥ e1f)
⊢ B(bc2c1)
Latex:
Latex:
.....antecedent.....
1. e : EuclideanPlaneStructure
2. \mforall{}a,b:Point. (a \# b {}\mRightarrow{} b \# a)
3. \mforall{}a,b,c,d:Point. (ab>cd {}\mRightarrow{} ab \mgeq{} cd)
4. \mforall{}a,b,c:Point. (ba>ac {}\mRightarrow{} b \# c)
5. \mforall{}a,b,c:Point. bc \mgeq{} aa
6. \mforall{}a,b,c,d,e@0,f:Point. (ab>cd {}\mRightarrow{} cd \mgeq{} e@0f {}\mRightarrow{} ab>e@0f)
7. \mforall{}a,b,c,d,e@0,f:Point. (ab \mgeq{} cd {}\mRightarrow{} cd>e@0f {}\mRightarrow{} ab>e@0f)
8. \mforall{}a,b,c:Point. (B(abc) {}\mRightarrow{} b \# c {}\mRightarrow{} ac>ab)
9. \mforall{}a,b,c:Point. (a leftof bc {}\mRightarrow{} b leftof ca)
10. \mforall{}a,b,c:Point. (a leftof bc {}\mRightarrow{} b \# c)
11. \mforall{}a,b,c,d:Point. (B(abd) {}\mRightarrow{} B(bcd) {}\mRightarrow{} B(abc))
12. \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)
13. \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))
14. \mforall{}a,b,x,y,z:Point. (x leftof ab {}\mRightarrow{} y leftof ab {}\mRightarrow{} B(xzy) {}\mRightarrow{} z leftof ab)
15. \mforall{}a,b,c,y:Point. (a \# bc {}\mRightarrow{} y \# b {}\mRightarrow{} (\mneg{}y \# ab) {}\mRightarrow{} y \# bc)
16. \mforall{}a,b1,b2,c:Point. (b1 \mequiv{} b2 {}\mRightarrow{} B(ab1c) {}\mRightarrow{} B(ab2c))
17. \mforall{}a1,a2,b,c:Point. (a1 \mequiv{} a2 {}\mRightarrow{} B(a1bc) {}\mRightarrow{} B(a2bc))
18. \mforall{}a:Point. a \mequiv{} a
19. \mforall{}a,b:Point. ab \mcong{} ba
20. \mforall{}a,b,c:Point. (a \mequiv{} b {}\mRightarrow{} ac \mcong{} bc)
21. \mforall{}a,b:Point. (a \# b {}\mRightarrow{} b \# a)
22. \mforall{}x,y:Point. (x \mequiv{} y {}\mRightarrow{} y \mequiv{} x)
23. \mforall{}x:Point. x \mequiv{} x
24. \mforall{}a,b,c,d:Point. (B(abd) {}\mRightarrow{} B(bcd) {}\mRightarrow{} B(abc))
25. a : Point
26. b : Point
27. c1 : Point
28. c2 : Point
29. c1 \mequiv{} c2
30. B(abc1)
\mvdash{} B(bc2c1)
By
Latex:
((Assert \mforall{}a,b,x,y:Point. ((\mneg{}ab>aa) {}\mRightarrow{} a leftof xy {}\mRightarrow{} b leftof xy) BY
(Auto
THEN (Assert B(a1b1a1) BY
(Unfold `geo-between` 0
THEN Auto
THEN (D 0 THEN Auto)
THEN Unfold `geo-lsep` -1
THEN D -1
THEN Auto))
THEN InstHyp [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{}] (14)\mcdot{}
THEN Auto))
THEN (Assert \mforall{}a,b,c,d,e1,f:Point. (ab \mgeq{} cd {}\mRightarrow{} cd \mgeq{} e1f {}\mRightarrow{} ab \mgeq{} e1f) BY
(Intros THEN RepeatFor 2 (ParallelLast) THEN Auto))
)
Home
Index