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