---

Step * 1 1 1 2 1 of Lemma int_mod_ring_wf


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
BY
{ (RWO "add_com_int_mod" 0 THEN Try (Complete (Auto))) }

1
.....wf..... 
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 ∈ ℤ_n

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  \mforall{}[x,y,z:\mBbbZ{}\_n].    ((x  +  y  +  z)  =  ((x  +  y)  +  z))
3.  \mforall{}[x:\mBbbZ{}\_n].  (((x  +  0)  =  x)  \mwedge{}  ((0  +  x)  =  x))
4.  x  :  \mBbbZ{}\_n
5.  (x  +  (-x))  =  0
\mvdash{}  ((-x)  +  x)  =  0


By

---

Latex:
(RWO  "add\_com\_int\_mod"  0  THEN  Try  (Complete  (Auto)))

---

Home Index