---

Step * 1 1 1 2 of Lemma int_mod_ring_wf


1. n : ℕ+
⊢ IsRing(ℤ_n;λu,v. (u + v);0;λu.(-u);λu,v. (u * v);1)
BY
{ (RepUR ``ring_p group_p monoid_p assoc ident inverse bilinear`` 0 THEN Auto) }

1
1. n : ℕ+
2. ∀[x,y,z:ℤ_n].  ((x + y + z) = ((x + y) + z) ∈ ℤ_n)
3. ∀[x:ℤ_n]. (((x + 0) = x ∈ ℤ_n) ∧ ((0 + x) = x ∈ ℤ_n))
4. x : ℤ_n
5. (x + (-x)) = 0 ∈ ℤ_n
⊢ ((-x) + x) = 0 ∈ ℤ_n

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
\mvdash{}  IsRing(\mBbbZ{}\_n;\mlambda{}u,v.  (u  +  v);0;\mlambda{}u.(-u);\mlambda{}u,v.  (u  *  v);1)


By

---

Latex:
(RepUR  ``ring\_p  group\_p  monoid\_p  assoc  ident  inverse  bilinear``  0  THEN  Auto)

---

Home Index