Theorem prmoval

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

	Ref	Expression
Assertion	prmoval	⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑛 = 𝑁 → ( 1 ... 𝑛 ) = ( 1 ... 𝑁 ) )
2	1	prodeq1d	⊢ ( 𝑛 = 𝑁 → ∏ 𝑘 ∈ ( 1 ... 𝑛 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
3		df-prmo	⊢ #p = ( 𝑛 ∈ ℕ0 ↦ ∏ 𝑘 ∈ ( 1 ... 𝑛 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
4		prodex	⊢ ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ V
5	2 3 4	fvmpt	⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )