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

Theorem quart1lem 22650
Description: Lemma for quart1 22651. (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 9543 . . . . . . . . . 10
54halfcld 10707 . . . . . . . . 9
61, 5subcld 9856 . . . . . . . 8
7 3nn0 10735 . . . . . . . . . 10
8 expcl 12040 . . . . . . . . . 10
92, 7, 8sylancl 662 . . . . . . . . 9
10 8cn 10545 . . . . . . . . . 10
1110a1i 11 . . . . . . . . 9
12 8nn 10623 . . . . . . . . . . 11
1312nnne0i 10494 . . . . . . . . . 10
1413a1i 11 . . . . . . . . 9
159, 11, 14divcld 10244 . . . . . . . 8
16 4cn 10537 . . . . . . . . . 10
1716a1i 11 . . . . . . . . 9
18 4ne0 10556 . . . . . . . . . 10
1918a1i 11 . . . . . . . . 9
202, 17, 19divcld 10244 . . . . . . . 8
216, 15, 20adddird 9548 . . . . . . 7
22 quart1.q . . . . . . . 8
2322oveq1d 6237 . . . . . . 7
241, 2, 17, 19divassd 10279 . . . . . . . . . 10
252sqvald 12162 . . . . . . . . . . . . . . 15
2625oveq1d 6237 . . . . . . . . . . . . . 14
272, 2, 3mul32d 9716 . . . . . . . . . . . . . 14
2826, 27eqtrd 2495 . . . . . . . . . . . . 13
2928oveq1d 6237 . . . . . . . . . . . 12
30 2cn 10530 . . . . . . . . . . . . . 14
31 4t2e8 10613 . . . . . . . . . . . . . 14
3216, 30, 31mulcomli 9530 . . . . . . . . . . . . 13
3332oveq2i 6233 . . . . . . . . . . . 12
3429, 33syl6eqr 2513 . . . . . . . . . . 11
3530a1i 11 . . . . . . . . . . . 12
36 2ne0 10552 . . . . . . . . . . . . 13
3736a1i 11 . . . . . . . . . . . 12
384, 35, 2, 17, 37, 19divmuldivd 10285 . . . . . . . . . . 11
3934, 38eqtr4d 2498 . . . . . . . . . 10
4024, 39oveq12d 6240 . . . . . . . . 9
411, 5, 20subdird 9938 . . . . . . . . 9
4240, 41eqtr4d 2498 . . . . . . . 8
43 df-4 10520 . . . . . . . . . . . . . 14
4443oveq2i 6233 . . . . . . . . . . . . 13
45 expp1 12029 . . . . . . . . . . . . . 14
462, 7, 45sylancl 662 . . . . . . . . . . . . 13
4744, 46syl5eq 2507 . . . . . . . . . . . 12
4847oveq1d 6237 . . . . . . . . . . 11
499, 2, 11, 14div23d 10281 . . . . . . . . . . 11
5048, 49eqtrd 2495 . . . . . . . . . 10
5150oveq1d 6237 . . . . . . . . 9
5215, 2, 17, 19divassd 10279 . . . . . . . . 9
5351, 52eqtrd 2495 . . . . . . . 8
5442, 53oveq12d 6240 . . . . . . 7
5521, 23, 543eqtr4d 2505 . . . . . 6
561, 2mulcld 9543 . . . . . . . 8
5756, 17, 19divcld 10244 . . . . . . 7
582sqcld 12163 . . . . . . . . 9
5958, 3mulcld 9543 . . . . . . . 8
6059, 11, 14divcld 10244 . . . . . . 7
61 4nn0 10736 . . . . . . . . . 10
62 expcl 12040 . . . . . . . . . 10
632, 61, 62sylancl 662 . . . . . . . . 9
6463, 11, 14divcld 10244 . . . . . . . 8
6564, 17, 19divcld 10244 . . . . . . 7
6657, 60, 65subadd23d 9878 . . . . . 6
6765, 60subcld 9856 . . . . . . 7
6857, 67addcomd 9708 . . . . . 6
6955, 66, 683eqtrd 2499 . . . . 5
70 quart1.r . . . . . 6
71 quart1.d . . . . . . 7
72 1nn0 10733 . . . . . . . . . . . 12
73 6nn 10621 . . . . . . . . . . . 12
7472, 73decnncl 10907 . . . . . . . . . . 11
7574nncni 10470 . . . . . . . . . 10
7675a1i 11 . . . . . . . . 9
7774nnne0i 10494 . . . . . . . . . 10
7877a1i 11 . . . . . . . . 9
7959, 76, 78divcld 10244 . . . . . . . 8
80 3cn 10534 . . . . . . . . . 10
81 2nn0 10734 . . . . . . . . . . . . 13
82 5nn0 10737 . . . . . . . . . . . . 13
8381, 82deccl 10908 . . . . . . . . . . . 12
8483, 73decnncl 10907 . . . . . . . . . . 11
8584nncni 10470 . . . . . . . . . 10
8684nnne0i 10494 . . . . . . . . . 10
8780, 85, 86divcli 10210 . . . . . . . . 9
88 mulcl 9503 . . . . . . . . 9
8987, 63, 88sylancr 663 . . . . . . . 8
9079, 89subcld 9856 . . . . . . 7
9171, 90, 57addsubd 9877 . . . . . 6
9270, 91eqtr4d 2498 . . . . 5
9369, 92oveq12d 6240 . . . 4
9471, 90addcld 9542 . . . . 5
9567, 57, 94ppncand 9896 . . . 4
9667, 71, 90add12d 9728 . . . . 5
9760, 89addcld 9542 . . . . . . . 8
9865, 79addcld 9542 . . . . . . . 8
9997, 98negsubdi2d 9872 . . . . . . 7
10065, 79addcomd 9708 . . . . . . . . . 10
101100oveq2d 6238 . . . . . . . . 9
10260, 89, 79, 65addsub4d 9903 . . . . . . . . 9
10380a1i 11 . . . . . . . . . . . . . . . 16
10485a1i 11 . . . . . . . . . . . . . . . 16
10586a1i 11 . . . . . . . . . . . . . . . 16
106103, 63, 104, 105divassd 10279 . . . . . . . . . . . . . . 15
107103, 63, 104, 105div23d 10281 . . . . . . . . . . . . . . 15
108 1p2e3 10584 . . . . . . . . . . . . . . . . . 18
109108oveq1i 6232 . . . . . . . . . . . . . . . . 17
110 ax-1cn 9477 . . . . . . . . . . . . . . . . . . 19
111110a1i 11 . . . . . . . . . . . . . . . . . 18
11263, 104, 105divcld 10244 . . . . . . . . . . . . . . . . . 18
113111, 35, 112adddird 9548 . . . . . . . . . . . . . . . . 17
114109, 113syl5eqr 2509 . . . . . . . . . . . . . . . 16
115112mulid2d 9541 . . . . . . . . . . . . . . . . 17
116115oveq1d 6237 . . . . . . . . . . . . . . . 16
117114, 116eqtrd 2495 . . . . . . . . . . . . . . 15
118106, 107, 1173eqtr3d 2503 . . . . . . . . . . . . . 14
11943oveq1i 6232 . . . . . . . . . . . . . . . 16
12065, 17, 19divcld 10244 . . . . . . . . . . . . . . . . 17
121103, 111, 120adddird 9548 . . . . . . . . . . . . . . . 16
122119, 121syl5eq 2507 . . . . . . . . . . . . . . 15
12365, 17, 19divcan2d 10246 . . . . . . . . . . . . . . 15
124120mulid2d 9541 . . . . . . . . . . . . . . . . 17
12564, 17, 17, 19, 19divdiv1d 10275 . . . . . . . . . . . . . . . . . 18
126 4t4e16 10967 . . . . . . . . . . . . . . . . . . 19
127126oveq2i 6233 . . . . . . . . . . . . . . . . . 18
128125, 127syl6eq 2511 . . . . . . . . . . . . . . . . 17
12963, 11, 76, 14, 78divdiv1d 10275 . . . . . . . . . . . . . . . . . 18
13010, 75mulcli 9528 . . . . . . . . . . . . . . . . . . . . 21
131130a1i 11 . . . . . . . . . . . . . . . . . . . 20
13210, 75, 13, 77mulne0i 10116 . . . . . . . . . . . . . . . . . . . . 21
133132a1i 11 . . . . . . . . . . . . . . . . . . . 20
13463, 131, 133divcld 10244 . . . . . . . . . . . . . . . . . . 19
135134, 35, 37divcan2d 10246 . . . . . . . . . . . . . . . . . 18
13663, 131, 35, 133, 37divdiv1d 10275 . . . . . . . . . . . . . . . . . . . 20
13710, 75, 30mul32i 9702 . . . . . . . . . . . . . . . . . . . . . 22
138 2exp4 14272 . . . . . . . . . . . . . . . . . . . . . . . 24
139 8t2e16 10982 . . . . . . . . . . . . . . . . . . . . . . . 24
140138, 139eqtr4i 2486 . . . . . . . . . . . . . . . . . . . . . . 23
141140, 138oveq12i 6234 . . . . . . . . . . . . . . . . . . . . . 22
142 4p4e8 10596 . . . . . . . . . . . . . . . . . . . . . . . 24
143142oveq2i 6233 . . . . . . . . . . . . . . . . . . . . . . 23
144 expadd 12063 . . . . . . . . . . . . . . . . . . . . . . . 24
14530, 61, 61, 144mp3an 1315 . . . . . . . . . . . . . . . . . . . . . . 23
146 2exp8 14274 . . . . . . . . . . . . . . . . . . . . . . 23
147143, 145, 1463eqtr3i 2491 . . . . . . . . . . . . . . . . . . . . . 22
148137, 141, 1473eqtr2i 2489 . . . . . . . . . . . . . . . . . . . . 21
149148oveq2i 6233 . . . . . . . . . . . . . . . . . . . 20
150136, 149syl6eq 2511 . . . . . . . . . . . . . . . . . . 19
151150oveq2d 6238 . . . . . . . . . . . . . . . . . 18
152129, 135, 1513eqtr2d 2501 . . . . . . . . . . . . . . . . 17
153124, 128, 1523eqtrd 2499 . . . . . . . . . . . . . . . 16
154153oveq2d 6238 . . . . . . . . . . . . . . 15
155122, 123, 1543eqtr3d 2503 . . . . . . . . . . . . . 14
156118, 155oveq12d 6240 . . . . . . . . . . . . 13
157 mulcl 9503 . . . . . . . . . . . . . . 15
15880, 120, 157sylancr 663 . . . . . . . . . . . . . 14
159 mulcl 9503 . . . . . . . . . . . . . . 15
16030, 112, 159sylancr 663 . . . . . . . . . . . . . 14
161112, 158, 160pnpcan2d 9894 . . . . . . . . . . . . 13
162156, 161eqtrd 2495 . . . . . . . . . . . 12
163162oveq2d 6238 . . . . . . . . . . 11
16479, 112, 158addsub12d 9879 . . . . . . . . . . 11
165163, 164eqtrd 2495 . . . . . . . . . 10
16659, 11, 35, 14, 37divdiv1d 10275 . . . . . . . . . . . . . . . 16
167139oveq2i 6233 . . . . . . . . . . . . . . . 16
168166, 167syl6eq 2511 . . . . . . . . . . . . . . 15
169168oveq2d 6238 . . . . . . . . . . . . . 14
17060, 35, 37divcan2d 10246 . . . . . . . . . . . . . 14
171792timesd 10705 . . . . . . . . . . . . . 14
172169, 170, 1713eqtr3d 2503 . . . . . . . . . . . . 13
173172oveq1d 6237 . . . . . . . . . . . 12
17479, 79pncand 9857 . . . . . . . . . . . 12
175173, 174eqtrd 2495 . . . . . . . . . . 11
176175oveq1d 6237 . . . . . . . . . 10
177 quart1.p . . . . . . . . . . . . 13
178177oveq1d 6237 . . . . . . . . . . . 12
17980, 10, 13divcli 10210 . . . . . . . . . . . . . 14
180 mulcl 9503 . . . . . . . . . . . . . 14
181179, 58, 180sylancr 663 . . . . . . . . . . . . 13
18220sqcld 12163 . . . . . . . . . . . . 13
1833, 181, 182subdird 9938 . . . . . . . . . . . 12
1842, 17, 19sqdivd 12178 . . . . . . . . . . . . . . . 16
18516sqvali 12102 . . . . . . . . . . . . . . . . . 18
186185, 126eqtri 2483 . . . . . . . . . . . . . . . . 17
187186oveq2i 6233 . . . . . . . . . . . . . . . 16
188184, 187syl6eq 2511 . . . . . . . . . . . . . . 15
189188oveq2d 6238 . . . . . . . . . . . . . 14
1903, 58, 76, 78divassd 10279 . . . . . . . . . . . . . 14
1913, 58mulcomd 9544 . . . . . . . . . . . . . . 15
192191oveq1d 6237 . . . . . . . . . . . . . 14
193189, 190, 1923eqtr2d 2501 . . . . . . . . . . . . 13
194179a1i 11 . . . . . . . . . . . . . . . . . 18
195194, 58, 58mulassd 9546 . . . . . . . . . . . . . . . . 17
196103, 63, 11, 14div23d 10281 . . . . . . . . . . . . . . . . . 18
197 2p2e4 10577 . . . . . . . . . . . . . . . . . . . . 21
198197oveq2i 6233 . . . . . . . . . . . . . . . . . . . 20
19981a1i 11 . . . . . . . . . . . . . . . . . . . . 21
2002, 199, 199expaddd 12167 . . . . . . . . . . . . . . . . . . . 20
201198, 200syl5eqr 2509 . . . . . . . . . . . . . . . . . . 19
202201oveq2d 6238 . . . . . . . . . . . . . . . . . 18
203196, 202eqtrd 2495 . . . . . . . . . . . . . . . . 17
204103, 63, 11, 14divassd 10279 . . . . . . . . . . . . . . . . 17
205195, 203, 2043eqtr2d 2501 . . . . . . . . . . . . . . . 16
206205oveq1d 6237 . . . . . . . . . . . . . . 15
207186, 76syl5eqel 2546 . . . . . . . . . . . . . . . 16
208186, 77eqnetri 2749 . . . . . . . . . . . . . . . . 17
209208a1i 11 . . . . . . . . . . . . . . . 16
210181, 58, 207, 209divassd 10279 . . . . . . . . . . . . . . 15
211103, 64, 207, 209divassd 10279 . . . . . . . . . . . . . . 15
212206, 210, 2113eqtr3d 2503 . . . . . . . . . . . . . 14
213184oveq2d 6238 . . . . . . . . . . . . . 14
214186oveq2i 6233 . . . . . . . . . . . . . . . 16
215128, 214syl6eqr 2513 . . . . . . . . . . . . . . 15
216215oveq2d 6238 . . . . . . . . . . . . . 14
217212, 213, 2163eqtr4d 2505 . . . . . . . . . . . . 13
218193, 217oveq12d 6240 . . . . . . . . . . . 12
219178, 183, 2183eqtrd 2499 . . . . . . . . . . 11
220219oveq2d 6238 . . . . . . . . . 10
221165, 176, 2203eqtr4d 2505 . . . . . . . . 9
222101, 102, 2213eqtrd 2499 . . . . . . . 8
223222negeqd 9741 . . . . . . 7
22465, 79, 60, 89addsub4d 9903 . . . . . . 7
22599, 223, 2243eqtr3rd 2504 . . . . . 6
226225oveq2d 6238 . . . . 5
2273, 181subcld 9856 . . . . . . . . 9
228177, 227eqeltrd 2542 . . . . . . . 8
229228, 182mulcld 9543 . . . . . . 7
230112, 229addcld 9542 . . . . . 6
23171, 230negsubd 9862 . . . . 5
23296, 226, 2313eqtrd 2499 . . . 4
23393, 95, 2323eqtrd 2499 . . 3
234233oveq2d 6238 . 2
235230, 71pncan3d 9859 . 2
236234, 235eqtr2d 2496 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1370  e.wcel 1758  =/=wne 2648  (class class class)co 6222   cc 9417  0cc0 9419  1c1 9420   caddc 9422   cmul 9424   cmin 9732  -ucneg 9733   cdiv 10130  2c2 10509  3c3 10510  4c4 10511  5c5 10512  6c6 10513  8c8 10515   cn0 10717  ;cdc 10894   cexp 12022
This theorem is referenced by:  quart1  22651
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4530  ax-nul 4538  ax-pow 4587  ax-pr 4648  ax-un 6505  ax-cnex 9475  ax-resscn 9476  ax-1cn 9477  ax-icn 9478  ax-addcl 9479  ax-addrcl 9480  ax-mulcl 9481  ax-mulrcl 9482  ax-mulcom 9483  ax-addass 9484  ax-mulass 9485  ax-distr 9486  ax-i2m1 9487  ax-1ne0 9488  ax-1rid 9489  ax-rnegex 9490  ax-rrecex 9491  ax-cnre 9492  ax-pre-lttri 9493  ax-pre-lttrn 9494  ax-pre-ltadd 9495  ax-pre-mulgt0 9496
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2805  df-rex 2806  df-reu 2807  df-rmo 2808  df-rab 2809  df-v 3083  df-sbc 3298  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3752  df-if 3906  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4209  df-iun 4290  df-br 4410  df-opab 4468  df-mpt 4469  df-tr 4503  df-eprel 4749  df-id 4753  df-po 4758  df-so 4759  df-fr 4796  df-we 4798  df-ord 4839  df-on 4840  df-lim 4841  df-suc 4842  df-xp 4963  df-rel 4964  df-cnv 4965  df-co 4966  df-dm 4967  df-rn 4968  df-res 4969  df-ima 4970  df-iota 5500  df-fun 5539  df-fn 5540  df-f 5541  df-f1 5542  df-fo 5543  df-f1o 5544  df-fv 5545  df-riota 6183  df-ov 6225  df-oprab 6226  df-mpt2 6227  df-om 6610  df-2nd 6711  df-recs 6966  df-rdg 7000  df-er 7235  df-en 7445  df-dom 7446  df-sdom 7447  df-pnf 9557  df-mnf 9558  df-xr 9559  df-ltxr 9560  df-le 9561  df-sub 9734  df-neg 9735  df-div 10131  df-nn 10461  df-2 10518  df-3 10519  df-4 10520  df-5 10521  df-6 10522  df-7 10523  df-8 10524  df-9 10525  df-10 10526  df-n0 10718  df-z 10785  df-dec 10895  df-uz 11001  df-seq 11964  df-exp 12023
  Copyright terms: Public domain W3C validator