Metamath Proof Explorer

Theorem lcmineqlem20

Description: Inequality for lcm lemma. (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypothesis lcmineqlem20.1 
|- ( ph -> N e. NN )
Assertion lcmineqlem20 
|- ( ph -> ( N x. ( 2 ^ ( 2 x. N ) ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 lcmineqlem20.1 
 |-  ( ph -> N e. NN )
2 1 nnred 
 |-  ( ph -> N e. RR )
3 2nn0 
 |-  2 e. NN0
4 3 a1i 
 |-  ( ph -> 2 e. NN0 )
5 1 nnnn0d 
 |-  ( ph -> N e. NN0 )
6 4 5 nn0mulcld 
 |-  ( ph -> ( 2 x. N ) e. NN0 )
7 2re 
 |-  2 e. RR
8 reexpcl 
 |-  ( ( 2 e. RR /\ ( 2 x. N ) e. NN0 ) -> ( 2 ^ ( 2 x. N ) ) e. RR )
9 7 8 mpan 
 |-  ( ( 2 x. N ) e. NN0 -> ( 2 ^ ( 2 x. N ) ) e. RR )
10 6 9 syl 
 |-  ( ph -> ( 2 ^ ( 2 x. N ) ) e. RR )
11 2 10 remulcld 
 |-  ( ph -> ( N x. ( 2 ^ ( 2 x. N ) ) ) e. RR )
12 7 a1i 
 |-  ( ph -> 2 e. RR )
13 12 2 remulcld 
 |-  ( ph -> ( 2 x. N ) e. RR )
14 1red 
 |-  ( ph -> 1 e. RR )
15 13 14 readdcld 
 |-  ( ph -> ( ( 2 x. N ) + 1 ) e. RR )
16 2nn 
 |-  2 e. NN
17 16 a1i 
 |-  ( ph -> 2 e. NN )
18 17 1 nnmulcld 
 |-  ( ph -> ( 2 x. N ) e. NN )
19 5 nn0ge0d 
 |-  ( ph -> 0 <_ N )
20 17 nnge1d 
 |-  ( ph -> 1 <_ 2 )
21 2 12 19 20 lemulge12d 
 |-  ( ph -> N <_ ( 2 x. N ) )
22 18 5 21 bccl2d 
 |-  ( ph -> ( ( 2 x. N ) _C N ) e. NN )
23 22 nnred 
 |-  ( ph -> ( ( 2 x. N ) _C N ) e. RR )
24 15 23 remulcld 
 |-  ( ph -> ( ( ( 2 x. N ) + 1 ) x. ( ( 2 x. N ) _C N ) ) e. RR )
25 2 24 remulcld 
 |-  ( ph -> ( N x. ( ( ( 2 x. N ) + 1 ) x. ( ( 2 x. N ) _C N ) ) ) e. RR )
26 fz1ssnn 
 |-  ( 1 ... ( ( 2 x. N ) + 1 ) ) C_ NN
27 fzfi 
 |-  ( 1 ... ( ( 2 x. N ) + 1 ) ) e. Fin
28 lcmfnncl 
 |-  ( ( ( 1 ... ( ( 2 x. N ) + 1 ) ) C_ NN /\ ( 1 ... ( ( 2 x. N ) + 1 ) ) e. Fin ) -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) e. NN )
29 26 27 28 mp2an 
 |-  ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) e. NN
30 29 a1i 
 |-  ( ph -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) e. NN )
31 30 nnred 
 |-  ( ph -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) e. RR )
32 5 lcmineqlem17 
 |-  ( ph -> ( 2 ^ ( 2 x. N ) ) <_ ( ( ( 2 x. N ) + 1 ) x. ( ( 2 x. N ) _C N ) ) )
33 1 nnrpd 
 |-  ( ph -> N e. RR+ )
34 10 24 33 lemul2d 
 |-  ( ph -> ( ( 2 ^ ( 2 x. N ) ) <_ ( ( ( 2 x. N ) + 1 ) x. ( ( 2 x. N ) _C N ) ) <-> ( N x. ( 2 ^ ( 2 x. N ) ) ) <_ ( N x. ( ( ( 2 x. N ) + 1 ) x. ( ( 2 x. N ) _C N ) ) ) ) )
35 32 34 mpbid 
 |-  ( ph -> ( N x. ( 2 ^ ( 2 x. N ) ) ) <_ ( N x. ( ( ( 2 x. N ) + 1 ) x. ( ( 2 x. N ) _C N ) ) ) )
36 2 recnd 
 |-  ( ph -> N e. CC )
37 15 recnd 
 |-  ( ph -> ( ( 2 x. N ) + 1 ) e. CC )
38 23 recnd 
 |-  ( ph -> ( ( 2 x. N ) _C N ) e. CC )
39 36 37 38 mulassd 
 |-  ( ph -> ( ( N x. ( ( 2 x. N ) + 1 ) ) x. ( ( 2 x. N ) _C N ) ) = ( N x. ( ( ( 2 x. N ) + 1 ) x. ( ( 2 x. N ) _C N ) ) ) )
40 1 lcmineqlem19 
 |-  ( ph -> ( ( N x. ( ( 2 x. N ) + 1 ) ) x. ( ( 2 x. N ) _C N ) ) || ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) )
41 18 peano2nnd 
 |-  ( ph -> ( ( 2 x. N ) + 1 ) e. NN )
42 1 41 nnmulcld 
 |-  ( ph -> ( N x. ( ( 2 x. N ) + 1 ) ) e. NN )
43 42 22 nnmulcld 
 |-  ( ph -> ( ( N x. ( ( 2 x. N ) + 1 ) ) x. ( ( 2 x. N ) _C N ) ) e. NN )
44 43 nnzd 
 |-  ( ph -> ( ( N x. ( ( 2 x. N ) + 1 ) ) x. ( ( 2 x. N ) _C N ) ) e. ZZ )
45 dvdsle 
 |-  ( ( ( ( N x. ( ( 2 x. N ) + 1 ) ) x. ( ( 2 x. N ) _C N ) ) e. ZZ /\ ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) e. NN ) -> ( ( ( N x. ( ( 2 x. N ) + 1 ) ) x. ( ( 2 x. N ) _C N ) ) || ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) -> ( ( N x. ( ( 2 x. N ) + 1 ) ) x. ( ( 2 x. N ) _C N ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) ) )
46 44 30 45 syl2anc 
 |-  ( ph -> ( ( ( N x. ( ( 2 x. N ) + 1 ) ) x. ( ( 2 x. N ) _C N ) ) || ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) -> ( ( N x. ( ( 2 x. N ) + 1 ) ) x. ( ( 2 x. N ) _C N ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) ) )
47 40 46 mpd 
 |-  ( ph -> ( ( N x. ( ( 2 x. N ) + 1 ) ) x. ( ( 2 x. N ) _C N ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) )
48 39 47 eqbrtrrd 
 |-  ( ph -> ( N x. ( ( ( 2 x. N ) + 1 ) x. ( ( 2 x. N ) _C N ) ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) )
49 11 25 31 35 48 letrd 
 |-  ( ph -> ( N x. ( 2 ^ ( 2 x. N ) ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) )