Metamath Proof Explorer


Theorem lcmineqlem1

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 lcmineqlem1.1 F = 0 1 x M 1 1 x N M dx
lcmineqlem1.2 φ N
lcmineqlem1.3 φ M
lcmineqlem1.4 φ M N
Assertion lcmineqlem1 φ F = 0 1 x M 1 k = 0 N M 1 k ( N M k) x k dx

Proof

Step Hyp Ref Expression
1 lcmineqlem1.1 F = 0 1 x M 1 1 x N M dx
2 lcmineqlem1.2 φ N
3 lcmineqlem1.3 φ M
4 lcmineqlem1.4 φ M N
5 elunitcn x 0 1 x
6 ax-1cn 1
7 negsub 1 x 1 + x = 1 x
8 6 7 mpan x 1 + x = 1 x
9 8 oveq1d x 1 + x N M = 1 x N M
10 9 adantl φ x 1 + x N M = 1 x N M
11 negcl x x
12 1cnd φ 1
13 3 nnnn0d φ M 0
14 2 nnnn0d φ N 0
15 nn0sub M 0 N 0 M N N M 0
16 13 14 15 syl2anc φ M N N M 0
17 4 16 mpbid φ N M 0
18 binom 1 x N M 0 1 + x N M = k = 0 N M ( N M k) 1 N - M - k x k
19 18 3com23 1 N M 0 x 1 + x N M = k = 0 N M ( N M k) 1 N - M - k x k
20 19 3expia 1 N M 0 x 1 + x N M = k = 0 N M ( N M k) 1 N - M - k x k
21 12 17 20 syl2anc φ x 1 + x N M = k = 0 N M ( N M k) 1 N - M - k x k
22 11 21 syl5 φ x 1 + x N M = k = 0 N M ( N M k) 1 N - M - k x k
23 22 imp φ x 1 + x N M = k = 0 N M ( N M k) 1 N - M - k x k
24 10 23 eqtr3d φ x 1 x N M = k = 0 N M ( N M k) 1 N - M - k x k
25 elfzelz k 0 N M k
26 2 nnzd φ N
27 3 nnzd φ M
28 zsubcl N M N M
29 26 27 28 syl2anc φ N M
30 zsubcl N M k N - M - k
31 29 30 sylan φ k N - M - k
32 25 31 sylan2 φ k 0 N M N - M - k
33 1exp N - M - k 1 N - M - k = 1
34 32 33 syl φ k 0 N M 1 N - M - k = 1
35 34 3adant2 φ x k 0 N M 1 N - M - k = 1
36 35 oveq1d φ x k 0 N M 1 N - M - k x k = 1 x k
37 11 3ad2ant2 φ x k 0 N M x
38 elfznn0 k 0 N M k 0
39 38 3ad2ant3 φ x k 0 N M k 0
40 expcl x k 0 x k
41 37 39 40 syl2anc φ x k 0 N M x k
42 41 mulid2d φ x k 0 N M 1 x k = x k
43 36 42 eqtrd φ x k 0 N M 1 N - M - k x k = x k
44 mulm1 x -1 x = x
45 44 oveq1d x -1 x k = x k
46 45 3ad2ant2 φ x k 0 N M -1 x k = x k
47 43 46 eqtr4d φ x k 0 N M 1 N - M - k x k = -1 x k
48 neg1cn 1
49 mulexp 1 x k 0 -1 x k = 1 k x k
50 48 49 mp3an1 x k 0 -1 x k = 1 k x k
51 38 50 sylan2 x k 0 N M -1 x k = 1 k x k
52 51 3adant1 φ x k 0 N M -1 x k = 1 k x k
53 47 52 eqtrd φ x k 0 N M 1 N - M - k x k = 1 k x k
54 53 oveq2d φ x k 0 N M ( N M k) 1 N - M - k x k = ( N M k) 1 k x k
55 bccl N M 0 k ( N M k) 0
56 17 25 55 syl2an φ k 0 N M ( N M k) 0
57 56 3adant2 φ x k 0 N M ( N M k) 0
58 57 nn0cnd φ x k 0 N M ( N M k)
59 expcl 1 k 0 1 k
60 48 39 59 sylancr φ x k 0 N M 1 k
61 expcl x k 0 x k
62 38 61 sylan2 x k 0 N M x k
63 62 3adant1 φ x k 0 N M x k
64 58 60 63 mulassd φ x k 0 N M ( N M k) 1 k x k = ( N M k) 1 k x k
65 54 64 eqtr4d φ x k 0 N M ( N M k) 1 N - M - k x k = ( N M k) 1 k x k
66 58 60 mulcomd φ x k 0 N M ( N M k) 1 k = 1 k ( N M k)
67 66 oveq1d φ x k 0 N M ( N M k) 1 k x k = 1 k ( N M k) x k
68 65 67 eqtrd φ x k 0 N M ( N M k) 1 N - M - k x k = 1 k ( N M k) x k
69 68 3expa φ x k 0 N M ( N M k) 1 N - M - k x k = 1 k ( N M k) x k
70 69 sumeq2dv φ x k = 0 N M ( N M k) 1 N - M - k x k = k = 0 N M 1 k ( N M k) x k
71 24 70 eqtrd φ x 1 x N M = k = 0 N M 1 k ( N M k) x k
72 5 71 sylan2 φ x 0 1 1 x N M = k = 0 N M 1 k ( N M k) x k
73 72 oveq2d φ x 0 1 x M 1 1 x N M = x M 1 k = 0 N M 1 k ( N M k) x k
74 73 itgeq2dv φ 0 1 x M 1 1 x N M dx = 0 1 x M 1 k = 0 N M 1 k ( N M k) x k dx
75 1 74 syl5eq φ F = 0 1 x M 1 k = 0 N M 1 k ( N M k) x k dx