Metamath Proof Explorer

Theorem lcmineqlem22

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

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

Proof

Step Hyp Ref Expression
1 lcmineqlem22.1 
 |-  ( ph -> N e. NN )
2 lcmineqlem22.2 
 |-  ( ph -> 4 <_ N )
3 2re 
 |-  2 e. RR
4 3 a1i 
 |-  ( ph -> 2 e. RR )
5 2nn0 
 |-  2 e. NN0
6 5 a1i 
 |-  ( ph -> 2 e. NN0 )
7 1 nnnn0d 
 |-  ( ph -> N e. NN0 )
8 6 7 nn0mulcld 
 |-  ( ph -> ( 2 x. N ) e. NN0 )
9 1nn0 
 |-  1 e. NN0
10 9 a1i 
 |-  ( ph -> 1 e. NN0 )
11 8 10 nn0addcld 
 |-  ( ph -> ( ( 2 x. N ) + 1 ) e. NN0 )
12 4 11 reexpcld 
 |-  ( ph -> ( 2 ^ ( ( 2 x. N ) + 1 ) ) e. RR )
13 8 6 nn0addcld 
 |-  ( ph -> ( ( 2 x. N ) + 2 ) e. NN0 )
14 4 13 reexpcld 
 |-  ( ph -> ( 2 ^ ( ( 2 x. N ) + 2 ) ) e. RR )
15 fz1ssnn 
 |-  ( 1 ... ( ( 2 x. N ) + 1 ) ) C_ NN
16 fzfi 
 |-  ( 1 ... ( ( 2 x. N ) + 1 ) ) e. Fin
17 lcmfnncl 
 |-  ( ( ( 1 ... ( ( 2 x. N ) + 1 ) ) C_ NN /\ ( 1 ... ( ( 2 x. N ) + 1 ) ) e. Fin ) -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) e. NN )
18 15 16 17 mp2an 
 |-  ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) e. NN
19 18 a1i 
 |-  ( ph -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) e. NN )
20 19 nnred 
 |-  ( ph -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) e. RR )
21 1red 
 |-  ( ph -> 1 e. RR )
22 1 nnred 
 |-  ( ph -> N e. RR )
23 4 22 remulcld 
 |-  ( ph -> ( 2 x. N ) e. RR )
24 1lt2 
 |-  1 < 2
25 24 a1i 
 |-  ( ph -> 1 < 2 )
26 21 4 25 ltled 
 |-  ( ph -> 1 <_ 2 )
27 21 4 23 26 leadd2dd 
 |-  ( ph -> ( ( 2 x. N ) + 1 ) <_ ( ( 2 x. N ) + 2 ) )
28 2z 
 |-  2 e. ZZ
29 28 a1i 
 |-  ( ph -> 2 e. ZZ )
30 1 nnzd 
 |-  ( ph -> N e. ZZ )
31 29 30 zmulcld 
 |-  ( ph -> ( 2 x. N ) e. ZZ )
32 31 peano2zd 
 |-  ( ph -> ( ( 2 x. N ) + 1 ) e. ZZ )
33 31 29 zaddcld 
 |-  ( ph -> ( ( 2 x. N ) + 2 ) e. ZZ )
34 4 32 33 25 leexp2d 
 |-  ( ph -> ( ( ( 2 x. N ) + 1 ) <_ ( ( 2 x. N ) + 2 ) <-> ( 2 ^ ( ( 2 x. N ) + 1 ) ) <_ ( 2 ^ ( ( 2 x. N ) + 2 ) ) ) )
35 27 34 mpbid 
 |-  ( ph -> ( 2 ^ ( ( 2 x. N ) + 1 ) ) <_ ( 2 ^ ( ( 2 x. N ) + 2 ) ) )
36 1 2 lcmineqlem21 
 |-  ( ph -> ( 2 ^ ( ( 2 x. N ) + 2 ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) )
37 12 14 20 35 36 letrd 
 |-  ( ph -> ( 2 ^ ( ( 2 x. N ) + 1 ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) )
38 fz1ssnn 
 |-  ( 1 ... ( ( 2 x. N ) + 2 ) ) C_ NN
39 fzfi 
 |-  ( 1 ... ( ( 2 x. N ) + 2 ) ) e. Fin
40 lcmfnncl 
 |-  ( ( ( 1 ... ( ( 2 x. N ) + 2 ) ) C_ NN /\ ( 1 ... ( ( 2 x. N ) + 2 ) ) e. Fin ) -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 2 ) ) ) e. NN )
