mul4sqlem - Intuitionistic Logic Explorer

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

Theorem mul4sqlem 12319

Description: Lemma for mul4sq 12320: 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 12298	. . . . . . . . . . 11
3	1, 2	syl 14	. . . . . . . . . 10
4		mul4sq.3	. . . . . . . . . . 11
5		gzcn 12298	. . . . . . . . . . 11
6	4, 5	syl 14	. . . . . . . . . 10
7	3, 6	mulcld 7915	. . . . . . . . 9
8	7	absvalsqd 11120	. . . . . . . 8
9	7	cjcld 10878	. . . . . . . . 9
10	7, 9	mulcld 7915	. . . . . . . 8
11	8, 10	eqeltrd 2242	. . . . . . 7
12		mul4sq.2	. . . . . . . . . . 11
13		gzcn 12298	. . . . . . . . . . 11
14	12, 13	syl 14	. . . . . . . . . 10
15		mul4sq.4	. . . . . . . . . . 11
16		gzcn 12298	. . . . . . . . . . 11
17	15, 16	syl 14	. . . . . . . . . 10
18	14, 17	mulcld 7915	. . . . . . . . 9
19	18	absvalsqd 11120	. . . . . . . 8
20	18	cjcld 10878	. . . . . . . . 9
21	18, 20	mulcld 7915	. . . . . . . 8
22	19, 21	eqeltrd 2242	. . . . . . 7
23	11, 22	addcld 7914	. . . . . 6
24	3	cjcld 10878	. . . . . . . . 9
25	24, 6	mulcld 7915	. . . . . . . 8
26	14	cjcld 10878	. . . . . . . . 9
27	26, 17	mulcld 7915	. . . . . . . 8
28	25, 27	mulcld 7915	. . . . . . 7
29	6	cjcld 10878	. . . . . . . . 9
30	14, 29	mulcld 7915	. . . . . . . 8
31	17	cjcld 10878	. . . . . . . . 9
32	3, 31	mulcld 7915	. . . . . . . 8
33	30, 32	mulcld 7915	. . . . . . 7
34	28, 33	addcld 7914	. . . . . 6
35	3, 17	mulcld 7915	. . . . . . . . 9
36	35	absvalsqd 11120	. . . . . . . 8
37	35	cjcld 10878	. . . . . . . . 9
38	35, 37	mulcld 7915	. . . . . . . 8
39	36, 38	eqeltrd 2242	. . . . . . 7
40	14, 6	mulcld 7915	. . . . . . . . 9
41	40	absvalsqd 11120	. . . . . . . 8
42	40	cjcld 10878	. . . . . . . . 9
43	40, 42	mulcld 7915	. . . . . . . 8
44	41, 43	eqeltrd 2242	. . . . . . 7
45	39, 44	addcld 7914	. . . . . 6
46	23, 34, 45	ppncand 8245	. . . . 5
47	14, 31	mulcld 7915	. . . . . . . . 9
48	25, 47	addcld 7914	. . . . . . . 8
49	48	absvalsqd 11120	. . . . . . 7
50	25, 47	cjaddd 10903	. . . . . . . . 9
51	24, 6	cjmuld 10904	. . . . . . . . . . 11
52	3	cjcjd 10881	. . . . . . . . . . . 12
53	52	oveq1d 5856	. . . . . . . . . . 11
54	51, 53	eqtrd 2198	. . . . . . . . . 10
55	14, 31	cjmuld 10904	. . . . . . . . . . 11
56	17	cjcjd 10881	. . . . . . . . . . . 12
57	56	oveq2d 5857	. . . . . . . . . . 11
58	55, 57	eqtrd 2198	. . . . . . . . . 10
59	54, 58	oveq12d 5859	. . . . . . . . 9
60	50, 59	eqtrd 2198	. . . . . . . 8
61	60	oveq2d 5857	. . . . . . 7
62	3, 29	mulcld 7915	. . . . . . . . . . 11
63	25, 62, 27	adddid 7919	. . . . . . . . . 10
64	6, 24, 3, 29	mul4d 8049	. . . . . . . . . . . . 13
65	24, 6	mulcomd 7916	. . . . . . . . . . . . . 14
66	65	oveq1d 5856	. . . . . . . . . . . . 13
67	3, 6	mulcomd 7916	. . . . . . . . . . . . . 14
68	3, 6	cjmuld 10904	. . . . . . . . . . . . . 14
69	67, 68	oveq12d 5859	. . . . . . . . . . . . 13
70	64, 66, 69	3eqtr4d 2208	. . . . . . . . . . . 12
71	70, 8	eqtr4d 2201	. . . . . . . . . . 11
72	71	oveq1d 5856	. . . . . . . . . 10
73	63, 72	eqtrd 2198	. . . . . . . . 9
74	47, 62, 27	adddid 7919	. . . . . . . . . 10
75	3, 29	mulcomd 7916	. . . . . . . . . . . . 13
76	75	oveq2d 5857	. . . . . . . . . . . 12
77	14, 31, 29, 3	mul4d 8049	. . . . . . . . . . . 12
78	31, 3	mulcomd 7916	. . . . . . . . . . . . 13
79	78	oveq2d 5857	. . . . . . . . . . . 12
80	76, 77, 79	3eqtrd 2202	. . . . . . . . . . 11
81	14, 31, 17, 26	mul4d 8049	. . . . . . . . . . . . 13
82	26, 17	mulcomd 7916	. . . . . . . . . . . . . 14
83	82	oveq2d 5857	. . . . . . . . . . . . 13
84	14, 17	cjmuld 10904	. . . . . . . . . . . . . . 15
85	26, 31	mulcomd 7916	. . . . . . . . . . . . . . 15
86	84, 85	eqtrd 2198	. . . . . . . . . . . . . 14
87	86	oveq2d 5857	. . . . . . . . . . . . 13
88	81, 83, 87	3eqtr4d 2208	. . . . . . . . . . . 12
89	88, 19	eqtr4d 2201	. . . . . . . . . . 11
90	80, 89	oveq12d 5859	. . . . . . . . . 10
91	74, 90	eqtrd 2198	. . . . . . . . 9
92	73, 91	oveq12d 5859	. . . . . . . 8
93	62, 27	addcld 7914	. . . . . . . . 9
94	25, 47, 93	adddird 7920	. . . . . . . 8
95	11, 22, 28, 33	add42d 8064	. . . . . . . 8
96	92, 94, 95	3eqtr4d 2208	. . . . . . 7
97	49, 61, 96	3eqtrd 2202	. . . . . 6
98	24, 17	mulcld 7915	. . . . . . . . 9
99	98, 30	subcld 8205	. . . . . . . 8
100	99	absvalsqd 11120	. . . . . . 7
101		cjsub 10830	. . . . . . . . . 10 $/\$
102	98, 30, 101	syl2anc 409	. . . . . . . . 9
103	24, 17	cjmuld 10904	. . . . . . . . . . 11
104	52	oveq1d 5856	. . . . . . . . . . 11
105	103, 104	eqtrd 2198	. . . . . . . . . 10
106	14, 29	cjmuld 10904	. . . . . . . . . . 11
107	6	cjcjd 10881	. . . . . . . . . . . 12
108	107	oveq2d 5857	. . . . . . . . . . 11
109	106, 108	eqtrd 2198	. . . . . . . . . 10
110	105, 109	oveq12d 5859	. . . . . . . . 9
111	102, 110	eqtrd 2198	. . . . . . . 8
112	111	oveq2d 5857	. . . . . . 7
113	26, 6	mulcld 7915	. . . . . . . . . 10
114	32, 113	subcld 8205	. . . . . . . . 9
115	98, 30, 114	subdird 8309	. . . . . . . 8
116	98, 32, 113	subdid 8308	. . . . . . . . . 10
117	17, 24, 3, 31	mul4d 8049	. . . . . . . . . . . . 13
118	24, 17	mulcomd 7916	. . . . . . . . . . . . . 14
119	118	oveq1d 5856	. . . . . . . . . . . . 13
120	3, 17	mulcomd 7916	. . . . . . . . . . . . . 14
121	3, 17	cjmuld 10904	. . . . . . . . . . . . . 14
122	120, 121	oveq12d 5859	. . . . . . . . . . . . 13
123	117, 119, 122	3eqtr4d 2208	. . . . . . . . . . . 12
124	123, 36	eqtr4d 2201	. . . . . . . . . . 11
125	26, 6	mulcomd 7916	. . . . . . . . . . . . 13
126	125	oveq2d 5857	. . . . . . . . . . . 12
127	24, 17, 6, 26	mul4d 8049	. . . . . . . . . . . 12
128	17, 26	mulcomd 7916	. . . . . . . . . . . . 13
129	128	oveq2d 5857	. . . . . . . . . . . 12
130	126, 127, 129	3eqtrd 2202	. . . . . . . . . . 11
131	124, 130	oveq12d 5859	. . . . . . . . . 10
132	116, 131	eqtrd 2198	. . . . . . . . 9
133	30, 32, 113	subdid 8308	. . . . . . . . . 10
134	125	oveq2d 5857	. . . . . . . . . . . . 13
135	14, 29, 6, 26	mul4d 8049	. . . . . . . . . . . . 13
136	29, 26	mulcomd 7916	. . . . . . . . . . . . . . 15
137	14, 6	cjmuld 10904	. . . . . . . . . . . . . . 15
138	136, 137	eqtr4d 2201	. . . . . . . . . . . . . 14
139	138	oveq2d 5857	. . . . . . . . . . . . 13
140	134, 135, 139	3eqtrd 2202	. . . . . . . . . . . 12
141	140, 41	eqtr4d 2201	. . . . . . . . . . 11
142	141	oveq2d 5857	. . . . . . . . . 10
143	133, 142	eqtrd 2198	. . . . . . . . 9
144	132, 143	oveq12d 5859	. . . . . . . 8
145	39, 28, 33, 44	subadd4d 8253	. . . . . . . 8
146	115, 144, 145	3eqtrd 2202	. . . . . . 7
147	100, 112, 146	3eqtrd 2202	. . . . . 6
148	97, 147	oveq12d 5859	. . . . 5
149	3, 24	mulcld 7915	. . . . . . . 8
150	14, 26	mulcld 7915	. . . . . . . 8
151	6, 29	mulcld 7915	. . . . . . . . 9
152	17, 31	mulcld 7915	. . . . . . . . 9
153	151, 152	addcld 7914	. . . . . . . 8
154	149, 150, 153	adddird 7920	. . . . . . 7
155	68	oveq2d 5857	. . . . . . . . . . 11
156	3, 6, 24, 29	mul4d 8049	. . . . . . . . . . 11
157	8, 155, 156	3eqtrd 2202	. . . . . . . . . 10
158	121	oveq2d 5857	. . . . . . . . . . 11
159	3, 17, 24, 31	mul4d 8049	. . . . . . . . . . 11
160	36, 158, 159	3eqtrd 2202	. . . . . . . . . 10
161	157, 160	oveq12d 5859	. . . . . . . . 9
162	149, 151, 152	adddid 7919	. . . . . . . . 9
163	161, 162	eqtr4d 2201	. . . . . . . 8
164	137	oveq2d 5857	. . . . . . . . . . 11
165	14, 6, 26, 29	mul4d 8049	. . . . . . . . . . 11
166	41, 164, 165	3eqtrd 2202	. . . . . . . . . 10
167	84	oveq2d 5857	. . . . . . . . . . 11
168	14, 17, 26, 31	mul4d 8049	. . . . . . . . . . 11
169	19, 167, 168	3eqtrd 2202	. . . . . . . . . 10
170	166, 169	oveq12d 5859	. . . . . . . . 9
171	150, 151, 152	adddid 7919	. . . . . . . . 9
172	170, 171	eqtr4d 2201	. . . . . . . 8
173	163, 172	oveq12d 5859	. . . . . . 7
174	154, 173	eqtr4d 2201	. . . . . 6
175		mul4sq.5	. . . . . . . 8
176	3	absvalsqd 11120	. . . . . . . . 9
177	14	absvalsqd 11120	. . . . . . . . 9
178	176, 177	oveq12d 5859	. . . . . . . 8
179	175, 178	syl5eq 2210	. . . . . . 7
180		mul4sq.6	. . . . . . . 8
181	6	absvalsqd 11120	. . . . . . . . 9
182	17	absvalsqd 11120	. . . . . . . . 9
183	181, 182	oveq12d 5859	. . . . . . . 8
184	180, 183	syl5eq 2210	. . . . . . 7
185	179, 184	oveq12d 5859	. . . . . 6
186	11, 22, 39, 44	add42d 8064	. . . . . 6
187	174, 185, 186	3eqtr4d 2208	. . . . 5
188	46, 148, 187	3eqtr4d 2208	. . . 4
189	188	oveq1d 5856	. . 3
190		mul4sq.7	. . . . . . . . . 10
191	190	nncnd 8867	. . . . . . . . 9
192	190	nnap0d 8899	. . . . . . . . 9 #
193	48, 191, 192	absdivapd 11133	. . . . . . . 8
194	190	nnred 8866	. . . . . . . . . 10
195	190	nnnn0d 9163	. . . . . . . . . . 11
196	195	nn0ge0d 9166	. . . . . . . . . 10
197	194, 196	absidd 11105	. . . . . . . . 9
198	197	oveq2d 5857	. . . . . . . 8
199	193, 198	eqtrd 2198	. . . . . . 7
200	199	oveq1d 5856	. . . . . 6
201	48	abscld 11119	. . . . . . . 8
202	201	recnd 7923	. . . . . . 7
203	202, 191, 192	sqdivapd 10597	. . . . . 6
204	200, 203	eqtrd 2198	. . . . 5
205	99, 191, 192	absdivapd 11133	. . . . . . . 8
206	197	oveq2d 5857	. . . . . . . 8
207	205, 206	eqtrd 2198	. . . . . . 7
208	207	oveq1d 5856	. . . . . 6
209	99	abscld 11119	. . . . . . . 8
210	209	recnd 7923	. . . . . . 7
211	210, 191, 192	sqdivapd 10597	. . . . . 6
212	208, 211	eqtrd 2198	. . . . 5
213	204, 212	oveq12d 5859	. . . 4
214	23, 34	addcld 7914	. . . . . 6
215	97, 214	eqeltrd 2242	. . . . 5
216	45, 34	subcld 8205	. . . . . 6
217	147, 216	eqeltrd 2242	. . . . 5
218	190	nnsqcld 10605	. . . . . 6
219	218	nncnd 8867	. . . . 5
220	218	nnap0d 8899	. . . . 5 #
221	215, 217, 219, 220	divdirapd 8721	. . . 4
222	213, 221	eqtr4d 2201	. . 3
223	176, 149	eqeltrd 2242	. . . . . . 7
224	177, 150	eqeltrd 2242	. . . . . . 7
225	223, 224	addcld 7914	. . . . . 6
226	175, 225	eqeltrid 2252	. . . . 5
227	184, 153	eqeltrd 2242	. . . . 5
228	226, 191, 227, 191, 192, 192	divmuldivapd 8724	. . . 4
229	191	sqvald 10581	. . . . 5
230	229	oveq2d 5857	. . . 4
231	228, 230	eqtr4d 2201	. . 3
232	189, 222, 231	3eqtr4d 2208	. 2
233	226, 48	nncand 8210	. . . . . . 7
234	149, 150, 25, 47	addsub4d 8252	. . . . . . . . 9
235	179	oveq1d 5856	. . . . . . . . 9
236	24, 3, 6	subdid 8308	. . . . . . . . . . 11
237	24, 3	mulcomd 7916	. . . . . . . . . . . 12
238	237	oveq1d 5856	. . . . . . . . . . 11
239	236, 238	eqtrd 2198	. . . . . . . . . 10
240		cjsub 10830	. . . . . . . . . . . . 13 $/\$
241	14, 17, 240	syl2anc 409	. . . . . . . . . . . 12
242	241	oveq2d 5857	. . . . . . . . . . 11
243	14, 26, 31	subdid 8308	. . . . . . . . . . 11
244	242, 243	eqtrd 2198	. . . . . . . . . 10
245	239, 244	oveq12d 5859	. . . . . . . . 9
246	234, 235, 245	3eqtr4d 2208	. . . . . . . 8
247	246	oveq2d 5857	. . . . . . 7
248	233, 247	eqtr3d 2200	. . . . . 6
249	248	oveq1d 5856	. . . . 5
250	3, 6	subcld 8205	. . . . . . . 8
251	24, 250	mulcld 7915	. . . . . . 7
252	14, 17	subcld 8205	. . . . . . . . 9
253	252	cjcld 10878	. . . . . . . 8
254	14, 253	mulcld 7915	. . . . . . 7
255	251, 254	addcld 7914	. . . . . 6
256	226, 255, 191, 192	divsubdirapd 8722	. . . . 5
257	251, 254, 191, 192	divdirapd 8721	. . . . . . 7
258	24, 250, 191, 192	divassapd 8718	. . . . . . . 8
259	14, 253, 191, 192	divassapd 8718	. . . . . . . . 9
260	252, 191, 192	cjdivapd 10906	. . . . . . . . . . 11
261	194	cjred 10909	. . . . . . . . . . . 12
262	261	oveq2d 5857	. . . . . . . . . . 11
263	260, 262	eqtrd 2198	. . . . . . . . . 10
264	263	oveq2d 5857	. . . . . . . . 9
265	259, 264	eqtr4d 2201	. . . . . . . 8
266	258, 265	oveq12d 5859	. . . . . . 7
267	257, 266	eqtrd 2198	. . . . . 6
268	267	oveq2d 5857	. . . . 5
269	249, 256, 268	3eqtrd 2202	. . . 4
270		mul4sq.10	. . . . . . 7
271	270	nn0zd 9307	. . . . . 6
272		zgz 12299	. . . . . 6
273	271, 272	syl 14	. . . . 5
274		gzcjcl 12302	. . . . . . . 8
275	1, 274	syl 14	. . . . . . 7
276		mul4sq.8	. . . . . . 7
277		gzmulcl 12304	. . . . . . 7 $/\$
278	275, 276, 277	syl2anc 409	. . . . . 6
279		mul4sq.9	. . . . . . . 8
280		gzcjcl 12302	. . . . . . . 8
281	279, 280	syl 14	. . . . . . 7
282		gzmulcl 12304	. . . . . . 7 $/\$
283	12, 281, 282	syl2anc 409	. . . . . 6
284		gzaddcl 12303	. . . . . 6 $/\$
285	278, 283, 284	syl2anc 409	. . . . 5
286		gzsubcl 12306	. . . . 5 $/\$
287	273, 285, 286	syl2anc 409	. . . 4
288	269, 287	eqeltrd 2242	. . 3
289	250	cjcld 10878	. . . . . . . 8
290	14, 289	mulcld 7915	. . . . . . 7
291	24, 252	mulcld 7915	. . . . . . 7
292	290, 291, 191, 192	divsubdirapd 8722	. . . . . 6
293		cjsub 10830	. . . . . . . . . . . 12 $/\$
294	3, 6, 293	syl2anc 409	. . . . . . . . . . 11
295	294	oveq2d 5857	. . . . . . . . . 10
296	14, 24, 29	subdid 8308	. . . . . . . . . 10
297	295, 296	eqtrd 2198	. . . . . . . . 9
298	24, 14, 17	subdid 8308	. . . . . . . . . 10
299	24, 14	mulcomd 7916	. . . . . . . . . . 11
300	299	oveq1d 5856	. . . . . . . . . 10
301	298, 300	eqtrd 2198	. . . . . . . . 9
302	297, 301	oveq12d 5859	. . . . . . . 8
303	14, 24	mulcld 7915	. . . . . . . . 9
304	303, 30, 98	nnncan1d 8239	. . . . . . . 8
305	302, 304	eqtrd 2198	. . . . . . 7
306	305	oveq1d 5856	. . . . . 6
307	292, 306	eqtr3d 2200	. . . . 5
308	14, 289, 191, 192	divassapd 8718	. . . . . . 7
309	250, 191, 192	cjdivapd 10906	. . . . . . . . 9
310	261	oveq2d 5857	. . . . . . . . 9
311	309, 310	eqtrd 2198	. . . . . . . 8
312	311	oveq2d 5857	. . . . . . 7
313	308, 312	eqtr4d 2201	. . . . . 6
314	24, 252, 191, 192	divassapd 8718	. . . . . 6
315	313, 314	oveq12d 5859	. . . . 5
316	307, 315	eqtr3d 2200	. . . 4
317		gzcjcl 12302	. . . . . . 7
318	276, 317	syl 14	. . . . . 6
319		gzmulcl 12304	. . . . . 6 $/\$
320	12, 318, 319	syl2anc 409	. . . . 5
321		gzmulcl 12304	. . . . . 6 $/\$
322	275, 279, 321	syl2anc 409	. . . . 5
323		gzsubcl 12306	. . . . 5 $/\$
324	320, 322, 323	syl2anc 409	. . . 4
325	316, 324	eqeltrd 2242	. . 3
326		4sq.1	. . . 4
327	326	4sqlem4a 12317	. . 3 $/\$
328	288, 325, 327	syl2anc 409	. 2
329	232, 328	eqeltrrd 2243	1

