---

Step * 1 of Lemma geo-axioms-imply


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)
BY
{ ((Assert ∀a,b:Point.  (b # a ⇒ a # b) BY
          (ThinVar `a' THEN ThinVar `b' THEN Auto THEN ParallelLast THEN (Assert ¬aa>bb BY Auto) THEN Auto))
   THEN (Assert ∀a,b,x,y:Point.  ((¬ab>aa) ⇒ a leftof xy ⇒ b leftof xy) BY
               (ThinVar `a'
                THEN ThinVar `b'
                THEN Auto
                THEN (Assert B(aba) BY
                            (D 0 THEN Auto THEN (D 0 THENA Auto) THEN D -1 THEN Auto))
                THEN Auto))
   THEN Fold `geo-sep` (-1)
   THEN (Assert ¬b # a BY
               (ParallelOp -4 THEN Auto))
   THEN (Assert ∀a,b,c,d,e,f:Point.  (ab ≥ cd ⇒ cd ≥ ef ⇒ ab ≥ ef) BY
               (Intros THEN RepeatFor 2 (ParallelLast) 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)
26. ∀a,b:Point.  (b # a ⇒ a # b)
27. ∀a,b,x,y:Point.  ((¬a # b) ⇒ a leftof xy ⇒ b leftof xy)
28. ¬b # a
29. ∀a,b,c,d,e,f:Point.  (ab ≥ cd ⇒ cd ≥ ef ⇒ ab ≥ ef)
⊢ B(xby)

---

Latex:

---

Latex:

1.  g  :  GeometryPrimitives
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,f:Point.    (ab>cd  {}\mRightarrow{}  cd  \mgeq{}  ef  {}\mRightarrow{}  ab>ef)
6.  \mforall{}a,b,c,d,e,f:Point.    (ab  \mgeq{}  cd  {}\mRightarrow{}  cd>ef  {}\mRightarrow{}  ab>ef)
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.  \mforall{}a,b,c,d,x,y:Point.    (ab  \mcong{}  cd  {}\mRightarrow{}  cd>xy  {}\mRightarrow{}  ab>xy)
16.  \mforall{}a:Point.  (\mneg{}a  \#  a)
17.  \mforall{}a,b:Point.    ba  \mgeq{}  ab
18.  \mforall{}a,b,c,d:Point.    (ab>cd  {}\mRightarrow{}  ba>cd)
19.  \mforall{}a,b,c,d:Point.    (ab>cd  {}\mRightarrow{}  ab>dc)
20.  a  :  Point
21.  b  :  Point
22.  x  :  Point
23.  y  :  Point
24.  \mneg{}a  \#  b
25.  B(xay)
\mvdash{}  B(xby)


By

---

Latex:
((Assert  \mforall{}a,b:Point.    (b  \#  a  {}\mRightarrow{}  a  \#  b)  BY
                (ThinVar  `a'
                  THEN  ThinVar  `b'
                  THEN  Auto
                  THEN  ParallelLast
                  THEN  (Assert  \mneg{}aa>bb  BY
                                          Auto)
                  THEN  Auto))
  THEN  (Assert  \mforall{}a,b,x,y:Point.    ((\mneg{}ab>aa)  {}\mRightarrow{}  a  leftof  xy  {}\mRightarrow{}  b  leftof  xy)  BY
                          (ThinVar  `a'
                            THEN  ThinVar  `b'
                            THEN  Auto
                            THEN  (Assert  B(aba)  BY
                                                    (D  0  THEN  Auto  THEN  (D  0  THENA  Auto)  THEN  D  -1  THEN  Auto))
                            THEN  Auto))
  THEN  Fold  `geo-sep`  (-1)
  THEN  (Assert  \mneg{}b  \#  a  BY
                          (ParallelOp  -4  THEN  Auto))
  THEN  (Assert  \mforall{}a,b,c,d,e,f:Point.    (ab  \mgeq{}  cd  {}\mRightarrow{}  cd  \mgeq{}  ef  {}\mRightarrow{}  ab  \mgeq{}  ef)  BY
                          (Intros  THEN  RepeatFor  2  (ParallelLast)  THEN  Auto)))

---

Home Index