---

Step * of Lemma int_mod_ring_wf_field

∀[p:ℕ+]. int_mod_ring(p) ∈ Field{i} supposing prime(p)
BY
{ (Auto THEN MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. p : ℕ+
2. prime(p)
⊢ IsField(int_mod_ring(p))

---

Latex:

---

Latex:
\mforall{}[p:\mBbbN{}\msupplus{}].  int\_mod\_ring(p)  \mmember{}  Field\{i\}  supposing  prime(p)


By

---

Latex:
(Auto  THEN  MemTypeCD  THEN  Auto)

---

Home Index