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

Theorem lgamgulmlem2 24767
 Description: Lemma for lgamgulm 24772. (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:   ,   ,,   ,,   ,
Allowed substitution hints:   ()   (,)   ()

Proof of Theorem lgamgulmlem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1elunit 10972 . . 3
2 0elunit 10971 . . 3
3 0re 9047 . . . . 5
43a1i 11 . . . 4
5 1re 9046 . . . . 5
65a1i 11 . . . 4
7 eqid 2404 . . . . 5 fld fld
87subcn 18849 . . . . . 6 fld fld fld
98a1i 11 . . . . 5 fld fld fld
107mulcn 18850 . . . . . . 7 fld fld fld
1110a1i 11 . . . . . 6 fld fld fld
12 lgamgulm.r . . . . . . . . . . 11
13 lgamgulm.u . . . . . . . . . . 11
1412, 13lgamgulmlem1 24766 . . . . . . . . . 10
15 lgamgulm.a . . . . . . . . . 10
1614, 15sseldd 3309 . . . . . . . . 9
1716eldifad 3292 . . . . . . . 8
18 lgamgulm.n . . . . . . . . . 10
1918nnred 9971 . . . . . . . . 9
2019recnd 9070 . . . . . . . 8
2118nnne0d 10000 . . . . . . . 8
2217, 20, 21divcld 9746 . . . . . . 7
23 unitssre 10998 . . . . . . . . 9
24 ax-resscn 9003 . . . . . . . . 9
2523, 24sstri 3317 . . . . . . . 8
2625a1i 11 . . . . . . 7
27 ssid 3327 . . . . . . . 8
2827a1i 11 . . . . . . 7
29 cncfmptc 18894 . . . . . . 7
3022, 26, 28, 29syl3anc 1184 . . . . . 6
31 cncfmptid 18895 . . . . . . 7
3225, 28, 31sylancr 645 . . . . . 6
337, 11, 30, 32cncfmpt2f 18897 . . . . 5
3422adantr 452 . . . . . . . . . . 11
35 simpr 448 . . . . . . . . . . . . 13
3623, 35sseldi 3306 . . . . . . . . . . . 12
3736recnd 9070 . . . . . . . . . . 11
3834, 37mulcld 9064 . . . . . . . . . 10
39 ax-1cn 9004 . . . . . . . . . . 11
4039a1i 11 . . . . . . . . . 10
4138, 40addcld 9063 . . . . . . . . 9
42 rere 11882 . . . . . . . . . . . 12
4342adantl 453 . . . . . . . . . . 11
4441recld 11954 . . . . . . . . . . . . 13
4538recld 11954 . . . . . . . . . . . . . . . . . . . . 21
4645recnd 9070 . . . . . . . . . . . . . . . . . . . 20
4746abscld 12193 . . . . . . . . . . . . . . . . . . 19
4838abscld 12193 . . . . . . . . . . . . . . . . . . 19
495a1i 11 . . . . . . . . . . . . . . . . . . 19
50 absrele 12068 . . . . . . . . . . . . . . . . . . . 20
5138, 50syl 16 . . . . . . . . . . . . . . . . . . 19
5249rehalfcld 10170 . . . . . . . . . . . . . . . . . . . 20
5312nnred 9971 . . . . . . . . . . . . . . . . . . . . . . 23
5453adantr 452 . . . . . . . . . . . . . . . . . . . . . 22
5518adantr 452 . . . . . . . . . . . . . . . . . . . . . 22
5654, 55nndivred 10004 . . . . . . . . . . . . . . . . . . . . 21
5722abscld 12193 . . . . . . . . . . . . . . . . . . . . . . . 24
5857adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
5934absge0d 12201 . . . . . . . . . . . . . . . . . . . . . . 23
603, 5elicc2i 10932 . . . . . . . . . . . . . . . . . . . . . . . . 25
6160simp2bi 973 . . . . . . . . . . . . . . . . . . . . . . . 24
6261adantl 453 . . . . . . . . . . . . . . . . . . . . . . 23
6317, 20, 21absdivd 12212 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6418nnrpd 10603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6564rpge0d 10608 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6619, 65absidd 12180 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6766oveq2d 6056 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6863, 67eqtr2d 2437 . . . . . . . . . . . . . . . . . . . . . . . . 25
6917abscld 12193 . . . . . . . . . . . . . . . . . . . . . . . . . 26
70 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
7170breq1d 4182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
72 oveq1 6047 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
7372fveq2d 5691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7473breq2d 4184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
7574ralbidv 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
7671, 75anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
7776, 13elrab2 3054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7877simprbi 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7915, 78syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8079simpld 446 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8169, 53, 64, 80lediv1dd 10658 . . . . . . . . . . . . . . . . . . . . . . . . 25
8268, 81eqbrtrrd 4194 . . . . . . . . . . . . . . . . . . . . . . . 24
8382adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
8460simp3bi 974 . . . . . . . . . . . . . . . . . . . . . . . 24
8584adantl 453 . . . . . . . . . . . . . . . . . . . . . . 23
8658, 56, 36, 49, 59, 62, 83, 85lemul12ad 9909 . . . . . . . . . . . . . . . . . . . . . 22
8734, 37absmuld 12211 . . . . . . . . . . . . . . . . . . . . . . 23
8836, 62absidd 12180 . . . . . . . . . . . . . . . . . . . . . . . 24
8988oveq2d 6056 . . . . . . . . . . . . . . . . . . . . . . 23
9087, 89eqtr2d 2437 . . . . . . . . . . . . . . . . . . . . . 22
9156recnd 9070 . . . . . . . . . . . . . . . . . . . . . . 23
9291mulid1d 9061 . . . . . . . . . . . . . . . . . . . . . 22
9386, 90, 923brtr3d 4201 . . . . . . . . . . . . . . . . . . . . 21
94 lgamgulm.l . . . . . . . . . . . . . . . . . . . . . . . . 25
95 2rp 10573 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9695a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9753, 19, 96lemuldiv2d 10650 . . . . . . . . . . . . . . . . . . . . . . . . 25
9894, 97mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . 24
99 2re 10025 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
10099a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26
101100recnd 9070 . . . . . . . . . . . . . . . . . . . . . . . . 25
102 2ne0 10039 . . . . . . . . . . . . . . . . . . . . . . . . . 26
103102a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25
10420, 101, 103divrecd 9749 . . . . . . . . . . . . . . . . . . . . . . . 24
10598, 104breqtrd 4196 . . . . . . . . . . . . . . . . . . . . . . 23
1066rehalfcld 10170 . . . . . . . . . . . . . . . . . . . . . . . 24
10753, 106, 64ledivmuld 10653 . . . . . . . . . . . . . . . . . . . . . . 23
108105, 107mpbird 224 . . . . . . . . . . . . . . . . . . . . . 22
109108adantr 452 . . . . . . . . . . . . . . . . . . . . 21
11048, 56, 52, 93, 109letrd 9183 . . . . . . . . . . . . . . . . . . . 20
111 halflt1 10145 . . . . . . . . . . . . . . . . . . . . 21
112111a1i 11 . . . . . . . . . . . . . . . . . . . 20
11348, 52, 49, 110, 112lelttrd 9184 . . . . . . . . . . . . . . . . . . 19
11447, 48, 49, 51, 113lelttrd 9184 . . . . . . . . . . . . . . . . . 18
11545, 49absltd 12187 . . . . . . . . . . . . . . . . . 18
116114, 115mpbid 202 . . . . . . . . . . . . . . . . 17
117116simpld 446 . . . . . . . . . . . . . . . 16
11849renegcld 9420 . . . . . . . . . . . . . . . . 17
119118, 45posdifd 9569 . . . . . . . . . . . . . . . 16
120117, 119mpbid 202 . . . . . . . . . . . . . . 15
12146, 40subnegd 9374 . . . . . . . . . . . . . . 15
122120, 121breqtrd 4196 . . . . . . . . . . . . . 14
12338, 40readdd 11974 . . . . . . . . . . . . . . 15
124 re1 11914 . . . . . . . . . . . . . . . 16
125124oveq2i 6051 . . . . . . . . . . . . . . 15
126123, 125syl6eq 2452 . . . . . . . . . . . . . 14
127122, 126breqtrrd 4198 . . . . . . . . . . . . 13
12844, 127elrpd 10602 . . . . . . . . . . . 12
129128adantr 452 . . . . . . . . . . 11
13043, 129eqeltrrd 2479 . . . . . . . . . 10
131130ex 424 . . . . . . . . 9
132 eqid 2404 . . . . . . . . . 10
133132ellogdm 20483 . . . . . . . . 9
13441, 131, 133sylanbrc 646 . . . . . . . 8
135 eqidd 2405 . . . . . . . 8
136132logcn 20491 . . . . . . . . . . 11
137136a1i 11 . . . . . . . . . 10
138 cncff 18876 . . . . . . . . . 10
139137, 138syl 16 . . . . . . . . 9
140139feqmptd 5738 . . . . . . . 8
141 fveq2 5687 . . . . . . . 8
142134, 135, 140, 141fmptco 5860 . . . . . . 7
143 fvres 5704 . . . . . . . . 9
144134, 143syl 16 . . . . . . . 8
145144mpteq2dva 4255 . . . . . . 7
146142, 145eqtrd 2436 . . . . . 6
147 eqid 2404 . . . . . . . . 9
148134, 147fmptd 5852 . . . . . . . 8
149 difss 3434 . . . . . . . . 9
1507addcn 18848 . . . . . . . . . . 11 fld fld fld
151150a1i 11 . . . . . . . . . 10 fld fld fld
15239a1i 11 . . . . . . . . . . 11
153 cncfmptc 18894 . . . . . . . . . . 11
154152, 26, 28, 153syl3anc 1184 . . . . . . . . . 10
1557, 151, 33, 154cncfmpt2f 18897 . . . . . . . . 9
156 cncffvrn 18881 . . . . . . . . 9
157149, 155, 156sylancr 645 . . . . . . . 8
158148, 157mpbird 224 . . . . . . 7
159158, 137cncfco 18890 . . . . . 6
160146, 159eqeltrrd 2479 . . . . 5
1617, 9, 33, 160cncfmpt2f 18897 . . . 4
16224a1i 11 . . . . . . . 8
16323a1i 11 . . . . . . . 8
164132logdmn0 20484 . . . . . . . . . . 11
165134, 164syl 16 . . . . . . . . . 10
16641, 165logcld 20421 . . . . . . . . 9
16738, 166subcld 9367 . . . . . . . 8
1687tgioo2 18787 . . . . . . . 8 fldt
169 iccntr 18805 . . . . . . . . 9
1703, 6, 169sylancr 645 . . . . . . . 8
171162, 163, 167, 168, 7, 170dvmptntr 19810 . . . . . . 7
172 reex 9037 . . . . . . . . . 10
173172prid1 3872 . . . . . . . . 9
174173a1i 11 . . . . . . . 8
17517adantr 452 . . . . . . . . . 10
17620adantr 452 . . . . . . . . . 10
17721adantr 452 . . . . . . . . . 10
178175, 176, 177divcld 9746 . . . . . . . . 9
179 ioossicc 10952 . . . . . . . . . . 11
180179sseli 3304 . . . . . . . . . 10
181180, 37sylan2 461 . . . . . . . . 9
182178, 181mulcld 9064 . . . . . . . 8
18317adantr 452 . . . . . . . . . . 11
18420adantr 452 . . . . . . . . . . 11
18521adantr 452 . . . . . . . . . . 11
186183, 184, 185divcld 9746 . . . . . . . . . 10
187162sselda 3308 . . . . . . . . . 10
188186, 187mulcld 9064 . . . . . . . . 9
18939a1i 11 . . . . . . . . . . 11
190174dvmptid 19796 . . . . . . . . . . 11
191174, 187, 189, 190, 22dvmptcmul 19803 . . . . . . . . . 10
19222mulid1d 9061 . . . . . . . . . . 11
193192mpteq2dv 4256 . . . . . . . . . 10
194191, 193eqtrd 2436 . . . . . . . . 9
195179, 163syl5ss 3319 . . . . . . . . 9
196 retop 18748 . . . . . . . . . . 11
197 iooretop 18753 . . . . . . . . . . 11
198 isopn3i 17101 . . . . . . . . . . 11
199196, 197, 198mp2an 654 . . . . . . . . . 10
200199a1i 11 . . . . . . . . 9
201174, 188, 186, 194, 195, 168, 7, 200dvmptres2 19801 . . . . . . . 8
202180, 166sylan2 461 . . . . . . . 8
20339a1i 11 . . . . . . . . . . 11
204182, 203addcld 9063 . . . . . . . . . 10
205180, 165sylan2 461 . . . . . . . . . 10
206204, 205reccld 9739 . . . . . . . . 9
207206, 178mulcld 9064 . . . . . . . 8
208 cnex 9027 . . . . . . . . . . 11
209208prid2 3873 . . . . . . . . . 10
210209a1i 11 . . . . . . . . 9
211180, 134sylan2 461 . . . . . . . . 9
212 eldifi 3429 . . . . . . . . . . 11
213212adantl 453 . . . . . . . . . 10
214132logdmn0 20484 . . . . . . . . . . 11
215214adantl 453 . . . . . . . . . 10
216213, 215logcld 20421 . . . . . . . . 9
217213, 215reccld 9739 . . . . . . . . 9
218188, 189addcld 9063 . . . . . . . . . 10
219 0cn 9040 . . . . . . . . . . . . 13
220219a1i 11 . . . . . . . . . . . 12
221174, 152dvmptc 19797 . . . . . . . . . . . 12
222174, 188, 186, 194, 189, 220, 221dvmptadd 19799 . . . . . . . . . . 11
22322addid1d 9222 . . . . . . . . . . . 12
224223mpteq2dv 4256 . . . . . . . . . . 11
225222, 224eqtrd 2436 . . . . . . . . . 10
226174, 218, 186, 225, 195, 168, 7, 200dvmptres2 19801 . . . . . . . . 9
227 fvres 5704 . . . . . . . . . . . . 13
228227mpteq2ia 4251 . . . . . . . . . . . 12
229140, 228syl6req 2453 . . . . . . . . . . 11
230229oveq2d 6056 . . . . . . . . . 10
231132dvlog 20495 . . . . . . . . . 10
232230, 231syl6eq 2452 . . . . . . . . 9
233 fveq2 5687 . . . . . . . . 9
234 oveq2 6048 . . . . . . . . 9
235174, 210, 211, 178, 216, 217, 226, 232, 233, 234dvmptco 19811 . . . . . . . 8
236174, 182, 178, 201, 202, 207, 235dvmptsub 19806 . . . . . . 7
237171, 236eqtrd 2436 . . . . . 6
238237dmeqd 5031 . . . . 5
239 ovex 6065 . . . . . 6
240 eqid 2404 . . . . . 6
241239, 240dmmpti 5533 . . . . 5
242238, 241syl6eq 2452 . . . 4
243100, 53remulcld 9072 . . . . . . . . 9
24412nnrpd 10603 . . . . . . . . . . 11
24553, 244ltaddrpd 10633 . . . . . . . . . 10
24653recnd 9070 . . . . . . . . . . 11
2472462timesd 10166 . . . . . . . . . 10
248245, 247breqtrrd 4198 . . . . . . . . 9
24953, 243, 19, 248, 94ltletrd 9186 . . . . . . . 8
250 difrp 10601 . . . . . . . . 9
25153, 19, 250syl2anc 643 . . . . . . . 8
252249, 251mpbid 202 . . . . . . 7
253252rprecred 10615 . . . . . 6
25418nnrecred 10001 . . . . . 6
255253, 254resubcld 9421 . . . . 5
25653, 255remulcld 9072 . . . 4
257237fveq1d 5689 . . . . . . 7
258257fveq2d 5691 . . . . . 6
259258adantr 452 . . . . 5
260 nfv 1626 . . . . . . 7
261 nfcv 2540 . . . . . . . . 9
262 nffvmpt1 5695 . . . . . . . . 9
263261, 262nffv 5694 . . . . . . . 8
264 nfcv 2540 . . . . . . . 8
265 nfcv 2540 . . . . . . . 8
266263, 264, 265nfbr 4216 . . . . . . 7
267260, 266nfim 1828 . . . . . 6
268 eleq1 2464 . . . . . . . 8
269268anbi2d 685 . . . . . . 7
270 fveq2 5687 . . . . . . . . 9
271270fveq2d 5691 . . . . . . . 8
272271breq1d 4182 . . . . . . 7
273269, 272imbi12d 312 . . . . . 6
274 simpr 448 . . . . . . . . . 10
275240fvmpt2 5771 . . . . . . . . . 10
276274, 239, 275sylancl 644 . . . . . . . . 9
277276fveq2d 5691 . . . . . . . 8
278178, 203, 206subdid 9445 . . . . . . . . . 10
279178mulid1d 9061 . . . . . . . . . . 11
280178, 206mulcomd 9065 . . . . . . . . . . 11
281279, 280oveq12d 6058 . . . . . . . . . 10
282278, 281eqtr2d 2437 . . . . . . . . 9
283282fveq2d 5691 . . . . . . . 8
284175, 176, 177absdivd 12212 . . . . . . . . . . 11
28519adantr 452 . . . . . . . . . . . . 13
28665adantr 452 . . . . . . . . . . . . 13
287285, 286absidd 12180 . . . . . . . . . . . 12
288287oveq2d 6056 . . . . . . . . . . 11
289284, 288eqtrd 2436 . . . . . . . . . 10
290289oveq1d 6055 . . . . . . . . 9
291203, 206subcld 9367 . . . . . . . . . 10
292178, 291absmuld 12211 . . . . . . . . 9
29369adantr 452 . . . . . . . . . . 11
294293recnd 9070 . . . . . . . . . 10
295291abscld 12193 . . . . . . . . . . 11
296295recnd 9070 . . . . . . . . . 10
297294, 296, 176, 177div23d 9783 . . . . . . . . 9
298290, 292, 2973eqtr4d 2446 . . . . . . . 8
299277, 283, 2983eqtrd 2440 . . . . . . 7
30053adantr 452 . . . . . . . . . 10
301253adantr 452 . . . . . . . . . . . 12
302254adantr 452 . . . . . . . . . . . 12
303301, 302resubcld 9421 . . . . . . . . . . 11
304285, 303remulcld 9072 . . . . . . . . . 10
30517absge0d 12201 . . . . . . . . . . 11
306305adantr 452 . . . . . . . . . 10
307291absge0d 12201 . . . . . . . . . 10
30880adantr 452 . . . . . . . . . 10
309252adantr 452 . . . . . . . . . . . . . 14
310244adantr 452 . . . . . . . . . . . . . 14
311309, 310rpdivcld 10621 . . . . . . . . . . . . 13
31216dmgmn0 24763 . . . . . . . . . . . . . . . . . . 19
313312adantr 452 . . . . . . . . . . . . . . . . . 18
314175, 176, 313, 177divne0d 9762 . . . . . . . . . . . . . . . . 17
315 eliooord 10926 . . . . . . . . . . . . . . . . . . . 20
316315adantl 453 . . . . . . . . . . . . . . . . . . 19
317316simpld 446 . . . . . . . . . . . . . . . . . 18
318317gt0ne0d 9547 . . . . . . . . . . . . . . . . 17
319178, 181, 314, 318mulne0d 9630 . . . . . . . . . . . . . . . 16
320182, 319reccld 9739 . . . . . . . . . . . . . . 15
321203, 320addcld 9063 . . . . . . . . . . . . . 14
322182, 203, 182, 319divdird 9784 . . . . . . . . . . . . . . . 16
323182, 319dividd 9744 . . . . . . . . . . . . . . . . 17
324323oveq1d 6055 . . . . . . . . . . . . . . . 16
325322, 324eqtrd 2436 . . . . . . . . . . . . . . 15
326204, 182, 205, 319divne0d 9762 . . . . . . . . . . . . . . 15
327325, 326eqnetrrd 2587 . . . . . . . . . . . . . 14
328321, 327absrpcld 12205 . . . . . . . . . . . . 13
3295a1i 11 . . . . . . . . . . . . 13
330 0le1 9507 . . . . . . . . . . . . . 14
331330a1i 11 . . . . . . . . . . . . 13
332311rpred 10604 . . . . . . . . . . . . . 14
333320negcld 9354 . . . . . . . . . . . . . . . 16
334333abscld 12193 . . . . . . . . . . . . . . 15
335334, 329resubcld 9421 . . . . . . . . . . . . . 14
336321abscld 12193 . . . . . . . . . . . . . 14
337246adantr 452 . . . . . . . . . . . . . . . . 17
338310rpne0d 10609 . . . . . . . . . . . . . . . . 17
339176, 337, 337, 338divsubdird 9785 . . . . . . . . . . . . . . . 16
340337, 338dividd 9744 . . . . . . . . . . . . . . . . 17
341340oveq2d 6056 . . . . . . . . . . . . . . . 16
342339, 341eqtrd 2436 . . . . . . . . . . . . . . 15
343285, 310rerpdivcld 10631 . . . . . . . . . . . . . . . 16
344337, 176, 338, 177recdivd 9763 . . . . . . . . . . . . . . . . . 18
345180, 93sylan2 461 . . . . . . . . . . . . . . . . . . 19
346182, 319absrpcld 12205 . . . . . . . . . . . . . . . . . . . 20
34764adantr 452 . . . . . . . . . . . . . . . . . . . . 21
348310, 347rpdivcld 10621 . . . . . . . . . . . . . . . . . . . 20
349346, 348lerecd 10623 . . . . . . . . . . . . . . . . . . 19
350345, 349mpbid 202 . . . . . . . . . . . . . . . . . 18
351344, 350eqbrtrrd 4194 . . . . . . . . . . . . . . . . 17
352320absnegd 12206 . . . . . . . . . . . . . . . . . 18
353203, 182, 319absdivd 12212 . . . . . . . . . . . . . . . . . . 19
354 abs1 12057 . . . . . . . . . . . . . . . . . . . 20
355354oveq1i 6050 . . . . . . . . . . . . . . . . . . 19
356353, 355syl6eq 2452 . . . . . . . . . . . . . . . . . 18
357352, 356eqtrd 2436 . . . . . . . . . . . . . . . . 17
358351, 357breqtrrd 4198 . . . . . . . . . . . . . . . 16
359343, 334, 329, 358lesub1dd 9598 . . . . . . . . . . . . . . 15
360342, 359eqbrtrd 4192 . . . . . . . . . . . . . 14
361354oveq2i 6051 . . . . . . . . . . . . . . . 16
362333, 203abs2difd 12214 . . . . . . . . . . . . . . . 16
363361, 362syl5eqbrr 4206 . . . . . . . . . . . . . . 15
364203, 320addcomd 9224 . . . . . . . . . . . . . . . . . . 19
365364negeqd 9256 . . . . . . . . . . . . . . . . . 18
366320, 203negdi2d 9381 . . . . . . . . . . . . . . . . . 18
367365, 366eqtrd 2436 . . . . . . . . . . . . . . . . 17
368367fveq2d 5691 . . . . . . . . . . . . . . . 16
369321absnegd 12206 . . . . . . . . . . . . . . . 16
370368, 369eqtr3d 2438 . . . . . . . . . . . . . . 15
371363, 370breqtrd 4196 . . . . . . . . . . . . . 14
372332, 335, 336, 360, 371letrd 9183 . . . . . . . . . . . . 13
373311, 328, 329, 331, 372lediv2ad 10626 . . . . . . . . . . . 12
37420, 246subcld 9367 . . . . . . . . . . . . . . 15
375374adantr 452 . . . . . . . . . . . . . 14
37653, 249gtned 9164 . . . . . . . . . . . . . . . 16
37720, 246, 376subne0d 9376 . . . . . . . . . . . . . . 15
378377adantr 452 . . . . . . . . . . . . . 14
379375, 337, 378, 338recdivd 9763 . . . . . . . . . . . . 13
380176, 337nncand 9372 . . . . . . . . . . . . . . 15
381380oveq1d 6055 . . . . . . . . . . . . . 14
382176, 375, 375, 378divsubdird 9785 . . . . . . . . . . . . . 14
383381, 382eqtr3d 2438 . . . . . . . . . . . . 13
384375, 378dividd 9744 . . . . . . . . . . . . . 14
385384oveq2d 6056 . . . . . . . . . . . . 13
386379, 383, 3853eqtrd 2440 . . . . . . . . . . . 12
387373, 386breqtrd 4196 . . . . . . . . . . 11
388204, 203, 204, 205divsubdird 9785 . . . . . . . . . . . . . . 15
389182, 203pncand 9368 . . . . . . . . . . . . . . . 16
390389oveq1d 6055 . . . . . . . . . . . . . . 15
391204, 205dividd 9744 . . . . . . . . . . . . . . . 16
392391oveq1d 6055 . . . . . . . . . . . . . . 15
393388, 390, 3923eqtr3rd 2445 . . . . . . . . . . . . . 14
394204, 182, 205, 319recdivd 9763 . . . . . . . . . . . . . 14
395325oveq2d 6056 . . . . . . . . . . . . . 14
396393, 394, 3953eqtr2d 2442 . . . . . . . . . . . . 13
397396fveq2d 5691 . . . . . . . . . . . 12
398203, 321, 327absdivd 12212 . . . . . . . . . . . . 13
399354oveq1i 6050 . . . . . . . . . . . . 13
400398, 399syl6eq 2452 . . . . . . . . . . . 12
401397, 400eqtrd 2436 . . . . . . . . . . 11
402374, 377reccld 9739 . . . . . . . . . . . . . 14
403402adantr 452 . . . . . . . . . . . . 13
404254recnd 9070 . . . . . . . . . . . . . 14
405404adantr 452 . . . . . . . . . . . . 13
406176, 403, 405subdid 9445 . . . . . . . . . . . 12
407176, 375, 378divrecd 9749 . . . . . . . . . . . . . 14
408407eqcomd 2409 . . . . . . . . . . . . 13
409176, 177recidd 9741 . . . . . . . . . . . . 13
410408, 409oveq12d 6058 . . . . . . . . . . . 12
411406, 410eqtrd 2436 . . . . . . . . . . 11
412387, 401, 4113brtr4d 4202 . . . . . . . . . 10
413293, 300, 295, 304, 306, 307, 308, 412lemul12ad 9909 . . . . . . . . 9
414255recnd 9070 . . . . . . . . . . 11
415414adantr 452 . . . . . . . . . 10
416337, 176, 415mul12d 9231 . . . . . . . . 9
417413, 416breqtrd 4196 . . . . . . . 8
418293, 295remulcld 9072 . . . . . . . . 9
419256adantr 452 . . . . . . . . 9
420418, 419, 347ledivmuld 10653 . . . . . . . 8
421417, 420mpbird 224 . . . . . . 7
422299, 421eqbrtrd 4192 . . . . . 6
423267, 273, 422chvar 2039 . . . . 5
424259, 423eqbrtrd 4192 . . . 4