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