---

Step * of Lemma posint_reduc_dec

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

1
1. a : |<ℤ+,*>|
⊢ Dec(∃b:|<ℤ+,*>|. ((¬(<ℤ+,*>-unit(b))) ∧ (b p| a)))

---

Latex:

---

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


By

---

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

---

Home Index