---

Step * 2 of Lemma geo-ge_functionality


1. e : EuclideanPlane
2. a1 : Point
3. a2 : Point
4. b1 : Point
5. b2 : Point
6. c1 : Point
7. c2 : Point
8. d1 : Point
9. d2 : Point
10. a1 ≡ a2
11. b1 ≡ b2
12. c1 ≡ c2
13. d1 ≡ d2
14. ∀a:Point. a ≡ a
15. ∀a,b:Point.  ab ≅ ba
16. ∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc)
17. ¬c2d2>a2b2
18. c1d1>a1b1
⊢ False
BY
{ ((Assert a1b1 ≥ a2b2 BY
          ((Assert a1b1 ≅ a2b2 BY
                  (Auto
                   THEN InstLemma  `geo-congruent-functionality-lemma` [⌜e⌝;⌜a1⌝;⌜a1⌝;⌜b1⌝;⌜b1⌝;⌜a1⌝;⌜a2⌝;⌜b1⌝;⌜b2⌝]⋅
                   THEN Auto))
           THEN (((D 0 THENA Auto) THEN Unfold `geo-congruent` -2 THEN D -2) THEN Unfold `geo-length-sep` 0 THEN OrLeft)
           THEN Auto))
   THEN Fold`geo-ge`(-3)
   THEN ((D 1 THEN Unhide) THEN D 2)
   THEN ExRepD
   THEN InstHyp [⌜c1⌝;⌜d1⌝;⌜a1⌝;⌜b1⌝;⌜a2⌝;⌜b2⌝] (5)⋅
   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. 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

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a1  :  Point
3.  a2  :  Point
4.  b1  :  Point
5.  b2  :  Point
6.  c1  :  Point
7.  c2  :  Point
8.  d1  :  Point
9.  d2  :  Point
10.  a1  \mequiv{}  a2
11.  b1  \mequiv{}  b2
12.  c1  \mequiv{}  c2
13.  d1  \mequiv{}  d2
14.  \mforall{}a:Point.  a  \mequiv{}  a
15.  \mforall{}a,b:Point.    ab  \mcong{}  ba
16.  \mforall{}a,b,c:Point.    (a  \mequiv{}  b  {}\mRightarrow{}  ac  \mcong{}  bc)
17.  \mneg{}c2d2>a2b2
18.  c1d1>a1b1
\mvdash{}  False


By

---

Latex:
((Assert  a1b1  \mgeq{}  a2b2  BY
                ((Assert  a1b1  \mcong{}  a2b2  BY
                                (Auto
                                  THEN  InstLemma    `geo-congruent-functionality-lemma`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};
                                  \mkleeneopen{}a2\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}b2\mkleeneclose{}]\mcdot{}
                                  THEN  Auto))
                  THEN  (((D  0  THENA  Auto)  THEN  Unfold  `geo-congruent`  -2  THEN  D  -2)
                              THEN  Unfold  `geo-length-sep`  0
                              THEN  OrLeft)
                  THEN  Auto))
  THEN  Fold`geo-ge`(-3)
  THEN  ((D  1  THEN  Unhide)  THEN  D  2)
  THEN  ExRepD
  THEN  InstHyp  [\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}d1\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}a2\mkleeneclose{};\mkleeneopen{}b2\mkleeneclose{}]  (5)\mcdot{}
  THEN  Auto)

---

Home Index