Metamath Proof Explorer

Theorem prmocl

Description: Closure of the primorial function. (Contributed by AV, 28-Aug-2020)

Ref Expression
Assertion prmocl 
|- ( N e. NN0 -> ( #p ` N ) e. NN )

Proof

Step Hyp Ref Expression
1 prmoval 
 |-  ( N e. NN0 -> ( #p ` N ) = prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) )
2 fzfid 
 |-  ( N e. NN0 -> ( 1 ... N ) e. Fin )
3 elfznn 
 |-  ( k e. ( 1 ... N ) -> k e. NN )
4 3 adantl 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> k e. NN )
5 1nn 
 |-  1 e. NN
6 5 a1i 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> 1 e. NN )
7 4 6 ifcld 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> if ( k e. Prime , k , 1 ) e. NN )
8 2 7 fprodnncl 
 |-  ( N e. NN0 -> prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) e. NN )
9 1 8 eqeltrd 
 |-  ( N e. NN0 -> ( #p ` N ) e. NN )