dquart - Metamath Proof Explorer

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

Theorem dquart 23300

Description: Solve a depressed quartic equation. To eliminate

, which is the square root of a solution

to the resolvent cubic equation, apply cubic 23296 or one of its variants. (Contributed by Mario Carneiro, 6-May-2015.)

**Hypotheses**
Ref	Expression
dquart.b
dquart.c
dquart.x
dquart.s
dquart.m
dquart.m0
dquart.i
dquart.i2
dquart.d
dquart.3
dquart.j
dquart.j2

**Assertion**
Ref	Expression
dquart	$\/$ $\/$ $\/$

**Proof of Theorem dquart**
Step	Hyp	Ref	Expression
1		dquart.x	. . . . . . . . 9
2	1	sqcld 12210	. . . . . . . 8
3		dquart.m	. . . . . . . . . . 11
4		2cn 10523	. . . . . . . . . . . . 13
5		dquart.s	. . . . . . . . . . . . 13
6		mulcl 9487	. . . . . . . . . . . . 13 $/\$
7	4, 5, 6	sylancr 661	. . . . . . . . . . . 12
8	7	sqcld 12210	. . . . . . . . . . 11
9	3, 8	eqeltrd 2470	. . . . . . . . . 10
10		dquart.b	. . . . . . . . . 10
11	9, 10	addcld 9526	. . . . . . . . 9
12	11	halfcld 10700	. . . . . . . 8
13		binom2 12185	. . . . . . . 8 $/\$
14	2, 12, 13	syl2anc 659	. . . . . . 7
15		2t2e4 10602	. . . . . . . . . . . 12
16	15	oveq2i 6207	. . . . . . . . . . 11
17		2nn0 10729	. . . . . . . . . . . . 13
18	17	a1i 11	. . . . . . . . . . . 12
19	1, 18, 18	expmuld 12215	. . . . . . . . . . 11
20	16, 19	syl5reqr 2438	. . . . . . . . . 10
21	4	a1i 11	. . . . . . . . . . . 12
22	21, 2, 12	mul12d 9700	. . . . . . . . . . 11
23		2ne0 10545	. . . . . . . . . . . . . . 15
24	23	a1i 11	. . . . . . . . . . . . . 14
25	11, 21, 24	divcan2d 10239	. . . . . . . . . . . . 13
26	25	oveq2d 6212	. . . . . . . . . . . 12
27	2, 11	mulcomd 9528	. . . . . . . . . . . 12
28	26, 27	eqtrd 2423	. . . . . . . . . . 11
29	9, 10, 2	adddird 9532	. . . . . . . . . . 11
30	22, 28, 29	3eqtrd 2427	. . . . . . . . . 10
31	20, 30	oveq12d 6214	. . . . . . . . 9
32		4nn0 10731	. . . . . . . . . . 11
33		expcl 12087	. . . . . . . . . . 11 $/\$
34	1, 32, 33	sylancl 660	. . . . . . . . . 10
35	9, 2	mulcld 9527	. . . . . . . . . 10
36	10, 2	mulcld 9527	. . . . . . . . . 10
37	34, 35, 36	add12d 9714	. . . . . . . . 9
38	31, 37	eqtrd 2423	. . . . . . . 8
39	38	oveq1d 6211	. . . . . . 7
40	34, 36	addcld 9526	. . . . . . . 8
41	12	sqcld 12210	. . . . . . . 8
42	35, 40, 41	addassd 9529	. . . . . . 7
43	14, 39, 42	3eqtrd 2427	. . . . . 6
44	9	halfcld 10700	. . . . . . . . . . . 12
45	44, 1	mulcld 9527	. . . . . . . . . . 11
46		dquart.c	. . . . . . . . . . . 12
47		4cn 10530	. . . . . . . . . . . . 13
48	47	a1i 11	. . . . . . . . . . . 12
49		4ne0 10549	. . . . . . . . . . . . 13
50	49	a1i 11	. . . . . . . . . . . 12
51	46, 48, 50	divcld 10237	. . . . . . . . . . 11
52	45, 51	subcld 9844	. . . . . . . . . 10
53		dquart.m0	. . . . . . . . . . . . . 14
54	3, 53	eqnetrrd 2676	. . . . . . . . . . . . 13
55		sqne0 12137	. . . . . . . . . . . . . 14
56	7, 55	syl 16	. . . . . . . . . . . . 13
57	54, 56	mpbid 210	. . . . . . . . . . . 12
58		mulne0b 10107	. . . . . . . . . . . . 13 $/\$ $/\$
59	4, 5, 58	sylancr 661	. . . . . . . . . . . 12 $/\$
60	57, 59	mpbird 232	. . . . . . . . . . 11 $/\$
61	60	simprd 461	. . . . . . . . . 10
62	52, 5, 21, 61, 24	divcan5d 10263	. . . . . . . . 9
63	21, 45, 51	subdid 9930	. . . . . . . . . . 11
64	21, 44, 1	mulassd 9530	. . . . . . . . . . . . 13
65	9, 21, 24	divcan2d 10239	. . . . . . . . . . . . . 14
66	65	oveq1d 6211	. . . . . . . . . . . . 13
67	64, 66	eqtr3d 2425	. . . . . . . . . . . 12
68	21, 46, 48, 50	divassd 10272	. . . . . . . . . . . . 13
69	15	oveq2i 6207	. . . . . . . . . . . . . 14
70	46, 21, 21, 24, 24	divcan5d 10263	. . . . . . . . . . . . . 14
71	69, 70	syl5eqr 2437	. . . . . . . . . . . . 13
72	68, 71	eqtr3d 2425	. . . . . . . . . . . 12
73	67, 72	oveq12d 6214	. . . . . . . . . . 11
74	63, 73	eqtrd 2423	. . . . . . . . . 10
75	74	oveq1d 6211	. . . . . . . . 9
76	62, 75	eqtr3d 2425	. . . . . . . 8
77	76	oveq1d 6211	. . . . . . 7
78	9, 1	mulcld 9527	. . . . . . . . 9
79	46	halfcld 10700	. . . . . . . . 9
80	78, 79	subcld 9844	. . . . . . . 8
81	80, 7, 57	sqdivd 12225	. . . . . . 7
82	9	sqcld 12210	. . . . . . . . . . 11
83	82, 2	mulcld 9527	. . . . . . . . . 10
84	78, 46	mulcld 9527	. . . . . . . . . 10
85	83, 84	subcld 9844	. . . . . . . . 9
86	46	sqcld 12210	. . . . . . . . . 10
87	86, 48, 50	divcld 10237	. . . . . . . . 9
88	85, 87, 9, 53	divdird 10275	. . . . . . . 8
89		binom2sub 12187	. . . . . . . . . . 11 $/\$
90	78, 79, 89	syl2anc 659	. . . . . . . . . 10
91	9, 1	sqmuld 12224	. . . . . . . . . . . 12
92	21, 78, 79	mul12d 9700	. . . . . . . . . . . . 13
93	46, 21, 24	divcan2d 10239	. . . . . . . . . . . . . 14
94	93	oveq2d 6212	. . . . . . . . . . . . 13
95	92, 94	eqtrd 2423	. . . . . . . . . . . 12
96	91, 95	oveq12d 6214	. . . . . . . . . . 11
97	46, 21, 24	sqdivd 12225	. . . . . . . . . . . 12
98		sq2 12167	. . . . . . . . . . . . 13
99	98	oveq2i 6207	. . . . . . . . . . . 12
100	97, 99	syl6eq 2439	. . . . . . . . . . 11
101	96, 100	oveq12d 6214	. . . . . . . . . 10
102	90, 101	eqtr2d 2424	. . . . . . . . 9
103	102, 3	oveq12d 6214	. . . . . . . 8
104	83, 84, 9, 53	divsubdird 10276	. . . . . . . . . . 11
105	82, 2, 9, 53	div23d 10274	. . . . . . . . . . . . 13
106	9	sqvald 12209	. . . . . . . . . . . . . . . 16
107	106	oveq1d 6211	. . . . . . . . . . . . . . 15
108	9, 9, 53	divcan3d 10242	. . . . . . . . . . . . . . 15
109	107, 108	eqtrd 2423	. . . . . . . . . . . . . 14
110	109	oveq1d 6211	. . . . . . . . . . . . 13
111	105, 110	eqtrd 2423	. . . . . . . . . . . 12
112	9, 1, 46	mul32d 9701	. . . . . . . . . . . . . . 15
113	9, 46, 1	mulassd 9530	. . . . . . . . . . . . . . 15
114	112, 113	eqtrd 2423	. . . . . . . . . . . . . 14
115	114	oveq1d 6211	. . . . . . . . . . . . 13
116	46, 1	mulcld 9527	. . . . . . . . . . . . . 14
117	116, 9, 53	divcan3d 10242	. . . . . . . . . . . . 13
118	115, 117	eqtrd 2423	. . . . . . . . . . . 12
119	111, 118	oveq12d 6214	. . . . . . . . . . 11
120	104, 119	eqtrd 2423	. . . . . . . . . 10
121	120	oveq1d 6211	. . . . . . . . 9
122	87, 9, 53	divcld 10237	. . . . . . . . . 10
123	35, 116, 122	subsubd 9872	. . . . . . . . 9
124	121, 123	eqtr4d 2426	. . . . . . . 8
125	88, 103, 124	3eqtr3d 2431	. . . . . . 7
126	77, 81, 125	3eqtrd 2427	. . . . . 6
127	43, 126	oveq12d 6214	. . . . 5
128	40, 41	addcld 9526	. . . . . 6
129	116, 122	subcld 9844	. . . . . 6
130	35, 128, 129	pnncand 9883	. . . . 5
131	122	negcld 9831	. . . . . . 7
132	40, 41, 116, 131	add4d 9716	. . . . . 6
133	116, 122	negsubd 9850	. . . . . . 7
134	133	oveq2d 6212	. . . . . 6
135	41, 122	negsubd 9850	. . . . . . . . 9
136		dquart.i	. . . . . . . . . 10
137		dquart.i2	. . . . . . . . . 10
138		dquart.d	. . . . . . . . . 10
139		dquart.3	. . . . . . . . . 10
140	10, 46, 1, 5, 3, 53, 136, 137, 138, 139	dquartlem2 23299	. . . . . . . . 9
141	135, 140	eqtrd 2423	. . . . . . . 8
142	141	oveq2d 6212	. . . . . . 7
143	40, 116, 138	addassd 9529	. . . . . . 7
144	142, 143	eqtrd 2423	. . . . . 6
145	132, 134, 144	3eqtr3d 2431	. . . . 5
146	127, 130, 145	3eqtrd 2427	. . . 4
147	2, 12	addcld 9526	. . . . 5
148	52, 5, 61	divcld 10237	. . . . 5
149		subsq 12178	. . . . 5 $/\$
150	147, 148, 149	syl2anc 659	. . . 4
151	146, 150	eqtr3d 2425	. . 3
152	151	eqeq1d 2384	. 2
153	147, 148	addcld 9526	. . 3
154	147, 148	subcld 9844	. . 3
155	153, 154	mul0ord 10116	. 2 $\/$
156	10, 46, 1, 5, 3, 53, 136, 137	dquartlem1 23298	. . 3 $\/$
157	5	negcld 9831	. . . . 5
158		sqneg 12131	. . . . . . . 8
159	7, 158	syl 16	. . . . . . 7
160	3, 159	eqtr4d 2426	. . . . . 6
161		mulneg2 9912	. . . . . . . 8 $/\$
162	4, 5, 161	sylancr 661	. . . . . . 7
163	162	oveq1d 6211	. . . . . 6
164	160, 163	eqtr4d 2426	. . . . 5
165		dquart.j	. . . . 5
166		dquart.j2	. . . . . 6
167	5	sqcld 12210	. . . . . . . . 9
168	167	negcld 9831	. . . . . . . 8
169	10	halfcld 10700	. . . . . . . 8
170	168, 169	subcld 9844	. . . . . . 7
171	51, 5, 61	divcld 10237	. . . . . . 7
172	170, 171	negsubd 9850	. . . . . 6
173		sqneg 12131	. . . . . . . . . . 11
174	5, 173	syl 16	. . . . . . . . . 10
175	174	eqcomd 2390	. . . . . . . . 9
176	175	negeqd 9727	. . . . . . . 8
177	176	oveq1d 6211	. . . . . . 7
178	51, 5, 61	divneg2d 10251	. . . . . . 7
179	177, 178	oveq12d 6214	. . . . . 6
180	166, 172, 179	3eqtr2d 2429	. . . . 5
181	10, 46, 1, 157, 164, 53, 165, 180	dquartlem1 23298	. . . 4 $\/$
182	52, 5, 61	divneg2d 10251	. . . . . . 7
183	182	oveq2d 6212	. . . . . 6
184	147, 148	negsubd 9850	. . . . . 6
185	183, 184	eqtr3d 2425	. . . . 5
186	185	eqeq1d 2384	. . . 4
187	5	negnegd 9835	. . . . . . 7
188	187	oveq1d 6211	. . . . . 6
189	188	eqeq2d 2396	. . . . 5
190	187	oveq1d 6211	. . . . . 6
191	190	eqeq2d 2396	. . . . 5
192	189, 191	orbi12d 707	. . . 4 $\/$ $\/$
193	181, 186, 192	3bitr3d 283	. . 3 $\/$
194	156, 193	orbi12d 707	. 2 $\/$ $\/$ $\/$ $\/$
195	152, 155, 194	3bitrd 279	1 $\/$ $\/$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $\/$ wo 366 $/\$ wa 367

