Metamath Proof Explorer


Theorem lcmineqlem2

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, 29-Apr-2024)

Ref Expression
Hypotheses lcmineqlem2.1 F = 0 1 x M 1 1 x N M dx
lcmineqlem2.2 φ N
lcmineqlem2.3 φ M
lcmineqlem2.4 φ M N
Assertion lcmineqlem2 φ F = k = 0 N M 1 k ( N M k) 0 1 x M 1 x k dx

Proof

Step Hyp Ref Expression
1 lcmineqlem2.1 F = 0 1 x M 1 1 x N M dx
2 lcmineqlem2.2 φ N
3 lcmineqlem2.3 φ M
4 lcmineqlem2.4 φ M N
5 1 2 3 4 lcmineqlem1 φ F = 0 1 x M 1 k = 0 N M 1 k ( N M k) x k dx
6 eqid 0 1 = 0 1
7 fzfid φ 0 N M Fin
8 0red φ 0
9 1red φ 1
10 unitsscn 0 1
11 resmpt 0 1 x x M 1 0 1 = x 0 1 x M 1
12 10 11 ax-mp x x M 1 0 1 = x 0 1 x M 1
13 nnm1nn0 M M 1 0
14 expcncf M 1 0 x x M 1 : cn
15 3 13 14 3syl φ x x M 1 : cn
16 rescncf 0 1 x x M 1 : cn x x M 1 0 1 : 0 1 cn
17 10 16 ax-mp x x M 1 : cn x x M 1 0 1 : 0 1 cn
18 15 17 syl φ x x M 1 0 1 : 0 1 cn
19 12 18 eqeltrrid φ x 0 1 x M 1 : 0 1 cn
20 elfznn0 k 0 N M k 0
21 neg1cn 1
22 expcl 1 k 0 1 k
23 21 22 mpan k 0 1 k
24 20 23 syl k 0 N M 1 k
25 24 adantl φ k 0 N M 1 k
26 3 nnnn0d φ M 0
27 2 nnnn0d φ N 0
28 nn0sub M 0 N 0 M N N M 0
29 26 27 28 syl2anc φ M N N M 0
30 4 29 mpbid φ N M 0
31 nn0z k 0 k
32 20 31 syl k 0 N M k
33 bccl N M 0 k ( N M k) 0
34 32 33 sylan2 N M 0 k 0 N M ( N M k) 0
35 30 34 sylan φ k 0 N M ( N M k) 0
36 35 nn0cnd φ k 0 N M ( N M k)
37 25 36 mulcld φ k 0 N M 1 k ( N M k)
38 resmpt 0 1 x x k 0 1 = x 0 1 x k
39 10 38 ax-mp x x k 0 1 = x 0 1 x k
40 expcncf k 0 x x k : cn
41 20 40 syl k 0 N M x x k : cn
42 rescncf 0 1 x x k : cn x x k 0 1 : 0 1 cn
43 10 42 ax-mp x x k : cn x x k 0 1 : 0 1 cn
44 41 43 syl k 0 N M x x k 0 1 : 0 1 cn
45 39 44 eqeltrrid k 0 N M x 0 1 x k : 0 1 cn
46 45 adantl φ k 0 N M x 0 1 x k : 0 1 cn
47 6 7 8 9 19 37 46 3factsumint φ 0 1 x M 1 k = 0 N M 1 k ( N M k) x k dx = k = 0 N M 1 k ( N M k) 0 1 x M 1 x k dx
48 5 47 eqtrd φ F = k = 0 N M 1 k ( N M k) 0 1 x M 1 x k dx