---

Step * of Lemma rless_transitivity2

∀x,y,z:ℝ.  (y < z) ⇒ (x < z) supposing x ≤ y
BY
{ (Auto
   THEN (RWO "rless-iff-large-diff" (-1) THENA Auto)
   THEN (InstHyp [⌜9⌝] (-1)⋅ THENA Auto)
   THEN (All (RWO "rless-iff4 rleq-iff4") THENA Auto)
   THEN RepeatFor 2 (ParallelLast)) }

1
1. x : ℝ@i
2. y : ℝ@i
3. z : ℝ@i
4. ∀n:ℕ+. ((x n) ≤ ((y n) + 4))
5. ∀b:ℕ+. ∃n:ℕ+. ∀m:ℕ+. ((n ≤ m) ⇒ (b ≤ ((z m) - y m)))
6. n : ℕ+
7. ∀m:ℕ+. ((n ≤ m) ⇒ (9 ≤ ((z m) - y m)))
8. m : {n...}@i
9. (n ≤ m) ⇒ (9 ≤ ((z m) - y m))
⊢ (x m) + 4 < z m

---

Latex:

---

Latex:
\mforall{}x,y,z:\mBbbR{}.    (y  <  z)  {}\mRightarrow{}  (x  <  z)  supposing  x  \mleq{}  y


By

---

Latex:
(Auto
  THEN  (RWO  "rless-iff-large-diff"  (-1)  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}9\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  (All  (RWO  "rless-iff4  rleq-iff4")  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast))

---

Home Index