mul4sqlem - Intuitionistic Logic Explorer

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

Theorem mul4sqlem 12345

Description: Lemma for mul4sq 12346: 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 12324	. . . . . . . . . . 11
3	1, 2	syl 14	. . . . . . . . . 10
4		mul4sq.3	. . . . . . . . . . 11
5		gzcn 12324	. . . . . . . . . . 11
6	4, 5	syl 14	. . . . . . . . . 10
7	3, 6	mulcld 7940	. . . . . . . . 9
8	7	absvalsqd 11146	. . . . . . . 8
9	7	cjcld 10904	. . . . . . . . 9
10	7, 9	mulcld 7940	. . . . . . . 8
11	8, 10	eqeltrd 2247	. . . . . . 7
12		mul4sq.2	. . . . . . . . . . 11
13		gzcn 12324	. . . . . . . . . . 11
14	12, 13	syl 14	. . . . . . . . . 10
15		mul4sq.4	. . . . . . . . . . 11
16		gzcn 12324	. . . . . . . . . . 11
17	15, 16	syl 14	. . . . . . . . . 10
18	14, 17	mulcld 7940	. . . . . . . . 9
19	18	absvalsqd 11146	. . . . . . . 8
20	18	cjcld 10904	. . . . . . . . 9
21	18, 20	mulcld 7940	. . . . . . . 8
22	19, 21	eqeltrd 2247	. . . . . . 7
23	11, 22	addcld 7939	. . . . . 6
24	3	cjcld 10904	. . . . . . . . 9
25	24, 6	mulcld 7940	. . . . . . . 8
26	14	cjcld 10904	. . . . . . . . 9
27	26, 17	mulcld 7940	. . . . . . . 8
28	25, 27	mulcld 7940	. . . . . . 7
29	6	cjcld 10904	. . . . . . . . 9
30	14, 29	mulcld 7940	. . . . . . . 8
31	17	cjcld 10904	. . . . . . . . 9
32	3, 31	mulcld 7940	. . . . . . . 8
33	30, 32	mulcld 7940	. . . . . . 7
34	28, 33	addcld 7939	. . . . . 6
35	3, 17	mulcld 7940	. . . . . . . . 9
36	35	absvalsqd 11146	. . . . . . . 8
37	35	cjcld 10904	. . . . . . . . 9
38	35, 37	mulcld 7940	. . . . . . . 8
39	36, 38	eqeltrd 2247	. . . . . . 7
40	14, 6	mulcld 7940	. . . . . . . . 9
41	40	absvalsqd 11146	. . . . . . . 8
42	40	cjcld 10904	. . . . . . . . 9
43	40, 42	mulcld 7940	. . . . . . . 8
44	41, 43	eqeltrd 2247	. . . . . . 7
45	39, 44	addcld 7939	. . . . . 6
46	23, 34, 45	ppncand 8270	. . . . 5
47	14, 31	mulcld 7940	. . . . . . . . 9
48	25, 47	addcld 7939	. . . . . . . 8
49	48	absvalsqd 11146	. . . . . . 7
50	25, 47	cjaddd 10929	. . . . . . . . 9
51	24, 6	cjmuld 10930	. . . . . . . . . . 11
52	3	cjcjd 10907	. . . . . . . . . . . 12
53	52	oveq1d 5868	. . . . . . . . . . 11
54	51, 53	eqtrd 2203	. . . . . . . . . 10
55	14, 31	cjmuld 10930	. . . . . . . . . . 11
56	17	cjcjd 10907	. . . . . . . . . . . 12
57	56	oveq2d 5869	. . . . . . . . . . 11
58	55, 57	eqtrd 2203	. . . . . . . . . 10
59	54, 58	oveq12d 5871	. . . . . . . . 9
60	50, 59	eqtrd 2203	. . . . . . . 8
61	60	oveq2d 5869	. . . . . . 7
62	3, 29	mulcld 7940	. . . . . . . . . . 11
63	25, 62, 27	adddid 7944	. . . . . . . . . 10
64	6, 24, 3, 29	mul4d 8074	. . . . . . . . . . . . 13
65	24, 6	mulcomd 7941	. . . . . . . . . . . . . 14
66	65	oveq1d 5868	. . . . . . . . . . . . 13
67	3, 6	mulcomd 7941	. . . . . . . . . . . . . 14
68	3, 6	cjmuld 10930	. . . . . . . . . . . . . 14
69	67, 68	oveq12d 5871	. . . . . . . . . . . . 13
70	64, 66, 69	3eqtr4d 2213	. . . . . . . . . . . 12
71	70, 8	eqtr4d 2206	. . . . . . . . . . 11
72	71	oveq1d 5868	. . . . . . . . . 10
73	63, 72	eqtrd 2203	. . . . . . . . 9
74	47, 62, 27	adddid 7944	. . . . . . . . . 10
75	3, 29	mulcomd 7941	. . . . . . . . . . . . 13
76	75	oveq2d 5869	. . . . . . . . . . . 12
77	14, 31, 29, 3	mul4d 8074	. . . . . . . . . . . 12
78	31, 3	mulcomd 7941	. . . . . . . . . . . . 13
79	78	oveq2d 5869	. . . . . . . . . . . 12
80	76, 77, 79	3eqtrd 2207	. . . . . . . . . . 11
81	14, 31, 17, 26	mul4d 8074	. . . . . . . . . . . . 13
82	26, 17	mulcomd 7941	. . . . . . . . . . . . . 14
83	82	oveq2d 5869	. . . . . . . . . . . . 13
84	14, 17	cjmuld 10930	. . . . . . . . . . . . . . 15
85	26, 31	mulcomd 7941	. . . . . . . . . . . . . . 15
86	84, 85	eqtrd 2203	. . . . . . . . . . . . . 14
87	86	oveq2d 5869	. . . . . . . . . . . . 13
88	81, 83, 87	3eqtr4d 2213	. . . . . . . . . . . 12
89	88, 19	eqtr4d 2206	. . . . . . . . . . 11
90	80, 89	oveq12d 5871	. . . . . . . . . 10
91	74, 90	eqtrd 2203	. . . . . . . . 9
92	73, 91	oveq12d 5871	. . . . . . . 8
93	62, 27	addcld 7939	. . . . . . . . 9
94	25, 47, 93	adddird 7945	. . . . . . . 8
95	11, 22, 28, 33	add42d 8089	. . . . . . . 8
96	92, 94, 95	3eqtr4d 2213	. . . . . . 7
97	49, 61, 96	3eqtrd 2207	. . . . . 6
98	24, 17	mulcld 7940	. . . . . . . . 9
99	98, 30	subcld 8230	. . . . . . . 8
100	99	absvalsqd 11146	. . . . . . 7
101		cjsub 10856	. . . . . . . . . 10 $/\$
102	98, 30, 101	syl2anc 409	. . . . . . . . 9
103	24, 17	cjmuld 10930	. . . . . . . . . . 11
104	52	oveq1d 5868	. . . . . . . . . . 11
105	103, 104	eqtrd 2203	. . . . . . . . . 10
106	14, 29	cjmuld 10930	. . . . . . . . . . 11
107	6	cjcjd 10907	. . . . . . . . . . . 12
108	107	oveq2d 5869	. . . . . . . . . . 11
109	106, 108	eqtrd 2203	. . . . . . . . . 10
110	105, 109	oveq12d 5871	. . . . . . . . 9
111	102, 110	eqtrd 2203	. . . . . . . 8
112	111	oveq2d 5869	. . . . . . 7
113	26, 6	mulcld 7940	. . . . . . . . . 10
114	32, 113	subcld 8230	. . . . . . . . 9
115	98, 30, 114	subdird 8334	. . . . . . . 8
116	98, 32, 113	subdid 8333	. . . . . . . . . 10
117	17, 24, 3, 31	mul4d 8074	. . . . . . . . . . . . 13
118	24, 17	mulcomd 7941	. . . . . . . . . . . . . 14
119	118	oveq1d 5868	. . . . . . . . . . . . 13
120	3, 17	mulcomd 7941	. . . . . . . . . . . . . 14
121	3, 17	cjmuld 10930	. . . . . . . . . . . . . 14
122	120, 121	oveq12d 5871	. . . . . . . . . . . . 13
123	117, 119, 122	3eqtr4d 2213	. . . . . . . . . . . 12
124	123, 36	eqtr4d 2206	. . . . . . . . . . 11
125	26, 6	mulcomd 7941	. . . . . . . . . . . . 13
126	125	oveq2d 5869	. . . . . . . . . . . 12
127	24, 17, 6, 26	mul4d 8074	. . . . . . . . . . . 12
128	17, 26	mulcomd 7941	. . . . . . . . . . . . 13
129	128	oveq2d 5869	. . . . . . . . . . . 12
130	126, 127, 129	3eqtrd 2207	. . . . . . . . . . 11
131	124, 130	oveq12d 5871	. . . . . . . . . 10
132	116, 131	eqtrd 2203	. . . . . . . . 9
133	30, 32, 113	subdid 8333	. . . . . . . . . 10
134	125	oveq2d 5869	. . . . . . . . . . . . 13
135	14, 29, 6, 26	mul4d 8074	. . . . . . . . . . . . 13
136	29, 26	mulcomd 7941	. . . . . . . . . . . . . . 15
137	14, 6	cjmuld 10930	. . . . . . . . . . . . . . 15
138	136, 137	eqtr4d 2206	. . . . . . . . . . . . . 14
139	138	oveq2d 5869	. . . . . . . . . . . . 13
140	134, 135, 139	3eqtrd 2207	. . . . . . . . . . . 12
141	140, 41	eqtr4d 2206	. . . . . . . . . . 11
142	141	oveq2d 5869	. . . . . . . . . 10
143	133, 142	eqtrd 2203	. . . . . . . . 9
144	132, 143	oveq12d 5871	. . . . . . . 8
145	39, 28, 33, 44	subadd4d 8278	. . . . . . . 8
146	115, 144, 145	3eqtrd 2207	. . . . . . 7
147	100, 112, 146	3eqtrd 2207	. . . . . 6
148	97, 147	oveq12d 5871	. . . . 5
149	3, 24	mulcld 7940	. . . . . . . 8
150	14, 26	mulcld 7940	. . . . . . . 8
151	6, 29	mulcld 7940	. . . . . . . . 9
152	17, 31	mulcld 7940	. . . . . . . . 9
153	151, 152	addcld 7939	. . . . . . . 8
154	149, 150, 153	adddird 7945	. . . . . . 7
155	68	oveq2d 5869	. . . . . . . . . . 11
156	3, 6, 24, 29	mul4d 8074	. . . . . . . . . . 11
157	8, 155, 156	3eqtrd 2207	. . . . . . . . . 10
158	121	oveq2d 5869	. . . . . . . . . . 11
159	3, 17, 24, 31	mul4d 8074	. . . . . . . . . . 11
160	36, 158, 159	3eqtrd 2207	. . . . . . . . . 10
161	157, 160	oveq12d 5871	. . . . . . . . 9
162	149, 151, 152	adddid 7944	. . . . . . . . 9
163	161, 162	eqtr4d 2206	. . . . . . . 8
164	137	oveq2d 5869	. . . . . . . . . . 11
165	14, 6, 26, 29	mul4d 8074	. . . . . . . . . . 11
166	41, 164, 165	3eqtrd 2207	. . . . . . . . . 10
167	84	oveq2d 5869	. . . . . . . . . . 11
168	14, 17, 26, 31	mul4d 8074	. . . . . . . . . . 11
169	19, 167, 168	3eqtrd 2207	. . . . . . . . . 10
170	166, 169	oveq12d 5871	. . . . . . . . 9
171	150, 151, 152	adddid 7944	. . . . . . . . 9
172	170, 171	eqtr4d 2206	. . . . . . . 8
173	163, 172	oveq12d 5871	. . . . . . 7
174	154, 173	eqtr4d 2206	. . . . . 6
175		mul4sq.5	. . . . . . . 8
176	3	absvalsqd 11146	. . . . . . . . 9
177	14	absvalsqd 11146	. . . . . . . . 9
178	176, 177	oveq12d 5871	. . . . . . . 8
179	175, 178	eqtrid 2215	. . . . . . 7
180		mul4sq.6	. . . . . . . 8
181	6	absvalsqd 11146	. . . . . . . . 9
182	17	absvalsqd 11146	. . . . . . . . 9
183	181, 182	oveq12d 5871	. . . . . . . 8
184	180, 183	eqtrid 2215	. . . . . . 7
185	179, 184	oveq12d 5871	. . . . . 6
186	11, 22, 39, 44	add42d 8089	. . . . . 6
187	174, 185, 186	3eqtr4d 2213	. . . . 5
188	46, 148, 187	3eqtr4d 2213	. . . 4
189	188	oveq1d 5868	. . 3
190		mul4sq.7	. . . . . . . . . 10
191	190	nncnd 8892	. . . . . . . . 9
192	190	nnap0d 8924	. . . . . . . . 9 #
193	48, 191, 192	absdivapd 11159	. . . . . . . 8
194	190	nnred 8891	. . . . . . . . . 10
195	190	nnnn0d 9188	. . . . . . . . . . 11
196	195	nn0ge0d 9191	. . . . . . . . . 10
197	194, 196	absidd 11131	. . . . . . . . 9
198	197	oveq2d 5869	. . . . . . . 8
199	193, 198	eqtrd 2203	. . . . . . 7
200	199	oveq1d 5868	. . . . . 6
201	48	abscld 11145	. . . . . . . 8
202	201	recnd 7948	. . . . . . 7
203	202, 191, 192	sqdivapd 10622	. . . . . 6
204	200, 203	eqtrd 2203	. . . . 5
205	99, 191, 192	absdivapd 11159	. . . . . . . 8
206	197	oveq2d 5869	. . . . . . . 8
207	205, 206	eqtrd 2203	. . . . . . 7
208	207	oveq1d 5868	. . . . . 6
209	99	abscld 11145	. . . . . . . 8
210	209	recnd 7948	. . . . . . 7
211	210, 191, 192	sqdivapd 10622	. . . . . 6
212	208, 211	eqtrd 2203	. . . . 5
213	204, 212	oveq12d 5871	. . . 4
214	23, 34	addcld 7939	. . . . . 6
215	97, 214	eqeltrd 2247	. . . . 5
216	45, 34	subcld 8230	. . . . . 6
217	147, 216	eqeltrd 2247	. . . . 5
218	190	nnsqcld 10630	. . . . . 6
219	218	nncnd 8892	. . . . 5
220	218	nnap0d 8924	. . . . 5 #
221	215, 217, 219, 220	divdirapd 8746	. . . 4
222	213, 221	eqtr4d 2206	. . 3
223	176, 149	eqeltrd 2247	. . . . . . 7
224	177, 150	eqeltrd 2247	. . . . . . 7
225	223, 224	addcld 7939	. . . . . 6
226	175, 225	eqeltrid 2257	. . . . 5
227	184, 153	eqeltrd 2247	. . . . 5
228	226, 191, 227, 191, 192, 192	divmuldivapd 8749	. . . 4
229	191	sqvald 10606	. . . . 5
230	229	oveq2d 5869	. . . 4
231	228, 230	eqtr4d 2206	. . 3
232	189, 222, 231	3eqtr4d 2213	. 2
233	226, 48	nncand 8235	. . . . . . 7
234	149, 150, 25, 47	addsub4d 8277	. . . . . . . . 9
235	179	oveq1d 5868	. . . . . . . . 9
236	24, 3, 6	subdid 8333	. . . . . . . . . . 11
237	24, 3	mulcomd 7941	. . . . . . . . . . . 12
238	237	oveq1d 5868	. . . . . . . . . . 11
239	236, 238	eqtrd 2203	. . . . . . . . . 10
240		cjsub 10856	. . . . . . . . . . . . 13 $/\$
241	14, 17, 240	syl2anc 409	. . . . . . . . . . . 12
242	241	oveq2d 5869	. . . . . . . . . . 11
243	14, 26, 31	subdid 8333	. . . . . . . . . . 11
244	242, 243	eqtrd 2203	. . . . . . . . . 10
245	239, 244	oveq12d 5871	. . . . . . . . 9
246	234, 235, 245	3eqtr4d 2213	. . . . . . . 8
247	246	oveq2d 5869	. . . . . . 7
248	233, 247	eqtr3d 2205	. . . . . 6
249	248	oveq1d 5868	. . . . 5
250	3, 6	subcld 8230	. . . . . . . 8
251	24, 250	mulcld 7940	. . . . . . 7
252	14, 17	subcld 8230	. . . . . . . . 9
253	252	cjcld 10904	. . . . . . . 8
254	14, 253	mulcld 7940	. . . . . . 7
255	251, 254	addcld 7939	. . . . . 6
256	226, 255, 191, 192	divsubdirapd 8747	. . . . 5
257	251, 254, 191, 192	divdirapd 8746	. . . . . . 7
258	24, 250, 191, 192	divassapd 8743	. . . . . . . 8
259	14, 253, 191, 192	divassapd 8743	. . . . . . . . 9
260	252, 191, 192	cjdivapd 10932	. . . . . . . . . . 11
261	194	cjred 10935	. . . . . . . . . . . 12
262	261	oveq2d 5869	. . . . . . . . . . 11
263	260, 262	eqtrd 2203	. . . . . . . . . 10
264	263	oveq2d 5869	. . . . . . . . 9
265	259, 264	eqtr4d 2206	. . . . . . . 8
266	258, 265	oveq12d 5871	. . . . . . 7
267	257, 266	eqtrd 2203	. . . . . 6
268	267	oveq2d 5869	. . . . 5
269	249, 256, 268	3eqtrd 2207	. . . 4
270		mul4sq.10	. . . . . . 7
271	270	nn0zd 9332	. . . . . 6
272		zgz 12325	. . . . . 6
273	271, 272	syl 14	. . . . 5
274		gzcjcl 12328	. . . . . . . 8
275	1, 274	syl 14	. . . . . . 7
276		mul4sq.8	. . . . . . 7
277		gzmulcl 12330	. . . . . . 7 $/\$
278	275, 276, 277	syl2anc 409	. . . . . 6
279		mul4sq.9	. . . . . . . 8
280		gzcjcl 12328	. . . . . . . 8
281	279, 280	syl 14	. . . . . . 7
282		gzmulcl 12330	. . . . . . 7 $/\$
283	12, 281, 282	syl2anc 409	. . . . . 6
284		gzaddcl 12329	. . . . . 6 $/\$
285	278, 283, 284	syl2anc 409	. . . . 5
286		gzsubcl 12332	. . . . 5 $/\$
287	273, 285, 286	syl2anc 409	. . . 4
288	269, 287	eqeltrd 2247	. . 3
289	250	cjcld 10904	. . . . . . . 8
290	14, 289	mulcld 7940	. . . . . . 7
291	24, 252	mulcld 7940	. . . . . . 7
292	290, 291, 191, 192	divsubdirapd 8747	. . . . . 6
293		cjsub 10856	. . . . . . . . . . . 12 $/\$
294	3, 6, 293	syl2anc 409	. . . . . . . . . . 11
295	294	oveq2d 5869	. . . . . . . . . 10
296	14, 24, 29	subdid 8333	. . . . . . . . . 10
297	295, 296	eqtrd 2203	. . . . . . . . 9
298	24, 14, 17	subdid 8333	. . . . . . . . . 10
299	24, 14	mulcomd 7941	. . . . . . . . . . 11
300	299	oveq1d 5868	. . . . . . . . . 10
301	298, 300	eqtrd 2203	. . . . . . . . 9
302	297, 301	oveq12d 5871	. . . . . . . 8
303	14, 24	mulcld 7940	. . . . . . . . 9
304	303, 30, 98	nnncan1d 8264	. . . . . . . 8
305	302, 304	eqtrd 2203	. . . . . . 7
306	305	oveq1d 5868	. . . . . 6
307	292, 306	eqtr3d 2205	. . . . 5
308	14, 289, 191, 192	divassapd 8743	. . . . . . 7
309	250, 191, 192	cjdivapd 10932	. . . . . . . . 9
310	261	oveq2d 5869	. . . . . . . . 9
311	309, 310	eqtrd 2203	. . . . . . . 8
312	311	oveq2d 5869	. . . . . . 7
313	308, 312	eqtr4d 2206	. . . . . 6
314	24, 252, 191, 192	divassapd 8743	. . . . . 6
315	313, 314	oveq12d 5871	. . . . 5
316	307, 315	eqtr3d 2205	. . . 4
317		gzcjcl 12328	. . . . . . 7
318	276, 317	syl 14	. . . . . 6
319		gzmulcl 12330	. . . . . 6 $/\$
320	12, 318, 319	syl2anc 409	. . . . 5
321		gzmulcl 12330	. . . . . 6 $/\$
322	275, 279, 321	syl2anc 409	. . . . 5
323		gzsubcl 12332	. . . . 5 $/\$
324	320, 322, 323	syl2anc 409	. . . 4
325	316, 324	eqeltrd 2247	. . 3
326		4sq.1	. . . 4
327	326	4sqlem4a 12343	. . 3 $/\$
328	288, 325, 327	syl2anc 409	. 2
329	232, 328	eqeltrrd 2248	1

