---

Step * 1 1 1 3 2 1 1 2 of Lemma geo-lt-add1-iff2


1. e : BasicGeometry
2. a1 : Point
3. a2 : Point
4. b1 : Point
5. b2 : Point
6. c1 : Point
7. c2 : Point
8. a : Point
9. b : Point
10. a # b
11. p' : Point
12. B(OXp')
13. q' : {p:Point| B(OXp)} 
14. p' = |a1a2| + |ab| ∈ Length
15. q' = |b1b2| ∈ Length
16. B(Xp'q')
17. a # b
18. X # p'
19. X # q'
20. P : Point
21. B(Xp'P)
22. p'P ≅ c1c2
23. Q : Point
24. B(Xq'Q)
25. q'Q ≅ c1c2
26. P = |a1a2| + |c1c2| + |ab| ∈ Length
27. Q = |b1b2| + |c1c2| ∈ Length
28. P # q'
29. B(Xq'P)
30. P # Q
31. B(XQP)
32. Q < P
33. Q ≤ P
34. Q # P
⊢ False
BY
{ (((Assert Q = |XQ| ∈ Length BY
           Auto)
    THEN (Assert P = |XP| ∈ Length BY
                Auto)
    THEN (RWO "-1" 32 THENA Auto)
    THEN (RWO "-2" 32 THENA Auto))
   THEN ((Subst' |XQ| = |b1b2| + |c1c2| ∈ Length 32 THEN Auto)
         THEN (Subst' |XP| = |a1a2| + |c1c2| + |ab| ∈ Length 32 THEN Auto)
         THEN Subst' |a1a2| + |c1c2| + |ab| = |a1a2| + |ab| + |c1c2| ∈ Length 32
         THEN Auto)
   THEN (FLemma `geo-add-length-cancel-right-lt` [32] THEN Auto)
   THEN (Assert p' ≤ q' BY
               (Unfold `geo-le` 0 THEN D 0 THEN InstConcl [⌜p'⌝;⌜q'⌝]⋅ THEN Auto))
   THEN InstLemma `not-lt-and-symm-le` [⌜e⌝;⌜p'⌝;⌜q'⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a1  :  Point
3.  a2  :  Point
4.  b1  :  Point
5.  b2  :  Point
6.  c1  :  Point
7.  c2  :  Point
8.  a  :  Point
9.  b  :  Point
10.  a  \#  b
11.  p'  :  Point
12.  B(OXp')
13.  q'  :  \{p:Point|  B(OXp)\} 
14.  p'  =  |a1a2|  +  |ab|
15.  q'  =  |b1b2|
16.  B(Xp'q')
17.  a  \#  b
18.  X  \#  p'
19.  X  \#  q'
20.  P  :  Point
21.  B(Xp'P)
22.  p'P  \mcong{}  c1c2
23.  Q  :  Point
24.  B(Xq'Q)
25.  q'Q  \mcong{}  c1c2
26.  P  =  |a1a2|  +  |c1c2|  +  |ab|
27.  Q  =  |b1b2|  +  |c1c2|
28.  P  \#  q'
29.  B(Xq'P)
30.  P  \#  Q
31.  B(XQP)
32.  Q  <  P
33.  Q  \mleq{}  P
34.  Q  \#  P
\mvdash{}  False


By

---

Latex:
(((Assert  Q  =  |XQ|  BY
                  Auto)
    THEN  (Assert  P  =  |XP|  BY
                            Auto)
    THEN  (RWO  "-1"  32  THENA  Auto)
    THEN  (RWO  "-2"  32  THENA  Auto))
  THEN  ((Subst'  |XQ|  =  |b1b2|  +  |c1c2|  32  THEN  Auto)
              THEN  (Subst'  |XP|  =  |a1a2|  +  |c1c2|  +  |ab|  32  THEN  Auto)
              THEN  Subst'  |a1a2|  +  |c1c2|  +  |ab|  =  |a1a2|  +  |ab|  +  |c1c2|  32
              THEN  Auto)
  THEN  (FLemma  `geo-add-length-cancel-right-lt`  [32]  THEN  Auto)
  THEN  (Assert  p'  \mleq{}  q'  BY
                          (Unfold  `geo-le`  0  THEN  D  0  THEN  InstConcl  [\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}q'\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  InstLemma  `not-lt-and-symm-le`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}q'\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index