dquart - Metamath Proof Explorer

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

Theorem dquart 23056

Description: Solve a depressed quartic equation. To eliminate

, which is the square root of a solution

to the resolvent cubic equation, apply cubic 23052 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 12287	. . . . . . . 8
3		dquart.m	. . . . . . . . . . 11
4		2cn 10612	. . . . . . . . . . . . 13
5		dquart.s	. . . . . . . . . . . . 13
6		mulcl 9579	. . . . . . . . . . . . 13 $/\$
7	4, 5, 6	sylancr 663	. . . . . . . . . . . 12
8	7	sqcld 12287	. . . . . . . . . . 11
9	3, 8	eqeltrd 2531	. . . . . . . . . 10
10		dquart.b	. . . . . . . . . 10
11	9, 10	addcld 9618	. . . . . . . . 9
12	11	halfcld 10789	. . . . . . . 8
13		binom2 12262	. . . . . . . 8 $/\$
14	2, 12, 13	syl2anc 661	. . . . . . 7
15		2t2e4 10691	. . . . . . . . . . . 12
16	15	oveq2i 6292	. . . . . . . . . . 11
17		2nn0 10818	. . . . . . . . . . . . 13
18	17	a1i 11	. . . . . . . . . . . 12
19	1, 18, 18	expmuld 12292	. . . . . . . . . . 11
20	16, 19	syl5reqr 2499	. . . . . . . . . 10
21	4	a1i 11	. . . . . . . . . . . 12
22	21, 2, 12	mul12d 9792	. . . . . . . . . . 11
23		2ne0 10634	. . . . . . . . . . . . . . 15
24	23	a1i 11	. . . . . . . . . . . . . 14
25	11, 21, 24	divcan2d 10328	. . . . . . . . . . . . 13
26	25	oveq2d 6297	. . . . . . . . . . . 12
27	2, 11	mulcomd 9620	. . . . . . . . . . . 12
28	26, 27	eqtrd 2484	. . . . . . . . . . 11
29	9, 10, 2	adddird 9624	. . . . . . . . . . 11
30	22, 28, 29	3eqtrd 2488	. . . . . . . . . 10
31	20, 30	oveq12d 6299	. . . . . . . . 9
32		4nn0 10820	. . . . . . . . . . 11
33		expcl 12163	. . . . . . . . . . 11 $/\$
34	1, 32, 33	sylancl 662	. . . . . . . . . 10
35	9, 2	mulcld 9619	. . . . . . . . . 10
36	10, 2	mulcld 9619	. . . . . . . . . 10
37	34, 35, 36	add12d 9806	. . . . . . . . 9
38	31, 37	eqtrd 2484	. . . . . . . 8
39	38	oveq1d 6296	. . . . . . 7
40	34, 36	addcld 9618	. . . . . . . 8
41	12	sqcld 12287	. . . . . . . 8
42	35, 40, 41	addassd 9621	. . . . . . 7
43	14, 39, 42	3eqtrd 2488	. . . . . 6
44	9	halfcld 10789	. . . . . . . . . . . 12
45	44, 1	mulcld 9619	. . . . . . . . . . 11
46		dquart.c	. . . . . . . . . . . 12
47		4cn 10619	. . . . . . . . . . . . 13
48	47	a1i 11	. . . . . . . . . . . 12
49		4ne0 10638	. . . . . . . . . . . . 13
50	49	a1i 11	. . . . . . . . . . . 12
51	46, 48, 50	divcld 10326	. . . . . . . . . . 11
52	45, 51	subcld 9936	. . . . . . . . . 10
53		dquart.m0	. . . . . . . . . . . . . 14
54	3, 53	eqnetrrd 2737	. . . . . . . . . . . . 13
55		sqne0 12213	. . . . . . . . . . . . . 14
56	7, 55	syl 16	. . . . . . . . . . . . 13
57	54, 56	mpbid 210	. . . . . . . . . . . 12
58		mulne0b 10196	. . . . . . . . . . . . 13 $/\$ $/\$
59	4, 5, 58	sylancr 663	. . . . . . . . . . . 12 $/\$
60	57, 59	mpbird 232	. . . . . . . . . . 11 $/\$
61	60	simprd 463	. . . . . . . . . 10
62	52, 5, 21, 61, 24	divcan5d 10352	. . . . . . . . 9
63	21, 45, 51	subdid 10018	. . . . . . . . . . 11
64	21, 44, 1	mulassd 9622	. . . . . . . . . . . . 13
65	9, 21, 24	divcan2d 10328	. . . . . . . . . . . . . 14
66	65	oveq1d 6296	. . . . . . . . . . . . 13
67	64, 66	eqtr3d 2486	. . . . . . . . . . . 12
68	21, 46, 48, 50	divassd 10361	. . . . . . . . . . . . 13
69	15	oveq2i 6292	. . . . . . . . . . . . . 14
70	46, 21, 21, 24, 24	divcan5d 10352	. . . . . . . . . . . . . 14
71	69, 70	syl5eqr 2498	. . . . . . . . . . . . 13
72	68, 71	eqtr3d 2486	. . . . . . . . . . . 12
73	67, 72	oveq12d 6299	. . . . . . . . . . 11
74	63, 73	eqtrd 2484	. . . . . . . . . 10
75	74	oveq1d 6296	. . . . . . . . 9
76	62, 75	eqtr3d 2486	. . . . . . . 8
77	76	oveq1d 6296	. . . . . . 7
78	9, 1	mulcld 9619	. . . . . . . . 9
79	46	halfcld 10789	. . . . . . . . 9
80	78, 79	subcld 9936	. . . . . . . 8
81	80, 7, 57	sqdivd 12302	. . . . . . 7
82	9	sqcld 12287	. . . . . . . . . . 11
83	82, 2	mulcld 9619	. . . . . . . . . 10
84	78, 46	mulcld 9619	. . . . . . . . . 10
85	83, 84	subcld 9936	. . . . . . . . 9
86	46	sqcld 12287	. . . . . . . . . 10
87	86, 48, 50	divcld 10326	. . . . . . . . 9
88	85, 87, 9, 53	divdird 10364	. . . . . . . 8
89		binom2sub 12264	. . . . . . . . . . 11 $/\$
90	78, 79, 89	syl2anc 661	. . . . . . . . . 10
91	9, 1	sqmuld 12301	. . . . . . . . . . . 12
92	21, 78, 79	mul12d 9792	. . . . . . . . . . . . 13
93	46, 21, 24	divcan2d 10328	. . . . . . . . . . . . . 14
94	93	oveq2d 6297	. . . . . . . . . . . . 13
95	92, 94	eqtrd 2484	. . . . . . . . . . . 12
96	91, 95	oveq12d 6299	. . . . . . . . . . 11
97	46, 21, 24	sqdivd 12302	. . . . . . . . . . . 12
98		sq2 12243	. . . . . . . . . . . . 13
99	98	oveq2i 6292	. . . . . . . . . . . 12
100	97, 99	syl6eq 2500	. . . . . . . . . . 11
101	96, 100	oveq12d 6299	. . . . . . . . . 10
102	90, 101	eqtr2d 2485	. . . . . . . . 9
103	102, 3	oveq12d 6299	. . . . . . . 8
104	83, 84, 9, 53	divsubdird 10365	. . . . . . . . . . 11
105	82, 2, 9, 53	div23d 10363	. . . . . . . . . . . . 13
106	9	sqvald 12286	. . . . . . . . . . . . . . . 16
107	106	oveq1d 6296	. . . . . . . . . . . . . . 15
108	9, 9, 53	divcan3d 10331	. . . . . . . . . . . . . . 15
109	107, 108	eqtrd 2484	. . . . . . . . . . . . . 14
110	109	oveq1d 6296	. . . . . . . . . . . . 13
111	105, 110	eqtrd 2484	. . . . . . . . . . . 12
112	9, 1, 46	mul32d 9793	. . . . . . . . . . . . . . 15
113	9, 46, 1	mulassd 9622	. . . . . . . . . . . . . . 15
114	112, 113	eqtrd 2484	. . . . . . . . . . . . . 14
115	114	oveq1d 6296	. . . . . . . . . . . . 13
116	46, 1	mulcld 9619	. . . . . . . . . . . . . 14
117	116, 9, 53	divcan3d 10331	. . . . . . . . . . . . 13
118	115, 117	eqtrd 2484	. . . . . . . . . . . 12
119	111, 118	oveq12d 6299	. . . . . . . . . . 11
120	104, 119	eqtrd 2484	. . . . . . . . . 10
121	120	oveq1d 6296	. . . . . . . . 9
122	87, 9, 53	divcld 10326	. . . . . . . . . 10
123	35, 116, 122	subsubd 9964	. . . . . . . . 9
124	121, 123	eqtr4d 2487	. . . . . . . 8
125	88, 103, 124	3eqtr3d 2492	. . . . . . 7
126	77, 81, 125	3eqtrd 2488	. . . . . 6
127	43, 126	oveq12d 6299	. . . . 5
128	40, 41	addcld 9618	. . . . . 6
129	116, 122	subcld 9936	. . . . . 6
130	35, 128, 129	pnncand 9975	. . . . 5
131	122	negcld 9923	. . . . . . 7
132	40, 41, 116, 131	add4d 9808	. . . . . 6
133	116, 122	negsubd 9942	. . . . . . 7
134	133	oveq2d 6297	. . . . . 6
135	41, 122	negsubd 9942	. . . . . . . . 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 23055	. . . . . . . . 9
141	135, 140	eqtrd 2484	. . . . . . . 8
142	141	oveq2d 6297	. . . . . . 7
143	40, 116, 138	addassd 9621	. . . . . . 7
144	142, 143	eqtrd 2484	. . . . . 6
145	132, 134, 144	3eqtr3d 2492	. . . . 5
146	127, 130, 145	3eqtrd 2488	. . . 4
147	2, 12	addcld 9618	. . . . 5
148	52, 5, 61	divcld 10326	. . . . 5
149		subsq 12254	. . . . 5 $/\$
150	147, 148, 149	syl2anc 661	. . . 4
151	146, 150	eqtr3d 2486	. . 3
152	151	eqeq1d 2445	. 2
153	147, 148	addcld 9618	. . 3
154	147, 148	subcld 9936	. . 3
155	153, 154	mul0ord 10205	. 2 $\/$
156	10, 46, 1, 5, 3, 53, 136, 137	dquartlem1 23054	. . 3 $\/$
157	5	negcld 9923	. . . . 5
158		sqneg 12207	. . . . . . . 8
159	7, 158	syl 16	. . . . . . 7
160	3, 159	eqtr4d 2487	. . . . . 6
161		mulneg2 10000	. . . . . . . 8 $/\$
162	4, 5, 161	sylancr 663	. . . . . . 7
163	162	oveq1d 6296	. . . . . 6
164	160, 163	eqtr4d 2487	. . . . 5
165		dquart.j	. . . . 5
166		dquart.j2	. . . . . 6
167	5	sqcld 12287	. . . . . . . . 9
168	167	negcld 9923	. . . . . . . 8
169	10	halfcld 10789	. . . . . . . 8
170	168, 169	subcld 9936	. . . . . . 7
171	51, 5, 61	divcld 10326	. . . . . . 7
172	170, 171	negsubd 9942	. . . . . 6
173		sqneg 12207	. . . . . . . . . . 11
174	5, 173	syl 16	. . . . . . . . . 10
175	174	eqcomd 2451	. . . . . . . . 9
176	175	negeqd 9819	. . . . . . . 8
177	176	oveq1d 6296	. . . . . . 7
178	51, 5, 61	divneg2d 10340	. . . . . . 7
179	177, 178	oveq12d 6299	. . . . . 6
180	166, 172, 179	3eqtr2d 2490	. . . . 5
181	10, 46, 1, 157, 164, 53, 165, 180	dquartlem1 23054	. . . 4 $\/$
182	52, 5, 61	divneg2d 10340	. . . . . . 7
183	182	oveq2d 6297	. . . . . 6
184	147, 148	negsubd 9942	. . . . . 6
185	183, 184	eqtr3d 2486	. . . . 5
186	185	eqeq1d 2445	. . . 4
187	5	negnegd 9927	. . . . . . 7
188	187	oveq1d 6296	. . . . . 6
189	188	eqeq2d 2457	. . . . 5
190	187	oveq1d 6296	. . . . . 6
191	190	eqeq2d 2457	. . . . 5
192	189, 191	orbi12d 709	. . . 4 $\/$ $\/$
193	181, 186, 192	3bitr3d 283	. . 3 $\/$
194	156, 193	orbi12d 709	. 2 $\/$ $\/$ $\/$ $\/$
195	152, 155, 194	3bitrd 279	1 $\/$ $\/$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369

