mul4sqlem - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > mul4sqlem		Unicode version

Theorem mul4sqlem 13029

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

would let us 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 13008	. . . . . . . . . . 11
3	1, 2	syl 14	. . . . . . . . . 10
4		mul4sq.3	. . . . . . . . . . 11
5		gzcn 13008	. . . . . . . . . . 11
6	4, 5	syl 14	. . . . . . . . . 10
7	3, 6	mulcld 8242	. . . . . . . . 9
8	7	absvalsqd 11805	. . . . . . . 8
9	7	cjcld 11563	. . . . . . . . 9
10	7, 9	mulcld 8242	. . . . . . . 8
11	8, 10	eqeltrd 2308	. . . . . . 7
12		mul4sq.2	. . . . . . . . . . 11
13		gzcn 13008	. . . . . . . . . . 11
14	12, 13	syl 14	. . . . . . . . . 10
15		mul4sq.4	. . . . . . . . . . 11
16		gzcn 13008	. . . . . . . . . . 11
17	15, 16	syl 14	. . . . . . . . . 10
18	14, 17	mulcld 8242	. . . . . . . . 9
19	18	absvalsqd 11805	. . . . . . . 8
20	18	cjcld 11563	. . . . . . . . 9
21	18, 20	mulcld 8242	. . . . . . . 8
22	19, 21	eqeltrd 2308	. . . . . . 7
23	11, 22	addcld 8241	. . . . . 6
24	3	cjcld 11563	. . . . . . . . 9
25	24, 6	mulcld 8242	. . . . . . . 8
26	14	cjcld 11563	. . . . . . . . 9
27	26, 17	mulcld 8242	. . . . . . . 8
28	25, 27	mulcld 8242	. . . . . . 7
29	6	cjcld 11563	. . . . . . . . 9
30	14, 29	mulcld 8242	. . . . . . . 8
31	17	cjcld 11563	. . . . . . . . 9
32	3, 31	mulcld 8242	. . . . . . . 8
33	30, 32	mulcld 8242	. . . . . . 7
34	28, 33	addcld 8241	. . . . . 6
35	3, 17	mulcld 8242	. . . . . . . . 9
36	35	absvalsqd 11805	. . . . . . . 8
37	35	cjcld 11563	. . . . . . . . 9
38	35, 37	mulcld 8242	. . . . . . . 8
39	36, 38	eqeltrd 2308	. . . . . . 7
40	14, 6	mulcld 8242	. . . . . . . . 9
41	40	absvalsqd 11805	. . . . . . . 8
42	40	cjcld 11563	. . . . . . . . 9
43	40, 42	mulcld 8242	. . . . . . . 8
44	41, 43	eqeltrd 2308	. . . . . . 7
45	39, 44	addcld 8241	. . . . . 6
46	23, 34, 45	ppncand 8572	. . . . 5
47	14, 31	mulcld 8242	. . . . . . . . 9
48	25, 47	addcld 8241	. . . . . . . 8
49	48	absvalsqd 11805	. . . . . . 7
50	25, 47	cjaddd 11588	. . . . . . . . 9
51	24, 6	cjmuld 11589	. . . . . . . . . . 11
52	3	cjcjd 11566	. . . . . . . . . . . 12
53	52	oveq1d 6043	. . . . . . . . . . 11
54	51, 53	eqtrd 2264	. . . . . . . . . 10
55	14, 31	cjmuld 11589	. . . . . . . . . . 11
56	17	cjcjd 11566	. . . . . . . . . . . 12
57	56	oveq2d 6044	. . . . . . . . . . 11
58	55, 57	eqtrd 2264	. . . . . . . . . 10
59	54, 58	oveq12d 6046	. . . . . . . . 9
60	50, 59	eqtrd 2264	. . . . . . . 8
61	60	oveq2d 6044	. . . . . . 7
62	3, 29	mulcld 8242	. . . . . . . . . . 11
63	25, 62, 27	adddid 8246	. . . . . . . . . 10
64	6, 24, 3, 29	mul4d 8376	. . . . . . . . . . . . 13
65	24, 6	mulcomd 8243	. . . . . . . . . . . . . 14
66	65	oveq1d 6043	. . . . . . . . . . . . 13
67	3, 6	mulcomd 8243	. . . . . . . . . . . . . 14
68	3, 6	cjmuld 11589	. . . . . . . . . . . . . 14
69	67, 68	oveq12d 6046	. . . . . . . . . . . . 13
70	64, 66, 69	3eqtr4d 2274	. . . . . . . . . . . 12
71	70, 8	eqtr4d 2267	. . . . . . . . . . 11
72	71	oveq1d 6043	. . . . . . . . . 10
73	63, 72	eqtrd 2264	. . . . . . . . 9
74	47, 62, 27	adddid 8246	. . . . . . . . . 10
75	3, 29	mulcomd 8243	. . . . . . . . . . . . 13
76	75	oveq2d 6044	. . . . . . . . . . . 12
77	14, 31, 29, 3	mul4d 8376	. . . . . . . . . . . 12
78	31, 3	mulcomd 8243	. . . . . . . . . . . . 13
79	78	oveq2d 6044	. . . . . . . . . . . 12
80	76, 77, 79	3eqtrd 2268	. . . . . . . . . . 11
81	14, 31, 17, 26	mul4d 8376	. . . . . . . . . . . . 13
82	26, 17	mulcomd 8243	. . . . . . . . . . . . . 14
83	82	oveq2d 6044	. . . . . . . . . . . . 13
84	14, 17	cjmuld 11589	. . . . . . . . . . . . . . 15
85	26, 31	mulcomd 8243	. . . . . . . . . . . . . . 15
86	84, 85	eqtrd 2264	. . . . . . . . . . . . . 14
87	86	oveq2d 6044	. . . . . . . . . . . . 13
88	81, 83, 87	3eqtr4d 2274	. . . . . . . . . . . 12
89	88, 19	eqtr4d 2267	. . . . . . . . . . 11
90	80, 89	oveq12d 6046	. . . . . . . . . 10
91	74, 90	eqtrd 2264	. . . . . . . . 9
92	73, 91	oveq12d 6046	. . . . . . . 8
93	62, 27	addcld 8241	. . . . . . . . 9
94	25, 47, 93	adddird 8247	. . . . . . . 8
95	11, 22, 28, 33	add42d 8391	. . . . . . . 8
96	92, 94, 95	3eqtr4d 2274	. . . . . . 7
97	49, 61, 96	3eqtrd 2268	. . . . . 6
98	24, 17	mulcld 8242	. . . . . . . . 9
99	98, 30	subcld 8532	. . . . . . . 8
100	99	absvalsqd 11805	. . . . . . 7
101		cjsub 11515	. . . . . . . . . 10 $/\$
102	98, 30, 101	syl2anc 411	. . . . . . . . 9
103	24, 17	cjmuld 11589	. . . . . . . . . . 11
104	52	oveq1d 6043	. . . . . . . . . . 11
105	103, 104	eqtrd 2264	. . . . . . . . . 10
106	14, 29	cjmuld 11589	. . . . . . . . . . 11
107	6	cjcjd 11566	. . . . . . . . . . . 12
108	107	oveq2d 6044	. . . . . . . . . . 11
109	106, 108	eqtrd 2264	. . . . . . . . . 10
110	105, 109	oveq12d 6046	. . . . . . . . 9
111	102, 110	eqtrd 2264	. . . . . . . 8
112	111	oveq2d 6044	. . . . . . 7
113	26, 6	mulcld 8242	. . . . . . . . . 10
114	32, 113	subcld 8532	. . . . . . . . 9
115	98, 30, 114	subdird 8636	. . . . . . . 8
116	98, 32, 113	subdid 8635	. . . . . . . . . 10
117	17, 24, 3, 31	mul4d 8376	. . . . . . . . . . . . 13
118	24, 17	mulcomd 8243	. . . . . . . . . . . . . 14
119	118	oveq1d 6043	. . . . . . . . . . . . 13
120	3, 17	mulcomd 8243	. . . . . . . . . . . . . 14
121	3, 17	cjmuld 11589	. . . . . . . . . . . . . 14
122	120, 121	oveq12d 6046	. . . . . . . . . . . . 13
123	117, 119, 122	3eqtr4d 2274	. . . . . . . . . . . 12
124	123, 36	eqtr4d 2267	. . . . . . . . . . 11
125	26, 6	mulcomd 8243	. . . . . . . . . . . . 13
126	125	oveq2d 6044	. . . . . . . . . . . 12
127	24, 17, 6, 26	mul4d 8376	. . . . . . . . . . . 12
128	17, 26	mulcomd 8243	. . . . . . . . . . . . 13
129	128	oveq2d 6044	. . . . . . . . . . . 12
130	126, 127, 129	3eqtrd 2268	. . . . . . . . . . 11
131	124, 130	oveq12d 6046	. . . . . . . . . 10
132	116, 131	eqtrd 2264	. . . . . . . . 9
133	30, 32, 113	subdid 8635	. . . . . . . . . 10
134	125	oveq2d 6044	. . . . . . . . . . . . 13
135	14, 29, 6, 26	mul4d 8376	. . . . . . . . . . . . 13
136	29, 26	mulcomd 8243	. . . . . . . . . . . . . . 15
137	14, 6	cjmuld 11589	. . . . . . . . . . . . . . 15
138	136, 137	eqtr4d 2267	. . . . . . . . . . . . . 14
139	138	oveq2d 6044	. . . . . . . . . . . . 13
140	134, 135, 139	3eqtrd 2268	. . . . . . . . . . . 12
141	140, 41	eqtr4d 2267	. . . . . . . . . . 11
142	141	oveq2d 6044	. . . . . . . . . 10
143	133, 142	eqtrd 2264	. . . . . . . . 9
144	132, 143	oveq12d 6046	. . . . . . . 8
145	39, 28, 33, 44	subadd4d 8580	. . . . . . . 8
146	115, 144, 145	3eqtrd 2268	. . . . . . 7
147	100, 112, 146	3eqtrd 2268	. . . . . 6
148	97, 147	oveq12d 6046	. . . . 5
149	3, 24	mulcld 8242	. . . . . . . 8
150	14, 26	mulcld 8242	. . . . . . . 8
151	6, 29	mulcld 8242	. . . . . . . . 9
152	17, 31	mulcld 8242	. . . . . . . . 9
153	151, 152	addcld 8241	. . . . . . . 8
154	149, 150, 153	adddird 8247	. . . . . . 7
155	68	oveq2d 6044	. . . . . . . . . . 11
156	3, 6, 24, 29	mul4d 8376	. . . . . . . . . . 11
157	8, 155, 156	3eqtrd 2268	. . . . . . . . . 10
158	121	oveq2d 6044	. . . . . . . . . . 11
159	3, 17, 24, 31	mul4d 8376	. . . . . . . . . . 11
160	36, 158, 159	3eqtrd 2268	. . . . . . . . . 10
161	157, 160	oveq12d 6046	. . . . . . . . 9
162	149, 151, 152	adddid 8246	. . . . . . . . 9
163	161, 162	eqtr4d 2267	. . . . . . . 8
164	137	oveq2d 6044	. . . . . . . . . . 11
165	14, 6, 26, 29	mul4d 8376	. . . . . . . . . . 11
166	41, 164, 165	3eqtrd 2268	. . . . . . . . . 10
167	84	oveq2d 6044	. . . . . . . . . . 11
168	14, 17, 26, 31	mul4d 8376	. . . . . . . . . . 11
169	19, 167, 168	3eqtrd 2268	. . . . . . . . . 10
170	166, 169	oveq12d 6046	. . . . . . . . 9
171	150, 151, 152	adddid 8246	. . . . . . . . 9
172	170, 171	eqtr4d 2267	. . . . . . . 8
173	163, 172	oveq12d 6046	. . . . . . 7
174	154, 173	eqtr4d 2267	. . . . . 6
175		mul4sq.5	. . . . . . . 8
176	3	absvalsqd 11805	. . . . . . . . 9
177	14	absvalsqd 11805	. . . . . . . . 9
178	176, 177	oveq12d 6046	. . . . . . . 8
179	175, 178	eqtrid 2276	. . . . . . 7
180		mul4sq.6	. . . . . . . 8
181	6	absvalsqd 11805	. . . . . . . . 9
182	17	absvalsqd 11805	. . . . . . . . 9
183	181, 182	oveq12d 6046	. . . . . . . 8
184	180, 183	eqtrid 2276	. . . . . . 7
185	179, 184	oveq12d 6046	. . . . . 6
186	11, 22, 39, 44	add42d 8391	. . . . . 6
187	174, 185, 186	3eqtr4d 2274	. . . . 5
188	46, 148, 187	3eqtr4d 2274	. . . 4
189	188	oveq1d 6043	. . 3
190		mul4sq.7	. . . . . . . . . 10
191	190	nncnd 9199	. . . . . . . . 9
192	190	nnap0d 9231	. . . . . . . . 9 #
193	48, 191, 192	absdivapd 11818	. . . . . . . 8
194	190	nnred 9198	. . . . . . . . . 10
195	190	nnnn0d 9499	. . . . . . . . . . 11
196	195	nn0ge0d 9502	. . . . . . . . . 10
197	194, 196	absidd 11790	. . . . . . . . 9
198	197	oveq2d 6044	. . . . . . . 8
199	193, 198	eqtrd 2264	. . . . . . 7
200	199	oveq1d 6043	. . . . . 6
201	48	abscld 11804	. . . . . . . 8
202	201	recnd 8250	. . . . . . 7
203	202, 191, 192	sqdivapd 10994	. . . . . 6
204	200, 203	eqtrd 2264	. . . . 5
205	99, 191, 192	absdivapd 11818	. . . . . . . 8
206	197	oveq2d 6044	. . . . . . . 8
207	205, 206	eqtrd 2264	. . . . . . 7
208	207	oveq1d 6043	. . . . . 6
209	99	abscld 11804	. . . . . . . 8
210	209	recnd 8250	. . . . . . 7
211	210, 191, 192	sqdivapd 10994	. . . . . 6
212	208, 211	eqtrd 2264	. . . . 5
213	204, 212	oveq12d 6046	. . . 4
214	23, 34	addcld 8241	. . . . . 6
215	97, 214	eqeltrd 2308	. . . . 5
216	45, 34	subcld 8532	. . . . . 6
217	147, 216	eqeltrd 2308	. . . . 5
218	190	nnsqcld 11002	. . . . . 6
219	218	nncnd 9199	. . . . 5
220	218	nnap0d 9231	. . . . 5 #
221	215, 217, 219, 220	divdirapd 9051	. . . 4
222	213, 221	eqtr4d 2267	. . 3
223	176, 149	eqeltrd 2308	. . . . . . 7
224	177, 150	eqeltrd 2308	. . . . . . 7
225	223, 224	addcld 8241	. . . . . 6
226	175, 225	eqeltrid 2318	. . . . 5
227	184, 153	eqeltrd 2308	. . . . 5
228	226, 191, 227, 191, 192, 192	divmuldivapd 9054	. . . 4
229	191	sqvald 10978	. . . . 5
230	229	oveq2d 6044	. . . 4
231	228, 230	eqtr4d 2267	. . 3
232	189, 222, 231	3eqtr4d 2274	. 2
233	226, 48	nncand 8537	. . . . . . 7
234	149, 150, 25, 47	addsub4d 8579	. . . . . . . . 9
235	179	oveq1d 6043	. . . . . . . . 9
236	24, 3, 6	subdid 8635	. . . . . . . . . . 11
237	24, 3	mulcomd 8243	. . . . . . . . . . . 12
238	237	oveq1d 6043	. . . . . . . . . . 11
239	236, 238	eqtrd 2264	. . . . . . . . . 10
240		cjsub 11515	. . . . . . . . . . . . 13 $/\$
241	14, 17, 240	syl2anc 411	. . . . . . . . . . . 12
242	241	oveq2d 6044	. . . . . . . . . . 11
243	14, 26, 31	subdid 8635	. . . . . . . . . . 11
244	242, 243	eqtrd 2264	. . . . . . . . . 10
245	239, 244	oveq12d 6046	. . . . . . . . 9
246	234, 235, 245	3eqtr4d 2274	. . . . . . . 8
247	246	oveq2d 6044	. . . . . . 7
248	233, 247	eqtr3d 2266	. . . . . 6
249	248	oveq1d 6043	. . . . 5
250	3, 6	subcld 8532	. . . . . . . 8
251	24, 250	mulcld 8242	. . . . . . 7
252	14, 17	subcld 8532	. . . . . . . . 9
253	252	cjcld 11563	. . . . . . . 8
254	14, 253	mulcld 8242	. . . . . . 7
255	251, 254	addcld 8241	. . . . . 6
256	226, 255, 191, 192	divsubdirapd 9052	. . . . 5
257	251, 254, 191, 192	divdirapd 9051	. . . . . . 7
258	24, 250, 191, 192	divassapd 9048	. . . . . . . 8
259	14, 253, 191, 192	divassapd 9048	. . . . . . . . 9
260	252, 191, 192	cjdivapd 11591	. . . . . . . . . . 11
261	194	cjred 11594	. . . . . . . . . . . 12
262	261	oveq2d 6044	. . . . . . . . . . 11
263	260, 262	eqtrd 2264	. . . . . . . . . 10
264	263	oveq2d 6044	. . . . . . . . 9
265	259, 264	eqtr4d 2267	. . . . . . . 8
266	258, 265	oveq12d 6046	. . . . . . 7
267	257, 266	eqtrd 2264	. . . . . 6
268	267	oveq2d 6044	. . . . 5
269	249, 256, 268	3eqtrd 2268	. . . 4
270		mul4sq.10	. . . . . . 7
271	270	nn0zd 9644	. . . . . 6
272		zgz 13009	. . . . . 6
273	271, 272	syl 14	. . . . 5
274		gzcjcl 13012	. . . . . . . 8
275	1, 274	syl 14	. . . . . . 7
276		mul4sq.8	. . . . . . 7
277		gzmulcl 13014	. . . . . . 7 $/\$
278	275, 276, 277	syl2anc 411	. . . . . 6
279		mul4sq.9	. . . . . . . 8
280		gzcjcl 13012	. . . . . . . 8
281	279, 280	syl 14	. . . . . . 7
282		gzmulcl 13014	. . . . . . 7 $/\$
283	12, 281, 282	syl2anc 411	. . . . . 6
284		gzaddcl 13013	. . . . . 6 $/\$
285	278, 283, 284	syl2anc 411	. . . . 5
286		gzsubcl 13016	. . . . 5 $/\$
287	273, 285, 286	syl2anc 411	. . . 4
288	269, 287	eqeltrd 2308	. . 3
289	250	cjcld 11563	. . . . . . . 8
290	14, 289	mulcld 8242	. . . . . . 7
291	24, 252	mulcld 8242	. . . . . . 7
292	290, 291, 191, 192	divsubdirapd 9052	. . . . . 6
293		cjsub 11515	. . . . . . . . . . . 12 $/\$
294	3, 6, 293	syl2anc 411	. . . . . . . . . . 11
295	294	oveq2d 6044	. . . . . . . . . 10
296	14, 24, 29	subdid 8635	. . . . . . . . . 10
297	295, 296	eqtrd 2264	. . . . . . . . 9
298	24, 14, 17	subdid 8635	. . . . . . . . . 10
299	24, 14	mulcomd 8243	. . . . . . . . . . 11
300	299	oveq1d 6043	. . . . . . . . . 10
301	298, 300	eqtrd 2264	. . . . . . . . 9
302	297, 301	oveq12d 6046	. . . . . . . 8
303	14, 24	mulcld 8242	. . . . . . . . 9
304	303, 30, 98	nnncan1d 8566	. . . . . . . 8
305	302, 304	eqtrd 2264	. . . . . . 7
306	305	oveq1d 6043	. . . . . 6
307	292, 306	eqtr3d 2266	. . . . 5
308	14, 289, 191, 192	divassapd 9048	. . . . . . 7
309	250, 191, 192	cjdivapd 11591	. . . . . . . . 9
310	261	oveq2d 6044	. . . . . . . . 9
311	309, 310	eqtrd 2264	. . . . . . . 8
312	311	oveq2d 6044	. . . . . . 7
313	308, 312	eqtr4d 2267	. . . . . 6
314	24, 252, 191, 192	divassapd 9048	. . . . . 6
315	313, 314	oveq12d 6046	. . . . 5
316	307, 315	eqtr3d 2266	. . . 4
317		gzcjcl 13012	. . . . . . 7
318	276, 317	syl 14	. . . . . 6
319		gzmulcl 13014	. . . . . 6 $/\$
320	12, 318, 319	syl2anc 411	. . . . 5
321		gzmulcl 13014	. . . . . 6 $/\$
322	275, 279, 321	syl2anc 411	. . . . 5
323		gzsubcl 13016	. . . . 5 $/\$
324	320, 322, 323	syl2anc 411	. . . 4
325	316, 324	eqeltrd 2308	. . 3
326		4sq.1	. . . 4
327	326	4sqlem4a 13027	. . 3 $/\$
328	288, 325, 327	syl2anc 411	. 2
329	232, 328	eqeltrrd 2309	1

