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 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 ) )