Step
*
1
1
of Lemma
basic-axioms-imply_between1
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. b : Point
18. c : Point
19. a1 ≡ a2
20. B(a1bc)
21. ∀a:Point. a ≡ a
22. ∀a,b:Point.  ab ≅ ba
23. ∀a,b,c:Point.  (a ≡ b 
⇒ ac ≅ bc)
24. ∀a,b:Point.  (a # b 
⇒ b # a)
25. ∀a,b,x,y:Point.  ((¬ab>aa) 
⇒ a leftof xy 
⇒ b leftof xy)
⊢ B(a2bc)
BY
{ (Fold `geo-sep` (-1)
   THEN (Unfold `geo-eq` -7 THEN (Assert ¬a2 # a1 BY (ParallelOp -7 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,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. b : Point
18. c : Point
19. ¬a1 # a2
20. B(a1bc)
21. ∀a:Point. a ≡ a
22. ∀a,b:Point.  ab ≅ ba
23. ∀a,b,c:Point.  (a ≡ b 
⇒ ac ≅ bc)
24. ∀a,b:Point.  (a # b 
⇒ b # a)
25. ∀a,b,x,y:Point.  ((¬a # b) 
⇒ a leftof xy 
⇒ b leftof xy)
26. ¬a2 # a1
27. ∀a,b,c,d,e1,f:Point.  (ab ≥ cd 
⇒ cd ≥ e1f 
⇒ ab ≥ e1f)
⊢ B(a2bc)
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.  b  :  Point
18.  c  :  Point
19.  a1  \mequiv{}  a2
20.  B(a1bc)
21.  \mforall{}a:Point.  a  \mequiv{}  a
22.  \mforall{}a,b:Point.    ab  \mcong{}  ba
23.  \mforall{}a,b,c:Point.    (a  \mequiv{}  b  {}\mRightarrow{}  ac  \mcong{}  bc)
24.  \mforall{}a,b:Point.    (a  \#  b  {}\mRightarrow{}  b  \#  a)
25.  \mforall{}a,b,x,y:Point.    ((\mneg{}ab>aa)  {}\mRightarrow{}  a  leftof  xy  {}\mRightarrow{}  b  leftof  xy)
\mvdash{}  B(a2bc)
By
Latex:
(Fold  `geo-sep`  (-1)
  THEN  (Unfold  `geo-eq`  -7  THEN  (Assert  \mneg{}a2  \#  a1  BY  (ParallelOp  -7  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