---

Step * of Lemma any_field_is_integ_dom

∀[r:CRng]. IsIntegDom(r) supposing IsField(r)
BY
{ Unfolds ``field_p integ_dom_p`` 0 
THEN Auto⋅⋅ }

1
1. r : CRng
2. 0 ≠ 1 ∈ |r| 
3. ∀u:|r|. (u ≠ 0 ∈ |r|  ⇒ u | 1 in r)
4. 0 ≠ 1 ∈ |r| 
5. u : |r|
6. v : |r|
7. ¬(v = 0 ∈ |r|)
8. (u * v) = 0 ∈ |r|
⊢ u = 0 ∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:CRng].  IsIntegDom(r)  supposing  IsField(r)


By

---

Latex:
Unfolds  ``field\_p  integ\_dom\_p``  0 
THEN  Auto\mcdot{}\mcdot{}

---

Home Index