---

Step * of Lemma rless-cases-proof

No Annotations
∀x,y:ℝ.  ((x < y) ⇒ (∀z:ℝ. ((x < z) ∨ (z < y))))
BY
{ (Auto
   THEN (FLemma `rless-iff8` [-2] THENA Auto)
   THEN D -1
   THEN (Evaluate ⌜n = m ∈ ℤ⌝⋅ THENA Auto)
   THEN (Decide ⌜(x n) + 4 < z n⌝⋅ THENA Auto)) }

1
1. x : ℝ
2. y : ℝ
3. x < y
4. z : ℝ
5. m : ℕ+
6. [%8] : (x m) + 8 < y m
7. n : ℤ
8. n = m ∈ ℤ
9. (x n) + 4 < z n
⊢ (x < z) ∨ (z < y)

2
1. x : ℝ
2. y : ℝ
3. x < y
4. z : ℝ
5. m : ℕ+
6. [%8] : (x m) + 8 < y m
7. n : ℤ
8. n = m ∈ ℤ
9. ¬(x n) + 4 < z n
⊢ (x < z) ∨ (z < y)

---

Latex:

---

Latex:
No  Annotations
\mforall{}x,y:\mBbbR{}.    ((x  <  y)  {}\mRightarrow{}  (\mforall{}z:\mBbbR{}.  ((x  <  z)  \mvee{}  (z  <  y))))


By

---

Latex:
(Auto
  THEN  (FLemma  `rless-iff8`  [-2]  THENA  Auto)
  THEN  D  -1
  THEN  (Evaluate  \mkleeneopen{}n  =  m\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Decide  \mkleeneopen{}(x  n)  +  4  <  z  n\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index