---

Step * of Lemma div_reduce_inequality

∀[a:ℤ]
  ((∀n:ℕ+. ∀x:ℤ.  uiff(0 ≤ (a + (n * x));0 ≤ ((a ÷↓ n) + x)))
  ∧ (∀n:{...-1}. ∀x:ℤ.  uiff(0 ≤ (a + (n * x));0 ≤ ((a ÷↓ (-n)) + ((-1) * x)))))
BY
{ (UnivCD THENA (Auto THEN All Thin THEN (D 1 THENA Auto) THEN Add ⌜1 - n⌝ (-1)⋅ THEN RW IntNormC  (-1) THEN Auto)) }

1
1. a : ℤ
⊢ (∀n:ℕ+. ∀x:ℤ.  uiff(0 ≤ (a + (n * x));0 ≤ ((a ÷↓ n) + x)))
∧ (∀n:{...-1}. ∀x:ℤ.  uiff(0 ≤ (a + (n * x));0 ≤ ((a ÷↓ (-n)) + ((-1) * x))))

---

Latex:

---

Latex:
\mforall{}[a:\mBbbZ{}]
    ((\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}x:\mBbbZ{}.    uiff(0  \mleq{}  (a  +  (n  *  x));0  \mleq{}  ((a  \mdiv{}\mdownarrow{}  n)  +  x)))
    \mwedge{}  (\mforall{}n:\{...-1\}.  \mforall{}x:\mBbbZ{}.    uiff(0  \mleq{}  (a  +  (n  *  x));0  \mleq{}  ((a  \mdiv{}\mdownarrow{}  (-n))  +  ((-1)  *  x)))))


By

---

Latex:
(UnivCD
  THENA  (Auto
                THEN  All  Thin
                THEN  (D  1  THENA  Auto)
                THEN  Add  \mkleeneopen{}1  -  n\mkleeneclose{}  (-1)\mcdot{}
                THEN  RW  IntNormC    (-1)
                THEN  Auto)
  )

---

Home Index