Metamath Proof Explorer

Theorem lcmineqlem23

Description: Penultimate step to the lcm inequality lemma. (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypotheses lcmineqlem23.1 
|- ( ph -> N e. NN )
lcmineqlem23.2 
|- ( ph -> 9 <_ N )
Assertion lcmineqlem23 
|- ( ph -> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) )

Proof

Step Hyp Ref Expression
1 lcmineqlem23.1 
 |-  ( ph -> N e. NN )
2 lcmineqlem23.2 
 |-  ( ph -> 9 <_ N )
3 2nn 
 |-  2 e. NN
4 3 a1i 
 |-  ( ph -> 2 e. NN )
5 1 4 jca 
 |-  ( ph -> ( N e. NN /\ 2 e. NN ) )
6 nndivdvds 
 |-  ( ( N e. NN /\ 2 e. NN ) -> ( 2 || N <-> ( N / 2 ) e. NN ) )
7 5 6 syl 
 |-  ( ph -> ( 2 || N <-> ( N / 2 ) e. NN ) )
8 7 biimpa 
 |-  ( ( ph /\ 2 || N ) -> ( N / 2 ) e. NN )
9 8 nnzd 
 |-  ( ( ph /\ 2 || N ) -> ( N / 2 ) e. ZZ )
10 1zzd 
 |-  ( ( ph /\ 2 || N ) -> 1 e. ZZ )
11 9 10 zsubcld 
 |-  ( ( ph /\ 2 || N ) -> ( ( N / 2 ) - 1 ) e. ZZ )
12 0red 
 |-  ( ( ph /\ 2 || N ) -> 0 e. RR )
13 4re 
 |-  4 e. RR
14 13 a1i 
 |-  ( ( ph /\ 2 || N ) -> 4 e. RR )
15 8 nnred 
 |-  ( ( ph /\ 2 || N ) -> ( N / 2 ) e. RR )
16 1red 
 |-  ( ( ph /\ 2 || N ) -> 1 e. RR )
17 15 16 resubcld 
 |-  ( ( ph /\ 2 || N ) -> ( ( N / 2 ) - 1 ) e. RR )
18 4pos 
 |-  0 < 4
19 18 a1i 
 |-  ( ( ph /\ 2 || N ) -> 0 < 4 )
20 5m1e4 
 |-  ( 5 - 1 ) = 4
21 5re 
 |-  5 e. RR
22 21 a1i 
 |-  ( ( ph /\ 2 || N ) -> 5 e. RR )
23 3 nncni 
 |-  2 e. CC
24 5cn 
 |-  5 e. CC
25 23 24 mulcomi 
 |-  ( 2 x. 5 ) = ( 5 x. 2 )
26 5t2e10 
 |-  ( 5 x. 2 ) = ; 1 0
27 25 26 eqtri 
 |-  ( 2 x. 5 ) = ; 1 0
28 10re 
 |-  ; 1 0 e. RR
29 28 recni 
 |-  ; 1 0 e. CC
30 3 nnne0i 
 |-  2 =/= 0
31 29 23 24 30 divmuli 
 |-  ( ( ; 1 0 / 2 ) = 5 <-> ( 2 x. 5 ) = ; 1 0 )
32 27 31 mpbir 
 |-  ( ; 1 0 / 2 ) = 5
33 28 a1i 
 |-  ( ( ph /\ 2 || N ) -> ; 1 0 e. RR )
34 1 nnred 
 |-  ( ph -> N e. RR )
35 34 adantr 
 |-  ( ( ph /\ 2 || N ) -> N e. RR )
36 2rp 
 |-  2 e. RR+
37 36 a1i 
 |-  ( ( ph /\ 2 || N ) -> 2 e. RR+ )
38 9p1e10 
 |-  ( 9 + 1 ) = ; 1 0
39 9re 
 |-  9 e. RR
40 39 a1i 
 |-  ( ph -> 9 e. RR )
41 40 34 leloed 
 |-  ( ph -> ( 9 <_ N <-> ( 9 < N \/ 9 = N ) ) )
42 2 41 mpbid 
 |-  ( ph -> ( 9 < N \/ 9 = N ) )
43 42 adantr 
 |-  ( ( ph /\ 2 || N ) -> ( 9 < N \/ 9 = N ) )
44 2t4e8 
 |-  ( 2 x. 4 ) = 8
45 8re 
 |-  8 e. RR
46 45 recni 
 |-  8 e. CC
