Metamath Proof Explorer

Theorem prmonn2

Description: Value of the primorial function expressed recursively. (Contributed by AV, 28-Aug-2020)

Ref Expression
Assertion prmonn2 ( 𝑁 ∈ ℕ → ( #p ‘ 𝑁 ) = if ( 𝑁 ∈ ℙ , ( ( #p ‘ ( 𝑁 − 1 ) ) · 𝑁 ) , ( #p ‘ ( 𝑁 − 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
2 npcan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
3 1 2 syl ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
4 3 eqcomd ⊢ ( 𝑁 ∈ ℕ → 𝑁 = ( ( 𝑁 − 1 ) + 1 ) )
5 4 fveq2d ⊢ ( 𝑁 ∈ ℕ → ( #p ‘ 𝑁 ) = ( #p ‘ ( ( 𝑁 − 1 ) + 1 ) ) )
6 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
7 prmop1 ⊢ ( ( 𝑁 − 1 ) ∈ ℕ0 → ( #p ‘ ( ( 𝑁 − 1 ) + 1 ) ) = if ( ( ( 𝑁 − 1 ) + 1 ) ∈ ℙ , ( ( #p ‘ ( 𝑁 − 1 ) ) · ( ( 𝑁 − 1 ) + 1 ) ) , ( #p ‘ ( 𝑁 − 1 ) ) ) )
8 6 7 syl ⊢ ( 𝑁 ∈ ℕ → ( #p ‘ ( ( 𝑁 − 1 ) + 1 ) ) = if ( ( ( 𝑁 − 1 ) + 1 ) ∈ ℙ , ( ( #p ‘ ( 𝑁 − 1 ) ) · ( ( 𝑁 − 1 ) + 1 ) ) , ( #p ‘ ( 𝑁 − 1 ) ) ) )
9 3 eleq1d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 − 1 ) + 1 ) ∈ ℙ ↔ 𝑁 ∈ ℙ ) )
10 3 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( ( #p ‘ ( 𝑁 − 1 ) ) · ( ( 𝑁 − 1 ) + 1 ) ) = ( ( #p ‘ ( 𝑁 − 1 ) ) · 𝑁 ) )
11 9 10 ifbieq1d ⊢ ( 𝑁 ∈ ℕ → if ( ( ( 𝑁 − 1 ) + 1 ) ∈ ℙ , ( ( #p ‘ ( 𝑁 − 1 ) ) · ( ( 𝑁 − 1 ) + 1 ) ) , ( #p ‘ ( 𝑁 − 1 ) ) ) = if ( 𝑁 ∈ ℙ , ( ( #p ‘ ( 𝑁 − 1 ) ) · 𝑁 ) , ( #p ‘ ( 𝑁 − 1 ) ) ) )
12 5 8 11 3eqtrd ⊢ ( 𝑁 ∈ ℕ → ( #p ‘ 𝑁 ) = if ( 𝑁 ∈ ℙ , ( ( #p ‘ ( 𝑁 − 1 ) ) · 𝑁 ) , ( #p ‘ ( 𝑁 − 1 ) ) ) )