---

Step * 1 1 1 1 1 of Lemma geo-lt-implies-gt


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. |cd| < |ab|
7. c ≠ d
8. a ≠ b
9. B : Point
10. b-a-B
11. aB ≅ dc
12. a' : Point
13. B_a_a'
14. aa' ≅ cd
15. a' ≠ b
16. |aa'| ≤ |ab| ⇐⇒ a_a'_b
⊢ ¬¬ab > cd
BY
{ (((D -1 THEN D -2)
    THENA ((InstLemma `geo-congruent-iff-length` [⌜g⌝;⌜a⌝;⌜a'⌝;⌜c⌝;⌜d⌝]⋅ THENA Auto)
           THEN D -1
           THEN D -2
           THEN ((Assert |cd| = |aa'| ∈ Length BY Auto) THEN RWO "-1" (6) THEN Auto)
           THEN EAuto 1)
    )
   THEN (RemoveDoubleNegation THEN Auto)
   THEN (Unfold `geo-gt` 0 THEN D 0 THEN D 0 With ⌜a'⌝ )
   THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  |cd|  <  |ab|
7.  c  \mneq{}  d
8.  a  \mneq{}  b
9.  B  :  Point
10.  b-a-B
11.  aB  \mcong{}  dc
12.  a'  :  Point
13.  B\_a\_a'
14.  aa'  \mcong{}  cd
15.  a'  \mneq{}  b
16.  |aa'|  \mleq{}  |ab|  \mLeftarrow{}{}\mRightarrow{}  a\_a'\_b
\mvdash{}  \mneg{}\mneg{}ab  >  cd


By

---

Latex:
(((D  -1  THEN  D  -2)
    THENA  ((InstLemma  `geo-congruent-iff-length`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto)
                  THEN  D  -1
                  THEN  D  -2
                  THEN  ((Assert  |cd|  =  |aa'|  BY  Auto)  THEN  RWO  "-1"  (6)  THEN  Auto)
                  THEN  EAuto  1)
    )
  THEN  (RemoveDoubleNegation  THEN  Auto)
  THEN  (Unfold  `geo-gt`  0  THEN  D  0  THEN  D  0  With  \mkleeneopen{}a'\mkleeneclose{}  )
  THEN  Auto)

---

Home Index