Metamath Proof Explorer

Theorem lcmineqlem16

Description: Technical divisibility lemma. (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypotheses lcmineqlem16.1 
|- ( ph -> M e. NN )
lcmineqlem16.2 
|- ( ph -> N e. NN )
lcmineqlem16.3 
|- ( ph -> M <_ N )
Assertion lcmineqlem16 
|- ( ph -> ( M x. ( N _C M ) ) || ( _lcm ` ( 1 ... N ) ) )

Proof

Step Hyp Ref Expression
1 lcmineqlem16.1 
 |-  ( ph -> M e. NN )
2 lcmineqlem16.2 
 |-  ( ph -> N e. NN )
3 lcmineqlem16.3 
 |-  ( ph -> M <_ N )
4 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
5 fzfi 
 |-  ( 1 ... N ) e. Fin
6 lcmfnncl 
 |-  ( ( ( 1 ... N ) C_ NN /\ ( 1 ... N ) e. Fin ) -> ( _lcm ` ( 1 ... N ) ) e. NN )
7 4 5 6 mp2an 
 |-  ( _lcm ` ( 1 ... N ) ) e. NN
8 7 a1i 
 |-  ( ph -> ( _lcm ` ( 1 ... N ) ) e. NN )
9 8 nncnd 
 |-  ( ph -> ( _lcm ` ( 1 ... N ) ) e. CC )
10 1 nncnd 
 |-  ( ph -> M e. CC )
11 1 nnnn0d 
 |-  ( ph -> M e. NN0 )
12 2 11 3 bccl2d 
 |-  ( ph -> ( N _C M ) e. NN )
13 12 nncnd 
 |-  ( ph -> ( N _C M ) e. CC )
14 10 13 mulcld 
 |-  ( ph -> ( M x. ( N _C M ) ) e. CC )
15 1 nnne0d 
 |-  ( ph -> M =/= 0 )
16 12 nnne0d 
 |-  ( ph -> ( N _C M ) =/= 0 )
17 10 13 15 16 mulne0d 
 |-  ( ph -> ( M x. ( N _C M ) ) =/= 0 )
18 9 14 17 divrecd 
 |-  ( ph -> ( ( _lcm ` ( 1 ... N ) ) / ( M x. ( N _C M ) ) ) = ( ( _lcm ` ( 1 ... N ) ) x. ( 1 / ( M x. ( N _C M ) ) ) ) )
19 eqid 
 |-  S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( ( 1 - x ) ^ ( N - M ) ) ) _d x = S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( ( 1 - x ) ^ ( N - M ) ) ) _d x
20 19 1 2 3 lcmineqlem13 
 |-  ( ph -> S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( ( 1 - x ) ^ ( N - M ) ) ) _d x = ( 1 / ( M x. ( N _C M ) ) ) )
21 20 oveq2d 
 |-  ( ph -> ( ( _lcm ` ( 1 ... N ) ) x. S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( ( 1 - x ) ^ ( N - M ) ) ) _d x ) = ( ( _lcm ` ( 1 ... N ) ) x. ( 1 / ( M x. ( N _C M ) ) ) ) )
22 19 2 1 3 lcmineqlem15 
 |-  ( ph -> ( ( _lcm ` ( 1 ... N ) ) x. S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( ( 1 - x ) ^ ( N - M ) ) ) _d x ) e. NN )
23 21 22 eqeltrrd 
 |-  ( ph -> ( ( _lcm ` ( 1 ... N ) ) x. ( 1 / ( M x. ( N _C M ) ) ) ) e. NN )
24 18 23 eqeltrd 
 |-  ( ph -> ( ( _lcm ` ( 1 ... N ) ) / ( M x. ( N _C M ) ) ) e. NN )
25 1 12 nnmulcld 
 |-  ( ph -> ( M x. ( N _C M ) ) e. NN )
26 25 8 nndivdvdsd 
 |-  ( ph -> ( ( M x. ( N _C M ) ) || ( _lcm ` ( 1 ... N ) ) <-> ( ( _lcm ` ( 1 ... N ) ) / ( M x. ( N _C M ) ) ) e. NN ) )
27 24 26 mpbird 
 |-  ( ph -> ( M x. ( N _C M ) ) || ( _lcm ` ( 1 ... N ) ) )