---

Step * of Lemma rem_fun_sat_rem_nrel

∀a:ℕ. ∀n:ℕ+.  Rem(a;n;a rem n)
BY
{ ((Unfold `rem_nrel` 0 THEN UnivCD) THENA Auto) }

1
1. a : ℕ
2. n : ℕ+
⊢ ∃q:ℕ. (Div(a;n;q) ∧ (((q * n) + (a rem n)) = a ∈ ℤ))

---

Latex:

---

Latex:
\mforall{}a:\mBbbN{}.  \mforall{}n:\mBbbN{}\msupplus{}.    Rem(a;n;a  rem  n)


By

---

Latex:
((Unfold  `rem\_nrel`  0  THEN  UnivCD)  THENA  Auto)

---

Home Index