---

Step * 1 1 1 of Lemma rneq-if-rabs2

.....assertion..... 
1. x : ℝ
2. y : ℝ
3. n : ℕ+
4. 4 < imax(((x (4 * n)) + (-(y (4 * n)))) ÷ 4;-(((x (4 * n)) + (-(y (4 * n)))) ÷ 4))
5. m : ℕ+
6. (4 * n) = m ∈ ℕ+
7. 4 < ((x m) + (-(y m))) ÷ 4 ∨ 4 < -(((x m) + (-(y m))) ÷ 4)
8. ¬(x m) + 4 < y m
⊢ 4 < (x m) + (-(y m))
BY
{ ((Assert ¬(x m) + (-(y m)) < -4 BY (ParallelLast THEN Auto)) THEN MoveToConcl (-1)) }

1
1. x : ℝ
2. y : ℝ
3. n : ℕ+
4. 4 < imax(((x (4 * n)) + (-(y (4 * n)))) ÷ 4;-(((x (4 * n)) + (-(y (4 * n)))) ÷ 4))
5. m : ℕ+
6. (4 * n) = m ∈ ℕ+
7. 4 < ((x m) + (-(y m))) ÷ 4 ∨ 4 < -(((x m) + (-(y m))) ÷ 4)
8. ¬(x m) + 4 < y m
⊢ (¬(x m) + (-(y m)) < -4) ⇒ 4 < (x m) + (-(y m))

---

Latex:

---

Latex:
.....assertion..... 
1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  n  :  \mBbbN{}\msupplus{}
4.  4  <  imax(((x  (4  *  n))  +  (-(y  (4  *  n))))  \mdiv{}  4;-(((x  (4  *  n))  +  (-(y  (4  *  n))))  \mdiv{}  4))
5.  m  :  \mBbbN{}\msupplus{}
6.  (4  *  n)  =  m
7.  4  <  ((x  m)  +  (-(y  m)))  \mdiv{}  4  \mvee{}  4  <  -(((x  m)  +  (-(y  m)))  \mdiv{}  4)
8.  \mneg{}(x  m)  +  4  <  y  m
\mvdash{}  4  <  (x  m)  +  (-(y  m))


By

---

Latex:
((Assert  \mneg{}(x  m)  +  (-(y  m))  <  -4  BY  (ParallelLast  THEN  Auto))  THEN  MoveToConcl  (-1))

---

Home Index