---

Step * 2 of Lemma int_ring_wf

.....set predicate..... 
IsIntegDom(ℤ-rng)
BY
{ UnfoldTopAb 0 THEN AbReduce 0⋅ }

1
0 ≠ 1 ∧ (∀u,v:ℤ.  ((¬(v = 0 ∈ ℤ)) ⇒ ((u * v) = 0 ∈ ℤ) ⇒ (u = 0 ∈ ℤ)))

---

Latex:

---

Latex:
.....set  predicate..... 
IsIntegDom(\mBbbZ{}-rng)


By

---

Latex:
UnfoldTopAb  0  THEN  AbReduce  0\mcdot{}

---

Home Index