---

Step * of Lemma nat-plus-ind-primes

No Annotations
∀[P:ℕ+ ⟶ ℙ]. (P[1] ⇒ (∀p:Prime. P[p]) ⇒ (∀n,m:ℕ+.  (P[n] ⇒ P[m] ⇒ P[n * m])) ⇒ (∀n:ℕ+. P[n]))
BY
{ (Auto
   THEN (CaseNat 1 `n'
         THENL [Trivial
               ; ((InstLemma `prime-factors` [⌜n⌝]⋅ THENA Auto) THEN ExRepD THEN HypSubst' -1 0 THEN ThinVar `n')]
        )
   ) }

1
1. [P] : ℕ+ ⟶ ℙ
2. P[1]
3. ∀p:Prime. P[p]
4. ∀n,m:ℕ+.  (P[n] ⇒ P[m] ⇒ P[n * m])
5. factors : {m:{2...}| prime(m)}  List
⊢ P[Π(factors) ]

---

Latex:

---

Latex:
No  Annotations
\mforall{}[P:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbP{}].  (P[1]  {}\mRightarrow{}  (\mforall{}p:Prime.  P[p])  {}\mRightarrow{}  (\mforall{}n,m:\mBbbN{}\msupplus{}.    (P[n]  {}\mRightarrow{}  P[m]  {}\mRightarrow{}  P[n  *  m]))  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}\msupplus{}.  P[n]))


By

---

Latex:
(Auto
  THEN  (CaseNat  1  `n'
              THENL  [Trivial
                          ;  ((InstLemma  `prime-factors`  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                THEN  ExRepD
                                THEN  HypSubst'  -1  0
                                THEN  ThinVar  `n')]
            )
  )

---

Home Index