Metamath Proof Explorer

Theorem prmop1

Description: The primorial of a successor. (Contributed by AV, 28-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
2 prmoval 
 |-  ( ( N + 1 ) e. NN0 -> ( #p ` ( N + 1 ) ) = prod_ k e. ( 1 ... ( N + 1 ) ) if ( k e. Prime , k , 1 ) )
3 1 2 syl 
 |-  ( N e. NN0 -> ( #p ` ( N + 1 ) ) = prod_ k e. ( 1 ... ( N + 1 ) ) if ( k e. Prime , k , 1 ) )
4 nn0p1nn 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN )
5 elnnuz 
 |-  ( ( N + 1 ) e. NN <-> ( N + 1 ) e. ( ZZ>= ` 1 ) )
6 4 5 sylib 
 |-  ( N e. NN0 -> ( N + 1 ) e. ( ZZ>= ` 1 ) )
7 elfzelz 
 |-  ( k e. ( 1 ... ( N + 1 ) ) -> k e. ZZ )
8 7 zcnd 
 |-  ( k e. ( 1 ... ( N + 1 ) ) -> k e. CC )
9 8 adantl 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... ( N + 1 ) ) ) -> k e. CC )
10 1cnd 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... ( N + 1 ) ) ) -> 1 e. CC )
11 9 10 ifcld 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... ( N + 1 ) ) ) -> if ( k e. Prime , k , 1 ) e. CC )
12 eleq1 
 |-  ( k = ( N + 1 ) -> ( k e. Prime <-> ( N + 1 ) e. Prime ) )
13 id 
 |-  ( k = ( N + 1 ) -> k = ( N + 1 ) )
14 12 13 ifbieq1d 
 |-  ( k = ( N + 1 ) -> if ( k e. Prime , k , 1 ) = if ( ( N + 1 ) e. Prime , ( N + 1 ) , 1 ) )
15 6 11 14 fprodm1 
 |-  ( N e. NN0 -> prod_ k e. ( 1 ... ( N + 1 ) ) if ( k e. Prime , k , 1 ) = ( prod_ k e. ( 1 ... ( ( N + 1 ) - 1 ) ) if ( k e. Prime , k , 1 ) x. if ( ( N + 1 ) e. Prime , ( N + 1 ) , 1 ) ) )
16 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
17 pncan1 
 |-  ( N e. CC -> ( ( N + 1 ) - 1 ) = N )
18 16 17 syl 
 |-  ( N e. NN0 -> ( ( N + 1 ) - 1 ) = N )
19 18 oveq2d 
 |-  ( N e. NN0 -> ( 1 ... ( ( N + 1 ) - 1 ) ) = ( 1 ... N ) )
20 19 prodeq1d 
 |-  ( N e. NN0 -> prod_ k e. ( 1 ... ( ( N + 1 ) - 1 ) ) if ( k e. Prime , k , 1 ) = prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) )
21 20 oveq1d 
 |-  ( N e. NN0 -> ( prod_ k e. ( 1 ... ( ( N + 1 ) - 1 ) ) if ( k e. Prime , k , 1 ) x. if ( ( N + 1 ) e. Prime , ( N + 1 ) , 1 ) ) = ( prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) x. if ( ( N + 1 ) e. Prime , ( N + 1 ) , 1 ) ) )
