Metamath Proof Explorer

Theorem lcmineqlem3

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

Ref Expression
Hypotheses lcmineqlem3.1 
|- F = S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( ( 1 - x ) ^ ( N - M ) ) ) _d x
lcmineqlem3.2 
|- ( ph -> N e. NN )
lcmineqlem3.3 
|- ( ph -> M e. NN )
lcmineqlem3.4 
|- ( ph -> M <_ N )
Assertion lcmineqlem3 
|- ( ph -> F = sum_ k e. ( 0 ... ( N - M ) ) ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. ( 1 / ( M + k ) ) ) )

Proof

Step Hyp Ref Expression
1 lcmineqlem3.1 
 |-  F = S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( ( 1 - x ) ^ ( N - M ) ) ) _d x
2 lcmineqlem3.2 
 |-  ( ph -> N e. NN )
3 lcmineqlem3.3 
 |-  ( ph -> M e. NN )
4 lcmineqlem3.4 
 |-  ( ph -> M <_ N )
5 1 2 3 4 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 ) )
6 elunitcn 
 |-  ( x e. ( 0 [,] 1 ) -> x e. CC )
7 6 3ad2ant3 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) /\ x e. ( 0 [,] 1 ) ) -> x e. CC )
8 elfznn0 
 |-  ( k e. ( 0 ... ( N - M ) ) -> k e. NN0 )
9 8 3ad2ant2 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) /\ x e. ( 0 [,] 1 ) ) -> k e. NN0 )
10 nnm1nn0 
 |-  ( M e. NN -> ( M - 1 ) e. NN0 )
11 3 10 syl 
 |-  ( ph -> ( M - 1 ) e. NN0 )
12 11 3ad2ant1 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) /\ x e. ( 0 [,] 1 ) ) -> ( M - 1 ) e. NN0 )
13 7 9 12 expaddd 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) /\ x e. ( 0 [,] 1 ) ) -> ( x ^ ( ( M - 1 ) + k ) ) = ( ( x ^ ( M - 1 ) ) x. ( x ^ k ) ) )
14 13 3expa 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) /\ x e. ( 0 [,] 1 ) ) -> ( x ^ ( ( M - 1 ) + k ) ) = ( ( x ^ ( M - 1 ) ) x. ( x ^ k ) ) )
15 14 itgeq2dv 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> S. ( 0 [,] 1 ) ( x ^ ( ( M - 1 ) + k ) ) _d x = S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( x ^ k ) ) _d x )
16 15 oveq2d 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. S. ( 0 [,] 1 ) ( x ^ ( ( M - 1 ) + k ) ) _d x ) = ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( x ^ k ) ) _d x ) )
17 16 sumeq2dv 
 |-  ( ph -> sum_ k e. ( 0 ... ( N - M ) ) ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. S. ( 0 [,] 1 ) ( x ^ ( ( M - 1 ) + 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 ) )
18 0red 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> 0 e. RR )
19 1red 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> 1 e. RR )
20 0le1 
 |-  0 <_ 1
21 20 a1i 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> 0 <_ 1 )
22 11 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( M - 1 ) e. NN0 )
23 8 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> k e. NN0 )
24 22 23 nn0addcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( ( M - 1 ) + k ) e. NN0 )
25 18 19 21 24 itgpowd 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> S. ( 0 [,] 1 ) ( x ^ ( ( M - 1 ) + k ) ) _d x = ( ( ( 1 ^ ( ( ( M - 1 ) + k ) + 1 ) ) - ( 0 ^ ( ( ( M - 1 ) + k ) + 1 ) ) ) / ( ( ( M - 1 ) + k ) + 1 ) ) )
26 3 nncnd 
 |-  ( ph -> M e. CC )
27 26 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> M e. CC )
28 1cnd 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> 1 e. CC )
29 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
30 8 29 syl 
 |-  ( k e. ( 0 ... ( N - M ) ) -> k e. CC )
31 30 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> k e. CC )
32 27 28 31 nppcand 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( ( ( M - 1 ) + k ) + 1 ) = ( M + k ) )
33 32 oveq2d 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( 1 ^ ( ( ( M - 1 ) + k ) + 1 ) ) = ( 1 ^ ( M + k ) ) )
34 32 oveq2d 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( 0 ^ ( ( ( M - 1 ) + k ) + 1 ) ) = ( 0 ^ ( M + k ) ) )
35 33 34 oveq12d 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( ( 1 ^ ( ( ( M - 1 ) + k ) + 1 ) ) - ( 0 ^ ( ( ( M - 1 ) + k ) + 1 ) ) ) = ( ( 1 ^ ( M + k ) ) - ( 0 ^ ( M + k ) ) ) )
36 3 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> M e. NN )
37 nnnn0addcl 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( M + k ) e. NN )
38 36 23 37 syl2anc 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( M + k ) e. NN )
39 38 nnzd 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( M + k ) e. ZZ )
40 1exp 
 |-  ( ( M + k ) e. ZZ -> ( 1 ^ ( M + k ) ) = 1 )
41 39 40 syl 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( 1 ^ ( M + k ) ) = 1 )
42 0exp 
 |-  ( ( M + k ) e. NN -> ( 0 ^ ( M + k ) ) = 0 )
43 38 42 syl 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( 0 ^ ( M + k ) ) = 0 )
44 41 43 oveq12d 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( ( 1 ^ ( M + k ) ) - ( 0 ^ ( M + k ) ) ) = ( 1 - 0 ) )
45 35 44 eqtrd 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( ( 1 ^ ( ( ( M - 1 ) + k ) + 1 ) ) - ( 0 ^ ( ( ( M - 1 ) + k ) + 1 ) ) ) = ( 1 - 0 ) )
46 1m0e1 
 |-  ( 1 - 0 ) = 1
47 45 46 eqtrdi 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( ( 1 ^ ( ( ( M - 1 ) + k ) + 1 ) ) - ( 0 ^ ( ( ( M - 1 ) + k ) + 1 ) ) ) = 1 )
48 47 32 oveq12d 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( ( ( 1 ^ ( ( ( M - 1 ) + k ) + 1 ) ) - ( 0 ^ ( ( ( M - 1 ) + k ) + 1 ) ) ) / ( ( ( M - 1 ) + k ) + 1 ) ) = ( 1 / ( M + k ) ) )
49 25 48 eqtrd 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> S. ( 0 [,] 1 ) ( x ^ ( ( M - 1 ) + k ) ) _d x = ( 1 / ( M + k ) ) )
50 49 oveq2d 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. S. ( 0 [,] 1 ) ( x ^ ( ( M - 1 ) + k ) ) _d x ) = ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. ( 1 / ( M + k ) ) ) )
51 50 sumeq2dv 
 |-  ( ph -> sum_ k e. ( 0 ... ( N - M ) ) ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. S. ( 0 [,] 1 ) ( x ^ ( ( M - 1 ) + k ) ) _d x ) = sum_ k e. ( 0 ... ( N - M ) ) ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. ( 1 / ( M + k ) ) ) )
52 5 17 51 3eqtr2d 
 |-  ( ph -> F = sum_ k e. ( 0 ... ( N - M ) ) ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. ( 1 / ( M + k ) ) ) )