mul4sqlem - Intuitionistic Logic Explorer

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

Theorem mul4sqlem 12562

Description: Lemma for mul4sq 12563: 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 12541	. . . . . . . . . . 11
3	1, 2	syl 14	. . . . . . . . . 10
4		mul4sq.3	. . . . . . . . . . 11
5		gzcn 12541	. . . . . . . . . . 11
6	4, 5	syl 14	. . . . . . . . . 10
7	3, 6	mulcld 8047	. . . . . . . . 9
8	7	absvalsqd 11347	. . . . . . . 8
9	7	cjcld 11105	. . . . . . . . 9
10	7, 9	mulcld 8047	. . . . . . . 8
11	8, 10	eqeltrd 2273	. . . . . . 7
12		mul4sq.2	. . . . . . . . . . 11
13		gzcn 12541	. . . . . . . . . . 11
14	12, 13	syl 14	. . . . . . . . . 10
15		mul4sq.4	. . . . . . . . . . 11
16		gzcn 12541	. . . . . . . . . . 11
17	15, 16	syl 14	. . . . . . . . . 10
18	14, 17	mulcld 8047	. . . . . . . . 9
19	18	absvalsqd 11347	. . . . . . . 8
20	18	cjcld 11105	. . . . . . . . 9
21	18, 20	mulcld 8047	. . . . . . . 8
22	19, 21	eqeltrd 2273	. . . . . . 7
23	11, 22	addcld 8046	. . . . . 6
24	3	cjcld 11105	. . . . . . . . 9
25	24, 6	mulcld 8047	. . . . . . . 8
26	14	cjcld 11105	. . . . . . . . 9
27	26, 17	mulcld 8047	. . . . . . . 8
28	25, 27	mulcld 8047	. . . . . . 7
29	6	cjcld 11105	. . . . . . . . 9
30	14, 29	mulcld 8047	. . . . . . . 8
31	17	cjcld 11105	. . . . . . . . 9
32	3, 31	mulcld 8047	. . . . . . . 8
33	30, 32	mulcld 8047	. . . . . . 7
34	28, 33	addcld 8046	. . . . . 6
35	3, 17	mulcld 8047	. . . . . . . . 9
36	35	absvalsqd 11347	. . . . . . . 8
37	35	cjcld 11105	. . . . . . . . 9
38	35, 37	mulcld 8047	. . . . . . . 8
39	36, 38	eqeltrd 2273	. . . . . . 7
40	14, 6	mulcld 8047	. . . . . . . . 9
41	40	absvalsqd 11347	. . . . . . . 8
42	40	cjcld 11105	. . . . . . . . 9
43	40, 42	mulcld 8047	. . . . . . . 8
44	41, 43	eqeltrd 2273	. . . . . . 7
45	39, 44	addcld 8046	. . . . . 6
46	23, 34, 45	ppncand 8377	. . . . 5
47	14, 31	mulcld 8047	. . . . . . . . 9
48	25, 47	addcld 8046	. . . . . . . 8
49	48	absvalsqd 11347	. . . . . . 7
50	25, 47	cjaddd 11130	. . . . . . . . 9
51	24, 6	cjmuld 11131	. . . . . . . . . . 11
52	3	cjcjd 11108	. . . . . . . . . . . 12
53	52	oveq1d 5937	. . . . . . . . . . 11
54	51, 53	eqtrd 2229	. . . . . . . . . 10
55	14, 31	cjmuld 11131	. . . . . . . . . . 11
56	17	cjcjd 11108	. . . . . . . . . . . 12
57	56	oveq2d 5938	. . . . . . . . . . 11
58	55, 57	eqtrd 2229	. . . . . . . . . 10
59	54, 58	oveq12d 5940	. . . . . . . . 9
60	50, 59	eqtrd 2229	. . . . . . . 8
61	60	oveq2d 5938	. . . . . . 7
62	3, 29	mulcld 8047	. . . . . . . . . . 11
63	25, 62, 27	adddid 8051	. . . . . . . . . 10
64	6, 24, 3, 29	mul4d 8181	. . . . . . . . . . . . 13
65	24, 6	mulcomd 8048	. . . . . . . . . . . . . 14
66	65	oveq1d 5937	. . . . . . . . . . . . 13
67	3, 6	mulcomd 8048	. . . . . . . . . . . . . 14
68	3, 6	cjmuld 11131	. . . . . . . . . . . . . 14
69	67, 68	oveq12d 5940	. . . . . . . . . . . . 13
70	64, 66, 69	3eqtr4d 2239	. . . . . . . . . . . 12
71	70, 8	eqtr4d 2232	. . . . . . . . . . 11
72	71	oveq1d 5937	. . . . . . . . . 10
73	63, 72	eqtrd 2229	. . . . . . . . 9
74	47, 62, 27	adddid 8051	. . . . . . . . . 10
75	3, 29	mulcomd 8048	. . . . . . . . . . . . 13
76	75	oveq2d 5938	. . . . . . . . . . . 12
77	14, 31, 29, 3	mul4d 8181	. . . . . . . . . . . 12
78	31, 3	mulcomd 8048	. . . . . . . . . . . . 13
79	78	oveq2d 5938	. . . . . . . . . . . 12
80	76, 77, 79	3eqtrd 2233	. . . . . . . . . . 11
81	14, 31, 17, 26	mul4d 8181	. . . . . . . . . . . . 13
82	26, 17	mulcomd 8048	. . . . . . . . . . . . . 14
83	82	oveq2d 5938	. . . . . . . . . . . . 13
84	14, 17	cjmuld 11131	. . . . . . . . . . . . . . 15
85	26, 31	mulcomd 8048	. . . . . . . . . . . . . . 15
86	84, 85	eqtrd 2229	. . . . . . . . . . . . . 14
87	86	oveq2d 5938	. . . . . . . . . . . . 13
88	81, 83, 87	3eqtr4d 2239	. . . . . . . . . . . 12
89	88, 19	eqtr4d 2232	. . . . . . . . . . 11
90	80, 89	oveq12d 5940	. . . . . . . . . 10
91	74, 90	eqtrd 2229	. . . . . . . . 9
92	73, 91	oveq12d 5940	. . . . . . . 8
93	62, 27	addcld 8046	. . . . . . . . 9
94	25, 47, 93	adddird 8052	. . . . . . . 8
95	11, 22, 28, 33	add42d 8196	. . . . . . . 8
96	92, 94, 95	3eqtr4d 2239	. . . . . . 7
97	49, 61, 96	3eqtrd 2233	. . . . . 6
98	24, 17	mulcld 8047	. . . . . . . . 9
99	98, 30	subcld 8337	. . . . . . . 8
100	99	absvalsqd 11347	. . . . . . 7
101		cjsub 11057	. . . . . . . . . 10 $/\$
102	98, 30, 101	syl2anc 411	. . . . . . . . 9
103	24, 17	cjmuld 11131	. . . . . . . . . . 11
104	52	oveq1d 5937	. . . . . . . . . . 11
105	103, 104	eqtrd 2229	. . . . . . . . . 10
106	14, 29	cjmuld 11131	. . . . . . . . . . 11
107	6	cjcjd 11108	. . . . . . . . . . . 12
108	107	oveq2d 5938	. . . . . . . . . . 11
109	106, 108	eqtrd 2229	. . . . . . . . . 10
110	105, 109	oveq12d 5940	. . . . . . . . 9
111	102, 110	eqtrd 2229	. . . . . . . 8
112	111	oveq2d 5938	. . . . . . 7
113	26, 6	mulcld 8047	. . . . . . . . . 10
114	32, 113	subcld 8337	. . . . . . . . 9
115	98, 30, 114	subdird 8441	. . . . . . . 8
116	98, 32, 113	subdid 8440	. . . . . . . . . 10
117	17, 24, 3, 31	mul4d 8181	. . . . . . . . . . . . 13
118	24, 17	mulcomd 8048	. . . . . . . . . . . . . 14
119	118	oveq1d 5937	. . . . . . . . . . . . 13
120	3, 17	mulcomd 8048	. . . . . . . . . . . . . 14
121	3, 17	cjmuld 11131	. . . . . . . . . . . . . 14
122	120, 121	oveq12d 5940	. . . . . . . . . . . . 13
123	117, 119, 122	3eqtr4d 2239	. . . . . . . . . . . 12
124	123, 36	eqtr4d 2232	. . . . . . . . . . 11
125	26, 6	mulcomd 8048	. . . . . . . . . . . . 13
126	125	oveq2d 5938	. . . . . . . . . . . 12
127	24, 17, 6, 26	mul4d 8181	. . . . . . . . . . . 12
128	17, 26	mulcomd 8048	. . . . . . . . . . . . 13
129	128	oveq2d 5938	. . . . . . . . . . . 12
130	126, 127, 129	3eqtrd 2233	. . . . . . . . . . 11
131	124, 130	oveq12d 5940	. . . . . . . . . 10
132	116, 131	eqtrd 2229	. . . . . . . . 9
133	30, 32, 113	subdid 8440	. . . . . . . . . 10
134	125	oveq2d 5938	. . . . . . . . . . . . 13
135	14, 29, 6, 26	mul4d 8181	. . . . . . . . . . . . 13
136	29, 26	mulcomd 8048	. . . . . . . . . . . . . . 15
137	14, 6	cjmuld 11131	. . . . . . . . . . . . . . 15
138	136, 137	eqtr4d 2232	. . . . . . . . . . . . . 14
139	138	oveq2d 5938	. . . . . . . . . . . . 13
140	134, 135, 139	3eqtrd 2233	. . . . . . . . . . . 12
141	140, 41	eqtr4d 2232	. . . . . . . . . . 11
142	141	oveq2d 5938	. . . . . . . . . 10
143	133, 142	eqtrd 2229	. . . . . . . . 9
144	132, 143	oveq12d 5940	. . . . . . . 8
145	39, 28, 33, 44	subadd4d 8385	. . . . . . . 8
146	115, 144, 145	3eqtrd 2233	. . . . . . 7
147	100, 112, 146	3eqtrd 2233	. . . . . 6
148	97, 147	oveq12d 5940	. . . . 5
149	3, 24	mulcld 8047	. . . . . . . 8
150	14, 26	mulcld 8047	. . . . . . . 8
151	6, 29	mulcld 8047	. . . . . . . . 9
152	17, 31	mulcld 8047	. . . . . . . . 9
153	151, 152	addcld 8046	. . . . . . . 8
154	149, 150, 153	adddird 8052	. . . . . . 7
155	68	oveq2d 5938	. . . . . . . . . . 11
156	3, 6, 24, 29	mul4d 8181	. . . . . . . . . . 11
157	8, 155, 156	3eqtrd 2233	. . . . . . . . . 10
158	121	oveq2d 5938	. . . . . . . . . . 11
159	3, 17, 24, 31	mul4d 8181	. . . . . . . . . . 11
160	36, 158, 159	3eqtrd 2233	. . . . . . . . . 10
161	157, 160	oveq12d 5940	. . . . . . . . 9
162	149, 151, 152	adddid 8051	. . . . . . . . 9
163	161, 162	eqtr4d 2232	. . . . . . . 8
164	137	oveq2d 5938	. . . . . . . . . . 11
165	14, 6, 26, 29	mul4d 8181	. . . . . . . . . . 11
166	41, 164, 165	3eqtrd 2233	. . . . . . . . . 10
167	84	oveq2d 5938	. . . . . . . . . . 11
168	14, 17, 26, 31	mul4d 8181	. . . . . . . . . . 11
169	19, 167, 168	3eqtrd 2233	. . . . . . . . . 10
170	166, 169	oveq12d 5940	. . . . . . . . 9
171	150, 151, 152	adddid 8051	. . . . . . . . 9
172	170, 171	eqtr4d 2232	. . . . . . . 8
173	163, 172	oveq12d 5940	. . . . . . 7
174	154, 173	eqtr4d 2232	. . . . . 6
175		mul4sq.5	. . . . . . . 8
176	3	absvalsqd 11347	. . . . . . . . 9
177	14	absvalsqd 11347	. . . . . . . . 9
178	176, 177	oveq12d 5940	. . . . . . . 8
179	175, 178	eqtrid 2241	. . . . . . 7
180		mul4sq.6	. . . . . . . 8
181	6	absvalsqd 11347	. . . . . . . . 9
182	17	absvalsqd 11347	. . . . . . . . 9
183	181, 182	oveq12d 5940	. . . . . . . 8
184	180, 183	eqtrid 2241	. . . . . . 7
185	179, 184	oveq12d 5940	. . . . . 6
186	11, 22, 39, 44	add42d 8196	. . . . . 6
187	174, 185, 186	3eqtr4d 2239	. . . . 5
188	46, 148, 187	3eqtr4d 2239	. . . 4
189	188	oveq1d 5937	. . 3
190		mul4sq.7	. . . . . . . . . 10
191	190	nncnd 9004	. . . . . . . . 9
192	190	nnap0d 9036	. . . . . . . . 9 #
193	48, 191, 192	absdivapd 11360	. . . . . . . 8
194	190	nnred 9003	. . . . . . . . . 10
195	190	nnnn0d 9302	. . . . . . . . . . 11
196	195	nn0ge0d 9305	. . . . . . . . . 10
197	194, 196	absidd 11332	. . . . . . . . 9
198	197	oveq2d 5938	. . . . . . . 8
199	193, 198	eqtrd 2229	. . . . . . 7
200	199	oveq1d 5937	. . . . . 6
201	48	abscld 11346	. . . . . . . 8
202	201	recnd 8055	. . . . . . 7
203	202, 191, 192	sqdivapd 10778	. . . . . 6
204	200, 203	eqtrd 2229	. . . . 5
205	99, 191, 192	absdivapd 11360	. . . . . . . 8
206	197	oveq2d 5938	. . . . . . . 8
207	205, 206	eqtrd 2229	. . . . . . 7
208	207	oveq1d 5937	. . . . . 6
209	99	abscld 11346	. . . . . . . 8
210	209	recnd 8055	. . . . . . 7
211	210, 191, 192	sqdivapd 10778	. . . . . 6
212	208, 211	eqtrd 2229	. . . . 5
213	204, 212	oveq12d 5940	. . . 4
214	23, 34	addcld 8046	. . . . . 6
215	97, 214	eqeltrd 2273	. . . . 5
216	45, 34	subcld 8337	. . . . . 6
217	147, 216	eqeltrd 2273	. . . . 5
218	190	nnsqcld 10786	. . . . . 6
219	218	nncnd 9004	. . . . 5
220	218	nnap0d 9036	. . . . 5 #
221	215, 217, 219, 220	divdirapd 8856	. . . 4
222	213, 221	eqtr4d 2232	. . 3
223	176, 149	eqeltrd 2273	. . . . . . 7
224	177, 150	eqeltrd 2273	. . . . . . 7
225	223, 224	addcld 8046	. . . . . 6
226	175, 225	eqeltrid 2283	. . . . 5
227	184, 153	eqeltrd 2273	. . . . 5
228	226, 191, 227, 191, 192, 192	divmuldivapd 8859	. . . 4
229	191	sqvald 10762	. . . . 5
230	229	oveq2d 5938	. . . 4
231	228, 230	eqtr4d 2232	. . 3
232	189, 222, 231	3eqtr4d 2239	. 2
233	226, 48	nncand 8342	. . . . . . 7
234	149, 150, 25, 47	addsub4d 8384	. . . . . . . . 9
235	179	oveq1d 5937	. . . . . . . . 9
236	24, 3, 6	subdid 8440	. . . . . . . . . . 11
237	24, 3	mulcomd 8048	. . . . . . . . . . . 12
238	237	oveq1d 5937	. . . . . . . . . . 11
239	236, 238	eqtrd 2229	. . . . . . . . . 10
240		cjsub 11057	. . . . . . . . . . . . 13 $/\$
241	14, 17, 240	syl2anc 411	. . . . . . . . . . . 12
242	241	oveq2d 5938	. . . . . . . . . . 11
243	14, 26, 31	subdid 8440	. . . . . . . . . . 11
244	242, 243	eqtrd 2229	. . . . . . . . . 10
245	239, 244	oveq12d 5940	. . . . . . . . 9
246	234, 235, 245	3eqtr4d 2239	. . . . . . . 8
247	246	oveq2d 5938	. . . . . . 7
248	233, 247	eqtr3d 2231	. . . . . 6
249	248	oveq1d 5937	. . . . 5
250	3, 6	subcld 8337	. . . . . . . 8
251	24, 250	mulcld 8047	. . . . . . 7
252	14, 17	subcld 8337	. . . . . . . . 9
253	252	cjcld 11105	. . . . . . . 8
254	14, 253	mulcld 8047	. . . . . . 7
255	251, 254	addcld 8046	. . . . . 6
256	226, 255, 191, 192	divsubdirapd 8857	. . . . 5
257	251, 254, 191, 192	divdirapd 8856	. . . . . . 7
258	24, 250, 191, 192	divassapd 8853	. . . . . . . 8
259	14, 253, 191, 192	divassapd 8853	. . . . . . . . 9
260	252, 191, 192	cjdivapd 11133	. . . . . . . . . . 11
261	194	cjred 11136	. . . . . . . . . . . 12
262	261	oveq2d 5938	. . . . . . . . . . 11
263	260, 262	eqtrd 2229	. . . . . . . . . 10
264	263	oveq2d 5938	. . . . . . . . 9
265	259, 264	eqtr4d 2232	. . . . . . . 8
266	258, 265	oveq12d 5940	. . . . . . 7
267	257, 266	eqtrd 2229	. . . . . 6
268	267	oveq2d 5938	. . . . 5
269	249, 256, 268	3eqtrd 2233	. . . 4
270		mul4sq.10	. . . . . . 7
271	270	nn0zd 9446	. . . . . 6
272		zgz 12542	. . . . . 6
273	271, 272	syl 14	. . . . 5
274		gzcjcl 12545	. . . . . . . 8
275	1, 274	syl 14	. . . . . . 7
276		mul4sq.8	. . . . . . 7
277		gzmulcl 12547	. . . . . . 7 $/\$
278	275, 276, 277	syl2anc 411	. . . . . 6
279		mul4sq.9	. . . . . . . 8
280		gzcjcl 12545	. . . . . . . 8
281	279, 280	syl 14	. . . . . . 7
282		gzmulcl 12547	. . . . . . 7 $/\$
283	12, 281, 282	syl2anc 411	. . . . . 6
284		gzaddcl 12546	. . . . . 6 $/\$
285	278, 283, 284	syl2anc 411	. . . . 5
286		gzsubcl 12549	. . . . 5 $/\$
287	273, 285, 286	syl2anc 411	. . . 4
288	269, 287	eqeltrd 2273	. . 3
289	250	cjcld 11105	. . . . . . . 8
290	14, 289	mulcld 8047	. . . . . . 7
291	24, 252	mulcld 8047	. . . . . . 7
292	290, 291, 191, 192	divsubdirapd 8857	. . . . . 6
293		cjsub 11057	. . . . . . . . . . . 12 $/\$
294	3, 6, 293	syl2anc 411	. . . . . . . . . . 11
295	294	oveq2d 5938	. . . . . . . . . 10
296	14, 24, 29	subdid 8440	. . . . . . . . . 10
297	295, 296	eqtrd 2229	. . . . . . . . 9
298	24, 14, 17	subdid 8440	. . . . . . . . . 10
299	24, 14	mulcomd 8048	. . . . . . . . . . 11
300	299	oveq1d 5937	. . . . . . . . . 10
301	298, 300	eqtrd 2229	. . . . . . . . 9
302	297, 301	oveq12d 5940	. . . . . . . 8
303	14, 24	mulcld 8047	. . . . . . . . 9
304	303, 30, 98	nnncan1d 8371	. . . . . . . 8
305	302, 304	eqtrd 2229	. . . . . . 7
306	305	oveq1d 5937	. . . . . 6
307	292, 306	eqtr3d 2231	. . . . 5
308	14, 289, 191, 192	divassapd 8853	. . . . . . 7
309	250, 191, 192	cjdivapd 11133	. . . . . . . . 9
310	261	oveq2d 5938	. . . . . . . . 9
311	309, 310	eqtrd 2229	. . . . . . . 8
312	311	oveq2d 5938	. . . . . . 7
313	308, 312	eqtr4d 2232	. . . . . 6
314	24, 252, 191, 192	divassapd 8853	. . . . . 6
315	313, 314	oveq12d 5940	. . . . 5
316	307, 315	eqtr3d 2231	. . . 4
317		gzcjcl 12545	. . . . . . 7
318	276, 317	syl 14	. . . . . 6
319		gzmulcl 12547	. . . . . 6 $/\$
320	12, 318, 319	syl2anc 411	. . . . 5
321		gzmulcl 12547	. . . . . 6 $/\$
322	275, 279, 321	syl2anc 411	. . . . 5
323		gzsubcl 12549	. . . . 5 $/\$
324	320, 322, 323	syl2anc 411	. . . 4
325	316, 324	eqeltrd 2273	. . 3
326		4sq.1	. . . 4
327	326	4sqlem4a 12560	. . 3 $/\$
328	288, 325, 327	syl2anc 411	. 2
329	232, 328	eqeltrrd 2274	1

