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

Proof

Step Hyp Ref Expression
1 lcmineqlem2.1 
 |-  F = S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( ( 1 - x ) ^ ( N - M ) ) ) _d x
2 lcmineqlem2.2 
 |-  ( ph -> N e. NN )
3 lcmineqlem2.3 
 |-  ( ph -> M e. NN )
4 lcmineqlem2.4 
 |-  ( ph -> M <_ N )
5 1 2 3 4 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 )
6 eqid 
 |-  ( 0 [,] 1 ) = ( 0 [,] 1 )
7 fzfid 
 |-  ( ph -> ( 0 ... ( N - M ) ) e. Fin )
8 0red 
 |-  ( ph -> 0 e. RR )
9 1red 
 |-  ( ph -> 1 e. RR )
10 unitsscn 
 |-  ( 0 [,] 1 ) C_ CC
11 resmpt 
 |-  ( ( 0 [,] 1 ) C_ CC -> ( ( x e. CC |-> ( x ^ ( M - 1 ) ) ) |` ( 0 [,] 1 ) ) = ( x e. ( 0 [,] 1 ) |-> ( x ^ ( M - 1 ) ) ) )
12 10 11 ax-mp 
 |-  ( ( x e. CC |-> ( x ^ ( M - 1 ) ) ) |` ( 0 [,] 1 ) ) = ( x e. ( 0 [,] 1 ) |-> ( x ^ ( M - 1 ) ) )
13 nnm1nn0 
 |-  ( M e. NN -> ( M - 1 ) e. NN0 )
14 expcncf 
 |-  ( ( M - 1 ) e. NN0 -> ( x e. CC |-> ( x ^ ( M - 1 ) ) ) e. ( CC -cn-> CC ) )
15 rescncf 
 |-  ( ( 0 [,] 1 ) C_ CC -> ( ( x e. CC |-> ( x ^ ( M - 1 ) ) ) e. ( CC -cn-> CC ) -> ( ( x e. CC |-> ( x ^ ( M - 1 ) ) ) |` ( 0 [,] 1 ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) ) )
16 10 15 ax-mp 
 |-  ( ( x e. CC |-> ( x ^ ( M - 1 ) ) ) e. ( CC -cn-> CC ) -> ( ( x e. CC |-> ( x ^ ( M - 1 ) ) ) |` ( 0 [,] 1 ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
17 3 13 14 16 4syl 
 |-  ( ph -> ( ( x e. CC |-> ( x ^ ( M - 1 ) ) ) |` ( 0 [,] 1 ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
18 12 17 eqeltrrid 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) |-> ( x ^ ( M - 1 ) ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
19 elfznn0 
 |-  ( k e. ( 0 ... ( N - M ) ) -> k e. NN0 )
20 neg1cn 
 |-  -u 1 e. CC
21 expcl 
 |-  ( ( -u 1 e. CC /\ k e. NN0 ) -> ( -u 1 ^ k ) e. CC )
22 20 21 mpan 
 |-  ( k e. NN0 -> ( -u 1 ^ k ) e. CC )
23 19 22 syl 
 |-  ( k e. ( 0 ... ( N - M ) ) -> ( -u 1 ^ k ) e. CC )
24 23 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( -u 1 ^ k ) e. CC )
25 3 nnnn0d 
 |-  ( ph -> M e. NN0 )
26 2 nnnn0d 
 |-  ( ph -> N e. NN0 )
27 nn0sub 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M <_ N <-> ( N - M ) e. NN0 ) )
28 25 26 27 syl2anc 
 |-  ( ph -> ( M <_ N <-> ( N - M ) e. NN0 ) )
29 4 28 mpbid 
 |-  ( ph -> ( N - M ) e. NN0 )
30 nn0z 
 |-  ( k e. NN0 -> k e. ZZ )
31 19 30 syl 
 |-  ( k e. ( 0 ... ( N - M ) ) -> k e. ZZ )
32 bccl 
 |-  ( ( ( N - M ) e. NN0 /\ k e. ZZ ) -> ( ( N - M ) _C k ) e. NN0 )
33 31 32 sylan2 
 |-  ( ( ( N - M ) e. NN0 /\ k e. ( 0 ... ( N - M ) ) ) -> ( ( N - M ) _C k ) e. NN0 )
34 29 33 sylan 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( ( N - M ) _C k ) e. NN0 )
35 34 nn0cnd 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( ( N - M ) _C k ) e. CC )
36 24 35 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) e. CC )
37 resmpt 
 |-  ( ( 0 [,] 1 ) C_ CC -> ( ( x e. CC |-> ( x ^ k ) ) |` ( 0 [,] 1 ) ) = ( x e. ( 0 [,] 1 ) |-> ( x ^ k ) ) )
38 10 37 ax-mp 
 |-  ( ( x e. CC |-> ( x ^ k ) ) |` ( 0 [,] 1 ) ) = ( x e. ( 0 [,] 1 ) |-> ( x ^ k ) )
39 expcncf 
 |-  ( k e. NN0 -> ( x e. CC |-> ( x ^ k ) ) e. ( CC -cn-> CC ) )
40 19 39 syl 
 |-  ( k e. ( 0 ... ( N - M ) ) -> ( x e. CC |-> ( x ^ k ) ) e. ( CC -cn-> CC ) )
41 rescncf 
 |-  ( ( 0 [,] 1 ) C_ CC -> ( ( x e. CC |-> ( x ^ k ) ) e. ( CC -cn-> CC ) -> ( ( x e. CC |-> ( x ^ k ) ) |` ( 0 [,] 1 ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) ) )
42 10 41 ax-mp 
 |-  ( ( x e. CC |-> ( x ^ k ) ) e. ( CC -cn-> CC ) -> ( ( x e. CC |-> ( x ^ k ) ) |` ( 0 [,] 1 ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
43 40 42 syl 
 |-  ( k e. ( 0 ... ( N - M ) ) -> ( ( x e. CC |-> ( x ^ k ) ) |` ( 0 [,] 1 ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
44 38 43 eqeltrrid 
 |-  ( k e. ( 0 ... ( N - M ) ) -> ( x e. ( 0 [,] 1 ) |-> ( x ^ k ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
45 44 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( x e. ( 0 [,] 1 ) |-> ( x ^ k ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
46 6 7 8 9 18 36 45 3factsumint 
 |-  ( ph -> 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 = sum_ k e. ( 0 ... ( N - M ) ) ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( x ^ k ) ) _d x ) )
47 5 46 eqtrd 
 |-  ( ph -> F = sum_ k e. ( 0 ... ( N - M ) ) ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( x ^ k ) ) _d x ) )