---

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


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))
BY
{ (MoveToConcl (-2) THEN (GenConclTerm ⌜(x m) + (-(y m))⌝⋅ THENA Auto)) }

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. ¬(x m) + 4 < y m
8. v : ℤ
9. ((x m) + (-(y m))) = v ∈ ℤ
⊢ (4 < v ÷ 4 ∨ 4 < -(v ÷ 4)) ⇒ (¬v < -4) ⇒ 4 < v

---

Latex:

---

Latex:

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{}  (\mneg{}(x  m)  +  (-(y  m))  <  -4)  {}\mRightarrow{}  4  <  (x  m)  +  (-(y  m))


By

---

Latex:
(MoveToConcl  (-2)  THEN  (GenConclTerm  \mkleeneopen{}(x  m)  +  (-(y  m))\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index