Metamath Proof Explorer


Theorem lcmineqlem6

Description: Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. (Contributed by metakunt, 10-May-2024)

Ref Expression
Hypotheses lcmineqlem6.1 F = 0 1 x M 1 1 x N M dx
lcmineqlem6.2 φ N
lcmineqlem6.3 φ M
lcmineqlem6.4 φ M N
Assertion lcmineqlem6 φ lcm _ 1 N F

Proof

Step Hyp Ref Expression
1 lcmineqlem6.1 F = 0 1 x M 1 1 x N M dx
2 lcmineqlem6.2 φ N
3 lcmineqlem6.3 φ M
4 lcmineqlem6.4 φ M N
5 1 2 3 4 lcmineqlem3 φ F = k = 0 N M 1 k ( N M k) 1 M + k
6 5 oveq2d φ lcm _ 1 N F = lcm _ 1 N k = 0 N M 1 k ( N M k) 1 M + k
7 fzfid φ 0 N M Fin
8 fz1ssnn 1 N
9 fzfi 1 N Fin
10 8 9 pm3.2i 1 N 1 N Fin
11 lcmfnncl 1 N 1 N Fin lcm _ 1 N
12 10 11 ax-mp lcm _ 1 N
13 12 nncni lcm _ 1 N
14 13 a1i φ lcm _ 1 N
15 elfzelz k 0 N M k
16 m1expcl k 1 k
17 15 16 syl k 0 N M 1 k
18 17 zcnd k 0 N M 1 k
19 18 adantl φ k 0 N M 1 k
20 bccl2 k 0 N M ( N M k)
21 20 nncnd k 0 N M ( N M k)
22 21 adantl φ k 0 N M ( N M k)
23 19 22 mulcld φ k 0 N M 1 k ( N M k)
24 3 nncnd φ M
25 24 adantr φ k 0 N M M
26 15 zcnd k 0 N M k
27 26 adantl φ k 0 N M k
28 25 27 addcld φ k 0 N M M + k
29 elfznn0 k 0 N M k 0
30 nnnn0addcl M k 0 M + k
31 29 30 sylan2 M k 0 N M M + k
32 3 31 sylan φ k 0 N M M + k
33 32 nnne0d φ k 0 N M M + k 0
34 28 33 reccld φ k 0 N M 1 M + k
35 23 34 mulcld φ k 0 N M 1 k ( N M k) 1 M + k
36 7 14 35 fsummulc2 φ lcm _ 1 N k = 0 N M 1 k ( N M k) 1 M + k = k = 0 N M lcm _ 1 N 1 k ( N M k) 1 M + k
37 6 36 eqtrd φ lcm _ 1 N F = k = 0 N M lcm _ 1 N 1 k ( N M k) 1 M + k
38 13 a1i φ k 0 N M lcm _ 1 N
39 38 23 28 33 lcmineqlem5 φ k 0 N M lcm _ 1 N 1 k ( N M k) 1 M + k = 1 k ( N M k) lcm _ 1 N M + k
40 39 sumeq2dv φ k = 0 N M lcm _ 1 N 1 k ( N M k) 1 M + k = k = 0 N M 1 k ( N M k) lcm _ 1 N M + k
41 37 40 eqtrd φ lcm _ 1 N F = k = 0 N M 1 k ( N M k) lcm _ 1 N M + k
42 17 adantl φ k 0 N M 1 k
43 20 nnzd k 0 N M ( N M k)
44 43 adantl φ k 0 N M ( N M k)
45 42 44 zmulcld φ k 0 N M 1 k ( N M k)
46 2 adantr φ k 0 N M N
47 3 adantr φ k 0 N M M
48 4 adantr φ k 0 N M M N
49 simpr φ k 0 N M k 0 N M
50 46 47 48 49 lcmineqlem4 φ k 0 N M lcm _ 1 N M + k
51 45 50 zmulcld φ k 0 N M 1 k ( N M k) lcm _ 1 N M + k
52 7 51 fsumzcl φ k = 0 N M 1 k ( N M k) lcm _ 1 N M + k
53 41 52 eqeltrd φ lcm _ 1 N F