---

Step * of Lemma mod_bounds_1

∀[a:ℤ]. ∀[n:ℤ-o].  ((0 ≤ (a mod n)) ∧ a mod n < |n|)
BY
{ (GenUnivCD THENA Auto) }

1
1. a : ℤ
2. n : ℤ-o
⊢ 0 ≤ (a mod n)

2
1. a : ℤ
2. n : ℤ-o
⊢ a mod n < |n|

---

Latex:

---

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[n:\mBbbZ{}\msupminus{}\msupzero{}].    ((0  \mleq{}  (a  mod  n))  \mwedge{}  a  mod  n  <  |n|)


By

---

Latex:
(GenUnivCD  THENA  Auto)

---

Home Index