Colors of variables: wff set class

Syntax hints:

wi 4

wceq 1343

wcel 2136

cab 2151

wrex 2444

cfv 5187 (class class class)co 5841

cc 7747

caddc 7752

cmul 7754

cmin 8065

cdiv 8564

cn 8853

c2 8904

cn0 9110

cz 9187

cexp 10450

ccj 10777

cabs 10935

cgz 12295

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-coll 4096 ax-sep 4099 ax-nul 4107 ax-pow 4152 ax-pr 4186 ax-un 4410 ax-setind 4513 ax-iinf 4564 ax-cnex 7840 ax-resscn 7841 ax-1cn 7842 ax-1re 7843 ax-icn 7844 ax-addcl 7845 ax-addrcl 7846 ax-mulcl 7847 ax-mulrcl 7848 ax-addcom 7849 ax-mulcom 7850 ax-addass 7851 ax-mulass 7852 ax-distr 7853 ax-i2m1 7854 ax-0lt1 7855 ax-1rid 7856 ax-0id 7857 ax-rnegex 7858 ax-precex 7859 ax-cnre 7860 ax-pre-ltirr 7861 ax-pre-ltwlin 7862 ax-pre-lttrn 7863 ax-pre-apti 7864 ax-pre-ltadd 7865 ax-pre-mulgt0 7866 ax-pre-mulext 7867 ax-arch 7868 ax-caucvg 7869

