Metamath Proof Explorer

Theorem prmoval

Description: Value of the primorial function for nonnegative integers. (Contributed by AV, 28-Aug-2020)

Ref Expression
Assertion prmoval ⊢ N ∈ ℕ 0 → # p ⁡ N = ∏ k = 1 N if k ∈ ℙ k 1

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ n = N → 1 … n = 1 … N
2 1 prodeq1d ⊢ n = N → ∏ k = 1 n if k ∈ ℙ k 1 = ∏ k = 1 N if k ∈ ℙ k 1
3 df-prmo ⊢ # p = n ∈ ℕ 0 ⟼ ∏ k = 1 n if k ∈ ℙ k 1
4 prodex ⊢ ∏ k = 1 N if k ∈ ℙ k 1 ∈ V
5 2 3 4 fvmpt ⊢ N ∈ ℕ 0 → # p ⁡ N = ∏ k = 1 N if k ∈ ℙ k 1