perfectALTVlem2 - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > perfectALTVlem2		Structured version Visualization version Unicode version

Theorem perfectALTVlem2 38989

Description: Lemma for perfectALTV 38990. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by AV, 1-Jul-2020.)

**Hypotheses**
Ref	Expression
perfectALTVlem.1
perfectALTVlem.2
perfectALTVlem.3	Odd
perfectALTVlem.4

**Assertion**
Ref	Expression
perfectALTVlem2	$/\$

Proof of Theorem perfectALTVlem2 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		perfectALTVlem.2	. . . 4
2		1re 9660	. . . . . 6
3	2	a1i 11	. . . . 5
4		perfectALTVlem.1	. . . . . . . 8
5		perfectALTVlem.3	. . . . . . . 8 Odd
6		perfectALTVlem.4	. . . . . . . 8
7	4, 1, 5, 6	perfectALTVlem1 38988	. . . . . . 7 $/\$ $/\$
8	7	simp3d 1044	. . . . . 6
9	8	nnred 10646	. . . . 5
10	1	nnred 10646	. . . . 5
11	8	nnge1d 10674	. . . . 5
12		2cn 10702	. . . . . . . . . . 11
13		exp1 12316	. . . . . . . . . . 11
14	12, 13	ax-mp 5	. . . . . . . . . 10
15		df-2 10690	. . . . . . . . . 10
16	14, 15	eqtri 2493	. . . . . . . . 9
17		2re 10701	. . . . . . . . . . 11
18	17	a1i 11	. . . . . . . . . 10
19		1zzd 10992	. . . . . . . . . 10
20	4	peano2nnd 10648	. . . . . . . . . . 11
21	20	nnzd 11062	. . . . . . . . . 10
22		1lt2 10799	. . . . . . . . . . 11
23	22	a1i 11	. . . . . . . . . 10
24	4	nnrpd 11362	. . . . . . . . . . . 12
25		ltaddrp 11359	. . . . . . . . . . . 12 $/\$
26	2, 24, 25	sylancr 676	. . . . . . . . . . 11
27		ax-1cn 9615	. . . . . . . . . . . 12
28	4	nncnd 10647	. . . . . . . . . . . 12
29		addcom 9837	. . . . . . . . . . . 12 $/\$
30	27, 28, 29	sylancr 676	. . . . . . . . . . 11
31	26, 30	breqtrd 4420	. . . . . . . . . 10
32		ltexp2a 12362	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
33	18, 19, 21, 23, 31, 32	syl32anc 1300	. . . . . . . . 9
34	16, 33	syl5eqbrr 4430	. . . . . . . 8
35	7	simp1d 1042	. . . . . . . . . 10
36	35	nnred 10646	. . . . . . . . 9
37	3, 3, 36	ltaddsubd 10234	. . . . . . . 8
38	34, 37	mpbid 215	. . . . . . 7
39		1rp 11329	. . . . . . . . 9
40	39	a1i 11	. . . . . . . 8
41		peano2rem 9961	. . . . . . . . . . 11
42	36, 41	syl 17	. . . . . . . . . 10
43		expgt1 12348	. . . . . . . . . . . 12 $/\$ $/\$
44	18, 20, 23, 43	syl3anc 1292	. . . . . . . . . . 11
45		posdif 10128	. . . . . . . . . . . 12 $/\$
46	2, 36, 45	sylancr 676	. . . . . . . . . . 11
47	44, 46	mpbid 215	. . . . . . . . . 10
48	42, 47	jca 541	. . . . . . . . 9 $/\$
49		elrp 11327	. . . . . . . . 9 $/\$
50	48, 49	sylibr 217	. . . . . . . 8
51		nnrp 11334	. . . . . . . . 9
52	1, 51	syl 17	. . . . . . . 8
53	40, 50, 52	ltdiv2d 11387	. . . . . . 7
54	38, 53	mpbid 215	. . . . . 6
55	1	nncnd 10647	. . . . . . 7
56	55	div1d 10397	. . . . . 6
57	54, 56	breqtrd 4420	. . . . 5
58	3, 9, 10, 11, 57	lelttrd 9810	. . . 4
59		eluz2b2 11254	. . . 4 $/\$
60	1, 58, 59	sylanbrc 677	. . 3
61		fzfid 12224	. . . . . . . . . . . 12
62		sgmss 24112	. . . . . . . . . . . . 13
63	1, 62	syl 17	. . . . . . . . . . . 12
64		ssfi 7810	. . . . . . . . . . . 12 $/\$
65	61, 63, 64	syl2anc 673	. . . . . . . . . . 11
66	65	ad2antrr 740	. . . . . . . . . 10 $/\$ $/\$ $/\$
67		ssrab2 3500	. . . . . . . . . . . . 13
68	67	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
69	68	sselda 3418	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
70	69	nnred 10646	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
71	69	nnnn0d 10949	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
72	71	nn0ge0d 10952	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
73		df-tp 3964	. . . . . . . . . . . 12
74		prssi 4119	. . . . . . . . . . . . . . 15 $/\$
75	8, 1, 74	syl2anc 673	. . . . . . . . . . . . . 14
76	75	ad2antrr 740	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
77		simplrl 778	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
78	77	snssd 4108	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
79	76, 78	unssd 3601	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
80	73, 79	syl5eqss 3462	. . . . . . . . . . 11 $/\$ $/\$ $/\$
81		eltpi 4007	. . . . . . . . . . . . 13 $\/$ $\/$
82	7	simp2d 1043	. . . . . . . . . . . . . . . . . . 19
83	82	nnzd 11062	. . . . . . . . . . . . . . . . . 18
84	8	nnzd 11062	. . . . . . . . . . . . . . . . . 18
85		dvdsmul2 14402	. . . . . . . . . . . . . . . . . 18 $/\$
86	83, 84, 85	syl2anc 673	. . . . . . . . . . . . . . . . 17
87	82	nncnd 10647	. . . . . . . . . . . . . . . . . 18
88	82	nnne0d 10676	. . . . . . . . . . . . . . . . . 18
89	55, 87, 88	divcan2d 10407	. . . . . . . . . . . . . . . . 17
90	86, 89	breqtrd 4420	. . . . . . . . . . . . . . . 16
91		breq1 4398	. . . . . . . . . . . . . . . 16
92	90, 91	syl5ibrcom 230	. . . . . . . . . . . . . . 15
93	92	ad2antrr 740	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
94	1	nnzd 11062	. . . . . . . . . . . . . . . . 17
95		iddvds 14393	. . . . . . . . . . . . . . . . 17
96	94, 95	syl 17	. . . . . . . . . . . . . . . 16
97		breq1 4398	. . . . . . . . . . . . . . . 16
98	96, 97	syl5ibrcom 230	. . . . . . . . . . . . . . 15
99	98	ad2antrr 740	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
100		simplrr 779	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
101		breq1 4398	. . . . . . . . . . . . . . 15
102	100, 101	syl5ibrcom 230	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
103	93, 99, 102	3jaod 1358	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\/$ $\/$
104	81, 103	syl5 32	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
105	104	imp 436	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
106	80, 105	ssrabdv 3494	. . . . . . . . . 10 $/\$ $/\$ $/\$
107	66, 70, 72, 106	fsumless 13933	. . . . . . . . 9 $/\$ $/\$ $/\$
108		simpr 468	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
109		disjsn 4023	. . . . . . . . . . . 12
110	108, 109	sylibr 217	. . . . . . . . . . 11 $/\$ $/\$ $/\$
111	73	a1i 11	. . . . . . . . . . 11 $/\$ $/\$ $/\$
112		tpfi 7865	. . . . . . . . . . . 12
113	112	a1i 11	. . . . . . . . . . 11 $/\$ $/\$ $/\$
114	80	sselda 3418	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
115	114	nncnd 10647	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
116	110, 111, 113, 115	fsumsplit 13883	. . . . . . . . . 10 $/\$ $/\$ $/\$
117	8	nncnd 10647	. . . . . . . . . . . . . . 15
118		id 22	. . . . . . . . . . . . . . . 16
119	118	sumsn 13884	. . . . . . . . . . . . . . 15 $/\$
120	8, 117, 119	syl2anc 673	. . . . . . . . . . . . . 14
121		id 22	. . . . . . . . . . . . . . . 16
122	121	sumsn 13884	. . . . . . . . . . . . . . 15 $/\$
123	1, 55, 122	syl2anc 673	. . . . . . . . . . . . . 14
124	120, 123	oveq12d 6326	. . . . . . . . . . . . 13
125		incom 3616	. . . . . . . . . . . . . . 15
126	9, 57	gtned 9787	. . . . . . . . . . . . . . . 16
127		disjsn2 4024	. . . . . . . . . . . . . . . 16
128	126, 127	syl 17	. . . . . . . . . . . . . . 15
129	125, 128	syl5eqr 2519	. . . . . . . . . . . . . 14
130		df-pr 3962	. . . . . . . . . . . . . . 15
131	130	a1i 11	. . . . . . . . . . . . . 14
132		prfi 7864	. . . . . . . . . . . . . . 15
133	132	a1i 11	. . . . . . . . . . . . . 14
134	75	sselda 3418	. . . . . . . . . . . . . . 15 $/\$
135	134	nncnd 10647	. . . . . . . . . . . . . 14 $/\$
136	129, 131, 133, 135	fsumsplit 13883	. . . . . . . . . . . . 13
137	87, 55	mulcld 9681	. . . . . . . . . . . . . . 15
138	55, 137, 87, 88	divdird 10443	. . . . . . . . . . . . . 14
139	35	nncnd 10647	. . . . . . . . . . . . . . . . . . . 20
140	27	a1i 11	. . . . . . . . . . . . . . . . . . . 20
141	139, 140, 55	subdird 10096	. . . . . . . . . . . . . . . . . . 19
142	55	mulid2d 9679	. . . . . . . . . . . . . . . . . . . 20
143	142	oveq2d 6324	. . . . . . . . . . . . . . . . . . 19
144	141, 143	eqtrd 2505	. . . . . . . . . . . . . . . . . 18
145	144	oveq2d 6324	. . . . . . . . . . . . . . . . 17
146	139, 55	mulcld 9681	. . . . . . . . . . . . . . . . . 18
147	55, 146	pncan3d 10008	. . . . . . . . . . . . . . . . 17
148	145, 147	eqtrd 2505	. . . . . . . . . . . . . . . 16
149	148	oveq1d 6323	. . . . . . . . . . . . . . 15
150	139, 55, 87, 88	divassd 10440	. . . . . . . . . . . . . . 15
151	149, 150	eqtrd 2505	. . . . . . . . . . . . . 14
152	55, 87, 88	divcan3d 10410	. . . . . . . . . . . . . . 15
153	152	oveq2d 6324	. . . . . . . . . . . . . 14
154	138, 151, 153	3eqtr3d 2513	. . . . . . . . . . . . 13
155	124, 136, 154	3eqtr4d 2515	. . . . . . . . . . . 12
156	155	ad2antrr 740	. . . . . . . . . . 11 $/\$ $/\$ $/\$
157	77	nncnd 10647	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
158		id 22	. . . . . . . . . . . . 13
159	158	sumsn 13884	. . . . . . . . . . . 12 $/\$
160	157, 157, 159	syl2anc 673	. . . . . . . . . . 11 $/\$ $/\$ $/\$
161	156, 160	oveq12d 6326	. . . . . . . . . 10 $/\$ $/\$ $/\$
162	116, 161	eqtrd 2505	. . . . . . . . 9 $/\$ $/\$ $/\$
163	4	nnnn0d 10949	. . . . . . . . . . . . . . . . 17
164		expp1 12317	. . . . . . . . . . . . . . . . 17 $/\$
165	12, 163, 164	sylancr 676	. . . . . . . . . . . . . . . 16
166		2nn 10790	. . . . . . . . . . . . . . . . . . 19
167		nnexpcl 12323	. . . . . . . . . . . . . . . . . . 19 $/\$
168	166, 163, 167	sylancr 676	. . . . . . . . . . . . . . . . . 18
169	168	nncnd 10647	. . . . . . . . . . . . . . . . 17
170		mulcom 9643	. . . . . . . . . . . . . . . . 17 $/\$
171	169, 12, 170	sylancl 675	. . . . . . . . . . . . . . . 16
172	165, 171	eqtrd 2505	. . . . . . . . . . . . . . 15
173	172	oveq1d 6323	. . . . . . . . . . . . . 14
174	12	a1i 11	. . . . . . . . . . . . . . 15
175	174, 169, 55	mulassd 9684	. . . . . . . . . . . . . 14
176		isodd7 38940	. . . . . . . . . . . . . . . . . . 19 Odd $/\$
177		simpr 468	. . . . . . . . . . . . . . . . . . 19 $/\$
178	176, 177	sylbi 200	. . . . . . . . . . . . . . . . . 18 Odd
179	5, 178	syl 17	. . . . . . . . . . . . . . . . 17
180		2z 10993	. . . . . . . . . . . . . . . . . . 19
181	180	a1i 11	. . . . . . . . . . . . . . . . . 18
182		rpexp1i 14752	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
183	181, 94, 163, 182	syl3anc 1292	. . . . . . . . . . . . . . . . 17
184	179, 183	mpd 15	. . . . . . . . . . . . . . . 16
185		sgmmul 24208	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
186	140, 168, 1, 184, 185	syl13anc 1294	. . . . . . . . . . . . . . 15
187		pncan 9901	. . . . . . . . . . . . . . . . . . . 20 $/\$
188	28, 27, 187	sylancl 675	. . . . . . . . . . . . . . . . . . 19
189	188	oveq2d 6324	. . . . . . . . . . . . . . . . . 18
190	189	oveq2d 6324	. . . . . . . . . . . . . . . . 17
191		1sgm2ppw 24207	. . . . . . . . . . . . . . . . . 18
192	20, 191	syl 17	. . . . . . . . . . . . . . . . 17
193	190, 192	eqtr3d 2507	. . . . . . . . . . . . . . . 16
194	193	oveq1d 6323	. . . . . . . . . . . . . . 15
195	186, 6, 194	3eqtr3d 2513	. . . . . . . . . . . . . 14
196	173, 175, 195	3eqtrd 2509	. . . . . . . . . . . . 13
197	196	oveq1d 6323	. . . . . . . . . . . 12
198		1nn0 10909	. . . . . . . . . . . . . . 15
199		sgmnncl 24153	. . . . . . . . . . . . . . 15 $/\$
200	198, 1, 199	sylancr 676	. . . . . . . . . . . . . 14
201	200	nncnd 10647	. . . . . . . . . . . . 13
202	201, 87, 88	divcan3d 10410	. . . . . . . . . . . 12
203	197, 150, 202	3eqtr3d 2513	. . . . . . . . . . 11
204		sgmval 24148	. . . . . . . . . . . 12 $/\$
205	27, 1, 204	sylancr 676	. . . . . . . . . . 11
206		simpr 468	. . . . . . . . . . . . . . 15 $/\$
207	67, 206	sseldi 3416	. . . . . . . . . . . . . 14 $/\$
208	207	nncnd 10647	. . . . . . . . . . . . 13 $/\$
209	208	cxp1d 23730	. . . . . . . . . . . 12 $/\$
210	209	sumeq2dv 13846	. . . . . . . . . . 11
211	203, 205, 210	3eqtrrd 2510	. . . . . . . . . 10
212	211	ad2antrr 740	. . . . . . . . 9 $/\$ $/\$ $/\$
213	107, 162, 212	3brtr3d 4425	. . . . . . . 8 $/\$ $/\$ $/\$
214	36, 9	remulcld 9689	. . . . . . . . . . 11
215	214	ad2antrr 740	. . . . . . . . . 10 $/\$ $/\$ $/\$
216	77	nnrpd 11362	. . . . . . . . . 10 $/\$ $/\$ $/\$
217	215, 216	ltaddrpd 11394	. . . . . . . . 9 $/\$ $/\$ $/\$
218	77	nnred 10646	. . . . . . . . . . 11 $/\$ $/\$ $/\$
219	215, 218	readdcld 9688	. . . . . . . . . 10 $/\$ $/\$ $/\$
220	215, 219	ltnled 9799	. . . . . . . . 9 $/\$ $/\$ $/\$
221	217, 220	mpbid 215	. . . . . . . 8 $/\$ $/\$ $/\$
222	213, 221	condan 811	. . . . . . 7 $/\$ $/\$
223		elpri 3976	. . . . . . 7 $\/$
224	222, 223	syl 17	. . . . . 6 $/\$ $/\$ $\/$
225	224	expr 626	. . . . 5 $/\$ $\/$
226	225	ralrimiva 2809	. . . 4 $\/$
227	3, 58	gtned 9787	. . . . . . . . . 10
228	227	necomd 2698	. . . . . . . . 9
229		1nn 10642	. . . . . . . . . . . . 13
230	229	a1i 11	. . . . . . . . . . . 12
231		1dvds 14394	. . . . . . . . . . . . 13
232	94, 231	syl 17	. . . . . . . . . . . 12
233		breq1 4398	. . . . . . . . . . . . . 14
234		eqeq1 2475	. . . . . . . . . . . . . . 15
235		eqeq1 2475	. . . . . . . . . . . . . . 15
236	234, 235	orbi12d 724	. . . . . . . . . . . . . 14 $\/$ $\/$
237	233, 236	imbi12d 327	. . . . . . . . . . . . 13 $\/$ $\/$
238	237	rspcv 3132	. . . . . . . . . . . 12 $\/$ $\/$
239	230, 226, 232, 238	syl3c 62	. . . . . . . . . . 11 $\/$
240	239	ord 384	. . . . . . . . . 10
241	240	necon1ad 2660	. . . . . . . . 9
242	228, 241	mpd 15	. . . . . . . 8
243	242	eqeq2d 2481	. . . . . . 7
244	243	orbi1d 717	. . . . . 6 $\/$ $\/$
245	244	imbi2d 323	. . . . 5 $\/$ $\/$
246	245	ralbidv 2829	. . . 4 $\/$ $\/$
247	226, 246	mpbird 240	. . 3 $\/$
248		isprm2 14711	. . 3 $/\$ $\/$
249	60, 247, 248	sylanbrc 677	. 2
250	214	ltp1d 10559	. . . 4
251		peano2re 9824	. . . . . 6
252	214, 251	syl 17	. . . . 5
253	214, 252	ltnled 9799	. . . 4
254	250, 253	mpbid 215	. . 3
255	207	nnred 10646	. . . . . . . 8 $/\$
256	207	nnnn0d 10949	. . . . . . . . 9 $/\$
257	256	nn0ge0d 10952	. . . . . . . 8 $/\$
258		df-tp 3964	. . . . . . . . . 10
259		snssi 4107	. . . . . . . . . . . 12
260	229, 259	mp1i 13	. . . . . . . . . . 11
261	75, 260	unssd 3601	. . . . . . . . . 10
262	258, 261	syl5eqss 3462	. . . . . . . . 9
263		eltpi 4007	. . . . . . . . . . 11 $\/$ $\/$
264		breq1 4398	. . . . . . . . . . . . 13
265	232, 264	syl5ibrcom 230	. . . . . . . . . . . 12
266	92, 98, 265	3jaod 1358	. . . . . . . . . . 11 $\/$ $\/$
267	263, 266	syl5 32	. . . . . . . . . 10
268	267	imp 436	. . . . . . . . 9 $/\$
269	262, 268	ssrabdv 3494	. . . . . . . 8
270	65, 255, 257, 269	fsumless 13933	. . . . . . 7
271	270	adantr 472	. . . . . 6 $/\$
272	55, 87, 88	diveq1ad 10414	. . . . . . . . . . . . 13
273	272	necon3bid 2687	. . . . . . . . . . . 12
274	273	biimpar 493	. . . . . . . . . . 11 $/\$
275	274	necomd 2698	. . . . . . . . . 10 $/\$
276	228	adantr 472	. . . . . . . . . 10 $/\$
277	275, 276	nelprd 3981	. . . . . . . . 9 $/\$
278		disjsn 4023	. . . . . . . . 9
279	277, 278	sylibr 217	. . . . . . . 8 $/\$
280	258	a1i 11	. . . . . . . 8 $/\$
281		tpfi 7865	. . . . . . . . 9
282	281	a1i 11	. . . . . . . 8 $/\$
283	262	adantr 472	. . . . . . . . . 10 $/\$
284	283	sselda 3418	. . . . . . . . 9 $/\$ $/\$
285	284	nncnd 10647	. . . . . . . 8 $/\$ $/\$
286	279, 280, 282, 285	fsumsplit 13883	. . . . . . 7 $/\$
287		id 22	. . . . . . . . . . 11
288	287	sumsn 13884	. . . . . . . . . 10 $/\$
289	140, 27, 288	sylancl 675	. . . . . . . . 9
290	155, 289	oveq12d 6326	. . . . . . . 8
291	290	adantr 472	. . . . . . 7 $/\$
292	286, 291	eqtrd 2505	. . . . . 6 $/\$
293	211	adantr 472	. . . . . 6 $/\$
294	271, 292, 293	3brtr3d 4425	. . . . 5 $/\$
295	294	ex 441	. . . 4
296	295	necon1bd 2661	. . 3
297	254, 296	mpd 15	. 2
298	249, 297	jca 541	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $\/$ wo 375 $/\$ wa 376 $\/$ w3o 1006

