Metamath Proof Explorer

Theorem prmodvdslcmf

Description: The primorial of a nonnegative integer divides the least common multiple of all positive integers less than or equal to the integer. (Contributed by AV, 19-Aug-2020) (Revised by AV, 29-Aug-2020)

Ref Expression
Assertion prmodvdslcmf 
|- ( N e. NN0 -> ( #p ` N ) || ( _lcm ` ( 1 ... N ) ) )

Proof

Step Hyp Ref Expression
1 prmoval 
 |-  ( N e. NN0 -> ( #p ` N ) = prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) )
2 eqidd 
 |-  ( k e. ( 1 ... N ) -> ( m e. NN |-> if ( m e. Prime , m , 1 ) ) = ( m e. NN |-> if ( m e. Prime , m , 1 ) ) )
3 simpr 
 |-  ( ( k e. ( 1 ... N ) /\ m = k ) -> m = k )
4 3 eleq1d 
 |-  ( ( k e. ( 1 ... N ) /\ m = k ) -> ( m e. Prime <-> k e. Prime ) )
5 4 3 ifbieq1d 
 |-  ( ( k e. ( 1 ... N ) /\ m = k ) -> if ( m e. Prime , m , 1 ) = if ( k e. Prime , k , 1 ) )
6 elfznn 
 |-  ( k e. ( 1 ... N ) -> k e. NN )
7 1nn 
 |-  1 e. NN
8 7 a1i 
 |-  ( k e. ( 1 ... N ) -> 1 e. NN )
9 6 8 ifcld 
 |-  ( k e. ( 1 ... N ) -> if ( k e. Prime , k , 1 ) e. NN )
10 2 5 6 9 fvmptd 
 |-  ( k e. ( 1 ... N ) -> ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) = if ( k e. Prime , k , 1 ) )
11 10 eqcomd 
 |-  ( k e. ( 1 ... N ) -> if ( k e. Prime , k , 1 ) = ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) )
12 11 prodeq2i 
 |-  prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) = prod_ k e. ( 1 ... N ) ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k )
13 1 12 eqtrdi 
 |-  ( N e. NN0 -> ( #p ` N ) = prod_ k e. ( 1 ... N ) ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) )
14 fzfid 
 |-  ( N e. NN0 -> ( 1 ... N ) e. Fin )
15 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
16 14 15 jctil 
 |-  ( N e. NN0 -> ( ( 1 ... N ) C_ NN /\ ( 1 ... N ) e. Fin ) )
17 fzssz 
 |-  ( 1 ... N ) C_ ZZ
18 17 a1i 
 |-  ( N e. NN0 -> ( 1 ... N ) C_ ZZ )
19 0nelfz1 
 |-  0 e/ ( 1 ... N )
20 19 a1i 
 |-  ( N e. NN0 -> 0 e/ ( 1 ... N ) )
21 lcmfn0cl 
 |-  ( ( ( 1 ... N ) C_ ZZ /\ ( 1 ... N ) e. Fin /\ 0 e/ ( 1 ... N ) ) -> ( _lcm ` ( 1 ... N ) ) e. NN )
22 18 14 20 21 syl3anc 
 |-  ( N e. NN0 -> ( _lcm ` ( 1 ... N ) ) e. NN )
23 id 
 |-  ( m e. NN -> m e. NN )
24 7 a1i 
 |-  ( m e. NN -> 1 e. NN )
25 23 24 ifcld 
 |-  ( m e. NN -> if ( m e. Prime , m , 1 ) e. NN )
26 25 adantl 
 |-  ( ( N e. NN0 /\ m e. NN ) -> if ( m e. Prime , m , 1 ) e. NN )
27 26 fmpttd 
 |-  ( N e. NN0 -> ( m e. NN |-> if ( m e. Prime , m , 1 ) ) : NN --> NN )
28 simpr 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> k e. ( 1 ... N ) )
29 28 adantr 
 |-  ( ( ( N e. NN0 /\ k e. ( 1 ... N ) ) /\ x e. ( ( 1 ... N ) \ { k } ) ) -> k e. ( 1 ... N ) )
30 eldifi 
 |-  ( x e. ( ( 1 ... N ) \ { k } ) -> x e. ( 1 ... N ) )
31 30 adantl 
 |-  ( ( ( N e. NN0 /\ k e. ( 1 ... N ) ) /\ x e. ( ( 1 ... N ) \ { k } ) ) -> x e. ( 1 ... N ) )
32 eldif 
 |-  ( x e. ( ( 1 ... N ) \ { k } ) <-> ( x e. ( 1 ... N ) /\ -. x e. { k } ) )
33 velsn 
 |-  ( x e. { k } <-> x = k )
34 33 biimpri 
 |-  ( x = k -> x e. { k } )
35 34 equcoms 
 |-  ( k = x -> x e. { k } )
36 35 necon3bi 
 |-  ( -. x e. { k } -> k =/= x )
37 32 36 simplbiim 
 |-  ( x e. ( ( 1 ... N ) \ { k } ) -> k =/= x )
38 37 adantl 
 |-  ( ( ( N e. NN0 /\ k e. ( 1 ... N ) ) /\ x e. ( ( 1 ... N ) \ { k } ) ) -> k =/= x )
39 eqid 
 |-  ( m e. NN |-> if ( m e. Prime , m , 1 ) ) = ( m e. NN |-> if ( m e. Prime , m , 1 ) )
40 39 fvprmselgcd1 
 |-  ( ( k e. ( 1 ... N ) /\ x e. ( 1 ... N ) /\ k =/= x ) -> ( ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) gcd ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` x ) ) = 1 )
41 29 31 38 40 syl3anc 
 |-  ( ( ( N e. NN0 /\ k e. ( 1 ... N ) ) /\ x e. ( ( 1 ... N ) \ { k } ) ) -> ( ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) gcd ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` x ) ) = 1 )
