Step
*
1
1
of Lemma
nat-plus-ind-primes
1. [P] : ℕ+ ⟶ ℙ
2. P[1]
3. ∀p:Prime. P[p]
4. ∀n,m:ℕ+. (P[n]
⇒ P[m]
⇒ P[n * m])
5. u : {m:{2...}| prime(m)}
6. v : {m:{2...}| prime(m)} List
7. P[Π(v) ]
⊢ P[Π([u / v]) ]
BY
{ ((Subst' Π([u / v]) ~ u * Π(v) 0 THENM BackThruSomeHyp) THEN Auto) }
Latex:
Latex:
1. [P] : \mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbP{}
2. P[1]
3. \mforall{}p:Prime. P[p]
4. \mforall{}n,m:\mBbbN{}\msupplus{}. (P[n] {}\mRightarrow{} P[m] {}\mRightarrow{} P[n * m])
5. u : \{m:\{2...\}| prime(m)\}
6. v : \{m:\{2...\}| prime(m)\} List
7. P[\mPi{}(v) ]
\mvdash{} P[\mPi{}([u / v]) ]
By
Latex:
((Subst' \mPi{}([u / v]) \msim{} u * \mPi{}(v) 0 THENM BackThruSomeHyp) THEN Auto)
Home
Index