wceq 1452

wcel 1904

wne 2641

wral 2756

crab 2760

cun 3388

cin 3389

wss 3390

c0 3722

csn 3959

cpr 3961

ctp 3963 class class class wbr 4395

cfv 5589 (class class class)co 6308

cfn 7587

cc 9555

cr 9556

cc0 9557

c1 9558

caddc 9560

cmul 9562

clt 9693

cle 9694

cmin 9880

cdiv 10291

cn 10631

c2 10681

cn0 10893

cz 10961

cuz 11182

crp 11325

cfz 11810

cexp 12310

csu 13829

cdvds 14382

cgcd 14547

cprime 14701

ccxp 23584

csgm 24101 Odd codd 38899

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635 ax-addf 9636 ax-mulf 9637

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-iin 4272 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-of 6550 df-om 6712 df-1st 6812 df-2nd 6813 df-supp 6934 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-er 7381 df-map 7492 df-pm 7493 df-ixp 7541 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-fsupp 7902 df-fi 7943 df-sup 7974 df-inf 7975 df-oi 8043 df-card 8391 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-4 10692 df-5 10693 df-6 10694 df-7 10695 df-8 10696 df-9 10697 df-10 10698 df-n0 10894 df-z 10962 df-dec 11075 df-uz 11183 df-q 11288 df-rp 11326 df-xneg 11432 df-xadd 11433 df-xmul 11434 df-ioo 11664 df-ioc 11665 df-ico 11666 df-icc 11667 df-fz 11811 df-fzo 11943 df-fl 12061 df-mod 12130 df-seq 12252 df-exp 12311 df-fac 12498 df-bc 12526 df-hash 12554 df-shft 13207 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-limsup 13603 df-clim 13629 df-rlim 13630 df-sum 13830 df-ef 14198 df-sin 14200 df-cos 14201 df-pi 14203 df-dvds 14383 df-gcd 14548 df-prm 14702 df-pc 14866 df-struct 15201 df-ndx 15202 df-slot 15203 df-base 15204 df-sets 15205 df-ress 15206 df-plusg 15281 df-mulr 15282 df-starv 15283 df-sca 15284 df-vsca 15285 df-ip 15286 df-tset 15287 df-ple 15288 df-ds 15290 df-unif 15291 df-hom 15292 df-cco 15293 df-rest 15399 df-topn 15400 df-0g 15418 df-gsum 15419 df-topgen 15420 df-pt 15421 df-prds 15424 df-xrs 15478 df-qtop 15484 df-imas 15485 df-xps 15488 df-mre 15570 df-mrc 15571 df-acs 15573 df-mgm 16566 df-sgrp 16605 df-mnd 16615 df-submnd 16661 df-mulg 16754 df-cntz 17049 df-cmn 17510 df-psmet 19039 df-xmet 19040 df-met 19041 df-bl 19042 df-mopn 19043 df-fbas 19044 df-fg 19045 df-cnfld 19048 df-top 19998 df-bases 19999 df-topon 20000 df-topsp 20001 df-cld 20111 df-ntr 20112 df-cls 20113 df-nei 20191 df-lp 20229 df-perf 20230 df-cn 20320 df-cnp 20321 df-haus 20408 df-tx 20654 df-hmeo 20847 df-fil 20939 df-fm 21031 df-flim 21032 df-flf 21033 df-xms 21413 df-ms 21414 df-tms 21415 df-cncf 21988 df-limc 22900 df-dv 22901 df-log 23585 df-cxp 23586 df-sgm 24107 df-even 38900 df-odd 38901

This theorem is referenced by: perfectALTV 38990

W3C validator