42 41 ralrimiva 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> A. x e. ( ( 1 ... N ) \ { k } ) ( ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) gcd ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` x ) ) = 1 )
43 42 ralrimiva 
 |-  ( N e. NN0 -> A. k e. ( 1 ... N ) A. x e. ( ( 1 ... N ) \ { k } ) ( ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) gcd ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` x ) ) = 1 )
44 eqidd 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> ( m e. NN |-> if ( m e. Prime , m , 1 ) ) = ( m e. NN |-> if ( m e. Prime , m , 1 ) ) )
45 simpr 
 |-  ( ( ( N e. NN0 /\ k e. ( 1 ... N ) ) /\ m = k ) -> m = k )
46 45 eleq1d 
 |-  ( ( ( N e. NN0 /\ k e. ( 1 ... N ) ) /\ m = k ) -> ( m e. Prime <-> k e. Prime ) )
47 46 45 ifbieq1d 
 |-  ( ( ( N e. NN0 /\ k e. ( 1 ... N ) ) /\ m = k ) -> if ( m e. Prime , m , 1 ) = if ( k e. Prime , k , 1 ) )
48 15 28 sseldi 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> k e. NN )
49 17 28 sseldi 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> k e. ZZ )
50 1zzd 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> 1 e. ZZ )
51 49 50 ifcld 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> if ( k e. Prime , k , 1 ) e. ZZ )
52 44 47 48 51 fvmptd 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) = if ( k e. Prime , k , 1 ) )
53 breq1 
 |-  ( x = if ( k e. Prime , k , 1 ) -> ( x || ( _lcm ` ( 1 ... N ) ) <-> if ( k e. Prime , k , 1 ) || ( _lcm ` ( 1 ... N ) ) ) )
54 16 adantr 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> ( ( 1 ... N ) C_ NN /\ ( 1 ... N ) e. Fin ) )
55 17 2a1i 
 |-  ( ( 1 ... N ) e. Fin -> ( ( 1 ... N ) C_ NN -> ( 1 ... N ) C_ ZZ ) )
56 55 imdistanri 
 |-  ( ( ( 1 ... N ) C_ NN /\ ( 1 ... N ) e. Fin ) -> ( ( 1 ... N ) C_ ZZ /\ ( 1 ... N ) e. Fin ) )
57 dvdslcmf 
 |-  ( ( ( 1 ... N ) C_ ZZ /\ ( 1 ... N ) e. Fin ) -> A. x e. ( 1 ... N ) x || ( _lcm ` ( 1 ... N ) ) )
58 54 56 57 3syl 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> A. x e. ( 1 ... N ) x || ( _lcm ` ( 1 ... N ) ) )
59 elfzuz2 
 |-  ( k e. ( 1 ... N ) -> N e. ( ZZ>= ` 1 ) )
60 59 adantl 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> N e. ( ZZ>= ` 1 ) )
61 eluzfz1 
 |-  ( N e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... N ) )
62 60 61 syl 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> 1 e. ( 1 ... N ) )
63 28 62 ifcld 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> if ( k e. Prime , k , 1 ) e. ( 1 ... N ) )
64 53 58 63 rspcdva 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> if ( k e. Prime , k , 1 ) || ( _lcm ` ( 1 ... N ) ) )
65 52 64 eqbrtrd 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) || ( _lcm ` ( 1 ... N ) ) )
66 65 ralrimiva 
 |-  ( N e. NN0 -> A. k e. ( 1 ... N ) ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) || ( _lcm ` ( 1 ... N ) ) )
67 coprmproddvds 
 |-  ( ( ( ( 1 ... N ) C_ NN /\ ( 1 ... N ) e. Fin ) /\ ( ( _lcm ` ( 1 ... N ) ) e. NN /\ ( m e. NN |-> if ( m e. Prime , m , 1 ) ) : NN --> NN ) /\ ( A. k e. ( 1 ... N ) A. x e. ( ( 1 ... N ) \ { k } ) ( ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) gcd ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` x ) ) = 1 /\ A. k e. ( 1 ... N ) ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) || ( _lcm ` ( 1 ... N ) ) ) ) -> prod_ k e. ( 1 ... N ) ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) || ( _lcm ` ( 1 ... N ) ) )
68 16 22 27 43 66 67 syl122anc 
 |-  ( N e. NN0 -> prod_ k e. ( 1 ... N ) ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) || ( _lcm ` ( 1 ... N ) ) )
69 13 68 eqbrtrd 
 |-  ( N e. NN0 -> ( #p ` N ) || ( _lcm ` ( 1 ... N ) ) )