Theorem prmlem2 15827

Description: Our last proving session got as far as 25 because we started with the two "bootstrap" primes 2 and 3, and the next prime is 5, so knowing that 2 and 3 are prime and 4 is not allows us to cover the numbers less than 5 ^ 2 = 2 5. Additionally, nonprimes are "easy", so we can extend this range of known prime/nonprimes all the way until 29, which is the first prime larger than 25. Thus, in this lemma we extend another blanket out to 2 9 ^ 2 = 8 4 1, from which we can prove even more primes. If we wanted, we could keep doing this, but the goal is Bertrand's postulate, and for that we only need a few large primes - we don't need to find them all, as we have been doing thus far. So after this blanket runs out, we'll have to switch to another method (see 1259prm 15843).

As a side note, you can see the pattern of the primes in the indentation pattern of this lemma! (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)

Hypotheses

Ref	Expression
prmlem2.n	|- N e. NN
prmlem2.lt	|- N < ;; 8 4 1
prmlem2.gt	|- 1 < N
prmlem2.2	|- -. 2 || N
prmlem2.3	|- -. 3 || N
prmlem2.5	|- -. 5 || N
prmlem2.7	|- -. 7 || N
prmlem2.11	|- -. ; 1 1 || N
prmlem2.13	|- -. ; 1 3 || N
prmlem2.17	|- -. ; 1 7 || N
prmlem2.19	|- -. ; 1 9 || N
prmlem2.23	|- -. ; 2 3 || N

Assertion

Ref	Expression
prmlem2	|- N e. Prime

