---

Step * of Lemma posint_unit_dec

∀a:|<ℤ+,*>|. Dec(<ℤ+,*>-unit(a))
BY
{ ((D 0 THENM RWH (LemmaC `posint_munit_elim`) 0) THENA Auto) }

1
1. a : |<ℤ+,*>|@i
⊢ Dec(a = 1 ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}a:|<\mBbbZ{}\msupplus{},*>|.  Dec(<\mBbbZ{}\msupplus{},*>-unit(a))


By

---

Latex:
((D  0  THENM  RWH  (LemmaC  `posint\_munit\_elim`)  0)  THENA  Auto)

---

Home Index