---

Step * 1 1 1 2 1 1 of Lemma int_mod_ring_wf

.....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
BY
{ (BLemma `minus_wf_int_mod` THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
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  \mmember{}  \mBbbZ{}\_n


By

---

Latex:
(BLemma  `minus\_wf\_int\_mod`  THEN  Auto)

---

Home Index