47 4cn 
 |-  4 e. CC
48 46 23 47 30 divmuli 
 |-  ( ( 8 / 2 ) = 4 <-> ( 2 x. 4 ) = 8 )
49 44 48 mpbir 
 |-  ( 8 / 2 ) = 4
50 4nn 
 |-  4 e. NN
51 49 50 eqeltri 
 |-  ( 8 / 2 ) e. NN
52 8nn 
 |-  8 e. NN
53 nndivdvds 
 |-  ( ( 8 e. NN /\ 2 e. NN ) -> ( 2 || 8 <-> ( 8 / 2 ) e. NN ) )
54 52 3 53 mp2an 
 |-  ( 2 || 8 <-> ( 8 / 2 ) e. NN )
55 51 54 mpbir 
 |-  2 || 8
56 9m1e8 
 |-  ( 9 - 1 ) = 8
57 55 56 breqtrri 
 |-  2 || ( 9 - 1 )
58 9nn 
 |-  9 e. NN
59 58 nnzi 
 |-  9 e. ZZ
60 oddm1even 
 |-  ( 9 e. ZZ -> ( -. 2 || 9 <-> 2 || ( 9 - 1 ) ) )
61 59 60 ax-mp 
 |-  ( -. 2 || 9 <-> 2 || ( 9 - 1 ) )
62 57 61 mpbir 
 |-  -. 2 || 9
63 breq2 
 |-  ( 9 = N -> ( 2 || 9 <-> 2 || N ) )
64 62 63 mtbii 
 |-  ( 9 = N -> -. 2 || N )
65 64 con2i 
 |-  ( 2 || N -> -. 9 = N )
66 65 adantl 
 |-  ( ( ph /\ 2 || N ) -> -. 9 = N )
67 43 66 olcnd 
 |-  ( ( ph /\ 2 || N ) -> 9 < N )
68 1 nnzd 
 |-  ( ph -> N e. ZZ )
69 zltp1le 
 |-  ( ( 9 e. ZZ /\ N e. ZZ ) -> ( 9 < N <-> ( 9 + 1 ) <_ N ) )
70 59 69 mpan 
 |-  ( N e. ZZ -> ( 9 < N <-> ( 9 + 1 ) <_ N ) )
71 68 70 syl 
 |-  ( ph -> ( 9 < N <-> ( 9 + 1 ) <_ N ) )
72 71 adantr 
 |-  ( ( ph /\ 2 || N ) -> ( 9 < N <-> ( 9 + 1 ) <_ N ) )
73 67 72 mpbid 
 |-  ( ( ph /\ 2 || N ) -> ( 9 + 1 ) <_ N )
74 38 73 eqbrtrrid 
 |-  ( ( ph /\ 2 || N ) -> ; 1 0 <_ N )
75 33 35 37 74 lediv1dd 
 |-  ( ( ph /\ 2 || N ) -> ( ; 1 0 / 2 ) <_ ( N / 2 ) )
76 32 75 eqbrtrrid 
 |-  ( ( ph /\ 2 || N ) -> 5 <_ ( N / 2 ) )
77 22 15 16 76 lesub1dd 
 |-  ( ( ph /\ 2 || N ) -> ( 5 - 1 ) <_ ( ( N / 2 ) - 1 ) )
78 20 77 eqbrtrrid 
 |-  ( ( ph /\ 2 || N ) -> 4 <_ ( ( N / 2 ) - 1 ) )
79 12 14 17 19 78 ltletrd 
 |-  ( ( ph /\ 2 || N ) -> 0 < ( ( N / 2 ) - 1 ) )
80 11 79 jca 
 |-  ( ( ph /\ 2 || N ) -> ( ( ( N / 2 ) - 1 ) e. ZZ /\ 0 < ( ( N / 2 ) - 1 ) ) )
81 elnnz 
 |-  ( ( ( N / 2 ) - 1 ) e. NN <-> ( ( ( N / 2 ) - 1 ) e. ZZ /\ 0 < ( ( N / 2 ) - 1 ) ) )
82 80 81 sylibr 
 |-  ( ( ph /\ 2 || N ) -> ( ( N / 2 ) - 1 ) e. NN )
83 82 78 lcmineqlem22 
 |-  ( ( ph /\ 2 || N ) -> ( ( 2 ^ ( ( 2 x. ( ( N / 2 ) - 1 ) ) + 1 ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. ( ( N / 2 ) - 1 ) ) + 1 ) ) ) /\ ( 2 ^ ( ( 2 x. ( ( N / 2 ) - 1 ) ) + 2 ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. ( ( N / 2 ) - 1 ) ) + 2 ) ) ) ) )
