Theorem prmoval

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

	Ref	Expression
Assertion	prmoval	|- ( N e. NN0 -> ( #p ` N ) = prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	|- ( n = N -> ( 1 ... n ) = ( 1 ... N ) )
2	1	prodeq1d	|- ( n = N -> prod_ k e. ( 1 ... n ) if ( k e. Prime , k , 1 ) = prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) )
3		df-prmo	|- #p = ( n e. NN0 |-> prod_ k e. ( 1 ... n ) if ( k e. Prime , k , 1 ) )
4		prodex	|- prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) e. _V
5	2 3 4	fvmpt	|- ( N e. NN0 -> ( #p ` N ) = prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) )