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

Theorem quart 20640
 Description: The quartic equation, writing out all roots using square and cube root functions so that only direct substitutions remain, and we can actually claim to have a "quartic equation". Naturally, this theorem is ridiculously long (see quartfull 24718) if all the substitutions are performed. (Contributed by Mario Carneiro, 6-May-2015.)
Hypotheses
Ref Expression
quart.a
quart.b
quart.c
quart.d
quart.x
quart.e
quart.p
quart.q
quart.r ; ;;
quart.u ;
quart.v ; ;
quart.w
quart.s
quart.m
quart.t
quart.t0
quart.m0
quart.i
quart.j
Assertion
Ref Expression
quart

Proof of Theorem quart
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 quart.a . . . 4
2 quart.b . . . 4
3 quart.c . . . 4
4 quart.d . . . 4
5 quart.p . . . 4
6 quart.q . . . 4
7 quart.r . . . 4 ; ;;
8 quart.x . . . 4
9 quart.e . . . . . 6
109oveq2d 6050 . . . . 5
11 4cn 10020 . . . . . . . 8
1211a1i 11 . . . . . . 7
13 4nn 10081 . . . . . . . . 9
1413nnne0i 9980 . . . . . . . 8
1514a1i 11 . . . . . . 7
161, 12, 15divcld 9736 . . . . . 6
178, 16subnegd 9364 . . . . 5
1810, 17eqtrd 2433 . . . 4
191, 2, 3, 4, 5, 6, 7, 8, 18quart1 20635 . . 3
2019eqeq1d 2409 . 2
211, 2, 3, 4, 5, 6, 7quart1cl 20633 . . . 4
2221simp1d 969 . . 3
2321simp2d 970 . . 3
2416negcld 9344 . . . . 5
259, 24eqeltrd 2475 . . . 4
268, 25subcld 9357 . . 3
27 quart.u . . . . 5 ;
28 quart.v . . . . 5 ; ;
29 quart.w . . . . 5
30 quart.s . . . . 5
31 quart.m . . . . 5
32 quart.t . . . . 5
33 quart.t0 . . . . 5
341, 2, 3, 4, 1, 9, 5, 6, 7, 27, 28, 29, 30, 31, 32, 33quartlem3 20638 . . . 4
3534simp1d 969 . . 3
3630oveq2d 6050 . . . . . 6
3734simp2d 970 . . . . . . . 8
3837sqrcld 12180 . . . . . . 7
39 2cn 10016 . . . . . . . 8
4039a1i 11 . . . . . . 7
41 2ne0 10029 . . . . . . . 8
4241a1i 11 . . . . . . 7
4338, 40, 42divcan2d 9738 . . . . . 6
4436, 43eqtrd 2433 . . . . 5
4544oveq1d 6049 . . . 4
4637sqsqrd 12182 . . . 4
4745, 46eqtr2d 2434 . . 3
48 quart.m0 . . 3
49 quart.i . . . . 5
50 quart.j . . . . 5
511, 2, 3, 4, 1, 9, 5, 6, 7, 27, 28, 29, 30, 31, 32, 33, 48, 49, 50quartlem4 20639 . . . 4
5251simp2d 970 . . 3
5349oveq1d 6049 . . . 4
5435sqcld 11462 . . . . . . . 8
5554negcld 9344 . . . . . . 7
5622halfcld 10158 . . . . . . 7
5755, 56subcld 9357 . . . . . 6
5823, 12, 15divcld 9736 . . . . . . 7
5951simp1d 969 . . . . . . 7
6058, 35, 59divcld 9736 . . . . . 6
6157, 60addcld 9054 . . . . 5
6261sqsqrd 12182 . . . 4
6353, 62eqtrd 2433 . . 3
6421simp3d 971 . . 3
65 ax-1cn 8995 . . . . . 6
6665a1i 11 . . . . 5
67 3nn 10080 . . . . . . 7
6867nnzi 10251 . . . . . 6
69 1exp 11350 . . . . . 6
7068, 69mp1i 12 . . . . 5
7134simp3d 971 . . . . . . . . . . 11
7271mulid2d 9053 . . . . . . . . . 10
7372oveq2d 6050 . . . . . . . . 9
7472oveq2d 6050 . . . . . . . . 9
7573, 74oveq12d 6052 . . . . . . . 8
7675oveq1d 6049 . . . . . . 7
7776negeqd 9246 . . . . . 6
7831, 77eqtr4d 2436 . . . . 5
79 oveq1 6041 . . . . . . . 8
8079eqeq1d 2409 . . . . . . 7
81 oveq1 6041 . . . . . . . . . . . 12
8281oveq2d 6050 . . . . . . . . . . 11
8381oveq2d 6050 . . . . . . . . . . 11
8482, 83oveq12d 6052 . . . . . . . . . 10
8584oveq1d 6049 . . . . . . . . 9
8685negeqd 9246 . . . . . . . 8
8786eqeq2d 2412 . . . . . . 7
8880, 87anbi12d 692 . . . . . 6
8988rspcev 3009 . . . . 5
9066, 70, 78, 89syl12anc 1182 . . . 4
91 mulcl 9021 . . . . . 6
9239, 22, 91sylancr 645 . . . . 5
9322sqcld 11462 . . . . . 6
94 mulcl 9021 . . . . . . 7
9511, 64, 94sylancr 645 . . . . . 6
9693, 95subcld 9357 . . . . 5
9723sqcld 11462 . . . . . 6
9897negcld 9344 . . . . 5
9932oveq1d 6049 . . . . . 6
1001, 2, 3, 4, 1, 9, 5, 6, 7, 27, 28, 29quartlem2 20637 . . . . . . . . . 10
101100simp2d 970 . . . . . . . . 9
102100simp3d 971 . . . . . . . . 9
103101, 102addcld 9054 . . . . . . . 8
104103halfcld 10158 . . . . . . 7
105 cxproot 20520 . . . . . . 7
106104, 67, 105sylancl 644 . . . . . 6
10799, 106eqtrd 2433 . . . . 5
10829oveq1d 6049 . . . . . 6
109101sqcld 11462 . . . . . . . 8
110100simp1d 969 . . . . . . . . . 10
111 3nn0 10185 . . . . . . . . . 10
112 expcl 11340 . . . . . . . . . 10
113110, 111, 112sylancl 644 . . . . . . . . 9
114 mulcl 9021 . . . . . . . . 9
11511, 113, 114sylancr 645 . . . . . . . 8
116109, 115subcld 9357 . . . . . . 7
117116sqsqrd 12182 . . . . . 6
118108, 117eqtrd 2433 . . . . 5
11922, 23, 64, 27, 28quartlem1 20636 . . . . . 6 ;
120119simpld 446 . . . . 5
121119simprd 450 . . . . 5 ;
12292, 96, 98, 37, 71, 107, 102, 118, 120, 121, 33mcubic 20626 . . . 4
12390, 122mpbird 224 . . 3
12451simp3d 971 . . 3
12550oveq1d 6049 . . . 4
12657, 60subcld 9357 . . . . 5
127126sqsqrd 12182 . . . 4
128125, 127eqtrd 2433 . . 3
12922, 23, 26, 35, 47, 48, 52, 63, 64, 123, 124, 128dquart 20632 . 2
13035negcld 9344 . . . . . . . 8
131130, 52addcld 9054 . . . . . . 7
1328, 25, 131subaddd 9375 . . . . . 6
13325, 35negsubd 9363 . . . . . . . . 9
134133oveq1d 6049 . . . . . . . 8
13525, 130, 52addassd 9057 . . . . . . . 8
136134, 135eqtr3d 2435 . . . . . . 7
137136eqeq1d 2409 . . . . . 6
138132, 137bitr4d 248 . . . . 5
139 eqcom 2403 . . . . 5
140138, 139syl6bb 253 . . . 4
141130, 52subcld 9357 . . . . . . 7
1428, 25, 141subaddd 9375 . . . . . 6
143133oveq1d 6049 . . . . . . . 8
14425, 130, 52addsubassd 9377 . . . . . . . 8
145143, 144eqtr3d 2435 . . . . . . 7
146145eqeq1d 2409 . . . . . 6
147142, 146bitr4d 248 . . . . 5
148 eqcom 2403 . . . . 5
149147, 148syl6bb 253 . . . 4
150140, 149orbi12d 691 . . 3
15135, 124addcld 9054 . . . . . . 7
1528, 25, 151subaddd 9375 . . . . . 6
15325, 35, 124addassd 9057 . . . . . . 7
154153eqeq1d 2409 . . . . . 6
155152, 154bitr4d 248 . . . . 5
156 eqcom 2403 . . . . 5
157155, 156syl6bb 253 . . . 4
15835, 124subcld 9357 . . . . . . 7
1598, 25, 158subaddd 9375 . . . . . 6
16025, 35, 124addsubassd 9377 . . . . . . 7
161160eqeq1d 2409 . . . . . 6
162159, 161bitr4d 248 . . . . 5
163 eqcom 2403 . . . . 5
164162, 163syl6bb 253 . . . 4
165157, 164orbi12d 691 . . 3
166150, 165orbi12d 691 . 2
16720, 129, 1663bitrd 271 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wo 358   wa 359   wceq 1649   wcel 1721   wne 2564  wrex 2664  cfv 5408  (class class class)co 6034  cc 8935  cc0 8937  c1 8938   caddc 8940   cmul 8942   cmin 9237  cneg 9238   cdiv 9623  cn 9946  c2 9995  c3 9996  c4 9997  c5 9998  c6 9999  c7 10000  c8 10001  c9 10002  cn0 10167  cz 10228  ;cdc 10328  cexp 11323  csqr 11979   ccxp 20392 This theorem is referenced by:  quartfull  24718 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-rep 4275  ax-sep 4285  ax-nul 4293  ax-pow 4332  ax-pr 4358  ax-un 4655  ax-inf2 7543  ax-cnex 8993  ax-resscn 8994  ax-1cn 8995  ax-icn 8996  ax-addcl 8997  ax-addrcl 8998  ax-mulcl 8999  ax-mulrcl 9000  ax-mulcom 9001  ax-addass 9002  ax-mulass 9003  ax-distr 9004  ax-i2m1 9005  ax-1ne0 9006  ax-1rid 9007  ax-rnegex 9008  ax-rrecex 9009  ax-cnre 9010  ax-pre-lttri 9011  ax-pre-lttrn 9012  ax-pre-ltadd 9013  ax-pre-mulgt0 9014  ax-pre-sup 9015  ax-addf 9016  ax-mulf 9017 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-nel 2567  df-ral 2668  df-rex 2669  df-reu 2670  df-rmo 2671  df-rab 2672  df-v 2915  df-sbc 3119  df-csb 3209  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-pss 3293  df-nul 3586  df-if 3697  df-pw 3758  df-sn 3777  df-pr 3778  df-tp 3779  df-op 3780  df-uni 3972  df-int 4007  df-iun 4051  df-iin 4052  df-br 4168  df-opab 4222  df-mpt 4223  df-tr 4258  df-eprel 4449  df-id 4453  df-po 4458  df-so 4459  df-fr 4496  df-se 4497  df-we 4498  df-ord 4539  df-on 4540  df-lim 4541  df-suc 4542  df-om 4800  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5372  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-isom 5417  df-ov 6037  df-oprab 6038  df-mpt2 6039  df-of 6258  df-1st 6302  df-2nd 6303  df-riota 6499  df-recs 6583  df-rdg 6618  df-1o 6674  df-2o 6675  df-oadd 6678  df-er 6855  df-map 6970  df-pm 6971  df-ixp 7014  df-en 7060  df-dom 7061  df-sdom 7062  df-fin 7063  df-fi 7365  df-sup 7395  df-oi 7426  df-card 7773  df-cda 7995  df-pnf 9069  df-mnf 9070  df-xr 9071  df-ltxr 9072  df-le 9073  df-sub 9239  df-neg 9240  df-div 9624  df-nn 9947  df-2 10004  df-3 10005  df-4 10006  df-5 10007  df-6 10008  df-7 10009  df-8 10010  df-9 10011  df-10 10012  df-n0 10168  df-z 10229  df-dec 10329  df-uz 10435  df-q 10521  df-rp 10559  df-xneg 10656  df-xadd 10657  df-xmul 10658  df-ioo 10866  df-ioc 10867  df-ico 10868  df-icc 10869  df-fz 10990  df-fzo 11080  df-fl 11143  df-mod 11192  df-seq 11265  df-exp 11324  df-fac 11508  df-bc 11535  df-hash 11560  df-shft 11823  df-cj 11845  df-re 11846  df-im 11847  df-sqr 11981  df-abs 11982  df-limsup 12206  df-clim 12223  df-rlim 12224  df-sum 12421  df-ef 12611  df-sin 12613  df-cos 12614  df-pi 12616  df-dvds 12794  df-struct 13412  df-ndx 13413  df-slot 13414  df-base 13415  df-sets 13416  df-ress 13417  df-plusg 13483  df-mulr 13484  df-starv 13485  df-sca 13486  df-vsca 13487  df-tset 13489  df-ple 13490  df-ds 13492  df-unif 13493  df-hom 13494  df-cco 13495  df-rest 13591  df-topn 13592  df-topgen 13608  df-pt 13609  df-prds 13612  df-xrs 13667  df-0g 13668  df-gsum 13669  df-qtop 13674  df-imas 13675  df-xps 13677  df-mre 13752  df-mrc 13753  df-acs 13755  df-mnd 14631  df-submnd 14680  df-mulg 14756  df-cntz 15057  df-cmn 15355  df-psmet 16635  df-xmet 16636  df-met 16637  df-bl 16638  df-mopn 16639  df-fbas 16640  df-fg 16641  df-cnfld 16645  df-top 16904  df-bases 16906  df-topon 16907  df-topsp 16908  df-cld 17024  df-ntr 17025  df-cls 17026  df-nei 17103  df-lp 17141  df-perf 17142  df-cn 17231  df-cnp 17232  df-haus 17319  df-tx 17533  df-hmeo 17726  df-fil 17817  df-fm 17909  df-flim 17910  df-flf 17911  df-xms 18289  df-ms 18290  df-tms 18291  df-cncf 18847  df-limc 19692  df-dv 19693  df-log 20393  df-cxp 20394
 Copyright terms: Public domain W3C validator