Colors of variables: wff set class

Syntax hints:

wi 4

wceq 1348

wcel 2141

cab 2156

wrex 2449

cfv 5198 (class class class)co 5853

cc 7772

caddc 7777

cmul 7779

cmin 8090

cdiv 8589

cn 8878

c2 8929

cn0 9135

cz 9212

cexp 10475

ccj 10803

cabs 10961

cgz 12321

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 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-coll 4104 ax-sep 4107 ax-nul 4115 ax-pow 4160 ax-pr 4194 ax-un 4418 ax-setind 4521 ax-iinf 4572 ax-cnex 7865 ax-resscn 7866 ax-1cn 7867 ax-1re 7868 ax-icn 7869 ax-addcl 7870 ax-addrcl 7871 ax-mulcl 7872 ax-mulrcl 7873 ax-addcom 7874 ax-mulcom 7875 ax-addass 7876 ax-mulass 7877 ax-distr 7878 ax-i2m1 7879 ax-0lt1 7880 ax-1rid 7881 ax-0id 7882 ax-rnegex 7883 ax-precex 7884 ax-cnre 7885 ax-pre-ltirr 7886 ax-pre-ltwlin 7887 ax-pre-lttrn 7888 ax-pre-apti 7889 ax-pre-ltadd 7890 ax-pre-mulgt0 7891 ax-pre-mulext 7892 ax-arch 7893 ax-caucvg 7894

