---

Step * 2 1 1 of Lemma geo-ge_functionality

.....antecedent..... 
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
⊢ a2b2>c2d2
BY
{ ((Assert e ∈ EuclideanPlane BY
          ((MemTypeCD THEN Auto) THEN D 0 THEN Auto))
   THEN (Assert c1d1 ≅ c2d2 BY
               (Auto
                THEN InstLemma  `geo-congruent-functionality-lemma` [⌜e⌝;⌜c1⌝;⌜c1⌝;⌜d1⌝;⌜d1⌝;⌜c1⌝;⌜c2⌝;⌜d1⌝;⌜d2⌝]⋅
                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
34. e ∈ EuclideanPlane
35. c1d1 ≅ c2d2
⊢ a2b2>c2d2

---

Latex:

---

Latex:
.....antecedent..... 
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.  b1  :  Point
18.  b2  :  Point
19.  c1  :  Point
20.  c2  :  Point
21.  d1  :  Point
22.  d2  :  Point
23.  a1  \mequiv{}  a2
24.  b1  \mequiv{}  b2
25.  c1  \mequiv{}  c2
26.  d1  \mequiv{}  d2
27.  \mforall{}a:Point.  a  \mequiv{}  a
28.  \mforall{}a,b:Point.    ab  \mcong{}  ba
29.  \mforall{}a,b,c:Point.    (a  \mequiv{}  b  {}\mRightarrow{}  ac  \mcong{}  bc)
30.  a2b2  \mgeq{}  c2d2
31.  c1d1>a1b1
32.  a1b1  \mgeq{}  a2b2
33.  c1d1>a2b2
\mvdash{}  a2b2>c2d2


By

---

Latex:
((Assert  e  \mmember{}  EuclideanPlane  BY
                ((MemTypeCD  THEN  Auto)  THEN  D  0  THEN  Auto))
  THEN  (Assert  c1d1  \mcong{}  c2d2  BY
                          (Auto
                            THEN  InstLemma    `geo-congruent-functionality-lemma`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}d1\mkleeneclose{};\mkleeneopen{}d1\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}c2\mkleeneclose{}
                            ;\mkleeneopen{}d1\mkleeneclose{};\mkleeneopen{}d2\mkleeneclose{}]\mcdot{}
                            THEN  Auto))
  )

---

Home Index