wceq 1383

wcel 1804

wne 2638 (class class class)co 6281

cc 9493

cc0 9495

caddc 9498

cmul 9500

cmin 9810

cneg 9811

cdiv 10212

c2 10591

c3 10592

c4 10593

cn0 10801

cexp 12145

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-8 1806 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-sep 4558 ax-nul 4566 ax-pow 4615 ax-pr 4676 ax-un 6577 ax-cnex 9551 ax-resscn 9552 ax-1cn 9553 ax-icn 9554 ax-addcl 9555 ax-addrcl 9556 ax-mulcl 9557 ax-mulrcl 9558 ax-mulcom 9559 ax-addass 9560 ax-mulass 9561 ax-distr 9562 ax-i2m1 9563 ax-1ne0 9564 ax-1rid 9565 ax-rnegex 9566 ax-rrecex 9567 ax-cnre 9568 ax-pre-lttri 9569 ax-pre-lttrn 9570 ax-pre-ltadd 9571 ax-pre-mulgt0 9572

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 975 df-3an 976 df-tru 1386 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-nel 2641 df-ral 2798 df-rex 2799 df-reu 2800 df-rmo 2801 df-rab 2802 df-v 3097 df-sbc 3314 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3771 df-if 3927 df-pw 3999 df-sn 4015 df-pr 4017 df-tp 4019 df-op 4021 df-uni 4235 df-iun 4317 df-br 4438 df-opab 4496 df-mpt 4497 df-tr 4531 df-eprel 4781 df-id 4785 df-po 4790 df-so 4791 df-fr 4828 df-we 4830 df-ord 4871 df-on 4872 df-lim 4873 df-suc 4874 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-res 5001 df-ima 5002 df-iota 5541 df-fun 5580 df-fn 5581 df-f 5582 df-f1 5583 df-fo 5584 df-f1o 5585 df-fv 5586 df-riota 6242 df-ov 6284 df-oprab 6285 df-mpt2 6286 df-om 6686 df-2nd 6786 df-recs 7044 df-rdg 7078 df-er 7313 df-en 7519 df-dom 7520 df-sdom 7521 df-pnf 9633 df-mnf 9634 df-xr 9635 df-ltxr 9636 df-le 9637 df-sub 9812 df-neg 9813 df-div 10213 df-nn 10543 df-2 10600 df-3 10601 df-4 10602 df-n0 10802 df-z 10871 df-uz 11091 df-seq 12087 df-exp 12146

This theorem is referenced by: quart 23064

W3C validator