---

Step * 1 of Lemma posint_fact_exists


1. i : ℕ+
⊢ ∃ps:{j:ℕ+| prime(j)}  List [(i = (Π ps) ∈ ℤ)]
BY
{ InstLemma `mfact_exists_a` [<ℤ+,*>;i] THEN Backchain ``posint_cancel posint_well_fnd 
  posint_reduc_dec posint_unit_dec`` THEN Auto⋅ }

1
1. i : ℕ+
2. ∃as:Atom{<ℤ+,*>} List. (i ~ (Π as))
⊢ ∃ps:{j:ℕ+| prime(j)}  List [(i = (Π ps) ∈ ℤ)]

---

Latex:

---

Latex:

1.  i  :  \mBbbN{}\msupplus{}
\mvdash{}  \mexists{}ps:\{j:\mBbbN{}\msupplus{}|  prime(j)\}    List  [(i  =  (\mPi{}  ps))]


By

---

Latex:
InstLemma  `mfact\_exists\_a`  [<\mBbbZ{}\msupplus{},*>i]  THEN  Backchain  ``posint\_cancel  posint\_well\_fnd 
    posint\_reduc\_dec  posint\_unit\_dec``  THEN  Auto\mcdot{}

---

Home Index