Step * of Lemma div_is_zero

∀[n:{2...}]. ∀[i:ℤ].  i ÷ n ~ 0 supposing |i| < n
BY
{ Auto }

1
1. n : {2...}
2. i : ℤ
3. |i| < n
⊢ (i ÷ n) = 0 ∈ ℤ


Latex:


Latex:
\mforall{}[n:\{2...\}].  \mforall{}[i:\mBbbZ{}].    i  \mdiv{}  n  \msim{}  0  supposing  |i|  <  n


By


Latex:
Auto




Home Index