84 83 simprd 
 |-  ( ( ph /\ 2 || N ) -> ( 2 ^ ( ( 2 x. ( ( N / 2 ) - 1 ) ) + 2 ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. ( ( N / 2 ) - 1 ) ) + 2 ) ) ) )
85 4 nncnd 
 |-  ( ph -> 2 e. CC )
86 1 nncnd 
 |-  ( ph -> N e. CC )
87 86 halfcld 
 |-  ( ph -> ( N / 2 ) e. CC )
88 85 87 muls1d 
 |-  ( ph -> ( 2 x. ( ( N / 2 ) - 1 ) ) = ( ( 2 x. ( N / 2 ) ) - 2 ) )
89 88 oveq1d 
 |-  ( ph -> ( ( 2 x. ( ( N / 2 ) - 1 ) ) + 2 ) = ( ( ( 2 x. ( N / 2 ) ) - 2 ) + 2 ) )
90 85 87 mulcld 
 |-  ( ph -> ( 2 x. ( N / 2 ) ) e. CC )
91 90 85 npcand 
 |-  ( ph -> ( ( ( 2 x. ( N / 2 ) ) - 2 ) + 2 ) = ( 2 x. ( N / 2 ) ) )
92 89 91 eqtrd 
 |-  ( ph -> ( ( 2 x. ( ( N / 2 ) - 1 ) ) + 2 ) = ( 2 x. ( N / 2 ) ) )
93 4 nnne0d 
 |-  ( ph -> 2 =/= 0 )
94 86 85 93 divcan2d 
 |-  ( ph -> ( 2 x. ( N / 2 ) ) = N )
95 92 94 eqtrd 
 |-  ( ph -> ( ( 2 x. ( ( N / 2 ) - 1 ) ) + 2 ) = N )
96 95 oveq2d 
 |-  ( ph -> ( 2 ^ ( ( 2 x. ( ( N / 2 ) - 1 ) ) + 2 ) ) = ( 2 ^ N ) )
97 95 oveq2d 
 |-  ( ph -> ( 1 ... ( ( 2 x. ( ( N / 2 ) - 1 ) ) + 2 ) ) = ( 1 ... N ) )
98 97 fveq2d 
 |-  ( ph -> ( _lcm ` ( 1 ... ( ( 2 x. ( ( N / 2 ) - 1 ) ) + 2 ) ) ) = ( _lcm ` ( 1 ... N ) ) )
99 96 98 breq12d 
 |-  ( ph -> ( ( 2 ^ ( ( 2 x. ( ( N / 2 ) - 1 ) ) + 2 ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. ( ( N / 2 ) - 1 ) ) + 2 ) ) ) <-> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) ) )
100 99 adantr 
 |-  ( ( ph /\ 2 || N ) -> ( ( 2 ^ ( ( 2 x. ( ( N / 2 ) - 1 ) ) + 2 ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. ( ( N / 2 ) - 1 ) ) + 2 ) ) ) <-> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) ) )
101 84 100 mpbid 
 |-  ( ( ph /\ 2 || N ) -> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) )
102 oddm1even 
 |-  ( N e. ZZ -> ( -. 2 || N <-> 2 || ( N - 1 ) ) )
103 68 102 syl 
 |-  ( ph -> ( -. 2 || N <-> 2 || ( N - 1 ) ) )
104 103 biimpa 
 |-  ( ( ph /\ -. 2 || N ) -> 2 || ( N - 1 ) )
105 3 a1i 
 |-  ( ( ph /\ -. 2 || N ) -> 2 e. NN )
106 1zzd 
 |-  ( ph -> 1 e. ZZ )
107 68 106 zsubcld 
 |-  ( ph -> ( N - 1 ) e. ZZ )
108 0red 
 |-  ( ph -> 0 e. RR )
109 45 a1i 
 |-  ( ph -> 8 e. RR )
110 1red 
 |-  ( ph -> 1 e. RR )
111 34 110 resubcld 
 |-  ( ph -> ( N - 1 ) e. RR )
112 8pos 
 |-  0 < 8
113 112 a1i 
 |-  ( ph -> 0 < 8 )
114 40 34 110 2 lesub1dd 
 |-  ( ph -> ( 9 - 1 ) <_ ( N - 1 ) )
