mul4sqlem - Metamath Proof Explorer

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

Theorem mul4sqlem 15657

Description: Lemma for mul4sq 15658: algebraic manipulations. The extra assumptions involving

are for a part of 4sqlem17 15665 which needs to know not just that the product is a sum of squares, but also that it preserves divisibility by

. (Contributed by Mario Carneiro, 14-Jul-2014.)

**Hypotheses**
Ref	Expression
4sq.1
mul4sq.1
mul4sq.2
mul4sq.3
mul4sq.4
mul4sq.5
mul4sq.6
mul4sq.7
mul4sq.8
mul4sq.9
mul4sq.10

**Assertion**
Ref	Expression
mul4sqlem

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

**Proof of Theorem mul4sqlem**
Step	Hyp	Ref	Expression
1		mul4sq.1	. . . . . . . . . . 11
2		gzcn 15636	. . . . . . . . . . 11
3	1, 2	syl 17	. . . . . . . . . 10
4		mul4sq.3	. . . . . . . . . . 11
5		gzcn 15636	. . . . . . . . . . 11
6	4, 5	syl 17	. . . . . . . . . 10
7	3, 6	mulcld 10060	. . . . . . . . 9
8	7	absvalsqd 14181	. . . . . . . 8
9	7	cjcld 13936	. . . . . . . . 9
10	7, 9	mulcld 10060	. . . . . . . 8
11	8, 10	eqeltrd 2701	. . . . . . 7
12		mul4sq.2	. . . . . . . . . . 11
13		gzcn 15636	. . . . . . . . . . 11
14	12, 13	syl 17	. . . . . . . . . 10
15		mul4sq.4	. . . . . . . . . . 11
16		gzcn 15636	. . . . . . . . . . 11
17	15, 16	syl 17	. . . . . . . . . 10
18	14, 17	mulcld 10060	. . . . . . . . 9
19	18	absvalsqd 14181	. . . . . . . 8
20	18	cjcld 13936	. . . . . . . . 9
21	18, 20	mulcld 10060	. . . . . . . 8
22	19, 21	eqeltrd 2701	. . . . . . 7
23	11, 22	addcld 10059	. . . . . 6
24	3	cjcld 13936	. . . . . . . . 9
25	24, 6	mulcld 10060	. . . . . . . 8
26	14	cjcld 13936	. . . . . . . . 9
27	26, 17	mulcld 10060	. . . . . . . 8
28	25, 27	mulcld 10060	. . . . . . 7
29	6	cjcld 13936	. . . . . . . . 9
30	14, 29	mulcld 10060	. . . . . . . 8
31	17	cjcld 13936	. . . . . . . . 9
32	3, 31	mulcld 10060	. . . . . . . 8
33	30, 32	mulcld 10060	. . . . . . 7
34	28, 33	addcld 10059	. . . . . 6
35	3, 17	mulcld 10060	. . . . . . . . 9
36	35	absvalsqd 14181	. . . . . . . 8
37	35	cjcld 13936	. . . . . . . . 9
38	35, 37	mulcld 10060	. . . . . . . 8
39	36, 38	eqeltrd 2701	. . . . . . 7
40	14, 6	mulcld 10060	. . . . . . . . 9
41	40	absvalsqd 14181	. . . . . . . 8
42	40	cjcld 13936	. . . . . . . . 9
43	40, 42	mulcld 10060	. . . . . . . 8
44	41, 43	eqeltrd 2701	. . . . . . 7
45	39, 44	addcld 10059	. . . . . 6
46	23, 34, 45	ppncand 10432	. . . . 5
47	14, 31	mulcld 10060	. . . . . . . . 9
48	25, 47	addcld 10059	. . . . . . . 8
49	48	absvalsqd 14181	. . . . . . 7
50	25, 47	cjaddd 13960	. . . . . . . . 9
51	24, 6	cjmuld 13961	. . . . . . . . . . 11
52	3	cjcjd 13939	. . . . . . . . . . . 12
53	52	oveq1d 6665	. . . . . . . . . . 11
54	51, 53	eqtrd 2656	. . . . . . . . . 10
55	14, 31	cjmuld 13961	. . . . . . . . . . 11
56	17	cjcjd 13939	. . . . . . . . . . . 12
57	56	oveq2d 6666	. . . . . . . . . . 11
58	55, 57	eqtrd 2656	. . . . . . . . . 10
59	54, 58	oveq12d 6668	. . . . . . . . 9
60	50, 59	eqtrd 2656	. . . . . . . 8
61	60	oveq2d 6666	. . . . . . 7
62	3, 29	mulcld 10060	. . . . . . . . . . 11
63	25, 62, 27	adddid 10064	. . . . . . . . . 10
64	6, 24, 3, 29	mul4d 10248	. . . . . . . . . . . . 13
65	24, 6	mulcomd 10061	. . . . . . . . . . . . . 14
66	65	oveq1d 6665	. . . . . . . . . . . . 13
67	3, 6	mulcomd 10061	. . . . . . . . . . . . . 14
68	3, 6	cjmuld 13961	. . . . . . . . . . . . . 14
69	67, 68	oveq12d 6668	. . . . . . . . . . . . 13
70	64, 66, 69	3eqtr4d 2666	. . . . . . . . . . . 12
71	70, 8	eqtr4d 2659	. . . . . . . . . . 11
72	71	oveq1d 6665	. . . . . . . . . 10
73	63, 72	eqtrd 2656	. . . . . . . . 9
74	47, 62, 27	adddid 10064	. . . . . . . . . 10
75	3, 29	mulcomd 10061	. . . . . . . . . . . . 13
76	75	oveq2d 6666	. . . . . . . . . . . 12
77	14, 31, 29, 3	mul4d 10248	. . . . . . . . . . . 12
78	31, 3	mulcomd 10061	. . . . . . . . . . . . 13
79	78	oveq2d 6666	. . . . . . . . . . . 12
80	76, 77, 79	3eqtrd 2660	. . . . . . . . . . 11
81	14, 31, 17, 26	mul4d 10248	. . . . . . . . . . . . 13
82	26, 17	mulcomd 10061	. . . . . . . . . . . . . 14
83	82	oveq2d 6666	. . . . . . . . . . . . 13
84	14, 17	cjmuld 13961	. . . . . . . . . . . . . . 15
85	26, 31	mulcomd 10061	. . . . . . . . . . . . . . 15
86	84, 85	eqtrd 2656	. . . . . . . . . . . . . 14
87	86	oveq2d 6666	. . . . . . . . . . . . 13
88	81, 83, 87	3eqtr4d 2666	. . . . . . . . . . . 12
89	88, 19	eqtr4d 2659	. . . . . . . . . . 11
90	80, 89	oveq12d 6668	. . . . . . . . . 10
91	74, 90	eqtrd 2656	. . . . . . . . 9
92	73, 91	oveq12d 6668	. . . . . . . 8
93	62, 27	addcld 10059	. . . . . . . . 9
94	25, 47, 93	adddird 10065	. . . . . . . 8
95	11, 22, 28, 33	add42d 10265	. . . . . . . 8
96	92, 94, 95	3eqtr4d 2666	. . . . . . 7
97	49, 61, 96	3eqtrd 2660	. . . . . 6
98	24, 17	mulcld 10060	. . . . . . . . 9
99	98, 30	subcld 10392	. . . . . . . 8
100	99	absvalsqd 14181	. . . . . . 7
101		cjsub 13889	. . . . . . . . . 10 $/\$
102	98, 30, 101	syl2anc 693	. . . . . . . . 9
103	24, 17	cjmuld 13961	. . . . . . . . . . 11
104	52	oveq1d 6665	. . . . . . . . . . 11
105	103, 104	eqtrd 2656	. . . . . . . . . 10
106	14, 29	cjmuld 13961	. . . . . . . . . . 11
107	6	cjcjd 13939	. . . . . . . . . . . 12
108	107	oveq2d 6666	. . . . . . . . . . 11
109	106, 108	eqtrd 2656	. . . . . . . . . 10
110	105, 109	oveq12d 6668	. . . . . . . . 9
111	102, 110	eqtrd 2656	. . . . . . . 8
112	111	oveq2d 6666	. . . . . . 7
113	26, 6	mulcld 10060	. . . . . . . . . 10
114	32, 113	subcld 10392	. . . . . . . . 9
115	98, 30, 114	subdird 10487	. . . . . . . 8
116	98, 32, 113	subdid 10486	. . . . . . . . . 10
117	17, 24, 3, 31	mul4d 10248	. . . . . . . . . . . . 13
118	24, 17	mulcomd 10061	. . . . . . . . . . . . . 14
119	118	oveq1d 6665	. . . . . . . . . . . . 13
120	3, 17	mulcomd 10061	. . . . . . . . . . . . . 14
121	3, 17	cjmuld 13961	. . . . . . . . . . . . . 14
122	120, 121	oveq12d 6668	. . . . . . . . . . . . 13
123	117, 119, 122	3eqtr4d 2666	. . . . . . . . . . . 12
124	123, 36	eqtr4d 2659	. . . . . . . . . . 11
125	26, 6	mulcomd 10061	. . . . . . . . . . . . 13
126	125	oveq2d 6666	. . . . . . . . . . . 12
127	24, 17, 6, 26	mul4d 10248	. . . . . . . . . . . 12
128	17, 26	mulcomd 10061	. . . . . . . . . . . . 13
129	128	oveq2d 6666	. . . . . . . . . . . 12
130	126, 127, 129	3eqtrd 2660	. . . . . . . . . . 11
131	124, 130	oveq12d 6668	. . . . . . . . . 10
132	116, 131	eqtrd 2656	. . . . . . . . 9
133	30, 32, 113	subdid 10486	. . . . . . . . . 10
134	125	oveq2d 6666	. . . . . . . . . . . . 13
135	14, 29, 6, 26	mul4d 10248	. . . . . . . . . . . . 13
136	29, 26	mulcomd 10061	. . . . . . . . . . . . . . 15
137	14, 6	cjmuld 13961	. . . . . . . . . . . . . . 15
138	136, 137	eqtr4d 2659	. . . . . . . . . . . . . 14
139	138	oveq2d 6666	. . . . . . . . . . . . 13
140	134, 135, 139	3eqtrd 2660	. . . . . . . . . . . 12
141	140, 41	eqtr4d 2659	. . . . . . . . . . 11
142	141	oveq2d 6666	. . . . . . . . . 10
143	133, 142	eqtrd 2656	. . . . . . . . 9
144	132, 143	oveq12d 6668	. . . . . . . 8
145	39, 28, 33, 44	subadd4d 10440	. . . . . . . 8
146	115, 144, 145	3eqtrd 2660	. . . . . . 7
147	100, 112, 146	3eqtrd 2660	. . . . . 6
148	97, 147	oveq12d 6668	. . . . 5
149	3, 24	mulcld 10060	. . . . . . . 8
150	14, 26	mulcld 10060	. . . . . . . 8
151	6, 29	mulcld 10060	. . . . . . . . 9
152	17, 31	mulcld 10060	. . . . . . . . 9
153	151, 152	addcld 10059	. . . . . . . 8
154	149, 150, 153	adddird 10065	. . . . . . 7
155	68	oveq2d 6666	. . . . . . . . . . 11
156	3, 6, 24, 29	mul4d 10248	. . . . . . . . . . 11
157	8, 155, 156	3eqtrd 2660	. . . . . . . . . 10
158	121	oveq2d 6666	. . . . . . . . . . 11
159	3, 17, 24, 31	mul4d 10248	. . . . . . . . . . 11
160	36, 158, 159	3eqtrd 2660	. . . . . . . . . 10
161	157, 160	oveq12d 6668	. . . . . . . . 9
162	149, 151, 152	adddid 10064	. . . . . . . . 9
163	161, 162	eqtr4d 2659	. . . . . . . 8
164	137	oveq2d 6666	. . . . . . . . . . 11
165	14, 6, 26, 29	mul4d 10248	. . . . . . . . . . 11
166	41, 164, 165	3eqtrd 2660	. . . . . . . . . 10
167	84	oveq2d 6666	. . . . . . . . . . 11
168	14, 17, 26, 31	mul4d 10248	. . . . . . . . . . 11
169	19, 167, 168	3eqtrd 2660	. . . . . . . . . 10
170	166, 169	oveq12d 6668	. . . . . . . . 9
171	150, 151, 152	adddid 10064	. . . . . . . . 9
172	170, 171	eqtr4d 2659	. . . . . . . 8
173	163, 172	oveq12d 6668	. . . . . . 7
174	154, 173	eqtr4d 2659	. . . . . 6
175		mul4sq.5	. . . . . . . 8
176	3	absvalsqd 14181	. . . . . . . . 9
177	14	absvalsqd 14181	. . . . . . . . 9
178	176, 177	oveq12d 6668	. . . . . . . 8
179	175, 178	syl5eq 2668	. . . . . . 7
180		mul4sq.6	. . . . . . . 8
181	6	absvalsqd 14181	. . . . . . . . 9
182	17	absvalsqd 14181	. . . . . . . . 9
183	181, 182	oveq12d 6668	. . . . . . . 8
184	180, 183	syl5eq 2668	. . . . . . 7
185	179, 184	oveq12d 6668	. . . . . 6
186	11, 22, 39, 44	add42d 10265	. . . . . 6
187	174, 185, 186	3eqtr4d 2666	. . . . 5
188	46, 148, 187	3eqtr4d 2666	. . . 4
189	188	oveq1d 6665	. . 3
190		mul4sq.7	. . . . . . . . . 10
191	190	nncnd 11036	. . . . . . . . 9
192	190	nnne0d 11065	. . . . . . . . 9
193	48, 191, 192	absdivd 14194	. . . . . . . 8
194	190	nnred 11035	. . . . . . . . . 10
195	190	nnnn0d 11351	. . . . . . . . . . 11
196	195	nn0ge0d 11354	. . . . . . . . . 10
197	194, 196	absidd 14161	. . . . . . . . 9
198	197	oveq2d 6666	. . . . . . . 8
199	193, 198	eqtrd 2656	. . . . . . 7
200	199	oveq1d 6665	. . . . . 6
201	48	abscld 14175	. . . . . . . 8
202	201	recnd 10068	. . . . . . 7
203	202, 191, 192	sqdivd 13021	. . . . . 6
204	200, 203	eqtrd 2656	. . . . 5
205	99, 191, 192	absdivd 14194	. . . . . . . 8
206	197	oveq2d 6666	. . . . . . . 8
207	205, 206	eqtrd 2656	. . . . . . 7
208	207	oveq1d 6665	. . . . . 6
209	99	abscld 14175	. . . . . . . 8
210	209	recnd 10068	. . . . . . 7
211	210, 191, 192	sqdivd 13021	. . . . . 6
212	208, 211	eqtrd 2656	. . . . 5
213	204, 212	oveq12d 6668	. . . 4
214	23, 34	addcld 10059	. . . . . 6
215	97, 214	eqeltrd 2701	. . . . 5
216	45, 34	subcld 10392	. . . . . 6
217	147, 216	eqeltrd 2701	. . . . 5
218	190	nnsqcld 13029	. . . . . 6
219	218	nncnd 11036	. . . . 5
220	218	nnne0d 11065	. . . . 5
221	215, 217, 219, 220	divdird 10839	. . . 4
222	213, 221	eqtr4d 2659	. . 3
223	176, 149	eqeltrd 2701	. . . . . . 7
224	177, 150	eqeltrd 2701	. . . . . . 7
225	223, 224	addcld 10059	. . . . . 6
226	175, 225	syl5eqel 2705	. . . . 5
227	184, 153	eqeltrd 2701	. . . . 5
228	226, 191, 227, 191, 192, 192	divmuldivd 10842	. . . 4
229	191	sqvald 13005	. . . . 5
230	229	oveq2d 6666	. . . 4
231	228, 230	eqtr4d 2659	. . 3
232	189, 222, 231	3eqtr4d 2666	. 2
233	226, 48	nncand 10397	. . . . . . 7
234	149, 150, 25, 47	addsub4d 10439	. . . . . . . . 9
235	179	oveq1d 6665	. . . . . . . . 9
236	24, 3, 6	subdid 10486	. . . . . . . . . . 11
237	24, 3	mulcomd 10061	. . . . . . . . . . . 12
238	237	oveq1d 6665	. . . . . . . . . . 11
239	236, 238	eqtrd 2656	. . . . . . . . . 10
240		cjsub 13889	. . . . . . . . . . . . 13 $/\$
241	14, 17, 240	syl2anc 693	. . . . . . . . . . . 12
242	241	oveq2d 6666	. . . . . . . . . . 11
243	14, 26, 31	subdid 10486	. . . . . . . . . . 11
244	242, 243	eqtrd 2656	. . . . . . . . . 10
245	239, 244	oveq12d 6668	. . . . . . . . 9
246	234, 235, 245	3eqtr4d 2666	. . . . . . . 8
247	246	oveq2d 6666	. . . . . . 7
248	233, 247	eqtr3d 2658	. . . . . 6
249	248	oveq1d 6665	. . . . 5
250	3, 6	subcld 10392	. . . . . . . 8
251	24, 250	mulcld 10060	. . . . . . 7
252	14, 17	subcld 10392	. . . . . . . . 9
253	252	cjcld 13936	. . . . . . . 8
254	14, 253	mulcld 10060	. . . . . . 7
255	251, 254	addcld 10059	. . . . . 6
256	226, 255, 191, 192	divsubdird 10840	. . . . 5
257	251, 254, 191, 192	divdird 10839	. . . . . . 7
258	24, 250, 191, 192	divassd 10836	. . . . . . . 8
259	14, 253, 191, 192	divassd 10836	. . . . . . . . 9
260	252, 191, 192	cjdivd 13963	. . . . . . . . . . 11
261	194	cjred 13966	. . . . . . . . . . . 12
262	261	oveq2d 6666	. . . . . . . . . . 11
263	260, 262	eqtrd 2656	. . . . . . . . . 10
264	263	oveq2d 6666	. . . . . . . . 9
265	259, 264	eqtr4d 2659	. . . . . . . 8
266	258, 265	oveq12d 6668	. . . . . . 7
267	257, 266	eqtrd 2656	. . . . . 6
268	267	oveq2d 6666	. . . . 5
269	249, 256, 268	3eqtrd 2660	. . . 4
270		mul4sq.10	. . . . . . 7
271	270	nn0zd 11480	. . . . . 6
272		zgz 15637	. . . . . 6
273	271, 272	syl 17	. . . . 5
274		gzcjcl 15640	. . . . . . . 8
275	1, 274	syl 17	. . . . . . 7
276		mul4sq.8	. . . . . . 7
277		gzmulcl 15642	. . . . . . 7 $/\$
278	275, 276, 277	syl2anc 693	. . . . . 6
279		mul4sq.9	. . . . . . . 8
280		gzcjcl 15640	. . . . . . . 8
281	279, 280	syl 17	. . . . . . 7
282		gzmulcl 15642	. . . . . . 7 $/\$
283	12, 281, 282	syl2anc 693	. . . . . 6
284		gzaddcl 15641	. . . . . 6 $/\$
285	278, 283, 284	syl2anc 693	. . . . 5
286		gzsubcl 15644	. . . . 5 $/\$
287	273, 285, 286	syl2anc 693	. . . 4
288	269, 287	eqeltrd 2701	. . 3
289	250	cjcld 13936	. . . . . . . 8
290	14, 289	mulcld 10060	. . . . . . 7
291	24, 252	mulcld 10060	. . . . . . 7
292	290, 291, 191, 192	divsubdird 10840	. . . . . 6
293		cjsub 13889	. . . . . . . . . . . 12 $/\$
294	3, 6, 293	syl2anc 693	. . . . . . . . . . 11
295	294	oveq2d 6666	. . . . . . . . . 10
296	14, 24, 29	subdid 10486	. . . . . . . . . 10
297	295, 296	eqtrd 2656	. . . . . . . . 9
298	24, 14, 17	subdid 10486	. . . . . . . . . 10
299	24, 14	mulcomd 10061	. . . . . . . . . . 11
300	299	oveq1d 6665	. . . . . . . . . 10
301	298, 300	eqtrd 2656	. . . . . . . . 9
302	297, 301	oveq12d 6668	. . . . . . . 8
303	14, 24	mulcld 10060	. . . . . . . . 9
304	303, 30, 98	nnncan1d 10426	. . . . . . . 8
305	302, 304	eqtrd 2656	. . . . . . 7
306	305	oveq1d 6665	. . . . . 6
307	292, 306	eqtr3d 2658	. . . . 5
308	14, 289, 191, 192	divassd 10836	. . . . . . 7
309	250, 191, 192	cjdivd 13963	. . . . . . . . 9
310	261	oveq2d 6666	. . . . . . . . 9
311	309, 310	eqtrd 2656	. . . . . . . 8
312	311	oveq2d 6666	. . . . . . 7
313	308, 312	eqtr4d 2659	. . . . . 6
314	24, 252, 191, 192	divassd 10836	. . . . . 6
315	313, 314	oveq12d 6668	. . . . 5
316	307, 315	eqtr3d 2658	. . . 4
317		gzcjcl 15640	. . . . . . 7
318	276, 317	syl 17	. . . . . 6
319		gzmulcl 15642	. . . . . 6 $/\$
320	12, 318, 319	syl2anc 693	. . . . 5
321		gzmulcl 15642	. . . . . 6 $/\$
322	275, 279, 321	syl2anc 693	. . . . 5
323		gzsubcl 15644	. . . . 5 $/\$
324	320, 322, 323	syl2anc 693	. . . 4
325	316, 324	eqeltrd 2701	. . 3
326		4sq.1	. . . 4
327	326	4sqlem4a 15655	. . 3 $/\$
328	288, 325, 327	syl2anc 693	. 2
329	232, 328	eqeltrrd 2702	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wceq 1483

wcel 1990

cab 2608

wrex 2913

cfv 5888 (class class class)co 6650

cc 9934

caddc 9939

cmul 9941

cmin 10266

cdiv 10684

cn 11020

c2 11070

cn0 11292

cz 11377

cexp 12860

ccj 13836

cabs 13974

cgz 15633

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 ax-pre-sup 10014

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-sup 8348 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-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-seq 12802 df-exp 12861 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-gz 15634

This theorem is referenced by: mul4sq 15658 4sqlem17 15665

W3C validator