Proof of Theorem prmlem2

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		prmlem2.n	. 2 |- N e. NN
2		prmlem2.gt	. 2 |- 1 < N
3		prmlem2.2	. 2 |- -. 2 || N
4		prmlem2.3	. 2 |- -. 3 || N
5		eluzelre 11698	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( ZZ>= ` ; 2 9 ) -> x e. RR )
6	5	resqcld 13035	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( ZZ>= ` ; 2 9 ) -> ( x ^ 2 ) e. RR )
7		eluzle 11700	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( ZZ>= ` ; 2 9 ) -> ; 2 9 <_ x )
8		2nn0 11309	. . . . . . . . . . . . . . . . . . . . . . 23 |- 2 e. NN0
9		9nn0 11316	. . . . . . . . . . . . . . . . . . . . . . 23 |- 9 e. NN0
10	8, 9	deccl 11512	. . . . . . . . . . . . . . . . . . . . . 22 |- ; 2 9 e. NN0
11	10	nn0rei 11303	. . . . . . . . . . . . . . . . . . . . 21 |- ; 2 9 e. RR
12	10	nn0ge0i 11320	. . . . . . . . . . . . . . . . . . . . 21 |- 0 <_ ; 2 9
13		le2sq2 12939	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( (; 2 9 e. RR /\ 0 <_ ; 2 9 ) /\ ( x e. RR /\ ; 2 9 <_ x ) ) -> (; 2 9 ^ 2 ) <_ ( x ^ 2 ) )
14	11, 12, 13	mpanl12 718	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x e. RR /\ ; 2 9 <_ x ) -> (; 2 9 ^ 2 ) <_ ( x ^ 2 ) )
15	5, 7, 14	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( ZZ>= ` ; 2 9 ) -> (; 2 9 ^ 2 ) <_ ( x ^ 2 ) )
16	1	nnrei 11029	. . . . . . . . . . . . . . . . . . . 20 |- N e. RR
17	11	resqcli 12949	. . . . . . . . . . . . . . . . . . . 20 |- (; 2 9 ^ 2 ) e. RR
18		prmlem2.lt	. . . . . . . . . . . . . . . . . . . . . 22 |- N < ;; 8 4 1
19	10	nn0cni 11304	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ; 2 9 e. CC
20	19	sqvali 12943	. . . . . . . . . . . . . . . . . . . . . . 23 |- (; 2 9 ^ 2 ) = (; 2 9 x. ; 2 9 )
21		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ; 2 9 = ; 2 9
22		1nn0 11308	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 1 e. NN0
23		6nn0 11313	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 6 e. NN0
24	8, 23	deccl 11512	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ; 2 6 e. NN0
25		5nn0 11312	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 5 e. NN0
26		8nn0 11315	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 8 e. NN0
27	19	2timesi 11147	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( 2 x. ; 2 9 ) = (; 2 9 + ; 2 9 )
28		2p2e4 11144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( 2 + 2 ) = 4
29	28	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( 2 + 2 ) + 1 ) = ( 4 + 1 )
30		4p1e5 11154	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( 4 + 1 ) = 5
31	29, 30	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( 2 + 2 ) + 1 ) = 5
32		9p9e18 11627	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( 9 + 9 ) = ; 1 8
33	8, 9, 8, 9, 21, 21, 31, 26, 32	decaddc 11572	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (; 2 9 + ; 2 9 ) = ; 5 8
34	27, 33	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 2 x. ; 2 9 ) = ; 5 8
35		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ; 2 6 = ; 2 6
36		5p2e7 11165	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( 5 + 2 ) = 7
37	36	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 5 + 2 ) + 1 ) = ( 7 + 1 )
38		7p1e8 11157	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( 7 + 1 ) = 8
39	37, 38	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 5 + 2 ) + 1 ) = 8
40		4nn0 11311	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 4 e. NN0
41		8p6e14 11616	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 8 + 6 ) = ; 1 4
42	25, 26, 8, 23, 34, 35, 39, 40, 41	decaddc 11572	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 2 x. ; 2 9 ) + ; 2 6 ) = ; 8 4
43		9t2e18 11663	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( 9 x. 2 ) = ; 1 8
44		1p1e2 11134	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( 1 + 1 ) = 2
45		8p8e16 11618	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( 8 + 8 ) = ; 1 6
46	22, 26, 26, 43, 44, 23, 45	decaddci 11580	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 9 x. 2 ) + 8 ) = ; 2 6
47		9t9e81 11670	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 9 x. 9 ) = ; 8 1
48	9, 8, 9, 21, 22, 26, 46, 47	decmul2c 11589	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 9 x. ; 2 9 ) = ;; 2 6 1
49	10, 8, 9, 21, 22, 24, 42, 48	decmul1c 11587	. . . . . . . . . . . . . . . . . . . . . . 23 |- (; 2 9 x. ; 2 9 ) = ;; 8 4 1
50	20, 49	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . 22 |- (; 2 9 ^ 2 ) = ;; 8 4 1
51	18, 50	breqtrri 4680	. . . . . . . . . . . . . . . . . . . . 21 |- N < (; 2 9 ^ 2 )
52		ltletr 10129	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( N e. RR /\ (; 2 9 ^ 2 ) e. RR /\ ( x ^ 2 ) e. RR ) -> ( ( N < (; 2 9 ^ 2 ) /\ (; 2 9 ^ 2 ) <_ ( x ^ 2 ) ) -> N < ( x ^ 2 ) ) )
53	51, 52	mpani 712	. . . . . . . . . . . . . . . . . . . 20 |- ( ( N e. RR /\ (; 2 9 ^ 2 ) e. RR /\ ( x ^ 2 ) e. RR ) -> ( (; 2 9 ^ 2 ) <_ ( x ^ 2 ) -> N < ( x ^ 2 ) ) )
54	16, 17, 53	mp3an12 1414	. . . . . . . . . . . . . . . . . . 19 |- ( ( x ^ 2 ) e. RR -> ( (; 2 9 ^ 2 ) <_ ( x ^ 2 ) -> N < ( x ^ 2 ) ) )
55	6, 15, 54	sylc 65	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( ZZ>= ` ; 2 9 ) -> N < ( x ^ 2 ) )
56		ltnle 10117	. . . . . . . . . . . . . . . . . . 19 |- ( ( N e. RR /\ ( x ^ 2 ) e. RR ) -> ( N < ( x ^ 2 ) <-> -. ( x ^ 2 ) <_ N ) )
57	16, 6, 56	sylancr 695	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( ZZ>= ` ; 2 9 ) -> ( N < ( x ^ 2 ) <-> -. ( x ^ 2 ) <_ N ) )
58	55, 57	mpbid 222	. . . . . . . . . . . . . . . . 17 |- ( x e. ( ZZ>= ` ; 2 9 ) -> -. ( x ^ 2 ) <_ N )
59	58	pm2.21d 118	. . . . . . . . . . . . . . . 16 |- ( x e. ( ZZ>= ` ; 2 9 ) -> ( ( x ^ 2 ) <_ N -> -. x || N ) )
60	59	adantld 483	. . . . . . . . . . . . . . 15 |- ( x e. ( ZZ>= ` ; 2 9 ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
61	60	adantl 482	. . . . . . . . . . . . . 14 |- ( ( -. 2 || ; 2 9 /\ x e. ( ZZ>= ` ; 2 9 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
62		9nn 11192	. . . . . . . . . . . . . . . 16 |- 9 e. NN
63		3nn 11186	. . . . . . . . . . . . . . . 16 |- 3 e. NN
64		1lt9 11229	. . . . . . . . . . . . . . . 16 |- 1 < 9
65		1lt3 11196	. . . . . . . . . . . . . . . 16 |- 1 < 3
66		9t3e27 11664	. . . . . . . . . . . . . . . 16 |- ( 9 x. 3 ) = ; 2 7
67	62, 63, 64, 65, 66	nprmi 15402	. . . . . . . . . . . . . . 15 |- -. ; 2 7 e. Prime
68	67	pm2.21i 116	. . . . . . . . . . . . . 14 |- (; 2 7 e. Prime -> -. ; 2 7 || N )
69		7nn0 11314	. . . . . . . . . . . . . . 15 |- 7 e. NN0
70		eqid 2622	. . . . . . . . . . . . . . 15 |- ; 2 7 = ; 2 7
71		7p2e9 11172	. . . . . . . . . . . . . . 15 |- ( 7 + 2 ) = 9
72	8, 69, 8, 70, 71	decaddi 11579	. . . . . . . . . . . . . 14 |- (; 2 7 + 2 ) = ; 2 9
73	61, 68, 72	prmlem0 15812	. . . . . . . . . . . . 13 |- ( ( -. 2 || ; 2 7 /\ x e. ( ZZ>= ` ; 2 7 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
74		5nn 11188	. . . . . . . . . . . . . . 15 |- 5 e. NN
75		1lt5 11203	. . . . . . . . . . . . . . 15 |- 1 < 5
76		5t5e25 11639	. . . . . . . . . . . . . . 15 |- ( 5 x. 5 ) = ; 2 5
77	74, 74, 75, 75, 76	nprmi 15402	. . . . . . . . . . . . . 14 |- -. ; 2 5 e. Prime
78	77	pm2.21i 116	. . . . . . . . . . . . 13 |- (; 2 5 e. Prime -> -. ; 2 5 || N )
79		eqid 2622	. . . . . . . . . . . . . 14 |- ; 2 5 = ; 2 5
80	8, 25, 8, 79, 36	decaddi 11579	. . . . . . . . . . . . 13 |- (; 2 5 + 2 ) = ; 2 7
81	73, 78, 80	prmlem0 15812	. . . . . . . . . . . 12 |- ( ( -. 2 || ; 2 5 /\ x e. ( ZZ>= ` ; 2 5 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
82		prmlem2.23	. . . . . . . . . . . . 13 |- -. ; 2 3 || N
83	82	a1i 11	. . . . . . . . . . . 12 |- (; 2 3 e. Prime -> -. ; 2 3 || N )
84		3nn0 11310	. . . . . . . . . . . . 13 |- 3 e. NN0
85		eqid 2622	. . . . . . . . . . . . 13 |- ; 2 3 = ; 2 3
86		3p2e5 11160	. . . . . . . . . . . . 13 |- ( 3 + 2 ) = 5
87	8, 84, 8, 85, 86	decaddi 11579	. . . . . . . . . . . 12 |- (; 2 3 + 2 ) = ; 2 5
88	81, 83, 87	prmlem0 15812	. . . . . . . . . . 11 |- ( ( -. 2 || ; 2 3 /\ x e. ( ZZ>= ` ; 2 3 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
89		7nn 11190	. . . . . . . . . . . . 13 |- 7 e. NN
90		1lt7 11214	. . . . . . . . . . . . 13 |- 1 < 7
91		7t3e21 11649	. . . . . . . . . . . . 13 |- ( 7 x. 3 ) = ; 2 1
92	89, 63, 90, 65, 91	nprmi 15402	. . . . . . . . . . . 12 |- -. ; 2 1 e. Prime
93	92	pm2.21i 116	. . . . . . . . . . 11 |- (; 2 1 e. Prime -> -. ; 2 1 || N )
94		eqid 2622	. . . . . . . . . . . 12 |- ; 2 1 = ; 2 1
95		1p2e3 11152	. . . . . . . . . . . 12 |- ( 1 + 2 ) = 3
96	8, 22, 8, 94, 95	decaddi 11579	. . . . . . . . . . 11 |- (; 2 1 + 2 ) = ; 2 3
97	88, 93, 96	prmlem0 15812	. . . . . . . . . 10 |- ( ( -. 2 || ; 2 1 /\ x e. ( ZZ>= ` ; 2 1 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
98		prmlem2.19	. . . . . . . . . . 11 |- -. ; 1 9 || N
99	98	a1i 11	. . . . . . . . . 10 |- (; 1 9 e. Prime -> -. ; 1 9 || N )
100		eqid 2622	. . . . . . . . . . 11 |- ; 1 9 = ; 1 9
101		9p2e11 11619	. . . . . . . . . . 11 |- ( 9 + 2 ) = ; 1 1
102	22, 9, 8, 100, 44, 22, 101	decaddci 11580	. . . . . . . . . 10 |- (; 1 9 + 2 ) = ; 2 1
103	97, 99, 102	prmlem0 15812	. . . . . . . . 9 |- ( ( -. 2 || ; 1 9 /\ x e. ( ZZ>= ` ; 1 9 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
104		prmlem2.17	. . . . . . . . . 10 |- -. ; 1 7 || N
105	104	a1i 11	. . . . . . . . 9 |- (; 1 7 e. Prime -> -. ; 1 7 || N )
106		eqid 2622	. . . . . . . . . 10 |- ; 1 7 = ; 1 7
107	22, 69, 8, 106, 71	decaddi 11579	. . . . . . . . 9 |- (; 1 7 + 2 ) = ; 1 9
108	103, 105, 107	prmlem0 15812	. . . . . . . 8 |- ( ( -. 2 || ; 1 7 /\ x e. ( ZZ>= ` ; 1 7 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
109		5t3e15 11635	. . . . . . . . . 10 |- ( 5 x. 3 ) = ; 1 5
110	74, 63, 75, 65, 109	nprmi 15402	. . . . . . . . 9 |- -. ; 1 5 e. Prime
111	110	pm2.21i 116	. . . . . . . 8 |- (; 1 5 e. Prime -> -. ; 1 5 || N )
112		eqid 2622	. . . . . . . . 9 |- ; 1 5 = ; 1 5
113	22, 25, 8, 112, 36	decaddi 11579	. . . . . . . 8 |- (; 1 5 + 2 ) = ; 1 7
114	108, 111, 113	prmlem0 15812	. . . . . . 7 |- ( ( -. 2 || ; 1 5 /\ x e. ( ZZ>= ` ; 1 5 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
115		prmlem2.13	. . . . . . . 8 |- -. ; 1 3 || N
116	115	a1i 11	. . . . . . 7 |- (; 1 3 e. Prime -> -. ; 1 3 || N )
117		eqid 2622	. . . . . . . 8 |- ; 1 3 = ; 1 3
118	22, 84, 8, 117, 86	decaddi 11579	. . . . . . 7 |- (; 1 3 + 2 ) = ; 1 5
119	114, 116, 118	prmlem0 15812	. . . . . 6 |- ( ( -. 2 || ; 1 3 /\ x e. ( ZZ>= ` ; 1 3 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
120		prmlem2.11	. . . . . . 7 |- -. ; 1 1 || N
121	120	a1i 11	. . . . . 6 |- (; 1 1 e. Prime -> -. ; 1 1 || N )
122		eqid 2622	. . . . . . 7 |- ; 1 1 = ; 1 1
123	22, 22, 8, 122, 95	decaddi 11579	. . . . . 6 |- (; 1 1 + 2 ) = ; 1 3
124	119, 121, 123	prmlem0 15812	. . . . 5 |- ( ( -. 2 || ; 1 1 /\ x e. ( ZZ>= ` ; 1 1 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
125		9nprm 15819	. . . . . 6 |- -. 9 e. Prime
126	125	pm2.21i 116	. . . . 5 |- ( 9 e. Prime -> -. 9 || N )
127	124, 126, 101	prmlem0 15812	. . . 4 |- ( ( -. 2 || 9 /\ x e. ( ZZ>= ` 9 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
128		prmlem2.7	. . . . 5 |- -. 7 || N
129	128	a1i 11	. . . 4 |- ( 7 e. Prime -> -. 7 || N )
130	127, 129, 71	prmlem0 15812	. . 3 |- ( ( -. 2 || 7 /\ x e. ( ZZ>= ` 7 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
131		prmlem2.5	. . . 4 |- -. 5 || N
132	131	a1i 11	. . 3 |- ( 5 e. Prime -> -. 5 || N )
133	130, 132, 36	prmlem0 15812	. 2 |- ( ( -. 2 || 5 /\ x e. ( ZZ>= ` 5 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
134	1, 2, 3, 4, 133	prmlem1a 15813	1 |- N e. Prime

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   e. wcel 1990   \ cdif 3571   {csn 4177   class class class wbr 4653   ` cfv 5888  (class class class)co 6650   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   < clt 10074   <_ cle 10075   NNcn 11020   2c2 11070   3c3 11071   4c4 11072   5c5 11073   6c6 11074   7c7 11075   8c8 11076   9c9 11077  ;cdc 11493   ZZ>=cuz 11687   ^cexp 12860   || cdvds 14983   Primecprime 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-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  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-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-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-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-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-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  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-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-rp 11833  df-fz 12327  df-seq 12802  df-exp 12861  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-dvds 14984  df-prm 15386

This theorem is referenced by:  37prm  15828  43prm  15829  83prm  15830  139prm  15831  163prm  15832  317prm  15833  631prm  15834  257prm  41473  139prmALT  41511  127prm  41515