prmreclem5 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > prmreclem5		Structured version Visualization version Unicode version

Theorem prmreclem5 15624

Description: Lemma for prmrec 15626. Here we show the inequality

by decomposing the set

into the disjoint union of the set

of those numbers that are not divisible by any "large" primes (above

) and the indexed union over

of the numbers

that divide the prime

. By prmreclem4 15623 the second of these has size less than

times the prime reciprocal series, which is less than

by assumption, we find that the complementary part

must be at least

large. (Contributed by Mario Carneiro, 6-Aug-2014.)

**Hypotheses**
Ref	Expression
prmrec.1
prmrec.2
prmrec.3
prmrec.4	$\$
prmrec.5
prmrec.6
prmrec.7	$/\$

**Assertion**
Ref	Expression
prmreclem5

Distinct variable groups:

Allowed substitution hints:

(

)

Proof of Theorem prmreclem5 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prmrec.3	. . . 4
2	1	nnred 11035	. . 3
3	2	rehalfcld 11279	. 2
4		fzfi 12771	. . . . . 6
5		prmrec.4	. . . . . . 7 $\$
6		ssrab2 3687	. . . . . . 7 $\$
7	5, 6	eqsstri 3635	. . . . . 6
8		ssfi 8180	. . . . . 6 $/\$
9	4, 7, 8	mp2an 708	. . . . 5
10		hashcl 13147	. . . . 5
11	9, 10	ax-mp 5	. . . 4
12	11	nn0rei 11303	. . 3
13	12	a1i 11	. 2
14		2nn 11185	. . . . 5
15		prmrec.2	. . . . . 6
16	15	nnnn0d 11351	. . . . 5
17		nnexpcl 12873	. . . . 5 $/\$
18	14, 16, 17	sylancr 695	. . . 4
19	18	nnred 11035	. . 3
20	1	nnrpd 11870	. . . . 5
21	20	rpsqrtcld 14150	. . . 4
22	21	rpred 11872	. . 3
23	19, 22	remulcld 10070	. 2
24	2	recnd 10068	. . . . . 6
25	24	2halvesd 11278	. . . . 5
26	7	a1i 11	. . . . . . . . 9
27	15	peano2nnd 11037	. . . . . . . . . . . . 13
28		elfzuz 12338	. . . . . . . . . . . . 13
29		eluznn 11758	. . . . . . . . . . . . 13 $/\$
30	27, 28, 29	syl2an 494	. . . . . . . . . . . 12 $/\$
31		eleq1 2689	. . . . . . . . . . . . . . . . 17
32		breq1 4656	. . . . . . . . . . . . . . . . 17
33	31, 32	anbi12d 747	. . . . . . . . . . . . . . . 16 $/\$ $/\$
34	33	rabbidv 3189	. . . . . . . . . . . . . . 15 $/\$ $/\$
35		prmrec.7	. . . . . . . . . . . . . . 15 $/\$
36		ovex 6678	. . . . . . . . . . . . . . . 16
37	36	rabex 4813	. . . . . . . . . . . . . . 15 $/\$
38	34, 35, 37	fvmpt 6282	. . . . . . . . . . . . . 14 $/\$
39	38	adantl 482	. . . . . . . . . . . . 13 $/\$ $/\$
40		ssrab2 3687	. . . . . . . . . . . . 13 $/\$
41	39, 40	syl6eqss 3655	. . . . . . . . . . . 12 $/\$
42	30, 41	syldan 487	. . . . . . . . . . 11 $/\$
43	42	ralrimiva 2966	. . . . . . . . . 10
44		iunss 4561	. . . . . . . . . 10
45	43, 44	sylibr 224	. . . . . . . . 9
46	26, 45	unssd 3789	. . . . . . . 8
47		breq1 4656	. . . . . . . . . . . . . . . . . 18
48	47	notbid 308	. . . . . . . . . . . . . . . . 17
49	48	cbvralv 3171	. . . . . . . . . . . . . . . 16 $\$ $\$
50		breq2 4657	. . . . . . . . . . . . . . . . . 18
51	50	notbid 308	. . . . . . . . . . . . . . . . 17
52	51	ralbidv 2986	. . . . . . . . . . . . . . . 16 $\$ $\$
53	49, 52	syl5bb 272	. . . . . . . . . . . . . . 15 $\$ $\$
54	53, 5	elrab2 3366	. . . . . . . . . . . . . 14 $/\$ $\$
55		elun1 3780	. . . . . . . . . . . . . 14
56	54, 55	sylbir 225	. . . . . . . . . . . . 13 $/\$ $\$
57	56	ex 450	. . . . . . . . . . . 12 $\$
58	57	adantl 482	. . . . . . . . . . 11 $/\$ $\$
59		dfrex2 2996	. . . . . . . . . . . 12 $\$ $\$
60		eldifn 3733	. . . . . . . . . . . . . . . . . . . 20 $\$
61	60	ad2antrl 764	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\$ $/\$
62		eldifi 3732	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
63	62	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $/\$
64		prmnn 15388	. . . . . . . . . . . . . . . . . . . . . 22
65	63, 64	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$ $/\$
66		nnuz 11723	. . . . . . . . . . . . . . . . . . . . 21
67	65, 66	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $/\$
68	15	nnzd 11481	. . . . . . . . . . . . . . . . . . . . 21
69	68	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $/\$
70		elfz5 12334	. . . . . . . . . . . . . . . . . . . 20 $/\$
71	67, 69, 70	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\$ $/\$
72	61, 71	mtbid 314	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $/\$
73	15	nnred 11035	. . . . . . . . . . . . . . . . . . . 20
74	73	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\$ $/\$
75	65	nnred 11035	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\$ $/\$
76	74, 75	ltnled 10184	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $/\$
77	72, 76	mpbird 247	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $/\$
78		prmz 15389	. . . . . . . . . . . . . . . . . . 19
79	63, 78	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $/\$
80		zltp1le 11427	. . . . . . . . . . . . . . . . . 18 $/\$
81	69, 79, 80	syl2anc 693	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $/\$
82	77, 81	mpbid 222	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$
83		elfznn 12370	. . . . . . . . . . . . . . . . . . 19
84	83	ad2antlr 763	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $/\$
85	84	nnred 11035	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $/\$
86	2	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $/\$
87		simprr 796	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $/\$
88		dvdsle 15032	. . . . . . . . . . . . . . . . . . 19 $/\$
89	79, 84, 88	syl2anc 693	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $/\$
90	87, 89	mpd 15	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $/\$
91		elfzle2 12345	. . . . . . . . . . . . . . . . . 18
92	91	ad2antlr 763	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $/\$
93	75, 85, 86, 90, 92	letrd 10194	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$
94	68	peano2zd 11485	. . . . . . . . . . . . . . . . . 18
95	94	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $/\$
96	1	nnzd 11481	. . . . . . . . . . . . . . . . . 18
97	96	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $/\$
98		elfz 12332	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
99	79, 95, 97, 98	syl3anc 1326	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$ $/\$
100	82, 93, 99	mpbir2and 957	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $/\$
101		simplr 792	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $/\$
102	63, 87	jca 554	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $/\$ $/\$
103	50	anbi2d 740	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
104	103	elrab 3363	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
105	101, 102, 104	sylanbrc 698	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$ $/\$
106		eleq1 2689	. . . . . . . . . . . . . . . . . . . 20
107	106, 47	anbi12d 747	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
108	107	rabbidv 3189	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
109	36	rabex 4813	. . . . . . . . . . . . . . . . . 18 $/\$
110	108, 35, 109	fvmpt 6282	. . . . . . . . . . . . . . . . 17 $/\$
111	65, 110	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$ $/\$
112	105, 111	eleqtrrd 2704	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $/\$
113		fveq2 6191	. . . . . . . . . . . . . . . 16
114	113	eliuni 4526	. . . . . . . . . . . . . . 15 $/\$
115	100, 112, 114	syl2anc 693	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $/\$
116		elun2 3781	. . . . . . . . . . . . . 14
117	115, 116	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$
118	117	rexlimdvaa 3032	. . . . . . . . . . . 12 $/\$ $\$
119	59, 118	syl5bir 233	. . . . . . . . . . 11 $/\$ $\$
120	58, 119	pm2.61d 170	. . . . . . . . . 10 $/\$
121	120	ex 450	. . . . . . . . 9
122	121	ssrdv 3609	. . . . . . . 8
123	46, 122	eqssd 3620	. . . . . . 7
124	123	fveq2d 6195	. . . . . 6
125	1	nnnn0d 11351	. . . . . . 7
126		hashfz1 13134	. . . . . . 7
127	125, 126	syl 17	. . . . . 6
128	124, 127	eqtr2d 2657	. . . . 5
129	9	a1i 11	. . . . . 6
130		ssfi 8180	. . . . . . 7 $/\$
131	4, 45, 130	sylancr 695	. . . . . 6
132		breq1 4656	. . . . . . . . . . . . . . . . 17
133	132	notbid 308	. . . . . . . . . . . . . . . 16
134		breq2 4657	. . . . . . . . . . . . . . . . . . . . 21
135	134	notbid 308	. . . . . . . . . . . . . . . . . . . 20
136	135	ralbidv 2986	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
137	136, 5	elrab2 3366	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
138	137	simprbi 480	. . . . . . . . . . . . . . . . 17 $\$
139	138	ad2antlr 763	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
140		simprr 796	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
141		noel 3919	. . . . . . . . . . . . . . . . . 18
142		simprl 794	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
143	142	biantrud 528	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
144		elin 3796	. . . . . . . . . . . . . . . . . . . 20 $/\$
145	143, 144	syl6bbr 278	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
146	73	ltp1d 10954	. . . . . . . . . . . . . . . . . . . . . 22
147		fzdisj 12368	. . . . . . . . . . . . . . . . . . . . . 22
148	146, 147	syl 17	. . . . . . . . . . . . . . . . . . . . 21
149	148	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
150	149	eleq2d 2687	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
151	145, 150	bitrd 268	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
152	141, 151	mtbiri 317	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
153	140, 152	eldifd 3585	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
154	133, 139, 153	rspcdva 3316	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
155	154	expr 643	. . . . . . . . . . . . . 14 $/\$ $/\$
156		imnan 438	. . . . . . . . . . . . . 14 $/\$
157	155, 156	sylib 208	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
158	30	adantlr 751	. . . . . . . . . . . . . . . 16 $/\$ $/\$
159	158, 38	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
160	159	eleq2d 2687	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
161		breq2 4657	. . . . . . . . . . . . . . . . 17
162	161	anbi2d 740	. . . . . . . . . . . . . . . 16 $/\$ $/\$
163	162	elrab 3363	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
164	163	simprbi 480	. . . . . . . . . . . . . 14 $/\$ $/\$
165	160, 164	syl6bi 243	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
166	157, 165	mtod 189	. . . . . . . . . . . 12 $/\$ $/\$
167	166	nrexdv 3001	. . . . . . . . . . 11 $/\$
168		eliun 4524	. . . . . . . . . . 11
169	167, 168	sylnibr 319	. . . . . . . . . 10 $/\$
170	169	ex 450	. . . . . . . . 9
171		imnan 438	. . . . . . . . 9 $/\$
172	170, 171	sylib 208	. . . . . . . 8 $/\$
173		elin 3796	. . . . . . . 8 $/\$
174	172, 173	sylnibr 319	. . . . . . 7
175	174	eq0rdv 3979	. . . . . 6
176		hashun 13171	. . . . . 6 $/\$ $/\$
177	129, 131, 175, 176	syl3anc 1326	. . . . 5
178	25, 128, 177	3eqtrd 2660	. . . 4
179		hashcl 13147	. . . . . . 7
180	131, 179	syl 17	. . . . . 6
181	180	nn0red 11352	. . . . 5
182		fzfid 12772	. . . . . . . 8
183	27, 29	sylan 488	. . . . . . . . . 10 $/\$
184		nnrecre 11057	. . . . . . . . . . 11
185		0re 10040	. . . . . . . . . . 11
186		ifcl 4130	. . . . . . . . . . 11 $/\$
187	184, 185, 186	sylancl 694	. . . . . . . . . 10
188	183, 187	syl 17	. . . . . . . . 9 $/\$
189	28, 188	sylan2 491	. . . . . . . 8 $/\$
190	182, 189	fsumrecl 14465	. . . . . . 7
191	2, 190	remulcld 10070	. . . . . 6
192		prmrec.1	. . . . . . . 8
193		prmrec.5	. . . . . . . 8
194		prmrec.6	. . . . . . . 8
195	192, 15, 1, 5, 193, 194, 35	prmreclem4 15623	. . . . . . 7
196		eluz 11701	. . . . . . . . . 10 $/\$
197	96, 68, 196	syl2anc 693	. . . . . . . . 9
198		nnleltp1 11432	. . . . . . . . . 10 $/\$
199	1, 15, 198	syl2anc 693	. . . . . . . . 9
200		fzn 12357	. . . . . . . . . 10 $/\$
201	94, 96, 200	syl2anc 693	. . . . . . . . 9
202	197, 199, 201	3bitrd 294	. . . . . . . 8
203		0le0 11110	. . . . . . . . . 10
204	24	mul01d 10235	. . . . . . . . . 10
205	203, 204	syl5breqr 4691	. . . . . . . . 9
206		iuneq1 4534	. . . . . . . . . . . . 13
207		0iun 4577	. . . . . . . . . . . . 13
208	206, 207	syl6eq 2672	. . . . . . . . . . . 12
209	208	fveq2d 6195	. . . . . . . . . . 11
210		hash0 13158	. . . . . . . . . . 11
211	209, 210	syl6eq 2672	. . . . . . . . . 10
212		sumeq1 14419	. . . . . . . . . . . 12
213		sum0 14452	. . . . . . . . . . . 12
214	212, 213	syl6eq 2672	. . . . . . . . . . 11
215	214	oveq2d 6666	. . . . . . . . . 10
216	211, 215	breq12d 4666	. . . . . . . . 9
217	205, 216	syl5ibrcom 237	. . . . . . . 8
218	202, 217	sylbid 230	. . . . . . 7
219		uztric 11709	. . . . . . . 8 $/\$ $\/$
220	68, 96, 219	syl2anc 693	. . . . . . 7 $\/$
221	195, 218, 220	mpjaod 396	. . . . . 6
222		eqid 2622	. . . . . . . . . 10
223		eleq1 2689	. . . . . . . . . . . . 13
224		oveq2 6658	. . . . . . . . . . . . 13
225	223, 224	ifbieq1d 4109	. . . . . . . . . . . 12
226		ovex 6678	. . . . . . . . . . . . 13
227		c0ex 10034	. . . . . . . . . . . . 13
228	226, 227	ifex 4156	. . . . . . . . . . . 12
229	225, 192, 228	fvmpt 6282	. . . . . . . . . . 11
230	183, 229	syl 17	. . . . . . . . . 10 $/\$
231	187	recnd 10068	. . . . . . . . . . . . . 14
232	229, 231	eqeltrd 2701	. . . . . . . . . . . . 13
233	232	adantl 482	. . . . . . . . . . . 12 $/\$
234	66, 27, 233	iserex 14387	. . . . . . . . . . 11
235	193, 234	mpbid 222	. . . . . . . . . 10
236	222, 94, 230, 188, 235	isumrecl 14496	. . . . . . . . 9
237		halfre 11246	. . . . . . . . . 10
238	237	a1i 11	. . . . . . . . 9
239		fzssuz 12382	. . . . . . . . . . 11
240	239	a1i 11	. . . . . . . . . 10
241		nnrp 11842	. . . . . . . . . . . . . 14
242	241	rpreccld 11882	. . . . . . . . . . . . 13
243	242	rpge0d 11876	. . . . . . . . . . . 12
244		breq2 4657	. . . . . . . . . . . . 13
245		breq2 4657	. . . . . . . . . . . . 13
246	244, 245	ifboth 4124	. . . . . . . . . . . 12 $/\$
247	243, 203, 246	sylancl 694	. . . . . . . . . . 11
248	183, 247	syl 17	. . . . . . . . . 10 $/\$
249	222, 94, 182, 240, 230, 188, 248, 235	isumless 14577	. . . . . . . . 9
250	190, 236, 238, 249, 194	lelttrd 10195	. . . . . . . 8
251	1	nngt0d 11064	. . . . . . . . 9
252		ltmul2 10874	. . . . . . . . 9 $/\$ $/\$ $/\$
253	190, 238, 2, 251, 252	syl112anc 1330	. . . . . . . 8
254	250, 253	mpbid 222	. . . . . . 7
255		2cn 11091	. . . . . . . . 9
256		2ne0 11113	. . . . . . . . 9
257		divrec 10701	. . . . . . . . 9 $/\$ $/\$
258	255, 256, 257	mp3an23 1416	. . . . . . . 8
259	24, 258	syl 17	. . . . . . 7
260	254, 259	breqtrrd 4681	. . . . . 6
261	181, 191, 3, 221, 260	lelttrd 10195	. . . . 5
262	181, 3, 13, 261	ltadd2dd 10196	. . . 4
263	178, 262	eqbrtrd 4675	. . 3
264	3, 13, 3	ltadd1d 10620	. . 3
265	263, 264	mpbird 247	. 2
266		oveq1 6657	. . . . . . . 8
267	266	breq1d 4663	. . . . . . 7
268	267	cbvrabv 3199	. . . . . 6
269		breq2 4657	. . . . . . 7
270	269	rabbidv 3189	. . . . . 6
271	268, 270	syl5eq 2668	. . . . 5
272	271	supeq1d 8352	. . . 4
273	272	cbvmptv 4750	. . 3
274	192, 15, 1, 5, 273	prmreclem3 15622	. 2
275	3, 13, 23, 265, 274	ltletrd 10197	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384

wceq 1483

wcel 1990

wne 2794

wral 2912

wrex 2913

crab 2916 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

c0 3915

cif 4086

ciun 4520 class class class wbr 4653

cmpt 4729

cdm 5114

cfv 5888 (class class class)co 6650

cfn 7955

csup 8346

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

clt 10074

cle 10075

cdiv 10684

cn 11020

c2 11070

cn0 11292

cz 11377

cuz 11687

cfz 12326

cseq 12801

cexp 12860

chash 13117

csqrt 13973

cli 14215

csu 14416

cdvds 14983

cprime 15385

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-q 11789 df-rp 11833 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-rlim 14220 df-sum 14417 df-dvds 14984 df-gcd 15217 df-prm 15386 df-pc 15542

This theorem is referenced by: prmreclem6 15625

W3C validator