---

Step * of Lemma absval_div_nat

∀[n:ℕ+]. ∀[i:ℤ].  (|i| ÷ n ~ |i ÷ n|)
BY
{ xxx(Auto THEN (Decide ⌜0 ≤ i⌝⋅ THENA Auto))xxx }

1
1. n : ℕ+
2. i : ℤ
3. 0 ≤ i
⊢ (|i| ÷ n) = |i ÷ n| ∈ ℤ

2
1. n : ℕ+
2. i : ℤ
3. ¬(0 ≤ i)
⊢ (|i| ÷ n) = |i ÷ n| ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[i:\mBbbZ{}].    (|i|  \mdiv{}  n  \msim{}  |i  \mdiv{}  n|)


By

---

Latex:
xxx(Auto  THEN  (Decide  \mkleeneopen{}0  \mleq{}  i\mkleeneclose{}\mcdot{}  THENA  Auto))xxx

---

Home Index