MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  quart1lem Unicode version

Theorem quart1lem 21991
Description: Lemma for quart1 21992. (Contributed by Mario Carneiro, 6-May-2015.)
Hypotheses
Ref Expression
quart1.a
quart1.b
quart1.c
quart1.d
quart1.p
quart1.q
quart1.r
quart1.x
quart1.y
Assertion
Ref Expression
quart1lem

Proof of Theorem quart1lem
StepHypRef Expression
1 quart1.c . . . . . . . . 9
2 quart1.a . . . . . . . . . . 11
3 quart1.b . . . . . . . . . . 11
42, 3mulcld 9352 . . . . . . . . . 10
54halfcld 10515 . . . . . . . . 9
61, 5subcld 9665 . . . . . . . 8
7 3nn0 10543 . . . . . . . . . 10
8 expcl 11824 . . . . . . . . . 10
92, 7, 8sylancl 647 . . . . . . . . 9
10 8cn 10353 . . . . . . . . . 10
1110a1i 11 . . . . . . . . 9
12 8nn 10431 . . . . . . . . . . 11
1312nnne0i 10302 . . . . . . . . . 10
1413a1i 11 . . . . . . . . 9
159, 11, 14divcld 10053 . . . . . . . 8
16 4cn 10345 . . . . . . . . . 10
1716a1i 11 . . . . . . . . 9
18 4ne0 10364 . . . . . . . . . 10
1918a1i 11 . . . . . . . . 9
202, 17, 19divcld 10053 . . . . . . . 8
216, 15, 20adddird 9357 . . . . . . 7
22 quart1.q . . . . . . . 8
2322oveq1d 6076 . . . . . . 7
241, 2, 17, 19divassd 10088 . . . . . . . . . 10
252sqvald 11946 . . . . . . . . . . . . . . 15
2625oveq1d 6076 . . . . . . . . . . . . . 14
272, 2, 3mul32d 9525 . . . . . . . . . . . . . 14
2826, 27eqtrd 2454 . . . . . . . . . . . . 13
2928oveq1d 6076 . . . . . . . . . . . 12
30 2cn 10338 . . . . . . . . . . . . . 14
31 4t2e8 10421 . . . . . . . . . . . . . 14
3216, 30, 31mulcomli 9339 . . . . . . . . . . . . 13
3332oveq2i 6072 . . . . . . . . . . . 12
3429, 33syl6eqr 2472 . . . . . . . . . . 11
3530a1i 11 . . . . . . . . . . . 12
36 2ne0 10360 . . . . . . . . . . . . 13
3736a1i 11 . . . . . . . . . . . 12
384, 35, 2, 17, 37, 19divmuldivd 10094 . . . . . . . . . . 11
3934, 38eqtr4d 2457 . . . . . . . . . 10
4024, 39oveq12d 6079 . . . . . . . . 9
411, 5, 20subdird 9747 . . . . . . . . 9
4240, 41eqtr4d 2457 . . . . . . . 8
43 df-4 10328 . . . . . . . . . . . . . 14
4443oveq2i 6072 . . . . . . . . . . . . 13
45 expp1 11813 . . . . . . . . . . . . . 14
462, 7, 45sylancl 647 . . . . . . . . . . . . 13
4744, 46syl5eq 2466 . . . . . . . . . . . 12
4847oveq1d 6076 . . . . . . . . . . 11
499, 2, 11, 14div23d 10090 . . . . . . . . . . 11
5048, 49eqtrd 2454 . . . . . . . . . 10
5150oveq1d 6076 . . . . . . . . 9
5215, 2, 17, 19divassd 10088 . . . . . . . . 9
5351, 52eqtrd 2454 . . . . . . . 8
5442, 53oveq12d 6079 . . . . . . 7
5521, 23, 543eqtr4d 2464 . . . . . 6
561, 2mulcld 9352 . . . . . . . 8
5756, 17, 19divcld 10053 . . . . . . 7
582sqcld 11947 . . . . . . . . 9
5958, 3mulcld 9352 . . . . . . . 8
6059, 11, 14divcld 10053 . . . . . . 7
61 4nn0 10544 . . . . . . . . . 10
62 expcl 11824 . . . . . . . . . 10
632, 61, 62sylancl 647 . . . . . . . . 9
6463, 11, 14divcld 10053 . . . . . . . 8
6564, 17, 19divcld 10053 . . . . . . 7
6657, 60, 65subadd23d 9687 . . . . . 6
6765, 60subcld 9665 . . . . . . 7
6857, 67addcomd 9517 . . . . . 6
6955, 66, 683eqtrd 2458 . . . . 5
70 quart1.r . . . . . 6
71 quart1.d . . . . . . 7
72 1nn0 10541 . . . . . . . . . . . 12
73 6nn 10429 . . . . . . . . . . . 12
7472, 73decnncl 10713 . . . . . . . . . . 11
7574nncni 10278 . . . . . . . . . 10
7675a1i 11 . . . . . . . . 9
7774nnne0i 10302 . . . . . . . . . 10
7877a1i 11 . . . . . . . . 9
7959, 76, 78divcld 10053 . . . . . . . 8
80 3cn 10342 . . . . . . . . . 10
81 2nn0 10542 . . . . . . . . . . . . 13
82 5nn0 10545 . . . . . . . . . . . . 13
8381, 82deccl 10714 . . . . . . . . . . . 12
8483, 73decnncl 10713 . . . . . . . . . . 11
8584nncni 10278 . . . . . . . . . 10
8684nnne0i 10302 . . . . . . . . . 10
8780, 85, 86divcli 10019 . . . . . . . . 9
88 mulcl 9312 . . . . . . . . 9
8987, 63, 88sylancr 648 . . . . . . . 8
9079, 89subcld 9665 . . . . . . 7
9171, 90, 57addsubd 9686 . . . . . 6
9270, 91eqtr4d 2457 . . . . 5
9369, 92oveq12d 6079 . . . 4
9471, 90addcld 9351 . . . . 5
9567, 57, 94ppncand 9705 . . . 4
9667, 71, 90add12d 9537 . . . . 5
9760, 89addcld 9351 . . . . . . . 8
9865, 79addcld 9351 . . . . . . . 8
9997, 98negsubdi2d 9681 . . . . . . 7
10065, 79addcomd 9517 . . . . . . . . . 10
101100oveq2d 6077 . . . . . . . . 9
10260, 89, 79, 65addsub4d 9712 . . . . . . . . 9
10380a1i 11 . . . . . . . . . . . . . . . 16
10485a1i 11 . . . . . . . . . . . . . . . 16
10586a1i 11 . . . . . . . . . . . . . . . 16
106103, 63, 104, 105divassd 10088 . . . . . . . . . . . . . . 15
107103, 63, 104, 105div23d 10090 . . . . . . . . . . . . . . 15
108 1p2e3 10392 . . . . . . . . . . . . . . . . . 18
109108oveq1i 6071 . . . . . . . . . . . . . . . . 17
110 ax-1cn 9286 . . . . . . . . . . . . . . . . . . 19
111110a1i 11 . . . . . . . . . . . . . . . . . 18
11263, 104, 105divcld 10053 . . . . . . . . . . . . . . . . . 18
113111, 35, 112adddird 9357 . . . . . . . . . . . . . . . . 17
114109, 113syl5eqr 2468 . . . . . . . . . . . . . . . 16
115112mulid2d 9350 . . . . . . . . . . . . . . . . 17
116115oveq1d 6076 . . . . . . . . . . . . . . . 16
117114, 116eqtrd 2454 . . . . . . . . . . . . . . 15
118106, 107, 1173eqtr3d 2462 . . . . . . . . . . . . . 14
11943oveq1i 6071 . . . . . . . . . . . . . . . 16
12065, 17, 19divcld 10053 . . . . . . . . . . . . . . . . 17
121103, 111, 120adddird 9357 . . . . . . . . . . . . . . . 16
122119, 121syl5eq 2466 . . . . . . . . . . . . . . 15
12365, 17, 19divcan2d 10055 . . . . . . . . . . . . . . 15
124120mulid2d 9350 . . . . . . . . . . . . . . . . 17
12564, 17, 17, 19, 19divdiv1d 10084 . . . . . . . . . . . . . . . . . 18
126 4t4e16 10773 . . . . . . . . . . . . . . . . . . 19
127126oveq2i 6072 . . . . . . . . . . . . . . . . . 18
128125, 127syl6eq 2470 . . . . . . . . . . . . . . . . 17
12963, 11, 76, 14, 78divdiv1d 10084 . . . . . . . . . . . . . . . . . 18
13010, 75mulcli 9337 . . . . . . . . . . . . . . . . . . . . 21
131130a1i 11 . . . . . . . . . . . . . . . . . . . 20
13210, 75, 13, 77mulne0i 9925 . . . . . . . . . . . . . . . . . . . . 21
133132a1i 11 . . . . . . . . . . . . . . . . . . . 20
13463, 131, 133divcld 10053 . . . . . . . . . . . . . . . . . . 19
135134, 35, 37divcan2d 10055 . . . . . . . . . . . . . . . . . 18
13663, 131, 35, 133, 37divdiv1d 10084 . . . . . . . . . . . . . . . . . . . 20
13710, 75, 30mul32i 9511 . . . . . . . . . . . . . . . . . . . . . 22
138 2exp4 14054 . . . . . . . . . . . . . . . . . . . . . . . 24
139 8t2e16 10788 . . . . . . . . . . . . . . . . . . . . . . . 24
140138, 139eqtr4i 2445 . . . . . . . . . . . . . . . . . . . . . . 23
141140, 138oveq12i 6073 . . . . . . . . . . . . . . . . . . . . . 22
142 4p4e8 10404 . . . . . . . . . . . . . . . . . . . . . . . 24
143142oveq2i 6072 . . . . . . . . . . . . . . . . . . . . . . 23
144 expadd 11847 . . . . . . . . . . . . . . . . . . . . . . . 24
14530, 61, 61, 144mp3an 1299 . . . . . . . . . . . . . . . . . . . . . . 23
146 2exp8 14056 . . . . . . . . . . . . . . . . . . . . . . 23
147143, 145, 1463eqtr3i 2450 . . . . . . . . . . . . . . . . . . . . . 22
148137, 141, 1473eqtr2i 2448 . . . . . . . . . . . . . . . . . . . . 21
149148oveq2i 6072 . . . . . . . . . . . . . . . . . . . 20
150136, 149syl6eq 2470 . . . . . . . . . . . . . . . . . . 19
151150oveq2d 6077 . . . . . . . . . . . . . . . . . 18
152129, 135, 1513eqtr2d 2460 . . . . . . . . . . . . . . . . 17
153124, 128, 1523eqtrd 2458 . . . . . . . . . . . . . . . 16
154153oveq2d 6077 . . . . . . . . . . . . . . 15
155122, 123, 1543eqtr3d 2462 . . . . . . . . . . . . . 14
156118, 155oveq12d 6079 . . . . . . . . . . . . 13
157 mulcl 9312 . . . . . . . . . . . . . . 15
15880, 120, 157sylancr 648 . . . . . . . . . . . . . 14
159 mulcl 9312 . . . . . . . . . . . . . . 15
16030, 112, 159sylancr 648 . . . . . . . . . . . . . 14
161112, 158, 160pnpcan2d 9703 . . . . . . . . . . . . 13
162156, 161eqtrd 2454 . . . . . . . . . . . 12
163162oveq2d 6077 . . . . . . . . . . 11
16479, 112, 158addsub12d 9688 . . . . . . . . . . 11
165163, 164eqtrd 2454 . . . . . . . . . 10
16659, 11, 35, 14, 37divdiv1d 10084 . . . . . . . . . . . . . . . 16
167139oveq2i 6072 . . . . . . . . . . . . . . . 16
168166, 167syl6eq 2470 . . . . . . . . . . . . . . 15
169168oveq2d 6077 . . . . . . . . . . . . . 14
17060, 35, 37divcan2d 10055 . . . . . . . . . . . . . 14
171792timesd 10513 . . . . . . . . . . . . . 14
172169, 170, 1713eqtr3d 2462 . . . . . . . . . . . . 13
173172oveq1d 6076 . . . . . . . . . . . 12
17479, 79pncand 9666 . . . . . . . . . . . 12
175173, 174eqtrd 2454 . . . . . . . . . . 11
176175oveq1d 6076 . . . . . . . . . 10
177 quart1.p . . . . . . . . . . . . 13
178177oveq1d 6076 . . . . . . . . . . . 12
17980, 10, 13divcli 10019 . . . . . . . . . . . . . 14
180 mulcl 9312 . . . . . . . . . . . . . 14
181179, 58, 180sylancr 648 . . . . . . . . . . . . 13
18220sqcld 11947 . . . . . . . . . . . . 13
1833, 181, 182subdird 9747 . . . . . . . . . . . 12
1842, 17, 19sqdivd 11962 . . . . . . . . . . . . . . . 16
18516sqvali 11886 . . . . . . . . . . . . . . . . . 18
186185, 126eqtri 2442 . . . . . . . . . . . . . . . . 17
187186oveq2i 6072 . . . . . . . . . . . . . . . 16
188184, 187syl6eq 2470 . . . . . . . . . . . . . . 15
189188oveq2d 6077 . . . . . . . . . . . . . 14
1903, 58, 76, 78divassd 10088 . . . . . . . . . . . . . 14
1913, 58mulcomd 9353 . . . . . . . . . . . . . . 15
192191oveq1d 6076 . . . . . . . . . . . . . 14
193189, 190, 1923eqtr2d 2460 . . . . . . . . . . . . 13
194179a1i 11 . . . . . . . . . . . . . . . . . 18
195194, 58, 58mulassd 9355 . . . . . . . . . . . . . . . . 17
196103, 63, 11, 14div23d 10090 . . . . . . . . . . . . . . . . . 18
197 2p2e4 10385 . . . . . . . . . . . . . . . . . . . . 21
198197oveq2i 6072 . . . . . . . . . . . . . . . . . . . 20
19981a1i 11 . . . . . . . . . . . . . . . . . . . . 21
2002, 199, 199expaddd 11951 . . . . . . . . . . . . . . . . . . . 20
201198, 200syl5eqr 2468 . . . . . . . . . . . . . . . . . . 19
202201oveq2d 6077 . . . . . . . . . . . . . . . . . 18
203196, 202eqtrd 2454 . . . . . . . . . . . . . . . . 17
204103, 63, 11, 14divassd 10088 . . . . . . . . . . . . . . . . 17
205195, 203, 2043eqtr2d 2460 . . . . . . . . . . . . . . . 16
206205oveq1d 6076 . . . . . . . . . . . . . . 15
207186, 76syl5eqel 2506 . . . . . . . . . . . . . . . 16
208186, 77eqnetri 2604 . . . . . . . . . . . . . . . . 17
209208a1i 11 . . . . . . . . . . . . . . . 16
210181, 58, 207, 209divassd 10088 . . . . . . . . . . . . . . 15
211103, 64, 207, 209divassd 10088 . . . . . . . . . . . . . . 15
212206, 210, 2113eqtr3d 2462 . . . . . . . . . . . . . 14
213184oveq2d 6077 . . . . . . . . . . . . . 14
214186oveq2i 6072 . . . . . . . . . . . . . . . 16
215128, 214syl6eqr 2472 . . . . . . . . . . . . . . 15
216215oveq2d 6077 . . . . . . . . . . . . . 14
217212, 213, 2163eqtr4d 2464 . . . . . . . . . . . . 13
218193, 217oveq12d 6079 . . . . . . . . . . . 12
219178, 183, 2183eqtrd 2458 . . . . . . . . . . 11
220219oveq2d 6077 . . . . . . . . . 10
221165, 176, 2203eqtr4d 2464 . . . . . . . . 9
222101, 102, 2213eqtrd 2458 . . . . . . . 8
223222negeqd 9550 . . . . . . 7
22465, 79, 60, 89addsub4d 9712 . . . . . . 7
22599, 223, 2243eqtr3rd 2463 . . . . . 6
226225oveq2d 6077 . . . . 5
2273, 181subcld 9665 . . . . . . . . 9
228177, 227eqeltrd 2496 . . . . . . . 8
229228, 182mulcld 9352 . . . . . . 7
230112, 229addcld 9351 . . . . . 6
23171, 230negsubd 9671 . . . . 5
23296, 226, 2313eqtrd 2458 . . . 4
23393, 95, 2323eqtrd 2458 . . 3
234233oveq2d 6077 . 2
235230, 71pncan3d 9668 . 2
236234, 235eqtr2d 2455 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1687  e.wcel 1749  =/=wne 2585  (class class class)co 6061   cc 9226  0cc0 9228  1c1 9229   caddc 9231   cmul 9233   cmin 9541  -ucneg 9542   cdiv 9939  2c2 10317  3c3 10318  4c4 10319  5c5 10320  6c6 10321  8c8 10323   cn0 10525  ;cdc 10700   cexp 11806
This theorem is referenced by:  quart1  21992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-8 1751  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-sep 4388  ax-nul 4396  ax-pow 4442  ax-pr 4503  ax-un 6342  ax-cnex 9284  ax-resscn 9285  ax-1cn 9286  ax-icn 9287  ax-addcl 9288  ax-addrcl 9289  ax-mulcl 9290  ax-mulrcl 9291  ax-mulcom 9292  ax-addass 9293  ax-mulass 9294  ax-distr 9295  ax-i2m1 9296  ax-1ne0 9297  ax-1rid 9298  ax-rnegex 9299  ax-rrecex 9300  ax-cnre 9301  ax-pre-lttri 9302  ax-pre-lttrn 9303  ax-pre-ltadd 9304  ax-pre-mulgt0 9305
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3or 951  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-eu 2248  df-mo 2249  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-nel 2588  df-ral 2699  df-rex 2700  df-reu 2701  df-rmo 2702  df-rab 2703  df-v 2953  df-sbc 3165  df-csb 3266  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-pss 3321  df-nul 3615  df-if 3769  df-pw 3839  df-sn 3859  df-pr 3860  df-tp 3861  df-op 3862  df-uni 4067  df-iun 4148  df-br 4268  df-opab 4326  df-mpt 4327  df-tr 4361  df-eprel 4603  df-id 4607  df-po 4612  df-so 4613  df-fr 4650  df-we 4652  df-ord 4693  df-on 4694  df-lim 4695  df-suc 4696  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5353  df-fun 5392  df-fn 5393  df-f 5394  df-f1 5395  df-fo 5396  df-f1o 5397  df-fv 5398  df-riota 6020  df-ov 6064  df-oprab 6065  df-mpt2 6066  df-om 6447  df-2nd 6547  df-recs 6791  df-rdg 6825  df-er 7062  df-en 7270  df-dom 7271  df-sdom 7272  df-pnf 9366  df-mnf 9367  df-xr 9368  df-ltxr 9369  df-le 9370  df-sub 9543  df-neg 9544  df-div 9940  df-nn 10269  df-2 10326  df-3 10327  df-4 10328  df-5 10329  df-6 10330  df-7 10331  df-8 10332  df-9 10333  df-10 10334  df-n0 10526  df-z 10592  df-dec 10701  df-uz 10807  df-seq 11748  df-exp 11807
  Copyright terms: Public domain W3C validator