wceq 1399

wcel 1826

wne 2577 (class class class)co 6196

cc 9401

cc0 9403

caddc 9406

cmul 9408

cmin 9718

cneg 9719

cdiv 10123

c2 10502

c3 10503

c4 10504

cn0 10712

cexp 12069

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-sep 4488 ax-nul 4496 ax-pow 4543 ax-pr 4601 ax-un 6491 ax-cnex 9459 ax-resscn 9460 ax-1cn 9461 ax-icn 9462 ax-addcl 9463 ax-addrcl 9464 ax-mulcl 9465 ax-mulrcl 9466 ax-mulcom 9467 ax-addass 9468 ax-mulass 9469 ax-distr 9470 ax-i2m1 9471 ax-1ne0 9472 ax-1rid 9473 ax-rnegex 9474 ax-rrecex 9475 ax-cnre 9476 ax-pre-lttri 9477 ax-pre-lttrn 9478 ax-pre-ltadd 9479 ax-pre-mulgt0 9480

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1402 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-nel 2580 df-ral 2737 df-rex 2738 df-reu 2739 df-rmo 2740 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-pss 3405 df-nul 3712 df-if 3858 df-pw 3929 df-sn 3945 df-pr 3947 df-tp 3949 df-op 3951 df-uni 4164 df-iun 4245 df-br 4368 df-opab 4426 df-mpt 4427 df-tr 4461 df-eprel 4705 df-id 4709 df-po 4714 df-so 4715 df-fr 4752 df-we 4754 df-ord 4795 df-on 4796 df-lim 4797 df-suc 4798 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-f1 5501 df-fo 5502 df-f1o 5503 df-fv 5504 df-riota 6158 df-ov 6199 df-oprab 6200 df-mpt2 6201 df-om 6600 df-2nd 6700 df-recs 6960 df-rdg 6994 df-er 7229 df-en 7436 df-dom 7437 df-sdom 7438 df-pnf 9541 df-mnf 9542 df-xr 9543 df-ltxr 9544 df-le 9545 df-sub 9720 df-neg 9721 df-div 10124 df-nn 10453 df-2 10511 df-3 10512 df-4 10513 df-n0 10713 df-z 10782 df-uz 11002 df-seq 12011 df-exp 12070

This theorem is referenced by: quart 23308

W3C validator