quart1 - Metamath Proof Explorer

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

Theorem quart1 24583

Description: Depress a quartic equation. (Contributed by Mario Carneiro, 6-May-2015.)

**Hypotheses**
Ref	Expression
quart1.a
quart1.b
quart1.c
quart1.d
quart1.p
quart1.q
quart1.r	; ;;
quart1.x
quart1.y

**Assertion**
Ref	Expression
quart1

**Proof of Theorem quart1**
Step	Hyp	Ref	Expression
1		quart1.y	. . . . . . 7
2	1	oveq1d 6665	. . . . . 6
3		quart1.x	. . . . . . 7
4		quart1.a	. . . . . . . 8
5		4cn 11098	. . . . . . . . 9
6	5	a1i 11	. . . . . . . 8
7		4ne0 11117	. . . . . . . . 9
8	7	a1i 11	. . . . . . . 8
9	4, 6, 8	divcld 10801	. . . . . . 7
10		binom4 24577	. . . . . . 7 $/\$
11	3, 9, 10	syl2anc 693	. . . . . 6
12		3nn0 11310	. . . . . . . . . . 11
13		expcl 12878	. . . . . . . . . . 11 $/\$
14	3, 12, 13	sylancl 694	. . . . . . . . . 10
15	6, 14, 9	mul12d 10245	. . . . . . . . 9
16	4, 6, 8	divcan2d 10803	. . . . . . . . . 10
17	16	oveq2d 6666	. . . . . . . . 9
18	14, 4	mulcomd 10061	. . . . . . . . 9
19	15, 17, 18	3eqtrd 2660	. . . . . . . 8
20	19	oveq2d 6666	. . . . . . 7
21		6nn 11189	. . . . . . . . . . . 12
22	21	nncni 11030	. . . . . . . . . . 11
23	22	a1i 11	. . . . . . . . . 10
24	9	sqcld 13006	. . . . . . . . . 10
25	3	sqcld 13006	. . . . . . . . . 10
26	23, 24, 25	mulassd 10063	. . . . . . . . 9
27		3cn 11095	. . . . . . . . . . . . . . . 16
28		2cn 11091	. . . . . . . . . . . . . . . 16
29		3t2e6 11179	. . . . . . . . . . . . . . . 16
30	27, 28, 29	mulcomli 10047	. . . . . . . . . . . . . . 15
31		8cn 11106	. . . . . . . . . . . . . . . 16
32		8t2e16 11654	. . . . . . . . . . . . . . . 16 ;
33	31, 28, 32	mulcomli 10047	. . . . . . . . . . . . . . 15 ;
34	30, 33	oveq12i 6662	. . . . . . . . . . . . . 14 ;
35		8nn 11191	. . . . . . . . . . . . . . . . 17
36	35	nnne0i 11055	. . . . . . . . . . . . . . . 16
37	31, 36	pm3.2i 471	. . . . . . . . . . . . . . 15 $/\$
38		2cnne0 11242	. . . . . . . . . . . . . . 15 $/\$
39		divcan5 10727	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
40	27, 37, 38, 39	mp3an 1424	. . . . . . . . . . . . . 14
41	34, 40	eqtr3i 2646	. . . . . . . . . . . . 13 ;
42	41	oveq2i 6661	. . . . . . . . . . . 12 ;
43	4	sqcld 13006	. . . . . . . . . . . . 13
44		1nn0 11308	. . . . . . . . . . . . . . . 16
45	44, 21	decnncl 11518	. . . . . . . . . . . . . . 15 ;
46	45	nncni 11030	. . . . . . . . . . . . . 14 ;
47	46	a1i 11	. . . . . . . . . . . . 13 ;
48	45	nnne0i 11055	. . . . . . . . . . . . . 14 ;
49	48	a1i 11	. . . . . . . . . . . . 13 ;
50	43, 23, 47, 49	div12d 10837	. . . . . . . . . . . 12 ; ;
51	42, 50	syl5eqr 2670	. . . . . . . . . . 11 ;
52	27, 31, 36	divcli 10767	. . . . . . . . . . . 12
53		mulcom 10022	. . . . . . . . . . . 12 $/\$
54	52, 43, 53	sylancr 695	. . . . . . . . . . 11
55	4, 6, 8	sqdivd 13021	. . . . . . . . . . . . 13
56	5	sqvali 12943	. . . . . . . . . . . . . . 15
57		4t4e16 11633	. . . . . . . . . . . . . . 15 ;
58	56, 57	eqtri 2644	. . . . . . . . . . . . . 14 ;
59	58	oveq2i 6661	. . . . . . . . . . . . 13 ;
60	55, 59	syl6eq 2672	. . . . . . . . . . . 12 ;
61	60	oveq2d 6666	. . . . . . . . . . 11 ;
62	51, 54, 61	3eqtr4d 2666	. . . . . . . . . 10
63	62	oveq1d 6665	. . . . . . . . 9
64	25, 24	mulcomd 10061	. . . . . . . . . 10
65	64	oveq2d 6666	. . . . . . . . 9
66	26, 63, 65	3eqtr4rd 2667	. . . . . . . 8
67		expcl 12878	. . . . . . . . . . . 12 $/\$
68	9, 12, 67	sylancl 694	. . . . . . . . . . 11
69	6, 3, 68	mul12d 10245	. . . . . . . . . 10
70	6, 68	mulcld 10060	. . . . . . . . . . 11
71	3, 70	mulcomd 10061	. . . . . . . . . 10
72		df-3 11080	. . . . . . . . . . . . . . . . 17
73	72	oveq2i 6661	. . . . . . . . . . . . . . . 16
74		2nn0 11309	. . . . . . . . . . . . . . . . 17
75		expp1 12867	. . . . . . . . . . . . . . . . 17 $/\$
76	5, 74, 75	mp2an 708	. . . . . . . . . . . . . . . 16
77	58	oveq1i 6660	. . . . . . . . . . . . . . . 16 ;
78	73, 76, 77	3eqtri 2648	. . . . . . . . . . . . . . 15 ;
79	78	oveq2i 6661	. . . . . . . . . . . . . 14 ;
80	12	a1i 11	. . . . . . . . . . . . . . 15
81	4, 6, 8, 80	expdivd 13022	. . . . . . . . . . . . . 14
82		expcl 12878	. . . . . . . . . . . . . . . 16 $/\$
83	4, 12, 82	sylancl 694	. . . . . . . . . . . . . . 15
84	83, 47, 6, 49, 8	divdiv1d 10832	. . . . . . . . . . . . . 14 ; ;
85	79, 81, 84	3eqtr4a 2682	. . . . . . . . . . . . 13 ;
86	85	oveq2d 6666	. . . . . . . . . . . 12 ;
87	32	oveq2i 6661	. . . . . . . . . . . . 13 ;
88	31	a1i 11	. . . . . . . . . . . . . 14
89	28	a1i 11	. . . . . . . . . . . . . 14
90	36	a1i 11	. . . . . . . . . . . . . 14
91		2ne0 11113	. . . . . . . . . . . . . . 15
92	91	a1i 11	. . . . . . . . . . . . . 14
93	83, 88, 89, 90, 92	divdiv1d 10832	. . . . . . . . . . . . 13
94	83, 47, 49	divcld 10801	. . . . . . . . . . . . . 14 ;
95	94, 6, 8	divcan2d 10803	. . . . . . . . . . . . 13 ; ;
96	87, 93, 95	3eqtr4a 2682	. . . . . . . . . . . 12 ;
97	86, 96	eqtr4d 2659	. . . . . . . . . . 11
98	97	oveq1d 6665	. . . . . . . . . 10
99	69, 71, 98	3eqtrd 2660	. . . . . . . . 9
100		4nn0 11311	. . . . . . . . . . . 12
101	100	a1i 11	. . . . . . . . . . 11
102	4, 6, 8, 101	expdivd 13022	. . . . . . . . . 10
103		expmul 12905	. . . . . . . . . . . . . . 15 $/\$ $/\$
104	28, 74, 100, 103	mp3an 1424	. . . . . . . . . . . . . 14
105		4t2e8 11181	. . . . . . . . . . . . . . . 16
106	5, 28, 105	mulcomli 10047	. . . . . . . . . . . . . . 15
107	106	oveq2i 6661	. . . . . . . . . . . . . 14
108	104, 107	eqtr3i 2646	. . . . . . . . . . . . 13
109		sq2 12960	. . . . . . . . . . . . . 14
110	109	oveq1i 6660	. . . . . . . . . . . . 13
111	108, 110	eqtr3i 2646	. . . . . . . . . . . 12
112		2exp8 15796	. . . . . . . . . . . 12 ;;
113	111, 112	eqtr3i 2646	. . . . . . . . . . 11 ;;
114	113	oveq2i 6661	. . . . . . . . . 10 ;;
115	102, 114	syl6eq 2672	. . . . . . . . 9 ;;
116	99, 115	oveq12d 6668	. . . . . . . 8 ;;
117	66, 116	oveq12d 6668	. . . . . . 7 ;;
118	20, 117	oveq12d 6668	. . . . . 6 ;;
119	2, 11, 118	3eqtrd 2660	. . . . 5 ;;
120	119	oveq1d 6665	. . . 4 ;;
121		expcl 12878	. . . . . . 7 $/\$
122	3, 100, 121	sylancl 694	. . . . . 6
123	4, 14	mulcld 10060	. . . . . 6
124	122, 123	addcld 10059	. . . . 5
125		mulcl 10020	. . . . . . . 8 $/\$
126	52, 43, 125	sylancr 695	. . . . . . 7
127	126, 25	mulcld 10060	. . . . . 6
128	83, 88, 90	divcld 10801	. . . . . . . . 9
129	128	halfcld 11277	. . . . . . . 8
130	129, 3	mulcld 10060	. . . . . . 7
131		expcl 12878	. . . . . . . . 9 $/\$
132	4, 100, 131	sylancl 694	. . . . . . . 8
133		5nn0 11312	. . . . . . . . . . . 12
134	74, 133	deccl 11512	. . . . . . . . . . 11 ;
135	134, 21	decnncl 11518	. . . . . . . . . 10 ;;
136	135	nncni 11030	. . . . . . . . 9 ;;
137	136	a1i 11	. . . . . . . 8 ;;
138	135	nnne0i 11055	. . . . . . . . 9 ;;
139	138	a1i 11	. . . . . . . 8 ;;
140	132, 137, 139	divcld 10801	. . . . . . 7 ;;
141	130, 140	addcld 10059	. . . . . 6 ;;
142	127, 141	addcld 10059	. . . . 5 ;;
143		quart1.b	. . . . . . . 8
144		quart1.c	. . . . . . . 8
145		quart1.d	. . . . . . . 8
146		quart1.p	. . . . . . . 8
147		quart1.q	. . . . . . . 8
148		quart1.r	. . . . . . . 8 ; ;;
149	4, 143, 144, 145, 146, 147, 148	quart1cl 24581	. . . . . . 7 $/\$ $/\$
150	149	simp1d 1073	. . . . . 6
151	3, 9	addcld 10059	. . . . . . . 8
152	1, 151	eqeltrd 2701	. . . . . . 7
153	152	sqcld 13006	. . . . . 6
154	150, 153	mulcld 10060	. . . . 5
155	124, 142, 154	addassd 10062	. . . 4 ;; ;;
156	120, 155	eqtrd 2656	. . 3 ;;
157	156	oveq1d 6665	. 2 ;;
158	142, 154	addcld 10059	. . 3 ;;
159	149	simp2d 1074	. . . . 5
160	159, 152	mulcld 10060	. . . 4
161	149	simp3d 1075	. . . 4
162	160, 161	addcld 10059	. . 3
163	124, 158, 162	addassd 10062	. 2 ;; ;;
164	1	oveq1d 6665	. . . . . . . . . 10
165		binom2 12979	. . . . . . . . . . 11 $/\$
166	3, 9, 165	syl2anc 693	. . . . . . . . . 10
167	3, 9	mulcld 10060	. . . . . . . . . . . 12
168		mulcl 10020	. . . . . . . . . . . 12 $/\$
169	28, 167, 168	sylancr 695	. . . . . . . . . . 11
170	25, 169, 24	addassd 10062	. . . . . . . . . 10
171	164, 166, 170	3eqtrd 2660	. . . . . . . . 9
172	171	oveq2d 6666	. . . . . . . 8
173	169, 24	addcld 10059	. . . . . . . . 9
174	150, 25, 173	adddid 10064	. . . . . . . 8
175	172, 174	eqtrd 2656	. . . . . . 7
176	175	oveq2d 6666	. . . . . 6 ;; ;;
177	150, 25	mulcld 10060	. . . . . . 7
178	150, 173	mulcld 10060	. . . . . . 7
179	127, 141, 177, 178	add4d 10264	. . . . . 6 ;; ;;
180	126, 150, 25	adddird 10065	. . . . . . . 8
181	146	oveq2d 6666	. . . . . . . . . 10
182	126, 143	pncan3d 10395	. . . . . . . . . 10
183	181, 182	eqtrd 2656	. . . . . . . . 9
184	183	oveq1d 6665	. . . . . . . 8
185	180, 184	eqtr3d 2658	. . . . . . 7
186	185	oveq1d 6665	. . . . . 6 ;; ;;
187	176, 179, 186	3eqtrd 2660	. . . . 5 ;; ;;
188	187	oveq1d 6665	. . . 4 ;; ;;
189	143, 25	mulcld 10060	. . . . 5
190	141, 178	addcld 10059	. . . . 5 ;;
191	189, 190, 162	addassd 10062	. . . 4 ;; ;;
192	4, 143	mulcld 10060	. . . . . . . . . 10
193	192	halfcld 11277	. . . . . . . . 9
194	193, 128	subcld 10392	. . . . . . . 8
195	194, 3	mulcld 10060	. . . . . . 7
196	150, 24	mulcld 10060	. . . . . . . 8
197	140, 196	addcld 10059	. . . . . . 7 ;;
198	159, 3	mulcld 10060	. . . . . . 7
199	159, 9	mulcld 10060	. . . . . . . 8
200	199, 161	addcld 10059	. . . . . . 7
201	195, 197, 198, 200	add4d 10264	. . . . . 6 ;; ;;
202	150, 169, 24	adddid 10064	. . . . . . . . 9
203	202	oveq2d 6666	. . . . . . . 8 ;; ;;
204	150, 169	mulcld 10060	. . . . . . . . 9
205	130, 140, 204, 196	add4d 10264	. . . . . . . 8 ;; ;;
206	4, 89, 89, 92, 92	divdiv1d 10832	. . . . . . . . . . . . . . . . . 18
207		2t2e4 11177	. . . . . . . . . . . . . . . . . . 19
208	207	oveq2i 6661	. . . . . . . . . . . . . . . . . 18
209	206, 208	syl6eq 2672	. . . . . . . . . . . . . . . . 17
210	209	oveq2d 6666	. . . . . . . . . . . . . . . 16
211	4	halfcld 11277	. . . . . . . . . . . . . . . . 17
212	211, 89, 92	divcan2d 10803	. . . . . . . . . . . . . . . 16
213	210, 212	eqtr3d 2658	. . . . . . . . . . . . . . 15
214	213	oveq2d 6666	. . . . . . . . . . . . . 14
215	3, 211	mulcomd 10061	. . . . . . . . . . . . . 14
216	214, 215	eqtrd 2656	. . . . . . . . . . . . 13
217	216	oveq2d 6666	. . . . . . . . . . . 12
218	89, 3, 9	mul12d 10245	. . . . . . . . . . . . 13
219	218	oveq2d 6666	. . . . . . . . . . . 12
220	150, 211, 3	mulassd 10063	. . . . . . . . . . . 12
221	217, 219, 220	3eqtr4d 2666	. . . . . . . . . . 11
222	221	oveq2d 6666	. . . . . . . . . 10
223	150, 211	mulcld 10060	. . . . . . . . . . 11
224	129, 223, 3	adddird 10065	. . . . . . . . . 10
225	146	oveq1d 6665	. . . . . . . . . . . . . 14
226	143, 126, 211	subdird 10487	. . . . . . . . . . . . . 14
227	143, 4, 89, 92	divassd 10836	. . . . . . . . . . . . . . . 16
228	143, 4	mulcomd 10061	. . . . . . . . . . . . . . . . 17
229	228	oveq1d 6665	. . . . . . . . . . . . . . . 16
230	227, 229	eqtr3d 2658	. . . . . . . . . . . . . . 15
231	72	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . 21
232		expp1 12867	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
233	4, 74, 232	sylancl 694	. . . . . . . . . . . . . . . . . . . . 21
234	231, 233	syl5eq 2668	. . . . . . . . . . . . . . . . . . . 20
235	234	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19
236	27	a1i 11	. . . . . . . . . . . . . . . . . . . 20
237	236, 83, 88, 90	div23d 10838	. . . . . . . . . . . . . . . . . . 19
238	52	a1i 11	. . . . . . . . . . . . . . . . . . . 20
239	238, 43, 4	mulassd 10063	. . . . . . . . . . . . . . . . . . 19
240	235, 237, 239	3eqtr4rd 2667	. . . . . . . . . . . . . . . . . 18
241	236, 83, 88, 90	divassd 10836	. . . . . . . . . . . . . . . . . 18
242	240, 241	eqtrd 2656	. . . . . . . . . . . . . . . . 17
243	242	oveq1d 6665	. . . . . . . . . . . . . . . 16
244	126, 4, 89, 92	divassd 10836	. . . . . . . . . . . . . . . 16
245	236, 128, 89, 92	divassd 10836	. . . . . . . . . . . . . . . 16
246	243, 244, 245	3eqtr3d 2664	. . . . . . . . . . . . . . 15
247	230, 246	oveq12d 6668	. . . . . . . . . . . . . 14
248	225, 226, 247	3eqtrd 2660	. . . . . . . . . . . . 13
249	248	oveq2d 6666	. . . . . . . . . . . 12
250		mulcl 10020	. . . . . . . . . . . . . . 15 $/\$
251	27, 129, 250	sylancr 695	. . . . . . . . . . . . . 14
252	129, 193, 251	addsub12d 10415	. . . . . . . . . . . . 13
253	193, 251, 129	subsub2d 10421	. . . . . . . . . . . . 13
254	129	mulid2d 10058	. . . . . . . . . . . . . . . 16
255	254	oveq2d 6666	. . . . . . . . . . . . . . 15
256		3m1e2 11137	. . . . . . . . . . . . . . . . 17
257	256	oveq1i 6660	. . . . . . . . . . . . . . . 16
258		1cnd 10056	. . . . . . . . . . . . . . . . 17
259	236, 258, 129	subdird 10487	. . . . . . . . . . . . . . . 16
260	128, 89, 92	divcan2d 10803	. . . . . . . . . . . . . . . 16
261	257, 259, 260	3eqtr3a 2680	. . . . . . . . . . . . . . 15
262	255, 261	eqtr3d 2658	. . . . . . . . . . . . . 14
263	262	oveq2d 6666	. . . . . . . . . . . . 13
264	252, 253, 263	3eqtr2d 2662	. . . . . . . . . . . 12
265	249, 264	eqtrd 2656	. . . . . . . . . . 11
266	265	oveq1d 6665	. . . . . . . . . 10
267	222, 224, 266	3eqtr2d 2662	. . . . . . . . 9
268	267	oveq1d 6665	. . . . . . . 8 ;; ;;
269	203, 205, 268	3eqtrd 2660	. . . . . . 7 ;; ;;
270	1	oveq2d 6666	. . . . . . . . . 10
271	159, 3, 9	adddid 10064	. . . . . . . . . 10
272	270, 271	eqtrd 2656	. . . . . . . . 9
273	272	oveq1d 6665	. . . . . . . 8
274	198, 199, 161	addassd 10062	. . . . . . . 8
275	273, 274	eqtrd 2656	. . . . . . 7
276	269, 275	oveq12d 6668	. . . . . 6 ;; ;;
277	194, 159	addcomd 10238	. . . . . . . . . 10
278	147	oveq1d 6665	. . . . . . . . . 10
279	144, 193	subcld 10392	. . . . . . . . . . . 12
280	279, 128, 193	ppncand 10432	. . . . . . . . . . 11
281	144, 193	npcand 10396	. . . . . . . . . . 11
282	280, 281	eqtrd 2656	. . . . . . . . . 10
283	277, 278, 282	3eqtrd 2660	. . . . . . . . 9
284	283	oveq1d 6665	. . . . . . . 8
285	194, 159, 3	adddird 10065	. . . . . . . 8
286	284, 285	eqtr3d 2658	. . . . . . 7
287	4, 143, 144, 145, 146, 147, 148, 3, 1	quart1lem 24582	. . . . . . 7 ;;
288	286, 287	oveq12d 6668	. . . . . 6 ;;
289	201, 276, 288	3eqtr4d 2666	. . . . 5 ;;
290	289	oveq2d 6666	. . . 4 ;;
291	188, 191, 290	3eqtrd 2660	. . 3 ;;
292	291	oveq2d 6666	. 2 ;;
293	157, 163, 292	3eqtrrd 2661	1

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 384

wceq 1483

wcel 1990

wne 2794 (class class class)co 6650

cc 9934

cc0 9936

c1 9937

caddc 9939

cmul 9941

cmin 10266

cdiv 10684

c2 11070

c3 11071

c4 11072

c5 11073

c6 11074

c8 11076

cn0 11292 ;cdc 11493

cexp 12860

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-seq 12802 df-exp 12861

This theorem is referenced by: quart 24588

W3C validator