Metamath Proof Explorer

Theorem prmdvdsprmo

Description: The primorial of a number is divisible by each prime less then or equal to the number. (Contributed by AV, 15-Aug-2020) (Revised by AV, 28-Aug-2020)

Ref Expression
Assertion prmdvdsprmo 
|- ( N e. NN -> A. p e. Prime ( p <_ N -> p || ( #p ` N ) ) )

Proof

Step Hyp Ref Expression
1 fzfi 
 |-  ( 1 ... N ) e. Fin
2 diffi 
 |-  ( ( 1 ... N ) e. Fin -> ( ( 1 ... N ) \ { p } ) e. Fin )
3 1 2 mp1i 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> ( ( 1 ... N ) \ { p } ) e. Fin )
4 eldifi 
 |-  ( k e. ( ( 1 ... N ) \ { p } ) -> k e. ( 1 ... N ) )
5 elfzelz 
 |-  ( k e. ( 1 ... N ) -> k e. ZZ )
6 4 5 syl 
 |-  ( k e. ( ( 1 ... N ) \ { p } ) -> k e. ZZ )
7 1zzd 
 |-  ( k e. ( ( 1 ... N ) \ { p } ) -> 1 e. ZZ )
8 6 7 ifcld 
 |-  ( k e. ( ( 1 ... N ) \ { p } ) -> if ( k e. Prime , k , 1 ) e. ZZ )
9 8 adantl 
 |-  ( ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) /\ k e. ( ( 1 ... N ) \ { p } ) ) -> if ( k e. Prime , k , 1 ) e. ZZ )
10 3 9 fprodzcl 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> prod_ k e. ( ( 1 ... N ) \ { p } ) if ( k e. Prime , k , 1 ) e. ZZ )
11 prmz 
 |-  ( p e. Prime -> p e. ZZ )
12 11 adantl 
 |-  ( ( N e. NN /\ p e. Prime ) -> p e. ZZ )
13 12 adantr 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> p e. ZZ )
14 dvdsmul2 
 |-  ( ( prod_ k e. ( ( 1 ... N ) \ { p } ) if ( k e. Prime , k , 1 ) e. ZZ /\ p e. ZZ ) -> p || ( prod_ k e. ( ( 1 ... N ) \ { p } ) if ( k e. Prime , k , 1 ) x. p ) )
15 10 13 14 syl2anc 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> p || ( prod_ k e. ( ( 1 ... N ) \ { p } ) if ( k e. Prime , k , 1 ) x. p ) )
16 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
17 prmoval 
 |-  ( N e. NN0 -> ( #p ` N ) = prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) )
18 16 17 syl 
 |-  ( N e. NN -> ( #p ` N ) = prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) )
19 18 ad2antrr 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> ( #p ` N ) = prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) )
20 19 breq2d 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> ( p || ( #p ` N ) <-> p || prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) ) )
21 neldifsnd 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> -. p e. ( ( 1 ... N ) \ { p } ) )
22 disjsn 
 |-  ( ( ( ( 1 ... N ) \ { p } ) i^i { p } ) = (/) <-> -. p e. ( ( 1 ... N ) \ { p } ) )
23 21 22 sylibr 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> ( ( ( 1 ... N ) \ { p } ) i^i { p } ) = (/) )
24 prmnn 
 |-  ( p e. Prime -> p e. NN )
25 24 adantl 
 |-  ( ( N e. NN /\ p e. Prime ) -> p e. NN )
26 25 anim1i 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> ( p e. NN /\ p <_ N ) )
27 nnz 
 |-  ( N e. NN -> N e. ZZ )
28 fznn 
 |-  ( N e. ZZ -> ( p e. ( 1 ... N ) <-> ( p e. NN /\ p <_ N ) ) )
29 27 28 syl 
 |-  ( N e. NN -> ( p e. ( 1 ... N ) <-> ( p e. NN /\ p <_ N ) ) )
30 29 ad2antrr 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> ( p e. ( 1 ... N ) <-> ( p e. NN /\ p <_ N ) ) )
31 26 30 mpbird 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> p e. ( 1 ... N ) )
32 difsnid 
 |-  ( p e. ( 1 ... N ) -> ( ( ( 1 ... N ) \ { p } ) u. { p } ) = ( 1 ... N ) )
33 32 eqcomd 
 |-  ( p e. ( 1 ... N ) -> ( 1 ... N ) = ( ( ( 1 ... N ) \ { p } ) u. { p } ) )
34 31 33 syl 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> ( 1 ... N ) = ( ( ( 1 ... N ) \ { p } ) u. { p } ) )
35 fzfid 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> ( 1 ... N ) e. Fin )
36 1zzd 
 |-  ( k e. ( 1 ... N ) -> 1 e. ZZ )
