dquart - Metamath Proof Explorer

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

Theorem dquart 23858

Description: Solve a depressed quartic equation. To eliminate

, which is the square root of a solution

to the resolvent cubic equation, apply cubic 23854 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 12452	. . . . . . . 8
3		dquart.m	. . . . . . . . . . 11
4		2cn 10702	. . . . . . . . . . . . 13
5		dquart.s	. . . . . . . . . . . . 13
6		mulcl 9641	. . . . . . . . . . . . 13 $/\$
7	4, 5, 6	sylancr 676	. . . . . . . . . . . 12
8	7	sqcld 12452	. . . . . . . . . . 11
9	3, 8	eqeltrd 2549	. . . . . . . . . 10
10		dquart.b	. . . . . . . . . 10
11	9, 10	addcld 9680	. . . . . . . . 9
12	11	halfcld 10880	. . . . . . . 8
13		binom2 12427	. . . . . . . 8 $/\$
14	2, 12, 13	syl2anc 673	. . . . . . 7
15		2t2e4 10782	. . . . . . . . . . . 12
16	15	oveq2i 6319	. . . . . . . . . . 11
17		2nn0 10910	. . . . . . . . . . . . 13
18	17	a1i 11	. . . . . . . . . . . 12
19	1, 18, 18	expmuld 12457	. . . . . . . . . . 11
20	16, 19	syl5reqr 2520	. . . . . . . . . 10
21	4	a1i 11	. . . . . . . . . . . 12
22	21, 2, 12	mul12d 9860	. . . . . . . . . . 11
23		2ne0 10724	. . . . . . . . . . . . . . 15
24	23	a1i 11	. . . . . . . . . . . . . 14
25	11, 21, 24	divcan2d 10407	. . . . . . . . . . . . 13
26	25	oveq2d 6324	. . . . . . . . . . . 12
27	2, 11	mulcomd 9682	. . . . . . . . . . . 12
28	26, 27	eqtrd 2505	. . . . . . . . . . 11
29	9, 10, 2	adddird 9686	. . . . . . . . . . 11
30	22, 28, 29	3eqtrd 2509	. . . . . . . . . 10
31	20, 30	oveq12d 6326	. . . . . . . . 9
32		4nn0 10912	. . . . . . . . . . 11
33		expcl 12328	. . . . . . . . . . 11 $/\$
34	1, 32, 33	sylancl 675	. . . . . . . . . 10
35	9, 2	mulcld 9681	. . . . . . . . . 10
36	10, 2	mulcld 9681	. . . . . . . . . 10
37	34, 35, 36	add12d 9876	. . . . . . . . 9
38	31, 37	eqtrd 2505	. . . . . . . 8
39	38	oveq1d 6323	. . . . . . 7
40	34, 36	addcld 9680	. . . . . . . 8
41	12	sqcld 12452	. . . . . . . 8
42	35, 40, 41	addassd 9683	. . . . . . 7
43	14, 39, 42	3eqtrd 2509	. . . . . 6
44	9	halfcld 10880	. . . . . . . . . . . 12
45	44, 1	mulcld 9681	. . . . . . . . . . 11
46		dquart.c	. . . . . . . . . . . 12
47		4cn 10709	. . . . . . . . . . . . 13
48	47	a1i 11	. . . . . . . . . . . 12
49		4ne0 10728	. . . . . . . . . . . . 13
50	49	a1i 11	. . . . . . . . . . . 12
51	46, 48, 50	divcld 10405	. . . . . . . . . . 11
52	45, 51	subcld 10005	. . . . . . . . . 10
53		dquart.m0	. . . . . . . . . . . . . 14
54	3, 53	eqnetrrd 2711	. . . . . . . . . . . . 13
55		sqne0 12379	. . . . . . . . . . . . . 14
56	7, 55	syl 17	. . . . . . . . . . . . 13
57	54, 56	mpbid 215	. . . . . . . . . . . 12
58		mulne0b 10275	. . . . . . . . . . . . 13 $/\$ $/\$
59	4, 5, 58	sylancr 676	. . . . . . . . . . . 12 $/\$
60	57, 59	mpbird 240	. . . . . . . . . . 11 $/\$
61	60	simprd 470	. . . . . . . . . 10
62	52, 5, 21, 61, 24	divcan5d 10431	. . . . . . . . 9
63	21, 45, 51	subdid 10095	. . . . . . . . . . 11
64	21, 44, 1	mulassd 9684	. . . . . . . . . . . . 13
65	9, 21, 24	divcan2d 10407	. . . . . . . . . . . . . 14
66	65	oveq1d 6323	. . . . . . . . . . . . 13
67	64, 66	eqtr3d 2507	. . . . . . . . . . . 12
68	21, 46, 48, 50	divassd 10440	. . . . . . . . . . . . 13
69	15	oveq2i 6319	. . . . . . . . . . . . . 14
70	46, 21, 21, 24, 24	divcan5d 10431	. . . . . . . . . . . . . 14
71	69, 70	syl5eqr 2519	. . . . . . . . . . . . 13
72	68, 71	eqtr3d 2507	. . . . . . . . . . . 12
73	67, 72	oveq12d 6326	. . . . . . . . . . 11
74	63, 73	eqtrd 2505	. . . . . . . . . 10
75	74	oveq1d 6323	. . . . . . . . 9
76	62, 75	eqtr3d 2507	. . . . . . . 8
77	76	oveq1d 6323	. . . . . . 7
78	9, 1	mulcld 9681	. . . . . . . . 9
79	46	halfcld 10880	. . . . . . . . 9
80	78, 79	subcld 10005	. . . . . . . 8
81	80, 7, 57	sqdivd 12467	. . . . . . 7
82	9	sqcld 12452	. . . . . . . . . . 11
83	82, 2	mulcld 9681	. . . . . . . . . 10
84	78, 46	mulcld 9681	. . . . . . . . . 10
85	83, 84	subcld 10005	. . . . . . . . 9
86	46	sqcld 12452	. . . . . . . . . 10
87	86, 48, 50	divcld 10405	. . . . . . . . 9
88	85, 87, 9, 53	divdird 10443	. . . . . . . 8
89		binom2sub 12429	. . . . . . . . . . 11 $/\$
90	78, 79, 89	syl2anc 673	. . . . . . . . . 10
91	9, 1	sqmuld 12466	. . . . . . . . . . . 12
92	21, 78, 79	mul12d 9860	. . . . . . . . . . . . 13
93	46, 21, 24	divcan2d 10407	. . . . . . . . . . . . . 14
94	93	oveq2d 6324	. . . . . . . . . . . . 13
95	92, 94	eqtrd 2505	. . . . . . . . . . . 12
96	91, 95	oveq12d 6326	. . . . . . . . . . 11
97	46, 21, 24	sqdivd 12467	. . . . . . . . . . . 12
98		sq2 12409	. . . . . . . . . . . . 13
99	98	oveq2i 6319	. . . . . . . . . . . 12
100	97, 99	syl6eq 2521	. . . . . . . . . . 11
101	96, 100	oveq12d 6326	. . . . . . . . . 10
102	90, 101	eqtr2d 2506	. . . . . . . . 9
103	102, 3	oveq12d 6326	. . . . . . . 8
104	83, 84, 9, 53	divsubdird 10444	. . . . . . . . . . 11
105	82, 2, 9, 53	div23d 10442	. . . . . . . . . . . . 13
106	9	sqvald 12451	. . . . . . . . . . . . . . . 16
107	106	oveq1d 6323	. . . . . . . . . . . . . . 15
108	9, 9, 53	divcan3d 10410	. . . . . . . . . . . . . . 15
109	107, 108	eqtrd 2505	. . . . . . . . . . . . . 14
110	109	oveq1d 6323	. . . . . . . . . . . . 13
111	105, 110	eqtrd 2505	. . . . . . . . . . . 12
112	9, 1, 46	mul32d 9861	. . . . . . . . . . . . . . 15
113	9, 46, 1	mulassd 9684	. . . . . . . . . . . . . . 15
114	112, 113	eqtrd 2505	. . . . . . . . . . . . . 14
115	114	oveq1d 6323	. . . . . . . . . . . . 13
116	46, 1	mulcld 9681	. . . . . . . . . . . . . 14
117	116, 9, 53	divcan3d 10410	. . . . . . . . . . . . 13
118	115, 117	eqtrd 2505	. . . . . . . . . . . 12
119	111, 118	oveq12d 6326	. . . . . . . . . . 11
120	104, 119	eqtrd 2505	. . . . . . . . . 10
121	120	oveq1d 6323	. . . . . . . . 9
122	87, 9, 53	divcld 10405	. . . . . . . . . 10
123	35, 116, 122	subsubd 10033	. . . . . . . . 9
124	121, 123	eqtr4d 2508	. . . . . . . 8
125	88, 103, 124	3eqtr3d 2513	. . . . . . 7
126	77, 81, 125	3eqtrd 2509	. . . . . 6
127	43, 126	oveq12d 6326	. . . . 5
128	40, 41	addcld 9680	. . . . . 6
129	116, 122	subcld 10005	. . . . . 6
130	35, 128, 129	pnncand 10044	. . . . 5
131	122	negcld 9992	. . . . . . 7
132	40, 41, 116, 131	add4d 9878	. . . . . 6
133	116, 122	negsubd 10011	. . . . . . 7
134	133	oveq2d 6324	. . . . . 6
135	41, 122	negsubd 10011	. . . . . . . . 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 23857	. . . . . . . . 9
141	135, 140	eqtrd 2505	. . . . . . . 8
142	141	oveq2d 6324	. . . . . . 7
143	40, 116, 138	addassd 9683	. . . . . . 7
144	142, 143	eqtrd 2505	. . . . . 6
145	132, 134, 144	3eqtr3d 2513	. . . . 5
146	127, 130, 145	3eqtrd 2509	. . . 4
147	2, 12	addcld 9680	. . . . 5
148	52, 5, 61	divcld 10405	. . . . 5
149		subsq 12420	. . . . 5 $/\$
150	147, 148, 149	syl2anc 673	. . . 4
151	146, 150	eqtr3d 2507	. . 3
152	151	eqeq1d 2473	. 2
153	147, 148	addcld 9680	. . 3
154	147, 148	subcld 10005	. . 3
155	153, 154	mul0ord 10284	. 2 $\/$
156	10, 46, 1, 5, 3, 53, 136, 137	dquartlem1 23856	. . 3 $\/$
157	5	negcld 9992	. . . . 5
158		sqneg 12373	. . . . . . . 8
159	7, 158	syl 17	. . . . . . 7
160	3, 159	eqtr4d 2508	. . . . . 6
161		mulneg2 10077	. . . . . . . 8 $/\$
162	4, 5, 161	sylancr 676	. . . . . . 7
163	162	oveq1d 6323	. . . . . 6
164	160, 163	eqtr4d 2508	. . . . 5
165		dquart.j	. . . . 5
166		dquart.j2	. . . . . 6
167	5	sqcld 12452	. . . . . . . . 9
168	167	negcld 9992	. . . . . . . 8
169	10	halfcld 10880	. . . . . . . 8
170	168, 169	subcld 10005	. . . . . . 7
171	51, 5, 61	divcld 10405	. . . . . . 7
172	170, 171	negsubd 10011	. . . . . 6
173		sqneg 12373	. . . . . . . . . . 11
174	5, 173	syl 17	. . . . . . . . . 10
175	174	eqcomd 2477	. . . . . . . . 9
176	175	negeqd 9889	. . . . . . . 8
177	176	oveq1d 6323	. . . . . . 7
178	51, 5, 61	divneg2d 10419	. . . . . . 7
179	177, 178	oveq12d 6326	. . . . . 6
180	166, 172, 179	3eqtr2d 2511	. . . . 5
181	10, 46, 1, 157, 164, 53, 165, 180	dquartlem1 23856	. . . 4 $\/$
182	52, 5, 61	divneg2d 10419	. . . . . . 7
183	182	oveq2d 6324	. . . . . 6
184	147, 148	negsubd 10011	. . . . . 6
185	183, 184	eqtr3d 2507	. . . . 5
186	185	eqeq1d 2473	. . . 4
187	5	negnegd 9996	. . . . . . 7
188	187	oveq1d 6323	. . . . . 6
189	188	eqeq2d 2481	. . . . 5
190	187	oveq1d 6323	. . . . . 6
191	190	eqeq2d 2481	. . . . 5
192	189, 191	orbi12d 724	. . . 4 $\/$ $\/$
193	181, 186, 192	3bitr3d 291	. . 3 $\/$
194	156, 193	orbi12d 724	. 2 $\/$ $\/$ $\/$ $\/$
195	152, 155, 194	3bitrd 287	1 $\/$ $\/$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $\/$ wo 375 $/\$ wa 376

wceq 1452

wcel 1904

wne 2641 (class class class)co 6308

cc 9555

cc0 9557

caddc 9560

cmul 9562

cmin 9880

cneg 9881

cdiv 10291

c2 10681

c3 10682

c4 10683

cn0 10893

cexp 12310

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-er 7381 df-en 7588 df-dom 7589 df-sdom 7590 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-4 10692 df-n0 10894 df-z 10962 df-uz 11183 df-seq 12252 df-exp 12311

This theorem is referenced by: quart 23866

W3C validator