115 56 114 eqbrtrrid 
 |-  ( ph -> 8 <_ ( N - 1 ) )
116 108 109 111 113 115 ltletrd 
 |-  ( ph -> 0 < ( N - 1 ) )
117 107 116 jca 
 |-  ( ph -> ( ( N - 1 ) e. ZZ /\ 0 < ( N - 1 ) ) )
118 elnnz 
 |-  ( ( N - 1 ) e. NN <-> ( ( N - 1 ) e. ZZ /\ 0 < ( N - 1 ) ) )
119 117 118 sylibr 
 |-  ( ph -> ( N - 1 ) e. NN )
120 119 adantr 
 |-  ( ( ph /\ -. 2 || N ) -> ( N - 1 ) e. NN )
121 105 120 nndivdvdsd 
 |-  ( ( ph /\ -. 2 || N ) -> ( 2 || ( N - 1 ) <-> ( ( N - 1 ) / 2 ) e. NN ) )
122 104 121 mpbid 
 |-  ( ( ph /\ -. 2 || N ) -> ( ( N - 1 ) / 2 ) e. NN )
123 4 nnrpd 
 |-  ( ph -> 2 e. RR+ )
124 109 111 123 115 lediv1dd 
 |-  ( ph -> ( 8 / 2 ) <_ ( ( N - 1 ) / 2 ) )
125 49 124 eqbrtrrid 
 |-  ( ph -> 4 <_ ( ( N - 1 ) / 2 ) )
126 125 adantr 
 |-  ( ( ph /\ -. 2 || N ) -> 4 <_ ( ( N - 1 ) / 2 ) )
127 122 126 lcmineqlem22 
 |-  ( ( ph /\ -. 2 || N ) -> ( ( 2 ^ ( ( 2 x. ( ( N - 1 ) / 2 ) ) + 1 ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. ( ( N - 1 ) / 2 ) ) + 1 ) ) ) /\ ( 2 ^ ( ( 2 x. ( ( N - 1 ) / 2 ) ) + 2 ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. ( ( N - 1 ) / 2 ) ) + 2 ) ) ) ) )
128 127 simpld 
 |-  ( ( ph /\ -. 2 || N ) -> ( 2 ^ ( ( 2 x. ( ( N - 1 ) / 2 ) ) + 1 ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. ( ( N - 1 ) / 2 ) ) + 1 ) ) ) )
129 1cnd 
 |-  ( ph -> 1 e. CC )
130 86 129 subcld 
 |-  ( ph -> ( N - 1 ) e. CC )
131 130 85 93 divcan2d 
 |-  ( ph -> ( 2 x. ( ( N - 1 ) / 2 ) ) = ( N - 1 ) )
132 131 oveq1d 
 |-  ( ph -> ( ( 2 x. ( ( N - 1 ) / 2 ) ) + 1 ) = ( ( N - 1 ) + 1 ) )
133 86 129 npcand 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
134 132 133 eqtrd 
 |-  ( ph -> ( ( 2 x. ( ( N - 1 ) / 2 ) ) + 1 ) = N )
135 134 oveq2d 
 |-  ( ph -> ( 2 ^ ( ( 2 x. ( ( N - 1 ) / 2 ) ) + 1 ) ) = ( 2 ^ N ) )
136 134 oveq2d 
 |-  ( ph -> ( 1 ... ( ( 2 x. ( ( N - 1 ) / 2 ) ) + 1 ) ) = ( 1 ... N ) )
137 136 fveq2d 
 |-  ( ph -> ( _lcm ` ( 1 ... ( ( 2 x. ( ( N - 1 ) / 2 ) ) + 1 ) ) ) = ( _lcm ` ( 1 ... N ) ) )
138 135 137 breq12d 
 |-  ( ph -> ( ( 2 ^ ( ( 2 x. ( ( N - 1 ) / 2 ) ) + 1 ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. ( ( N - 1 ) / 2 ) ) + 1 ) ) ) <-> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) ) )
139 138 adantr 
 |-  ( ( ph /\ -. 2 || N ) -> ( ( 2 ^ ( ( 2 x. ( ( N - 1 ) / 2 ) ) + 1 ) ) <_ ( _lcm ` ( 1 ... ( ( 2 x. ( ( N - 1 ) / 2 ) ) + 1 ) ) ) <-> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) ) )
140 128 139 mpbid 
 |-  ( ( ph /\ -. 2 || N ) -> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) )
141 101 140 pm2.61dan 
 |-  ( ph -> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) )