37 5 36 ifcld 
 |-  ( k e. ( 1 ... N ) -> if ( k e. Prime , k , 1 ) e. ZZ )
38 37 zcnd 
 |-  ( k e. ( 1 ... N ) -> if ( k e. Prime , k , 1 ) e. CC )
39 38 adantl 
 |-  ( ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) /\ k e. ( 1 ... N ) ) -> if ( k e. Prime , k , 1 ) e. CC )
40 23 34 35 39 fprodsplit 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) = ( prod_ k e. ( ( 1 ... N ) \ { p } ) if ( k e. Prime , k , 1 ) x. prod_ k e. { p } if ( k e. Prime , k , 1 ) ) )
41 simplr 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> p e. Prime )
42 25 adantr 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> p e. NN )
43 42 nncnd 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> p e. CC )
44 1cnd 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> 1 e. CC )
45 43 44 ifcld 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> if ( p e. Prime , p , 1 ) e. CC )
46 eleq1w 
 |-  ( k = p -> ( k e. Prime <-> p e. Prime ) )
47 id 
 |-  ( k = p -> k = p )
48 46 47 ifbieq1d 
 |-  ( k = p -> if ( k e. Prime , k , 1 ) = if ( p e. Prime , p , 1 ) )
49 48 prodsn 
 |-  ( ( p e. Prime /\ if ( p e. Prime , p , 1 ) e. CC ) -> prod_ k e. { p } if ( k e. Prime , k , 1 ) = if ( p e. Prime , p , 1 ) )
50 41 45 49 syl2anc 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> prod_ k e. { p } if ( k e. Prime , k , 1 ) = if ( p e. Prime , p , 1 ) )
51 simpr 
 |-  ( ( N e. NN /\ p e. Prime ) -> p e. Prime )
52 51 iftrued 
 |-  ( ( N e. NN /\ p e. Prime ) -> if ( p e. Prime , p , 1 ) = p )
53 52 adantr 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> if ( p e. Prime , p , 1 ) = p )
54 50 53 eqtrd 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> prod_ k e. { p } if ( k e. Prime , k , 1 ) = p )
55 54 oveq2d 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> ( prod_ k e. ( ( 1 ... N ) \ { p } ) if ( k e. Prime , k , 1 ) x. prod_ k e. { p } if ( k e. Prime , k , 1 ) ) = ( prod_ k e. ( ( 1 ... N ) \ { p } ) if ( k e. Prime , k , 1 ) x. p ) )
56 40 55 eqtrd 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) = ( prod_ k e. ( ( 1 ... N ) \ { p } ) if ( k e. Prime , k , 1 ) x. p ) )
57 56 breq2d 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> ( p || prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) <-> p || ( prod_ k e. ( ( 1 ... N ) \ { p } ) if ( k e. Prime , k , 1 ) x. p ) ) )
58 20 57 bitrd 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> ( p || ( #p ` N ) <-> p || ( prod_ k e. ( ( 1 ... N ) \ { p } ) if ( k e. Prime , k , 1 ) x. p ) ) )
59 15 58 mpbird 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ N ) -> p || ( #p ` N ) )
60 59 ex 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p <_ N -> p || ( #p ` N ) ) )
61 60 ralrimiva 
 |-  ( N e. NN -> A. p e. Prime ( p <_ N -> p || ( #p ` N ) ) )