Colors of variables: wff set class

Syntax hints:

wi 4

wceq 1398

wcel 2202

cab 2217

wrex 2512

cfv 5333 (class class class)co 6028

cc 8073

caddc 8078

cmul 8080

cmin 8392

cdiv 8894

cn 9185

c2 9236

cn0 9444

cz 9523

cexp 10846

ccj 11462

cabs 11620

cgz 13005

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4209 ax-sep 4212 ax-nul 4220 ax-pow 4270 ax-pr 4305 ax-un 4536 ax-setind 4641 ax-iinf 4692 ax-cnex 8166 ax-resscn 8167 ax-1cn 8168 ax-1re 8169 ax-icn 8170 ax-addcl 8171 ax-addrcl 8172 ax-mulcl 8173 ax-mulrcl 8174 ax-addcom 8175 ax-mulcom 8176 ax-addass 8177 ax-mulass 8178 ax-distr 8179 ax-i2m1 8180 ax-0lt1 8181 ax-1rid 8182 ax-0id 8183 ax-rnegex 8184 ax-precex 8185 ax-cnre 8186 ax-pre-ltirr 8187 ax-pre-ltwlin 8188 ax-pre-lttrn 8189 ax-pre-apti 8190 ax-pre-ltadd 8191 ax-pre-mulgt0 8192 ax-pre-mulext 8193 ax-arch 8194 ax-caucvg 8195

