Metamath Proof Explorer

Theorem prmonn2

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

Ref Expression
Assertion prmonn2 
|- ( N e. NN -> ( #p ` N ) = if ( N e. Prime , ( ( #p ` ( N - 1 ) ) x. N ) , ( #p ` ( N - 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 nncn 
 |-  ( N e. NN -> N e. CC )
2 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
3 1 2 syl 
 |-  ( N e. NN -> ( ( N - 1 ) + 1 ) = N )
4 3 eqcomd 
 |-  ( N e. NN -> N = ( ( N - 1 ) + 1 ) )
5 4 fveq2d 
 |-  ( N e. NN -> ( #p ` N ) = ( #p ` ( ( N - 1 ) + 1 ) ) )
6 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
7 prmop1 
 |-  ( ( N - 1 ) e. NN0 -> ( #p ` ( ( N - 1 ) + 1 ) ) = if ( ( ( N - 1 ) + 1 ) e. Prime , ( ( #p ` ( N - 1 ) ) x. ( ( N - 1 ) + 1 ) ) , ( #p ` ( N - 1 ) ) ) )
8 6 7 syl 
 |-  ( N e. NN -> ( #p ` ( ( N - 1 ) + 1 ) ) = if ( ( ( N - 1 ) + 1 ) e. Prime , ( ( #p ` ( N - 1 ) ) x. ( ( N - 1 ) + 1 ) ) , ( #p ` ( N - 1 ) ) ) )
9 3 eleq1d 
 |-  ( N e. NN -> ( ( ( N - 1 ) + 1 ) e. Prime <-> N e. Prime ) )
10 3 oveq2d 
 |-  ( N e. NN -> ( ( #p ` ( N - 1 ) ) x. ( ( N - 1 ) + 1 ) ) = ( ( #p ` ( N - 1 ) ) x. N ) )
11 9 10 ifbieq1d 
 |-  ( N e. NN -> if ( ( ( N - 1 ) + 1 ) e. Prime , ( ( #p ` ( N - 1 ) ) x. ( ( N - 1 ) + 1 ) ) , ( #p ` ( N - 1 ) ) ) = if ( N e. Prime , ( ( #p ` ( N - 1 ) ) x. N ) , ( #p ` ( N - 1 ) ) ) )
12 5 8 11 3eqtrd 
 |-  ( N e. NN -> ( #p ` N ) = if ( N e. Prime , ( ( #p ` ( N - 1 ) ) x. N ) , ( #p ` ( N - 1 ) ) ) )