Metamath Proof Explorer

Theorem prmonn2

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

Ref Expression
Assertion prmonn2 ⊢ N ∈ ℕ → # p ⁡ N = if N ∈ ℙ # p ⁡ N − 1 ⋅ N # p ⁡ N − 1

Proof

Step Hyp Ref Expression
1 nncn ⊢ N ∈ ℕ → N ∈ ℂ
2 npcan1 ⊢ N ∈ ℂ → N - 1 + 1 = N
3 1 2 syl ⊢ N ∈ ℕ → N - 1 + 1 = N
4 3 eqcomd ⊢ N ∈ ℕ → N = N - 1 + 1
5 4 fveq2d ⊢ N ∈ ℕ → # p ⁡ N = # p ⁡ N - 1 + 1
6 nnm1nn0 ⊢ N ∈ ℕ → N − 1 ∈ ℕ 0
7 prmop1 ⊢ N − 1 ∈ ℕ 0 → # p ⁡ N - 1 + 1 = if N - 1 + 1 ∈ ℙ # p ⁡ N − 1 ⁢ N - 1 + 1 # p ⁡ N − 1
8 6 7 syl ⊢ N ∈ ℕ → # p ⁡ N - 1 + 1 = if N - 1 + 1 ∈ ℙ # p ⁡ N − 1 ⁢ N - 1 + 1 # p ⁡ N − 1
9 3 eleq1d ⊢ N ∈ ℕ → N - 1 + 1 ∈ ℙ ↔ N ∈ ℙ
10 3 oveq2d ⊢ N ∈ ℕ → # p ⁡ N − 1 ⁢ N - 1 + 1 = # p ⁡ N − 1 ⋅ N
11 9 10 ifbieq1d ⊢ N ∈ ℕ → if N - 1 + 1 ∈ ℙ # p ⁡ N − 1 ⁢ N - 1 + 1 # p ⁡ N − 1 = if N ∈ ℙ # p ⁡ N − 1 ⋅ N # p ⁡ N − 1
12 5 8 11 3eqtrd ⊢ N ∈ ℕ → # p ⁡ N = if N ∈ ℙ # p ⁡ N − 1 ⋅ N # p ⁡ N − 1