Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lgamgulmlem2 Unicode version

Theorem lgamgulmlem2 26719
Description: Lemma for lgamgulm 26724. (Contributed by Mario Carneiro, 3-Jul-2017.)
Hypotheses
Ref Expression
lgamgulm.r
lgamgulm.u
lgamgulm.n
lgamgulm.a
lgamgulm.l
Assertion
Ref Expression
lgamgulmlem2
Distinct variable groups:   ,N   , ,   , ,   ,

Proof of Theorem lgamgulmlem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1elunit 11348 . . 3
2 0elunit 11347 . . 3
3 0re 9332 . . . . 5
43a1i 11 . . . 4
5 1re 9331 . . . . 5
65a1i 11 . . . 4
7 eqid 2422 . . . . 5
87subcn 20142 . . . . . 6
98a1i 11 . . . . 5
107mulcn 20143 . . . . . . 7
1110a1i 11 . . . . . 6
12 lgamgulm.r . . . . . . . . . . 11
13 lgamgulm.u . . . . . . . . . . 11
1412, 13lgamgulmlem1 26718 . . . . . . . . . 10
15 lgamgulm.a . . . . . . . . . 10
1614, 15sseldd 3334 . . . . . . . . 9
1716eldifad 3317 . . . . . . . 8
18 lgamgulm.n . . . . . . . . . 10
1918nnred 10283 . . . . . . . . 9
2019recnd 9358 . . . . . . . 8
2118nnne0d 10312 . . . . . . . 8
2217, 20, 21divcld 10053 . . . . . . 7
23 unitssre 11376 . . . . . . . . 9
24 ax-resscn 9285 . . . . . . . . 9
2523, 24sstri 3342 . . . . . . . 8
2625a1i 11 . . . . . . 7
27 ssid 3352 . . . . . . . 8
2827a1i 11 . . . . . . 7
29 cncfmptc 20187 . . . . . . 7
3022, 26, 28, 29syl3anc 1203 . . . . . 6
31 cncfmptid 20188 . . . . . . 7
3225, 28, 31sylancr 648 . . . . . 6
337, 11, 30, 32cncfmpt2f 20190 . . . . 5
3422adantr 455 . . . . . . . . . . 11
35 simpr 451 . . . . . . . . . . . . 13
3623, 35sseldi 3331 . . . . . . . . . . . 12
3736recnd 9358 . . . . . . . . . . 11
3834, 37mulcld 9352 . . . . . . . . . 10
39 ax-1cn 9286 . . . . . . . . . . 11
4039a1i 11 . . . . . . . . . 10
4138, 40addcld 9351 . . . . . . . . 9
42 rere 12552 . . . . . . . . . . . 12
4342adantl 456 . . . . . . . . . . 11
4441recld 12624 . . . . . . . . . . . . 13
4538recld 12624 . . . . . . . . . . . . . . . . . . . . 21
4645recnd 9358 . . . . . . . . . . . . . . . . . . . 20
4746abscld 12863 . . . . . . . . . . . . . . . . . . 19
4838abscld 12863 . . . . . . . . . . . . . . . . . . 19
495a1i 11 . . . . . . . . . . . . . . . . . . 19
50 absrele 12738 . . . . . . . . . . . . . . . . . . . 20
5138, 50syl 16 . . . . . . . . . . . . . . . . . . 19
5249rehalfcld 10517 . . . . . . . . . . . . . . . . . . . 20
5312nnred 10283 . . . . . . . . . . . . . . . . . . . . . . 23
5453adantr 455 . . . . . . . . . . . . . . . . . . . . . 22
5518adantr 455 . . . . . . . . . . . . . . . . . . . . . 22
5654, 55nndivred 10316 . . . . . . . . . . . . . . . . . . . . 21
5722abscld 12863 . . . . . . . . . . . . . . . . . . . . . . . 24
5857adantr 455 . . . . . . . . . . . . . . . . . . . . . . 23
5934absge0d 12871 . . . . . . . . . . . . . . . . . . . . . . 23
603, 5elicc2i 11306 . . . . . . . . . . . . . . . . . . . . . . . . 25
6160simp2bi 989 . . . . . . . . . . . . . . . . . . . . . . . 24
6261adantl 456 . . . . . . . . . . . . . . . . . . . . . . 23
6317, 20, 21absdivd 12882 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6418nnrpd 10971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6564rpge0d 10976 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6619, 65absidd 12850 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6766oveq2d 6077 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6863, 67eqtr2d 2455 . . . . . . . . . . . . . . . . . . . . . . . . 25
6917abscld 12863 . . . . . . . . . . . . . . . . . . . . . . . . . 26
70 fveq2 5661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
7170breq1d 4277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
72 oveq1 6068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
7372fveq2d 5665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7473breq2d 4279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
7574ralbidv 2714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
7671, 75anbi12d 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
7776, 13elrab2 3097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7877simprbi 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7915, 78syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8079simpld 449 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8169, 53, 64, 80lediv1dd 11026 . . . . . . . . . . . . . . . . . . . . . . . . 25
8268, 81eqbrtrrd 4289 . . . . . . . . . . . . . . . . . . . . . . . 24
8382adantr 455 . . . . . . . . . . . . . . . . . . . . . . 23
8460simp3bi 990 . . . . . . . . . . . . . . . . . . . . . . . 24
8584adantl 456 . . . . . . . . . . . . . . . . . . . . . . 23
8658, 56, 36, 49, 59, 62, 83, 85lemul12ad 10221 . . . . . . . . . . . . . . . . . . . . . 22
8734, 37absmuld 12881 . . . . . . . . . . . . . . . . . . . . . . 23
8836, 62absidd 12850 . . . . . . . . . . . . . . . . . . . . . . . 24
8988oveq2d 6077 . . . . . . . . . . . . . . . . . . . . . . 23
9087, 89eqtr2d 2455 . . . . . . . . . . . . . . . . . . . . . 22
9156recnd 9358 . . . . . . . . . . . . . . . . . . . . . . 23
9291mulid1d 9349 . . . . . . . . . . . . . . . . . . . . . 22
9386, 90, 923brtr3d 4296 . . . . . . . . . . . . . . . . . . . . 21
94 lgamgulm.l . . . . . . . . . . . . . . . . . . . . . . . . 25
95 2rp 10941 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9695a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9753, 19, 96lemuldiv2d 11018 . . . . . . . . . . . . . . . . . . . . . . . . 25
9894, 97mpbid 204 . . . . . . . . . . . . . . . . . . . . . . . 24
99 2cnd 10340 . . . . . . . . . . . . . . . . . . . . . . . . 25
100 2ne0 10360 . . . . . . . . . . . . . . . . . . . . . . . . . 26
101100a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25
10220, 99, 101divrecd 10056 . . . . . . . . . . . . . . . . . . . . . . . 24
10398, 102breqtrd 4291 . . . . . . . . . . . . . . . . . . . . . . 23
1046rehalfcld 10517 . . . . . . . . . . . . . . . . . . . . . . . 24
10553, 104, 64ledivmuld 11021 . . . . . . . . . . . . . . . . . . . . . . 23
106103, 105mpbird 226 . . . . . . . . . . . . . . . . . . . . . 22
107106adantr 455 . . . . . . . . . . . . . . . . . . . . 21
10848, 56, 52, 93, 107letrd 9474 . . . . . . . . . . . . . . . . . . . 20
109 halflt1 10489 . . . . . . . . . . . . . . . . . . . . 21
110109a1i 11 . . . . . . . . . . . . . . . . . . . 20
11148, 52, 49, 108, 110lelttrd 9475 . . . . . . . . . . . . . . . . . . 19
11247, 48, 49, 51, 111lelttrd 9475 . . . . . . . . . . . . . . . . . 18
11345, 49absltd 12857 . . . . . . . . . . . . . . . . . 18
114112, 113mpbid 204 . . . . . . . . . . . . . . . . 17
115114simpld 449 . . . . . . . . . . . . . . . 16
11649renegcld 9721 . . . . . . . . . . . . . . . . 17
117116, 45posdifd 9872 . . . . . . . . . . . . . . . 16
118115, 117mpbid 204 . . . . . . . . . . . . . . 15
11946, 40subnegd 9672 . . . . . . . . . . . . . . 15
120118, 119breqtrd 4291 . . . . . . . . . . . . . 14
12138, 40readdd 12644 . . . . . . . . . . . . . . 15
122 re1 12584 . . . . . . . . . . . . . . . 16
123122oveq2i 6072 . . . . . . . . . . . . . . 15
124121, 123syl6eq 2470 . . . . . . . . . . . . . 14
125120, 124breqtrrd 4293 . . . . . . . . . . . . 13
12644, 125elrpd 10970 . . . . . . . . . . . 12
127126adantr 455 . . . . . . . . . . 11
12843, 127eqeltrrd 2497 . . . . . . . . . 10
129128ex 427 . . . . . . . . 9
130 eqid 2422 . . . . . . . . . 10
131130ellogdm 21825 . . . . . . . . 9
13241, 129, 131sylanbrc 649 . . . . . . . 8
133 eqidd 2423 . . . . . . . 8
134130logcn 21833 . . . . . . . . . . 11
135134a1i 11 . . . . . . . . . 10
136 cncff 20169 . . . . . . . . . 10
137135, 136syl 16 . . . . . . . . 9
138137feqmptd 5714 . . . . . . . 8
139 fveq2 5661 . . . . . . . 8
140132, 133, 138, 139fmptco 5845 . . . . . . 7
141 fvres 5674 . . . . . . . . 9
142132, 141syl 16 . . . . . . . 8
143142mpteq2dva 4353 . . . . . . 7
144140, 143eqtrd 2454 . . . . . 6
145 eqid 2422 . . . . . . . . 9
146132, 145fmptd 5837 . . . . . . . 8
147 difss 3460 . . . . . . . . 9
1487addcn 20141 . . . . . . . . . . 11
149148a1i 11 . . . . . . . . . 10
15039a1i 11 . . . . . . . . . . 11
151 cncfmptc 20187 . . . . . . . . . . 11
152150, 26, 28, 151syl3anc 1203 . . . . . . . . . 10
1537, 149, 33, 152cncfmpt2f 20190 . . . . . . . . 9
154 cncffvrn 20174 . . . . . . . . 9
155147, 153, 154sylancr 648 . . . . . . . 8
156146, 155mpbird 226 . . . . . . 7
157156, 135cncfco 20183 . . . . . 6
158144, 157eqeltrrd 2497 . . . . 5
1597, 9, 33, 158cncfmpt2f 20190 . . . 4
16024a1i 11 . . . . . . . 8
16123a1i 11 . . . . . . . 8
162130logdmn0 21826 . . . . . . . . . . 11
163132, 162syl 16 . . . . . . . . . 10
16441, 163logcld 21763 . . . . . . . . 9
16538, 164subcld 9665 . . . . . . . 8
1667tgioo2 20080 . . . . . . . 8
167 iccntr 20098 . . . . . . . . 9
1683, 6, 167sylancr 648 . . . . . . . 8
169160, 161, 165, 166, 7, 168dvmptntr 21145 . . . . . . 7
170 reelprrecn 9320 . . . . . . . . 9
171170a1i 11 . . . . . . . 8
17217adantr 455 . . . . . . . . . 10
17320adantr 455 . . . . . . . . . 10
17421adantr 455 . . . . . . . . . 10
175172, 173, 174divcld 10053 . . . . . . . . 9
176 ioossicc 11326 . . . . . . . . . . 11
177176sseli 3329 . . . . . . . . . 10
178177, 37sylan2 464 . . . . . . . . 9
179175, 178mulcld 9352 . . . . . . . 8
18017adantr 455 . . . . . . . . . . 11
18120adantr 455 . . . . . . . . . . 11
18221adantr 455 . . . . . . . . . . 11
183180, 181, 182divcld 10053 . . . . . . . . . 10
184160sselda 3333 . . . . . . . . . 10
185183, 184mulcld 9352 . . . . . . . . 9
18639a1i 11 . . . . . . . . . . 11
187171dvmptid 21131 . . . . . . . . . . 11
188171, 184, 186, 187, 22dvmptcmul 21138 . . . . . . . . . 10
18922mulid1d 9349 . . . . . . . . . . 11
190189mpteq2dv 4354 . . . . . . . . . 10
191188, 190eqtrd 2454 . . . . . . . . 9
192176, 161syl5ss 3344 . . . . . . . . 9
193 retop 20040 . . . . . . . . . . 11
194 iooretop 20045 . . . . . . . . . . 11
195 isopn3i 18390 . . . . . . . . . . 11
196193, 194, 195mp2an 657 . . . . . . . . . 10
197196a1i 11 . . . . . . . . 9
198171, 185, 183, 191, 192, 166, 7, 197dvmptres2 21136 . . . . . . . 8
199177, 164sylan2 464 . . . . . . . 8
20039a1i 11 . . . . . . . . . . 11
201179, 200addcld 9351 . . . . . . . . . 10
202177, 163sylan2 464 . . . . . . . . . 10
203201, 202reccld 10046 . . . . . . . . 9
204203, 175mulcld 9352 . . . . . . . 8
205 cnelprrecn 9321 . . . . . . . . . 10
206205a1i 11 . . . . . . . . 9
207177, 132sylan2 464 . . . . . . . . 9
208 eldifi 3455 . . . . . . . . . . 11
209208adantl 456 . . . . . . . . . 10
210130logdmn0 21826 . . . . . . . . . . 11
211210adantl 456 . . . . . . . . . 10
212209, 211logcld 21763 . . . . . . . . 9
213209, 211reccld 10046 . . . . . . . . 9
214185, 186addcld 9351 . . . . . . . . . 10
215 0cnd 9325 . . . . . . . . . . . 12
216171, 150dvmptc 21132 . . . . . . . . . . . 12
217171, 185, 183, 191, 186, 215, 216dvmptadd 21134 . . . . . . . . . . 11
21822addid1d 9515 . . . . . . . . . . . 12
219218mpteq2dv 4354 . . . . . . . . . . 11
220217, 219eqtrd 2454 . . . . . . . . . 10
221171, 214, 183, 220, 192, 166, 7, 197dvmptres2 21136 . . . . . . . . 9
222 fvres 5674 . . . . . . . . . . . . 13
223222mpteq2ia 4349 . . . . . . . . . . . 12
224138, 223syl6req 2471 . . . . . . . . . . 11
225224oveq2d 6077 . . . . . . . . . 10
226130dvlog 21837 . . . . . . . . . 10
227225, 226syl6eq 2470 . . . . . . . . 9
228 fveq2 5661 . . . . . . . . 9
229 oveq2 6069 . . . . . . . . 9
230171, 206, 207, 175, 212, 213, 221, 227, 228, 229dvmptco 21146 . . . . . . . 8
231171, 179, 175, 198, 199, 204, 230dvmptsub 21141 . . . . . . 7
232169, 231eqtrd 2454 . . . . . 6
233232dmeqd 5013 . . . . 5
234 ovex 6086 . . . . . 6
235 eqid 2422 . . . . . 6
236234, 235dmmpti 5510 . . . . 5
237233, 236syl6eq 2470 . . . 4
238 2re 10337 . . . . . . . . . . 11
239238a1i 11 . . . . . . . . . 10
240239, 53remulcld 9360 . . . . . . . . 9
24112nnrpd 10971 . . . . . . . . . . 11
24253, 241ltaddrpd 11001 . . . . . . . . . 10
24353recnd 9358 . . . . . . . . . . 11
2442432timesd 10513 . . . . . . . . . 10
245242, 244breqtrrd 4293 . . . . . . . . 9
24653, 240, 19, 245, 94ltletrd 9477 . . . . . . . 8
247 difrp 10969 . . . . . . . . 9
24853, 19, 247syl2anc 646 . . . . . . . 8
249246, 248mpbid 204 . . . . . . 7
250249rprecred 10983 . . . . . 6
25118nnrecred 10313 . . . . . 6
252250, 251resubcld 9722 . . . . 5
25353, 252remulcld 9360 . . . 4
254232fveq1d 5663 . . . . . . 7
255254fveq2d 5665 . . . . . 6
256255adantr 455 . . . . 5
257 nfv 1664 . . . . . . 7
258 nfcv 2558 . . . . . . . . 9
259 nffvmpt1 5669 . . . . . . . . 9
260258, 259nffv 5668 . . . . . . . 8
261 nfcv 2558 . . . . . . . 8
262 nfcv 2558 . . . . . . . 8
263260, 261, 262nfbr 4311 . . . . . . 7 </