22 prmoval 
 |-  ( N e. NN0 -> ( #p ` N ) = prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) )
23 22 eqcomd 
 |-  ( N e. NN0 -> prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) = ( #p ` N ) )
24 23 adantl 
 |-  ( ( ( N + 1 ) e. Prime /\ N e. NN0 ) -> prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) = ( #p ` N ) )
25 24 oveq1d 
 |-  ( ( ( N + 1 ) e. Prime /\ N e. NN0 ) -> ( prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) x. ( N + 1 ) ) = ( ( #p ` N ) x. ( N + 1 ) ) )
26 iftrue 
 |-  ( ( N + 1 ) e. Prime -> if ( ( N + 1 ) e. Prime , ( N + 1 ) , 1 ) = ( N + 1 ) )
27 26 oveq2d 
 |-  ( ( N + 1 ) e. Prime -> ( prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) x. if ( ( N + 1 ) e. Prime , ( N + 1 ) , 1 ) ) = ( prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) x. ( N + 1 ) ) )
28 iftrue 
 |-  ( ( N + 1 ) e. Prime -> if ( ( N + 1 ) e. Prime , ( ( #p ` N ) x. ( N + 1 ) ) , ( #p ` N ) ) = ( ( #p ` N ) x. ( N + 1 ) ) )
29 27 28 eqeq12d 
 |-  ( ( N + 1 ) e. Prime -> ( ( prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) x. if ( ( N + 1 ) e. Prime , ( N + 1 ) , 1 ) ) = if ( ( N + 1 ) e. Prime , ( ( #p ` N ) x. ( N + 1 ) ) , ( #p ` N ) ) <-> ( prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) x. ( N + 1 ) ) = ( ( #p ` N ) x. ( N + 1 ) ) ) )
30 29 adantr 
 |-  ( ( ( N + 1 ) e. Prime /\ N e. NN0 ) -> ( ( prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) x. if ( ( N + 1 ) e. Prime , ( N + 1 ) , 1 ) ) = if ( ( N + 1 ) e. Prime , ( ( #p ` N ) x. ( N + 1 ) ) , ( #p ` N ) ) <-> ( prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) x. ( N + 1 ) ) = ( ( #p ` N ) x. ( N + 1 ) ) ) )
31 25 30 mpbird 
 |-  ( ( ( N + 1 ) e. Prime /\ N e. NN0 ) -> ( prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) x. if ( ( N + 1 ) e. Prime , ( N + 1 ) , 1 ) ) = if ( ( N + 1 ) e. Prime , ( ( #p ` N ) x. ( N + 1 ) ) , ( #p ` N ) ) )
32 fzfid 
 |-  ( N e. NN0 -> ( 1 ... N ) e. Fin )
33 elfznn 
 |-  ( k e. ( 1 ... N ) -> k e. NN )
34 1nn 
 |-  1 e. NN
35 34 a1i 
 |-  ( k e. ( 1 ... N ) -> 1 e. NN )
36 33 35 ifcld 
 |-  ( k e. ( 1 ... N ) -> if ( k e. Prime , k , 1 ) e. NN )
37 36 adantl 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> if ( k e. Prime , k , 1 ) e. NN )
38 32 37 fprodnncl 
 |-  ( N e. NN0 -> prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) e. NN )
39 38 nncnd 
 |-  ( N e. NN0 -> prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) e. CC )
40 39 adantl 
 |-  ( ( -. ( N + 1 ) e. Prime /\ N e. NN0 ) -> prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) e. CC )
41 40 mulid1d 
 |-  ( ( -. ( N + 1 ) e. Prime /\ N e. NN0 ) -> ( prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) x. 1 ) = prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) )
42 22 adantl 
 |-  ( ( -. ( N + 1 ) e. Prime /\ N e. NN0 ) -> ( #p ` N ) = prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) )
43 41 42 eqtr4d 
 |-  ( ( -. ( N + 1 ) e. Prime /\ N e. NN0 ) -> ( prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) x. 1 ) = ( #p ` N ) )
44 iffalse 
 |-  ( -. ( N + 1 ) e. Prime -> if ( ( N + 1 ) e. Prime , ( N + 1 ) , 1 ) = 1 )
45 44 oveq2d 
 |-  ( -. ( N + 1 ) e. Prime -> ( prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) x. if ( ( N + 1 ) e. Prime , ( N + 1 ) , 1 ) ) = ( prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) x. 1 ) )
46 iffalse 
 |-  ( -. ( N + 1 ) e. Prime -> if ( ( N + 1 ) e. Prime , ( ( #p ` N ) x. ( N + 1 ) ) , ( #p ` N ) ) = ( #p ` N ) )
47 45 46 eqeq12d 
 |-  ( -. ( N + 1 ) e. Prime -> ( ( prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) x. if ( ( N + 1 ) e. Prime , ( N + 1 ) , 1 ) ) = if ( ( N + 1 ) e. Prime , ( ( #p ` N ) x. ( N + 1 ) ) , ( #p ` N ) ) <-> ( prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) x. 1 ) = ( #p ` N ) ) )
48 47 adantr 
 |-  ( ( -. ( N + 1 ) e. Prime /\ N e. NN0 ) -> ( ( prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) x. if ( ( N + 1 ) e. Prime , ( N + 1 ) , 1 ) ) = if ( ( N + 1 ) e. Prime , ( ( #p ` N ) x. ( N + 1 ) ) , ( #p ` N ) ) <-> ( prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) x. 1 ) = ( #p ` N ) ) )
49 43 48 mpbird 
 |-  ( ( -. ( N + 1 ) e. Prime /\ N e. NN0 ) -> ( prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) x. if ( ( N + 1 ) e. Prime , ( N + 1 ) , 1 ) ) = if ( ( N + 1 ) e. Prime , ( ( #p ` N ) x. ( N + 1 ) ) , ( #p ` N ) ) )
50 31 49 pm2.61ian 
 |-  ( N e. NN0 -> ( prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) x. if ( ( N + 1 ) e. Prime , ( N + 1 ) , 1 ) ) = if ( ( N + 1 ) e. Prime , ( ( #p ` N ) x. ( N + 1 ) ) , ( #p ` N ) ) )
51 21 50 eqtrd 
 |-  ( N e. NN0 -> ( prod_ k e. ( 1 ... ( ( N + 1 ) - 1 ) ) if ( k e. Prime , k , 1 ) x. if ( ( N + 1 ) e. Prime , ( N + 1 ) , 1 ) ) = if ( ( N + 1 ) e. Prime , ( ( #p ` N ) x. ( N + 1 ) ) , ( #p ` N ) ) )
52 3 15 51 3eqtrd 
 |-  ( N e. NN0 -> ( #p ` ( N + 1 ) ) = if ( ( N + 1 ) e. Prime , ( ( #p ` N ) x. ( N + 1 ) ) , ( #p ` N ) ) )