---

Step * of Lemma rless-implies-rless

∀a,b:ℝ.  ∀[c,d:ℝ].  (a < b) supposing ((c < d) and ((d - c) = (b - a)))
BY
{ (Auto
   THEN Unhide
   THEN Auto
   THEN (RW (nRAddC ⌜-(a)⌝) 0⋅ THENA Auto)
   THEN (RW (nRAddC ⌜-(c)⌝) (-1)⋅ THENA Auto)
   THEN ((Assert (-(c) + c) = r0 BY Auto) THEN (RWO "-1" (-2) THENA Auto))
   THEN (Assert (-(a) + a) = r0 BY
               Auto)
   THEN (RWO "-1" 0 THENA Auto)) }

1
1. a : ℝ
2. b : ℝ
3. c : ℝ
4. d : ℝ
5. (d - c) = (b - a)
6. r0 < (-(c) + d)
7. (-(c) + c) = r0
8. (-(a) + a) = r0
⊢ r0 < (-(a) + b)

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.    \mforall{}[c,d:\mBbbR{}].    (a  <  b)  supposing  ((c  <  d)  and  ((d  -  c)  =  (b  -  a)))


By

---

Latex:
(Auto
  THEN  Unhide
  THEN  Auto
  THEN  (RW  (nRAddC  \mkleeneopen{}-(a)\mkleeneclose{})  0\mcdot{}  THENA  Auto)
  THEN  (RW  (nRAddC  \mkleeneopen{}-(c)\mkleeneclose{})  (-1)\mcdot{}  THENA  Auto)
  THEN  ((Assert  (-(c)  +  c)  =  r0  BY  Auto)  THEN  (RWO  "-1"  (-2)  THENA  Auto))
  THEN  (Assert  (-(a)  +  a)  =  r0  BY
                          Auto)
  THEN  (RWO  "-1"  0  THENA  Auto))

---

Home Index