---

Step * of Lemma rless_transitivity1

∀x,y,z:ℝ.  ((x < y) ⇒ x < z supposing y ≤ z)
BY
{ (Auto
   THEN (RWO "rless-iff-large-diff" (-2) THENA Auto)
   THEN (InstHyp [⌜9⌝] (-2)⋅ 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. ∀b:ℕ+. ∃n:ℕ+. ∀m:ℕ+. ((n ≤ m) ⇒ (b ≤ ((y m) - x m)))
5. ∀n:ℕ+. ((y n) ≤ ((z n) + 4))
6. n : ℕ+
7. ∀m:ℕ+. ((n ≤ m) ⇒ (9 ≤ ((y m) - x m)))
8. m : {n...}@i
9. (n ≤ m) ⇒ (9 ≤ ((y m) - x m))
⊢ (x m) + 4 < z m

---

Latex:

---

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


By

---

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

---

Home Index