41 38 39 40 mp2an 
 |-  ( _lcm ` ( 1 ... ( ( 2 x. N ) + 2 ) ) ) e. NN
42 41 a1i 
 |-  ( ph -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 2 ) ) ) e. NN )
43 42 nnred 
 |-  ( ph -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 2 ) ) ) e. RR )
44 19 nnzd 
 |-  ( ph -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) e. ZZ )
45 44 33 jca 
 |-  ( ph -> ( ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) e. ZZ /\ ( ( 2 x. N ) + 2 ) e. ZZ ) )
46 dvdslcm 
 |-  ( ( ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) e. ZZ /\ ( ( 2 x. N ) + 2 ) e. ZZ ) -> ( ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) || ( ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) lcm ( ( 2 x. N ) + 2 ) ) /\ ( ( 2 x. N ) + 2 ) || ( ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) lcm ( ( 2 x. N ) + 2 ) ) ) )
47 45 46 syl 
 |-  ( ph -> ( ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) || ( ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) lcm ( ( 2 x. N ) + 2 ) ) /\ ( ( 2 x. N ) + 2 ) || ( ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) lcm ( ( 2 x. N ) + 2 ) ) ) )
48 47 simpld 
 |-  ( ph -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) || ( ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) lcm ( ( 2 x. N ) + 2 ) ) )
49 2nn 
 |-  2 e. NN
50 49 a1i 
 |-  ( ph -> 2 e. NN )
51 50 1 nnmulcld 
 |-  ( ph -> ( 2 x. N ) e. NN )
52 51 50 nnaddcld 
 |-  ( ph -> ( ( 2 x. N ) + 2 ) e. NN )
53 52 lcmfunnnd 
 |-  ( ph -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 2 ) ) ) = ( ( _lcm ` ( 1 ... ( ( ( 2 x. N ) + 2 ) - 1 ) ) ) lcm ( ( 2 x. N ) + 2 ) ) )
54 23 recnd 
 |-  ( ph -> ( 2 x. N ) e. CC )
55 4 recnd 
 |-  ( ph -> 2 e. CC )
56 1cnd 
 |-  ( ph -> 1 e. CC )
57 54 55 56 addsubassd 
 |-  ( ph -> ( ( ( 2 x. N ) + 2 ) - 1 ) = ( ( 2 x. N ) + ( 2 - 1 ) ) )
58 2m1e1 
 |-  ( 2 - 1 ) = 1
59 58 oveq2i 
 |-  ( ( 2 x. N ) + ( 2 - 1 ) ) = ( ( 2 x. N ) + 1 )
60 57 59 eqtrdi 
 |-  ( ph -> ( ( ( 2 x. N ) + 2 ) - 1 ) = ( ( 2 x. N ) + 1 ) )
61 60 oveq2d 
 |-  ( ph -> ( 1 ... ( ( ( 2 x. N ) + 2 ) - 1 ) ) = ( 1 ... ( ( 2 x. N ) + 1 ) ) )
62 61 fveq2d 
 |-  ( ph -> ( _lcm ` ( 1 ... ( ( ( 2 x. N ) + 2 ) - 1 ) ) ) = ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) )
63 62 oveq1d 
 |-  ( ph -> ( ( _lcm ` ( 1 ... ( ( ( 2 x. N ) + 2 ) - 1 ) ) ) lcm ( ( 2 x. N ) + 2 ) ) = ( ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) lcm ( ( 2 x. N ) + 2 ) ) )
64 53 63 eqtrd 
 |-  ( ph -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 2 ) ) ) = ( ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) lcm ( ( 2 x. N ) + 2 ) ) )
65 48 64 breqtrrd 
 |-  ( ph -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) || ( _lcm ` ( 1 ... ( ( 2 x. N ) + 2 ) ) ) )
66 44 42 jca 
 |-  ( ph -> ( ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) e. ZZ /\ ( _lcm ` ( 1 ... ( ( 2 x. N ) + 2 ) ) ) e. NN ) )
67 dvdsle 
 |-  ( ( ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) e. ZZ /\ ( _lcm ` ( 1 ... ( ( 2 x. N ) + 2 ) ) ) e. NN ) -> ( ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) || ( _lcm ` ( 1 ... ( ( 2 x. N ) + 2 ) ) ) -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. N ) + 2 ) ) ) ) )
68 66 67 syl 
 |-  ( ph -> ( ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) || ( _lcm ` ( 1 ... ( ( 2 x. N ) + 2 ) ) ) -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. N ) + 2 ) ) ) ) )
69 65 68 mpd 
 |-  ( ph -> ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. N ) + 2 ) ) ) )
70 14 20 43 36 69 letrd 
 |-  ( ph -> ( 2 ^ ( ( 2 x. N ) + 2 ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. N ) + 2 ) ) ) )
71 37 70 jca 
 |-  ( ph -> ( ( 2 ^ ( ( 2 x. N ) + 1 ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. N ) + 1 ) ) ) /\ ( 2 ^ ( ( 2 x. N ) + 2 ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. N ) + 2 ) ) ) ) )