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 = S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( ( 1 - x ) ^ ( N - M ) ) ) _d x
lcmineqlem1.2 
|- ( ph -> N e. NN )
lcmineqlem1.3 
|- ( ph -> M e. NN )
lcmineqlem1.4 
|- ( ph -> M <_ N )
Assertion lcmineqlem1 
|- ( ph -> F = S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. sum_ k e. ( 0 ... ( N - M ) ) ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. ( x ^ k ) ) ) _d x )

Proof

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