Metamath Proof Explorer

Theorem lcmineqlem21

Description: The lcm inequality lemma without base cases 7 and 8. (Contributed by metakunt, 12-May-2024)

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

Proof

Step Hyp Ref Expression
1 lcmineqlem21.1 
 |-  ( ph -> N e. NN )
2 lcmineqlem21.2 
 |-  ( ph -> 4 <_ N )
3 2nn0 
 |-  2 e. NN0
4 3 a1i 
 |-  ( ph -> 2 e. NN0 )
5 4 nn0red 
 |-  ( ph -> 2 e. RR )
6 1 nnnn0d 
 |-  ( ph -> N e. NN0 )
7 4 6 nn0mulcld 
 |-  ( ph -> ( 2 x. N ) e. NN0 )
8 7 4 nn0addcld 
 |-  ( ph -> ( ( 2 x. N ) + 2 ) e. NN0 )
9 5 8 reexpcld 
 |-  ( ph -> ( 2 ^ ( ( 2 x. N ) + 2 ) ) e. RR )
10 1 nnred 
 |-  ( ph -> N e. RR )
11 2rp 
 |-  2 e. RR+
12 11 a1i 
 |-  ( ph -> 2 e. RR+ )
13 2z 
 |-  2 e. ZZ
14 13 a1i 
 |-  ( ph -> 2 e. ZZ )
15 1 nnzd 
 |-  ( ph -> N e. ZZ )
16 14 15 zmulcld 
 |-  ( ph -> ( 2 x. N ) e. ZZ )
17 12 16 rpexpcld 
 |-  ( ph -> ( 2 ^ ( 2 x. N ) ) e. RR+ )
18 17 rpred 
 |-  ( ph -> ( 2 ^ ( 2 x. N ) ) e. RR )
19 10 18 remulcld 
 |-  ( ph -> ( N x. ( 2 ^ ( 2 x. N ) ) ) e. RR )
20 fz1ssnn 
 |-  ( 1 ... ( ( 2 x. N ) + 1 ) ) C_ NN
21 fzfi 
 |-  ( 1 ... ( ( 2 x. N ) + 1 ) ) e. Fin
22 lcmfnncl 
 |-  ( ( ( 1 ... ( ( 2 x. N ) + 1 ) ) C_ NN /\ ( 1 ... ( ( 2 x. N ) + 1 ) ) e. Fin ) -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) e. NN )
23 20 21 22 mp2an 
 |-  ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) e. NN
24 23 a1i 
 |-  ( ph -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) e. NN )
25 24 nnred 
 |-  ( ph -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) e. RR )
26 4re 
 |-  4 e. RR
27 26 a1i 
 |-  ( ph -> 4 e. RR )
28 27 10 17 lemul1d 
 |-  ( ph -> ( 4 <_ N <-> ( 4 x. ( 2 ^ ( 2 x. N ) ) ) <_ ( N x. ( 2 ^ ( 2 x. N ) ) ) ) )
29 2 28 mpbid 
 |-  ( ph -> ( 4 x. ( 2 ^ ( 2 x. N ) ) ) <_ ( N x. ( 2 ^ ( 2 x. N ) ) ) )
30 2cnd 
 |-  ( ph -> 2 e. CC )
31 30 4 7 expaddd 
 |-  ( ph -> ( 2 ^ ( ( 2 x. N ) + 2 ) ) = ( ( 2 ^ ( 2 x. N ) ) x. ( 2 ^ 2 ) ) )
32 sq2 
 |-  ( 2 ^ 2 ) = 4
33 32 oveq2i 
 |-  ( ( 2 ^ ( 2 x. N ) ) x. ( 2 ^ 2 ) ) = ( ( 2 ^ ( 2 x. N ) ) x. 4 )
34 31 33 eqtrdi 
 |-  ( ph -> ( 2 ^ ( ( 2 x. N ) + 2 ) ) = ( ( 2 ^ ( 2 x. N ) ) x. 4 ) )
35 17 rpcnd 
 |-  ( ph -> ( 2 ^ ( 2 x. N ) ) e. CC )
36 27 recnd 
 |-  ( ph -> 4 e. CC )
37 35 36 mulcomd 
 |-  ( ph -> ( ( 2 ^ ( 2 x. N ) ) x. 4 ) = ( 4 x. ( 2 ^ ( 2 x. N ) ) ) )
38 34 37 eqtrd 
 |-  ( ph -> ( 2 ^ ( ( 2 x. N ) + 2 ) ) = ( 4 x. ( 2 ^ ( 2 x. N ) ) ) )
39 38 breq1d 
 |-  ( ph -> ( ( 2 ^ ( ( 2 x. N ) + 2 ) ) <_ ( N x. ( 2 ^ ( 2 x. N ) ) ) <-> ( 4 x. ( 2 ^ ( 2 x. N ) ) ) <_ ( N x. ( 2 ^ ( 2 x. N ) ) ) ) )
40 29 39 mpbird 
 |-  ( ph -> ( 2 ^ ( ( 2 x. N ) + 2 ) ) <_ ( N x. ( 2 ^ ( 2 x. N ) ) ) )
41 1 lcmineqlem20 
 |-  ( ph -> ( N x. ( 2 ^ ( 2 x. N ) ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) )
42 9 19 25 40 41 letrd 
 |-  ( ph -> ( 2 ^ ( ( 2 x. N ) + 2 ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) )