This theorem depends on definitions: df-bi 117 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2364 df-ne 2404 df-nel 2499 df-ral 2516 df-rex 2517 df-reu 2518 df-rmo 2519 df-rab 2520 df-v 2805 df-sbc 3033 df-csb 3129 df-dif 3203 df-un 3205 df-in 3207 df-ss 3214 df-nul 3497 df-if 3608 df-pw 3658 df-sn 3679 df-pr 3680 df-op 3682 df-uni 3899 df-int 3934 df-iun 3977 df-br 4094 df-opab 4156 df-mpt 4157 df-tr 4193 df-id 4396 df-po 4399 df-iso 4400 df-iord 4469 df-on 4471 df-ilim 4472 df-suc 4474 df-iom 4695 df-xp 4737 df-rel 4738 df-cnv 4739 df-co 4740 df-dm 4741 df-rn 4742 df-res 4743 df-ima 4744 df-iota 5293 df-fun 5335 df-fn 5336 df-f 5337 df-f1 5338 df-fo 5339 df-f1o 5340 df-fv 5341 df-riota 5981 df-ov 6031 df-oprab 6032 df-mpo 6033 df-1st 6312 df-2nd 6313 df-recs 6514 df-frec 6600 df-pnf 8258 df-mnf 8259 df-xr 8260 df-ltxr 8261 df-le 8262 df-sub 8394 df-neg 8395 df-reap 8797 df-ap 8804 df-div 8895 df-inn 9186 df-2 9244 df-3 9245 df-4 9246 df-n0 9445 df-z 9524 df-uz 9800 df-rp 9933 df-seqfrec 10756 df-exp 10847 df-cj 11465 df-re 11466 df-im 11467 df-rsqrt 11621 df-abs 11622 df-gz 13006

This theorem is referenced by: mul4sq 13030 4sqlem17 13043

W3C validator