---

Step * 3 of Lemma posint_is_ufm


1. a : Atom{<ℤ+,*>}@i
⊢ IsPrime(a)
BY
{ ((BLemma `posint_atom_imp_prime`) THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  Atom\{<\mBbbZ{}\msupplus{},*>\}@i
\mvdash{}  IsPrime(a)


By

---

Latex:
((BLemma  `posint\_atom\_imp\_prime`)  THEN  Auto)

---

Home Index