---

Step * of Lemma posint_munit_elim

∀a:|<ℤ+,*>|. (<ℤ+,*>-unit(a) ⇐⇒ a = 1 ∈ ℤ)
BY
{ AbEval ``munit mdivides`` 0 }

1
∀a:ℕ+. (∃c:ℕ+. (1 = (a * c) ∈ ℕ+) ⇐⇒ a = 1 ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}a:|<\mBbbZ{}\msupplus{},*>|.  (<\mBbbZ{}\msupplus{},*>-unit(a)  \mLeftarrow{}{}\mRightarrow{}  a  =  1)


By

---

Latex:
AbEval  ``munit  mdivides``  0

---

Home Index