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 0 # p N lcm _ 1 N

Proof

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