This theorem depends on definitions: df-bi 116 df-dc 825 df-3or 969 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2296 df-ne 2336 df-nel 2431 df-ral 2448 df-rex 2449 df-reu 2450 df-rmo 2451 df-rab 2452 df-v 2727 df-sbc 2951 df-csb 3045 df-dif 3117 df-un 3119 df-in 3121 df-ss 3128 df-nul 3409 df-if 3520 df-pw 3560 df-sn 3581 df-pr 3582 df-op 3584 df-uni 3789 df-int 3824 df-iun 3867 df-br 3982 df-opab 4043 df-mpt 4044 df-tr 4080 df-id 4270 df-po 4273 df-iso 4274 df-iord 4343 df-on 4345 df-ilim 4346 df-suc 4348 df-iom 4567 df-xp 4609 df-rel 4610 df-cnv 4611 df-co 4612 df-dm 4613 df-rn 4614 df-res 4615 df-ima 4616 df-iota 5152 df-fun 5189 df-fn 5190 df-f 5191 df-f1 5192 df-fo 5193 df-f1o 5194 df-fv 5195 df-riota 5797 df-ov 5844 df-oprab 5845 df-mpo 5846 df-1st 6105 df-2nd 6106 df-recs 6269 df-frec 6355 df-pnf 7931 df-mnf 7932 df-xr 7933 df-ltxr 7934 df-le 7935 df-sub 8067 df-neg 8068 df-reap 8469 df-ap 8476 df-div 8565 df-inn 8854 df-2 8912 df-3 8913 df-4 8914 df-n0 9111 df-z 9188 df-uz 9463 df-rp 9586 df-seqfrec 10377 df-exp 10451 df-cj 10780 df-re 10781 df-im 10782 df-rsqrt 10936 df-abs 10937 df-gz 12296

This theorem is referenced by: mul4sq 12320

W3C validator