Colors of variables: wff set class

Syntax hints:

wi 4

wceq 1364

wcel 2167

cab 2182

wrex 2476

cfv 5258 (class class class)co 5922

cc 7877

caddc 7882

cmul 7884

cmin 8197

cdiv 8699

cn 8990

c2 9041

cn0 9249

cz 9326

cexp 10630

ccj 11004

cabs 11162

cgz 12538

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 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4148 ax-sep 4151 ax-nul 4159 ax-pow 4207 ax-pr 4242 ax-un 4468 ax-setind 4573 ax-iinf 4624 ax-cnex 7970 ax-resscn 7971 ax-1cn 7972 ax-1re 7973 ax-icn 7974 ax-addcl 7975 ax-addrcl 7976 ax-mulcl 7977 ax-mulrcl 7978 ax-addcom 7979 ax-mulcom 7980 ax-addass 7981 ax-mulass 7982 ax-distr 7983 ax-i2m1 7984 ax-0lt1 7985 ax-1rid 7986 ax-0id 7987 ax-rnegex 7988 ax-precex 7989 ax-cnre 7990 ax-pre-ltirr 7991 ax-pre-ltwlin 7992 ax-pre-lttrn 7993 ax-pre-apti 7994 ax-pre-ltadd 7995 ax-pre-mulgt0 7996 ax-pre-mulext 7997 ax-arch 7998 ax-caucvg 7999

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3451 df-if 3562 df-pw 3607 df-sn 3628 df-pr 3629 df-op 3631 df-uni 3840 df-int 3875 df-iun 3918 df-br 4034 df-opab 4095 df-mpt 4096 df-tr 4132 df-id 4328 df-po 4331 df-iso 4332 df-iord 4401 df-on 4403 df-ilim 4404 df-suc 4406 df-iom 4627 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-rn 4674 df-res 4675 df-ima 4676 df-iota 5219 df-fun 5260 df-fn 5261 df-f 5262 df-f1 5263 df-fo 5264 df-f1o 5265 df-fv 5266 df-riota 5877 df-ov 5925 df-oprab 5926 df-mpo 5927 df-1st 6198 df-2nd 6199 df-recs 6363 df-frec 6449 df-pnf 8063 df-mnf 8064 df-xr 8065 df-ltxr 8066 df-le 8067 df-sub 8199 df-neg 8200 df-reap 8602 df-ap 8609 df-div 8700 df-inn 8991 df-2 9049 df-3 9050 df-4 9051 df-n0 9250 df-z 9327 df-uz 9602 df-rp 9729 df-seqfrec 10540 df-exp 10631 df-cj 11007 df-re 11008 df-im 11009 df-rsqrt 11163 df-abs 11164 df-gz 12539

This theorem is referenced by: mul4sq 12563 4sqlem17 12576

W3C validator