---

Step * of Lemma implies-geo-between_functionality

No Annotations
∀e:EuclideanPlaneStructure
  (BasicGeometryAxioms(e) ⇒ (∀a1,a2,b1,b2,c1,c2:Point.  (a1 ≡ a2 ⇒ b1 ≡ b2 ⇒ c1 ≡ c2 ⇒ (B(a1b1c1) ⇐⇒ B(a2b2c2)))))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (((InstLemma `basic-axioms-imply_between2` [⌜e⌝]⋅ THENA Auto)
          THEN (InstLemma `basic-axioms-imply_between1` [⌜e⌝]⋅ THENA Auto)
          )
         THEN (InstLemma `basic-geo-axioms-imply` [⌜e⌝]⋅ THENA Auto)
         THEN (InstLemma `basic-geo-sep-sym` [⌜e⌝]⋅ THENA Auto))
   THEN (InstLemma `basic-geo-sep-sym` [⌜e⌝]⋅ THENA Auto)
   THEN PromoteHyp (-1) 2
   THEN (D -5 THEN SplitAndHyps)
   THEN (Assert ∀x,y:Point.  (x ≡ y ⇒ y ≡ x) BY
               (Auto THEN RepeatFor 2 (ParallelLast) THEN Auto))
   THEN (Assert ∀x:Point. x ≡ x BY
               ((Auto THEN Unfold `geo-eq` 0 THEN Auto)
                THEN (D 0 THEN Auto)
                THEN Unfold `geo-sep` -1
                THEN InstHyp [⌜x⌝;⌜x⌝;⌜x⌝] (4)⋅
                THEN Auto))
   THEN Assert ⌜∀a1,a2,b1,b2,c1,c2:Point.  (a1 ≡ a2 ⇒ b1 ≡ b2 ⇒ c1 ≡ c2 ⇒ B(a1b1c1) ⇒ B(a2b2c2))⌝⋅) }

1
.....assertion..... 
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
⊢ ∀a1,a2,b1,b2,c1,c2:Point.  (a1 ≡ a2 ⇒ b1 ≡ b2 ⇒ c1 ≡ c2 ⇒ B(a1b1c1) ⇒ B(a2b2c2))

2
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. ∀a1,a2,b1,b2,c1,c2:Point.  (a1 ≡ a2 ⇒ b1 ≡ b2 ⇒ c1 ≡ c2 ⇒ B(a1b1c1) ⇒ B(a2b2c2))
⊢ ∀a1,a2,b1,b2,c1,c2:Point.  (a1 ≡ a2 ⇒ b1 ≡ b2 ⇒ c1 ≡ c2 ⇒ (B(a1b1c1) ⇐⇒ B(a2b2c2)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlaneStructure
    (BasicGeometryAxioms(e)
    {}\mRightarrow{}  (\mforall{}a1,a2,b1,b2,c1,c2:Point.    (a1  \mequiv{}  a2  {}\mRightarrow{}  b1  \mequiv{}  b2  {}\mRightarrow{}  c1  \mequiv{}  c2  {}\mRightarrow{}  (B(a1b1c1)  \mLeftarrow{}{}\mRightarrow{}  B(a2b2c2)))))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (((InstLemma  `basic-axioms-imply\_between2`  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (InstLemma  `basic-axioms-imply\_between1`  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
                )
              THEN  (InstLemma  `basic-geo-axioms-imply`  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (InstLemma  `basic-geo-sep-sym`  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  (InstLemma  `basic-geo-sep-sym`  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  PromoteHyp  (-1)  2
  THEN  (D  -5  THEN  SplitAndHyps)
  THEN  (Assert  \mforall{}x,y:Point.    (x  \mequiv{}  y  {}\mRightarrow{}  y  \mequiv{}  x)  BY
                          (Auto  THEN  RepeatFor  2  (ParallelLast)  THEN  Auto))
  THEN  (Assert  \mforall{}x:Point.  x  \mequiv{}  x  BY
                          ((Auto  THEN  Unfold  `geo-eq`  0  THEN  Auto)
                            THEN  (D  0  THEN  Auto)
                            THEN  Unfold  `geo-sep`  -1
                            THEN  InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  (4)\mcdot{}
                            THEN  Auto))
  THEN  Assert  \mkleeneopen{}\mforall{}a1,a2,b1,b2,c1,c2:Point.    (a1  \mequiv{}  a2  {}\mRightarrow{}  b1  \mequiv{}  b2  {}\mRightarrow{}  c1  \mequiv{}  c2  {}\mRightarrow{}  B(a1b1c1)  {}\mRightarrow{}  B(a2b2c2))\mkleeneclose{}
  \mcdot{})

---

Home Index