---

Step * 1 2 of Lemma int_mod_ring_wf


1. n : ℕ+
⊢ IsEqFun(ℤ_n;λu,v. (u mod n =z v mod n))
BY
{ TACTIC:(RepUR ``eqfun_p`` 0 THEN UnivCD THEN Try (Complete (Auto))) }

1
1. n : ℕ+
2. x : ℤ_n
3. y : ℤ_n
⊢ uiff(↑(x mod n =z y mod n);x = y ∈ ℤ_n)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
\mvdash{}  IsEqFun(\mBbbZ{}\_n;\mlambda{}u,v.  (u  mod  n  =\msubz{}  v  mod  n))


By

---

Latex:
TACTIC:(RepUR  ``eqfun\_p``  0  THEN  UnivCD  THEN  Try  (Complete  (Auto)))

---

Home Index