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