---

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


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
BY
{ (All Thin
   THEN (InstLemma `div_rem_sum` [⌜v⌝;⌜4⌝]⋅ THENA Auto)
   THEN (InstLemma `rem_bounds_absval` [⌜4⌝;⌜v⌝]⋅ THENA Auto)) }

1
1. v : ℤ
2. v = (((v ÷ 4) * 4) + (v rem 4)) ∈ ℤ
3. |v rem 4| < |4|
⊢ (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.  \mneg{}(x  m)  +  4  <  y  m
8.  v  :  \mBbbZ{}
9.  ((x  m)  +  (-(y  m)))  =  v
\mvdash{}  (4  <  v  \mdiv{}  4  \mvee{}  4  <  -(v  \mdiv{}  4))  {}\mRightarrow{}  (\mneg{}v  <  -4)  {}\mRightarrow{}  4  <  v


By

---

Latex:
(All  Thin
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}4\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `rem\_bounds\_absval`  [\mkleeneopen{}4\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index