Metamath Proof Explorer

Theorem lcmineqlem6

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, 10-May-2024)

Ref Expression
Hypotheses lcmineqlem6.1 
|- F = S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( ( 1 - x ) ^ ( N - M ) ) ) _d x
lcmineqlem6.2 
|- ( ph -> N e. NN )
lcmineqlem6.3 
|- ( ph -> M e. NN )
lcmineqlem6.4 
|- ( ph -> M <_ N )
Assertion lcmineqlem6 
|- ( ph -> ( ( _lcm ` ( 1 ... N ) ) x. F ) e. ZZ )

Proof

Step Hyp Ref Expression
1 lcmineqlem6.1 
 |-  F = S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( ( 1 - x ) ^ ( N - M ) ) ) _d x
2 lcmineqlem6.2 
 |-  ( ph -> N e. NN )
3 lcmineqlem6.3 
 |-  ( ph -> M e. NN )
4 lcmineqlem6.4 
 |-  ( ph -> M <_ N )
5 1 2 3 4 lcmineqlem3 
 |-  ( ph -> F = sum_ k e. ( 0 ... ( N - M ) ) ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. ( 1 / ( M + k ) ) ) )
6 5 oveq2d 
 |-  ( ph -> ( ( _lcm ` ( 1 ... N ) ) x. F ) = ( ( _lcm ` ( 1 ... N ) ) x. sum_ k e. ( 0 ... ( N - M ) ) ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. ( 1 / ( M + k ) ) ) ) )
7 fzfid 
 |-  ( ph -> ( 0 ... ( N - M ) ) e. Fin )
8 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
9 fzfi 
 |-  ( 1 ... N ) e. Fin
10 8 9 pm3.2i 
 |-  ( ( 1 ... N ) C_ NN /\ ( 1 ... N ) e. Fin )
11 lcmfnncl 
 |-  ( ( ( 1 ... N ) C_ NN /\ ( 1 ... N ) e. Fin ) -> ( _lcm ` ( 1 ... N ) ) e. NN )
12 10 11 ax-mp 
 |-  ( _lcm ` ( 1 ... N ) ) e. NN
13 12 nncni 
 |-  ( _lcm ` ( 1 ... N ) ) e. CC
14 13 a1i 
 |-  ( ph -> ( _lcm ` ( 1 ... N ) ) e. CC )
15 elfzelz 
 |-  ( k e. ( 0 ... ( N - M ) ) -> k e. ZZ )
16 m1expcl 
 |-  ( k e. ZZ -> ( -u 1 ^ k ) e. ZZ )
17 15 16 syl 
 |-  ( k e. ( 0 ... ( N - M ) ) -> ( -u 1 ^ k ) e. ZZ )
18 17 zcnd 
 |-  ( k e. ( 0 ... ( N - M ) ) -> ( -u 1 ^ k ) e. CC )
19 18 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( -u 1 ^ k ) e. CC )
20 bccl2 
 |-  ( k e. ( 0 ... ( N - M ) ) -> ( ( N - M ) _C k ) e. NN )
21 20 nncnd 
 |-  ( k e. ( 0 ... ( N - M ) ) -> ( ( N - M ) _C k ) e. CC )
22 21 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( ( N - M ) _C k ) e. CC )
23 19 22 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) e. CC )
24 3 nncnd 
 |-  ( ph -> M e. CC )
25 24 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> M e. CC )
26 15 zcnd 
 |-  ( k e. ( 0 ... ( N - M ) ) -> k e. CC )
27 26 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> k e. CC )
28 25 27 addcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( M + k ) e. CC )
29 elfznn0 
 |-  ( k e. ( 0 ... ( N - M ) ) -> k e. NN0 )
30 nnnn0addcl 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( M + k ) e. NN )
31 29 30 sylan2 
 |-  ( ( M e. NN /\ k e. ( 0 ... ( N - M ) ) ) -> ( M + k ) e. NN )
32 3 31 sylan 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( M + k ) e. NN )
33 32 nnne0d 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( M + k ) =/= 0 )
34 28 33 reccld 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( 1 / ( M + k ) ) e. CC )
35 23 34 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. ( 1 / ( M + k ) ) ) e. CC )
36 7 14 35 fsummulc2 
 |-  ( ph -> ( ( _lcm ` ( 1 ... N ) ) x. sum_ k e. ( 0 ... ( N - M ) ) ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. ( 1 / ( M + k ) ) ) ) = sum_ k e. ( 0 ... ( N - M ) ) ( ( _lcm ` ( 1 ... N ) ) x. ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. ( 1 / ( M + k ) ) ) ) )
37 6 36 eqtrd 
 |-  ( ph -> ( ( _lcm ` ( 1 ... N ) ) x. F ) = sum_ k e. ( 0 ... ( N - M ) ) ( ( _lcm ` ( 1 ... N ) ) x. ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. ( 1 / ( M + k ) ) ) ) )
38 13 a1i 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( _lcm ` ( 1 ... N ) ) e. CC )
39 38 23 28 33 lcmineqlem5 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( ( _lcm ` ( 1 ... N ) ) x. ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. ( 1 / ( M + k ) ) ) ) = ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. ( ( _lcm ` ( 1 ... N ) ) / ( M + k ) ) ) )
40 39 sumeq2dv 
 |-  ( ph -> sum_ k e. ( 0 ... ( N - M ) ) ( ( _lcm ` ( 1 ... N ) ) x. ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. ( 1 / ( M + k ) ) ) ) = sum_ k e. ( 0 ... ( N - M ) ) ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. ( ( _lcm ` ( 1 ... N ) ) / ( M + k ) ) ) )
41 37 40 eqtrd 
 |-  ( ph -> ( ( _lcm ` ( 1 ... N ) ) x. F ) = sum_ k e. ( 0 ... ( N - M ) ) ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. ( ( _lcm ` ( 1 ... N ) ) / ( M + k ) ) ) )
42 17 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( -u 1 ^ k ) e. ZZ )
43 20 nnzd 
 |-  ( k e. ( 0 ... ( N - M ) ) -> ( ( N - M ) _C k ) e. ZZ )
44 43 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( ( N - M ) _C k ) e. ZZ )
45 42 44 zmulcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) e. ZZ )
46 2 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> N e. NN )
47 3 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> M e. NN )
48 4 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> M <_ N )
49 simpr 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> k e. ( 0 ... ( N - M ) ) )
50 46 47 48 49 lcmineqlem4 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( ( _lcm ` ( 1 ... N ) ) / ( M + k ) ) e. ZZ )
51 45 50 zmulcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N - M ) ) ) -> ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. ( ( _lcm ` ( 1 ... N ) ) / ( M + k ) ) ) e. ZZ )
52 7 51 fsumzcl 
 |-  ( ph -> sum_ k e. ( 0 ... ( N - M ) ) ( ( ( -u 1 ^ k ) x. ( ( N - M ) _C k ) ) x. ( ( _lcm ` ( 1 ... N ) ) / ( M + k ) ) ) e. ZZ )
53 41 52 eqeltrd 
 |-  ( ph -> ( ( _lcm ` ( 1 ... N ) ) x. F ) e. ZZ )