---

Step * 1 of Lemma posint_reduc_dec


1. a : |<ℤ+,*>|
⊢ Dec(∃b:|<ℤ+,*>|. ((¬(<ℤ+,*>-unit(b))) ∧ (b p| a)))
BY
{ AbEval ``mpdivides mdivides`` 0 
 }

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

---

Latex:

---

Latex:

1.  a  :  |<\mBbbZ{}\msupplus{},*>|
\mvdash{}  Dec(\mexists{}b:|<\mBbbZ{}\msupplus{},*>|.  ((\mneg{}(<\mBbbZ{}\msupplus{},*>-unit(b)))  \mwedge{}  (b  p|  a)))


By

---

Latex:
AbEval  ``mpdivides  mdivides``  0 

---

Home Index