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

Theorem cubic2 20641
 Description: The solution to the general cubic equation, for arbitrary choices and of the square and cube roots. (Contributed by Mario Carneiro, 23-Apr-2015.)
Hypotheses
Ref Expression
cubic2.a
cubic2.z
cubic2.b
cubic2.c
cubic2.d
cubic2.x
cubic2.t
cubic2.3
cubic2.g
cubic2.2
cubic2.m
cubic2.n ;
cubic2.0
Assertion
Ref Expression
cubic2
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem cubic2
StepHypRef Expression
1 cubic2.a . . . . . . 7
2 cubic2.x . . . . . . . 8
3 3nn0 10195 . . . . . . . 8
4 expcl 11354 . . . . . . . 8
52, 3, 4sylancl 644 . . . . . . 7
61, 5mulcld 9064 . . . . . 6
7 cubic2.b . . . . . . 7
82sqcld 11476 . . . . . . 7
97, 8mulcld 9064 . . . . . 6
106, 9addcld 9063 . . . . 5
11 cubic2.c . . . . . . 7
1211, 2mulcld 9064 . . . . . 6
13 cubic2.d . . . . . 6
1412, 13addcld 9063 . . . . 5
1510, 14addcld 9063 . . . 4
16 cubic2.z . . . 4
1715, 1, 16diveq0ad 9756 . . 3
1810, 14, 1, 16divdird 9784 . . . . 5
196, 9, 1, 16divdird 9784 . . . . . . 7
205, 1, 16divcan3d 9751 . . . . . . . 8
217, 8, 1, 16div23d 9783 . . . . . . . 8
2220, 21oveq12d 6058 . . . . . . 7
2319, 22eqtrd 2436 . . . . . 6
2412, 13, 1, 16divdird 9784 . . . . . . 7
2511, 2, 1, 16div23d 9783 . . . . . . . 8
2625oveq1d 6055 . . . . . . 7
2724, 26eqtrd 2436 . . . . . 6
2823, 27oveq12d 6058 . . . . 5
2918, 28eqtrd 2436 . . . 4
3029eqeq1d 2412 . . 3
3117, 30bitr3d 247 . 2
327, 1, 16divcld 9746 . . 3
3311, 1, 16divcld 9746 . . 3
3413, 1, 16divcld 9746 . . 3
35 cubic2.t . . . 4
3635, 1, 16divcld 9746 . . 3
373a1i 11 . . . . 5
3835, 1, 16, 37expdivd 11492 . . . 4
39 cubic2.3 . . . . 5
4039oveq1d 6055 . . . 4
41 cubic2.n . . . . . . . 8 ;
42 2cn 10026 . . . . . . . . . . 11
43 expcl 11354 . . . . . . . . . . . 12
447, 3, 43sylancl 644 . . . . . . . . . . 11
45 mulcl 9030 . . . . . . . . . . 11
4642, 44, 45sylancr 645 . . . . . . . . . 10
47 9nn 10096 . . . . . . . . . . . . 13
4847nncni 9966 . . . . . . . . . . . 12
49 mulcl 9030 . . . . . . . . . . . 12
5048, 1, 49sylancr 645 . . . . . . . . . . 11
517, 11mulcld 9064 . . . . . . . . . . 11
5250, 51mulcld 9064 . . . . . . . . . 10
5346, 52subcld 9367 . . . . . . . . 9
54 2nn0 10194 . . . . . . . . . . . 12
55 7nn 10094 . . . . . . . . . . . 12
5654, 55decnncl 10351 . . . . . . . . . . 11 ;
5756nncni 9966 . . . . . . . . . 10 ;
581sqcld 11476 . . . . . . . . . . 11
5958, 13mulcld 9064 . . . . . . . . . 10
60 mulcl 9030 . . . . . . . . . 10 ; ;
6157, 59, 60sylancr 645 . . . . . . . . 9 ;
6253, 61addcld 9063 . . . . . . . 8 ;
6341, 62eqeltrd 2478 . . . . . . 7
64 cubic2.g . . . . . . 7
6563, 64addcld 9063 . . . . . 6
6642a1i 11 . . . . . 6
67 expcl 11354 . . . . . . 7
681, 3, 67sylancl 644 . . . . . 6
69 2ne0 10039 . . . . . . 7
7069a1i 11 . . . . . 6
713nn0zi 10262 . . . . . . . 8
7271a1i 11 . . . . . . 7
731, 16, 72expne0d 11484 . . . . . 6
7465, 66, 68, 70, 73divdiv32d 9771 . . . . 5
7563, 64, 68, 73divdird 9784 . . . . . 6
7675oveq1d 6055 . . . . 5
7774, 76eqtrd 2436 . . . 4
7838, 40, 773eqtrd 2440 . . 3
7964, 68, 73divcld 9746 . . 3
8064, 68, 73sqdivd 11491 . . . 4
81 cubic2.2 . . . . 5
8281oveq1d 6055 . . . 4
8363sqcld 11476 . . . . . 6
84 4cn 10030 . . . . . . 7
85 cubic2.m . . . . . . . . 9
867sqcld 11476 . . . . . . . . . 10
87 3cn 10028 . . . . . . . . . . 11
881, 11mulcld 9064 . . . . . . . . . . 11
89 mulcl 9030 . . . . . . . . . . 11
9087, 88, 89sylancr 645 . . . . . . . . . 10
9186, 90subcld 9367 . . . . . . . . 9
9285, 91eqeltrd 2478 . . . . . . . 8
93 expcl 11354 . . . . . . . 8
9492, 3, 93sylancl 644 . . . . . . 7
95 mulcl 9030 . . . . . . 7
9684, 94, 95sylancr 645 . . . . . 6
9768sqcld 11476 . . . . . 6
98 sqne0 11403 . . . . . . . 8
9968, 98syl 16 . . . . . . 7
10073, 99mpbird 224 . . . . . 6
10183, 96, 97, 100divsubdird 9785 . . . . 5
10263, 68, 73sqdivd 11491 . . . . . 6
103 2z 10268 . . . . . . . . . . . 12
104103a1i 11 . . . . . . . . . . 11
1051, 16, 104expne0d 11484 . . . . . . . . . 10
10692, 58, 105, 37expdivd 11492 . . . . . . . . 9
10742, 87mulcomi 9052 . . . . . . . . . . . 12
108107oveq2i 6051 . . . . . . . . . . 11
10954a1i 11 . . . . . . . . . . . 12
1101, 37, 109expmuld 11481 . . . . . . . . . . 11
1111, 109, 37expmuld 11481 . . . . . . . . . . 11
112108, 110, 1113eqtr3a 2460 . . . . . . . . . 10
113112oveq2d 6056 . . . . . . . . 9
114106, 113eqtrd 2436 . . . . . . . 8
115114oveq2d 6056 . . . . . . 7
11684a1i 11 . . . . . . . 8
117116, 94, 97, 100divassd 9781 . . . . . . 7
118115, 117eqtr4d 2439 . . . . . 6
119102, 118oveq12d 6058 . . . . 5
120101, 119eqtr4d 2439 . . . 4
12180, 82, 1203eqtrd 2440 . . 3
12286, 90, 58, 105divsubdird 9785 . . . 4
12385oveq1d 6055 . . . 4
1247, 1, 16sqdivd 11491 . . . . 5
1251sqvald 11475 . . . . . . . . 9
126125oveq2d 6056 . . . . . . . 8
12711, 1, 1, 16, 16divcan5d 9772 . . . . . . . 8
128126, 127eqtr2d 2437 . . . . . . 7
129128oveq2d 6056 . . . . . 6
13087a1i 11 . . . . . . 7
131130, 88, 58, 105divassd 9781 . . . . . 6
132129, 131eqtr4d 2439 . . . . 5
133124, 132oveq12d 6058 . . . 4
134122, 123, 1333eqtr4d 2446 . . 3
13553, 61, 68, 73divdird 9784 . . . 4 ; ;
13641oveq1d 6055 . . . 4 ;
1377, 1, 16, 37expdivd 11492 . . . . . . . . 9
138137oveq2d 6056 . . . . . . . 8
13966, 44, 68, 73divassd 9781 . . . . . . . 8
140138, 139eqtr4d 2439 . . . . . . 7
14148a1i 11 . . . . . . . . 9
1421, 51mulcld 9064 . . . . . . . . 9
143141, 142, 68, 73divassd 9781 . . . . . . . 8
144141, 1, 51mulassd 9067 . . . . . . . . 9
145144oveq1d 6055 . . . . . . . 8
14651, 58, 1, 105, 16divcan5d 9772 . . . . . . . . . 10
147 df-3 10015 . . . . . . . . . . . . . 14
148147oveq2i 6051 . . . . . . . . . . . . 13
149 expp1 11343 . . . . . . . . . . . . . 14
1501, 54, 149sylancl 644 . . . . . . . . . . . . 13
151148, 150syl5eq 2448 . . . . . . . . . . . 12
15258, 1mulcomd 9065 . . . . . . . . . . . 12
153151, 152eqtrd 2436 . . . . . . . . . . 11
154153oveq2d 6056 . . . . . . . . . 10
1557, 1, 11, 1, 16, 16divmuldivd 9787 . . . . . . . . . . 11
156125oveq2d 6056 . . . . . . . . . . 11
157155, 156eqtr4d 2439 . . . . . . . . . 10
158146, 154, 1573eqtr4rd 2447 . . . . . . . . 9
159158oveq2d 6056 . . . . . . . 8
160143, 145, 1593eqtr4rd 2447 . . . . . . 7
161140, 160oveq12d 6058 . . . . . 6
16246, 52, 68, 73divsubdird 9785 . . . . . 6
163161, 162eqtr4d 2439 . . . . 5
164151oveq2d 6056 . . . . . . . 8
16513, 1, 58, 16, 105divcan5d 9772 . . . . . . . 8
166164, 165eqtr2d 2437 . . . . . . 7
167166oveq2d 6056 . . . . . 6 ; ;
16857a1i 11 . . . . . . 7 ;
169168, 59, 68, 73divassd 9781 . . . . . 6 ; ;
170167, 169eqtr4d 2439 . . . . 5 ; ;
171163, 170oveq12d 6058 . . . 4 ; ;
172135, 136, 1713eqtr4d 2446 . . 3 ;
173 cubic2.0 . . . 4
17435, 1, 173, 16divne0d 9762 . . 3
17532, 33, 34, 2, 36, 78, 79, 121, 134, 172, 174mcubic 20640 . 2
176 oveq1 6047 . . . . . . . 8
177 3nn 10090 . . . . . . . . 9
178 0exp 11370 . . . . . . . . 9
179177, 178ax-mp 8 . . . . . . . 8
180176, 179syl6eq 2452 . . . . . . 7
181 ax-1ne0 9015 . . . . . . . . 9
182181necomi 2649 . . . . . . . 8
183182a1i 11 . . . . . . 7
184180, 183eqnetrd 2585 . . . . . 6
185184necon2i 2614 . . . . 5
186 simprl 733 . . . . . . . . . . . . . . . 16
18735adantr 452 . . . . . . . . . . . . . . . 16
1881adantr 452 . . . . . . . . . . . . . . . 16
18916adantr 452 . . . . . . . . . . . . . . . 16
190186, 187, 188, 189divassd 9781 . . . . . . . . . . . . . . 15
191190eqcomd 2409 . . . . . . . . . . . . . 14
192191oveq2d 6056 . . . . . . . . . . . . 13
1937adantr 452 . . . . . . . . . . . . . 14
194186, 187mulcld 9064 . . . . . . . . . . . . . 14
195193, 194, 188, 189divdird 9784 . . . . . . . . . . . . 13
196192, 195eqtr4d 2439 . . . . . . . . . . . 12
19792adantr 452 . . . . . . . . . . . . . . 15
198197, 188, 189divcld 9746 . . . . . . . . . . . . . 14
199 simprr 734 . . . . . . . . . . . . . . 15
200173adantr 452 . . . . . . . . . . . . . . 15
201186, 187, 199, 200mulne0d 9630 . . . . . . . . . . . . . 14
202198, 194, 188, 201, 189divcan7d 9774 . . . . . . . . . . . . 13
203197, 188, 188, 189, 189divdiv1d 9777 . . . . . . . . . . . . . . 15
204188sqvald 11475 . . . . . . . . . . . . . . . 16
205204oveq2d 6056 . . . . . . . . . . . . . . 15
206203, 205eqtr4d 2439 . . . . . . . . . . . . . 14
207206, 190oveq12d 6058 . . . . . . . . . . . . 13
208197, 188, 194, 189, 201divdiv32d 9771 . . . . . . . . . . . . 13
209202, 207, 2083eqtr3d 2444 . . . . . . . . . . . 12
210196, 209oveq12d 6058 . . . . . . . . . . 11
211193, 194addcld 9063 . . . . . . . . . . . 12
212197, 194, 201divcld 9746 . . . . . . . . . . . 12
213211, 212, 188, 189divdird 9784 . . . . . . . . . . 11
214210, 213eqtr4d 2439 . . . . . . . . . 10
215214oveq1d 6055 . . . . . . . . 9
216211, 212addcld 9063 . . . . . . . . . 10
21787a1i 11 . . . . . . . . . 10
218 3ne0 10041 . . . . . . . . . . 11
219218a1i 11 . . . . . . . . . 10
220216, 188, 217, 189, 219divdiv1d 9777 . . . . . . . . 9
221 mulcom 9032 . . . . . . . . . . 11
222188, 87, 221sylancl 644 . . . . . . . . . 10
223222oveq2d 6056 . . . . . . . . 9
224215, 220, 2233eqtrd 2440 . . . . . . . 8
225224negeqd 9256 . . . . . . 7
226225eqeq2d 2415 . . . . . 6
227226anassrs 630 . . . . 5
228185, 227sylan2 461 . . . 4
229228pm5.32da 623 . . 3
230229rexbidva 2683 . 2
23131, 175, 2303bitrd 271 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   wceq 1649   wcel 1721   wne 2567  wrex 2667  (class class class)co 6040  cc 8944  cc0 8946  c1 8947   caddc 8949   cmul 8951   cmin 9247  cneg 9248   cdiv 9633  cn 9956  c2 10005  c3 10006  c4 10007  c7 10010  c9 10012  cn0 10177  cz 10238  ;cdc 10338  cexp 11337 This theorem is referenced by:  cubic  20642 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 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024 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 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-sup 7404  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-4 10016  df-5 10017  df-6 10018  df-7 10019  df-8 10020  df-9 10021  df-10 10022  df-n0 10178  df-z 10239  df-dec 10339  df-uz 10445  df-rp 10569  df-fz 11000  df-seq 11279  df-exp 11338  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-dvds 12808
 Copyright terms: Public domain W3C validator