This theorem depends on definitions: df-bi 116 df-dc 830 df-3or 974 df-3an 975 df-tru 1351 df-fal 1354 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-nel 2436 df-ral 2453 df-rex 2454 df-reu 2455 df-rmo 2456 df-rab 2457 df-v 2732 df-sbc 2956 df-csb 3050 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-nul 3415 df-if 3527 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-int 3832 df-iun 3875 df-br 3990 df-opab 4051 df-mpt 4052 df-tr 4088 df-id 4278 df-po 4281 df-iso 4282 df-iord 4351 df-on 4353 df-ilim 4354 df-suc 4356 df-iom 4575 df-xp 4617 df-rel 4618 df-cnv 4619 df-co 4620 df-dm 4621 df-rn 4622 df-res 4623 df-ima 4624 df-iota 5160 df-fun 5200 df-fn 5201 df-f 5202 df-f1 5203 df-fo 5204 df-f1o 5205 df-fv 5206 df-riota 5809 df-ov 5856 df-oprab 5857 df-mpo 5858 df-1st 6119 df-2nd 6120 df-recs 6284 df-frec 6370 df-pnf 7956 df-mnf 7957 df-xr 7958 df-ltxr 7959 df-le 7960 df-sub 8092 df-neg 8093 df-reap 8494 df-ap 8501 df-div 8590 df-inn 8879 df-2 8937 df-3 8938 df-4 8939 df-n0 9136 df-z 9213 df-uz 9488 df-rp 9611 df-seqfrec 10402 df-exp 10476 df-cj 10806 df-re 10807 df-im 10808 df-rsqrt 10962 df-abs 10963 df-gz 12322

This theorem is referenced by: mul4sq 12346

W3C validator