Theorem prmlem2 13257

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 to cover the numbers less than 5↑2 = 25. 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 29↑2 = 841, 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 13270).

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	⊢ 𝑁 ∈ ℕ
prmlem2.lt	⊢ 𝑁 < ;;841
prmlem2.gt	⊢ 1 < 𝑁
prmlem2.2	⊢ ¬ 2 ∥ 𝑁
prmlem2.3	⊢ ¬ 3 ∥ 𝑁
prmlem2.5	⊢ ¬ 5 ∥ 𝑁
prmlem2.7	⊢ ¬ 7 ∥ 𝑁
prmlem2.11	⊢ ¬ ;11 ∥ 𝑁
prmlem2.13	⊢ ¬ ;13 ∥ 𝑁
prmlem2.17	⊢ ¬ ;17 ∥ 𝑁
prmlem2.19	⊢ ¬ ;19 ∥ 𝑁
prmlem2.23	⊢ ¬ ;23 ∥ 𝑁

Assertion

Ref	Expression
prmlem2	⊢ 𝑁 ∈ ℙ

Proof of Theorem prmlem2

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		prmlem2.n	. 2 ⊢ 𝑁 ∈ ℕ
2		prmlem2.gt	. 2 ⊢ 1 < 𝑁
3		prmlem2.2	. 2 ⊢ ¬ 2 ∥ 𝑁
4		prmlem2.3	. 2 ⊢ ¬ 3 ∥ 𝑁
5		eluzelre 9942	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (ℤ≥‘;29) → 𝑥 ∈ ℝ)
6	5	resqcld 11152	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (ℤ≥‘;29) → (𝑥↑2) ∈ ℝ)
7		eluzle 9944	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (ℤ≥‘;29) → ;29 ≤ 𝑥)
8		2nn0 9585	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℕ0
9		9nn0 9592	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 9 ∈ ℕ0
10	8, 9	deccl 9796	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ;29 ∈ ℕ0
11	10	nn0rei 9579	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ;29 ∈ ℝ
12	10	nn0ge0i 9595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ≤ ;29
13		le2sq2 11067	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((;29 ∈ ℝ ∧ 0 ≤ ;29) ∧ (𝑥 ∈ ℝ ∧ ;29 ≤ 𝑥)) → (;29↑2) ≤ (𝑥↑2))
14	11, 12, 13	mpanl12 440	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℝ ∧ ;29 ≤ 𝑥) → (;29↑2) ≤ (𝑥↑2))
15	5, 7, 14	syl2anc 415	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (ℤ≥‘;29) → (;29↑2) ≤ (𝑥↑2))
16	1	nnrei 9316	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑁 ∈ ℝ
17	11	resqcli 11076	. . . . . . . . . . . . . . . . . . . 20 ⊢ (;29↑2) ∈ ℝ
18		prmlem2.lt	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑁 < ;;841
19	10	nn0cni 9580	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ;29 ∈ ℂ
20	19	sqvali 11071	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (;29↑2) = (;29 · ;29)
21		eqid 2238	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ;29 = ;29
22		1nn0 9584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℕ0
23		6nn0 9589	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 6 ∈ ℕ0
24	8, 23	deccl 9796	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ;26 ∈ ℕ0
25		5nn0 9588	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 5 ∈ ℕ0
26		8nn0 9591	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 8 ∈ ℕ0
27	19	2timesi 9437	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (2 · ;29) = (;29 + ;29)
28		2p2e4 9434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (2 + 2) = 4
29	28	oveq1i 6095	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((2 + 2) + 1) = (4 + 1)
30		4p1e5 9444	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (4 + 1) = 5
31	29, 30	eqtri 2259	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((2 + 2) + 1) = 5
32		9p9e18 9880	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (9 + 9) = ;18
33	8, 9, 8, 9, 21, 21, 31, 26, 32	decaddc 9841	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (;29 + ;29) = ;58
34	27, 33	eqtri 2259	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2 · ;29) = ;58
35		eqid 2238	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ;26 = ;26
36		5p2e7 9454	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (5 + 2) = 7
37	36	oveq1i 6095	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((5 + 2) + 1) = (7 + 1)
38		7p1e8 9447	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (7 + 1) = 8
39	37, 38	eqtri 2259	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((5 + 2) + 1) = 8
40		4nn0 9587	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 4 ∈ ℕ0
41		8p6e14 9870	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (8 + 6) = ;14
42	25, 26, 8, 23, 34, 35, 39, 40, 41	decaddc 9841	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2 · ;29) + ;26) = ;84
43		9t2e18 9908	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (9 · 2) = ;18
44		1p1e2 9424	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (1 + 1) = 2
45		8p8e16 9872	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (8 + 8) = ;16
46	22, 26, 26, 43, 44, 23, 45	decaddci 9847	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((9 · 2) + 8) = ;26
47		9t9e81 9915	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (9 · 9) = ;81
48	9, 8, 9, 21, 22, 26, 46, 47	decmul2c 9852	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (9 · ;29) = ;;261
49	10, 8, 9, 21, 22, 24, 42, 48	decmul1c 9851	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (;29 · ;29) = ;;841
50	20, 49	eqtri 2259	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (;29↑2) = ;;841
51	18, 50	breqtrri 4157	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑁 < (;29↑2)
52		ltletr 8416	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℝ ∧ (;29↑2) ∈ ℝ ∧ (𝑥↑2) ∈ ℝ) → ((𝑁 < (;29↑2) ∧ (;29↑2) ≤ (𝑥↑2)) → 𝑁 < (𝑥↑2)))
53	51, 52	mpani 434	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℝ ∧ (;29↑2) ∈ ℝ ∧ (𝑥↑2) ∈ ℝ) → ((;29↑2) ≤ (𝑥↑2) → 𝑁 < (𝑥↑2)))
54	16, 17, 53	mp3an12 1368	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥↑2) ∈ ℝ → ((;29↑2) ≤ (𝑥↑2) → 𝑁 < (𝑥↑2)))
55	6, 15, 54	sylc 62	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (ℤ≥‘;29) → 𝑁 < (𝑥↑2))
56	1	nnzi 9670	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑁 ∈ ℤ
57		eluzelz 9941	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (ℤ≥‘;29) → 𝑥 ∈ ℤ)
58		zsqcl 11062	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℤ → (𝑥↑2) ∈ ℤ)
59	57, 58	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (ℤ≥‘;29) → (𝑥↑2) ∈ ℤ)
60		zltnle 9695	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ (𝑥↑2) ∈ ℤ) → (𝑁 < (𝑥↑2) ↔ ¬ (𝑥↑2) ≤ 𝑁))
61	56, 59, 60	sylancr 418	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (ℤ≥‘;29) → (𝑁 < (𝑥↑2) ↔ ¬ (𝑥↑2) ≤ 𝑁))
62	55, 61	mpbid 147	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (ℤ≥‘;29) → ¬ (𝑥↑2) ≤ 𝑁)
63	62	pm2.21d 628	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (ℤ≥‘;29) → ((𝑥↑2) ≤ 𝑁 → ¬ 𝑥 ∥ 𝑁))
64	63	adantld 278	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (ℤ≥‘;29) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))
65	64	adantl 277	. . . . . . . . . . . . . 14 ⊢ ((¬ 2 ∥ ;29 ∧ 𝑥 ∈ (ℤ≥‘;29)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))
66		9nn 9478	. . . . . . . . . . . . . . . 16 ⊢ 9 ∈ ℕ
67		3nn 9472	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℕ
68		1lt9 9514	. . . . . . . . . . . . . . . 16 ⊢ 1 < 9
69		1lt3 9481	. . . . . . . . . . . . . . . 16 ⊢ 1 < 3
70		9t3e27 9909	. . . . . . . . . . . . . . . 16 ⊢ (9 · 3) = ;27
71	66, 67, 68, 69, 70	nprmi 12921	. . . . . . . . . . . . . . 15 ⊢ ¬ ;27 ∈ ℙ
72	71	pm2.21i 655	. . . . . . . . . . . . . 14 ⊢ (;27 ∈ ℙ → ¬ ;27 ∥ 𝑁)
73		7nn0 9590	. . . . . . . . . . . . . . 15 ⊢ 7 ∈ ℕ0
74		eqid 2238	. . . . . . . . . . . . . . 15 ⊢ ;27 = ;27
75		7p2e9 9459	. . . . . . . . . . . . . . 15 ⊢ (7 + 2) = 9
76	8, 73, 8, 74, 75	decaddi 9846	. . . . . . . . . . . . . 14 ⊢ (;27 + 2) = ;29
77	65, 72, 76	prmlem0 13243	. . . . . . . . . . . . 13 ⊢ ((¬ 2 ∥ ;27 ∧ 𝑥 ∈ (ℤ≥‘;27)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))
78		5nn 9474	. . . . . . . . . . . . . . 15 ⊢ 5 ∈ ℕ
79		1lt5 9488	. . . . . . . . . . . . . . 15 ⊢ 1 < 5
80		5t5e25 9889	. . . . . . . . . . . . . . 15 ⊢ (5 · 5) = ;25
81	78, 78, 79, 79, 80	nprmi 12921	. . . . . . . . . . . . . 14 ⊢ ¬ ;25 ∈ ℙ
82	81	pm2.21i 655	. . . . . . . . . . . . 13 ⊢ (;25 ∈ ℙ → ¬ ;25 ∥ 𝑁)
83		eqid 2238	. . . . . . . . . . . . . 14 ⊢ ;25 = ;25
84	8, 25, 8, 83, 36	decaddi 9846	. . . . . . . . . . . . 13 ⊢ (;25 + 2) = ;27
85	77, 82, 84	prmlem0 13243	. . . . . . . . . . . 12 ⊢ ((¬ 2 ∥ ;25 ∧ 𝑥 ∈ (ℤ≥‘;25)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))
86		prmlem2.23	. . . . . . . . . . . . 13 ⊢ ¬ ;23 ∥ 𝑁
87	86	a1i 9	. . . . . . . . . . . 12 ⊢ (;23 ∈ ℙ → ¬ ;23 ∥ 𝑁)
88		3nn0 9586	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℕ0
89		eqid 2238	. . . . . . . . . . . . 13 ⊢ ;23 = ;23
90		3p2e5 9449	. . . . . . . . . . . . 13 ⊢ (3 + 2) = 5
91	8, 88, 8, 89, 90	decaddi 9846	. . . . . . . . . . . 12 ⊢ (;23 + 2) = ;25
92	85, 87, 91	prmlem0 13243	. . . . . . . . . . 11 ⊢ ((¬ 2 ∥ ;23 ∧ 𝑥 ∈ (ℤ≥‘;23)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))
93		7nn 9476	. . . . . . . . . . . . 13 ⊢ 7 ∈ ℕ
94		1lt7 9499	. . . . . . . . . . . . 13 ⊢ 1 < 7
95		7t3e21 9896	. . . . . . . . . . . . 13 ⊢ (7 · 3) = ;21
96	93, 67, 94, 69, 95	nprmi 12921	. . . . . . . . . . . 12 ⊢ ¬ ;21 ∈ ℙ
97	96	pm2.21i 655	. . . . . . . . . . 11 ⊢ (;21 ∈ ℙ → ¬ ;21 ∥ 𝑁)
98		eqid 2238	. . . . . . . . . . . 12 ⊢ ;21 = ;21
99		1p2e3 9442	. . . . . . . . . . . 12 ⊢ (1 + 2) = 3
100	8, 22, 8, 98, 99	decaddi 9846	. . . . . . . . . . 11 ⊢ (;21 + 2) = ;23
101	92, 97, 100	prmlem0 13243	. . . . . . . . . 10 ⊢ ((¬ 2 ∥ ;21 ∧ 𝑥 ∈ (ℤ≥‘;21)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))
102		prmlem2.19	. . . . . . . . . . 11 ⊢ ¬ ;19 ∥ 𝑁
103	102	a1i 9	. . . . . . . . . 10 ⊢ (;19 ∈ ℙ → ¬ ;19 ∥ 𝑁)
104		eqid 2238	. . . . . . . . . . 11 ⊢ ;19 = ;19
105		9p2e11 9873	. . . . . . . . . . 11 ⊢ (9 + 2) = ;11
106	22, 9, 8, 104, 44, 22, 105	decaddci 9847	. . . . . . . . . 10 ⊢ (;19 + 2) = ;21
107	101, 103, 106	prmlem0 13243	. . . . . . . . 9 ⊢ ((¬ 2 ∥ ;19 ∧ 𝑥 ∈ (ℤ≥‘;19)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))
108		prmlem2.17	. . . . . . . . . 10 ⊢ ¬ ;17 ∥ 𝑁
109	108	a1i 9	. . . . . . . . 9 ⊢ (;17 ∈ ℙ → ¬ ;17 ∥ 𝑁)
110		eqid 2238	. . . . . . . . . 10 ⊢ ;17 = ;17
111	22, 73, 8, 110, 75	decaddi 9846	. . . . . . . . 9 ⊢ (;17 + 2) = ;19
112	107, 109, 111	prmlem0 13243	. . . . . . . 8 ⊢ ((¬ 2 ∥ ;17 ∧ 𝑥 ∈ (ℤ≥‘;17)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))
113		5t3e15 9887	. . . . . . . . . 10 ⊢ (5 · 3) = ;15
114	78, 67, 79, 69, 113	nprmi 12921	. . . . . . . . 9 ⊢ ¬ ;15 ∈ ℙ
115	114	pm2.21i 655	. . . . . . . 8 ⊢ (;15 ∈ ℙ → ¬ ;15 ∥ 𝑁)
116		eqid 2238	. . . . . . . . 9 ⊢ ;15 = ;15
117	22, 25, 8, 116, 36	decaddi 9846	. . . . . . . 8 ⊢ (;15 + 2) = ;17
118	112, 115, 117	prmlem0 13243	. . . . . . 7 ⊢ ((¬ 2 ∥ ;15 ∧ 𝑥 ∈ (ℤ≥‘;15)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))
119		prmlem2.13	. . . . . . . 8 ⊢ ¬ ;13 ∥ 𝑁
120	119	a1i 9	. . . . . . 7 ⊢ (;13 ∈ ℙ → ¬ ;13 ∥ 𝑁)
121		eqid 2238	. . . . . . . 8 ⊢ ;13 = ;13
122	22, 88, 8, 121, 90	decaddi 9846	. . . . . . 7 ⊢ (;13 + 2) = ;15
123	118, 120, 122	prmlem0 13243	. . . . . 6 ⊢ ((¬ 2 ∥ ;13 ∧ 𝑥 ∈ (ℤ≥‘;13)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))
124		prmlem2.11	. . . . . . 7 ⊢ ¬ ;11 ∥ 𝑁
125	124	a1i 9	. . . . . 6 ⊢ (;11 ∈ ℙ → ¬ ;11 ∥ 𝑁)
126		eqid 2238	. . . . . . 7 ⊢ ;11 = ;11
127	22, 22, 8, 126, 99	decaddi 9846	. . . . . 6 ⊢ (;11 + 2) = ;13
128	123, 125, 127	prmlem0 13243	. . . . 5 ⊢ ((¬ 2 ∥ ;11 ∧ 𝑥 ∈ (ℤ≥‘;11)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))
129		9nprm 13250	. . . . . 6 ⊢ ¬ 9 ∈ ℙ
130	129	pm2.21i 655	. . . . 5 ⊢ (9 ∈ ℙ → ¬ 9 ∥ 𝑁)
131	128, 130, 105	prmlem0 13243	. . . 4 ⊢ ((¬ 2 ∥ 9 ∧ 𝑥 ∈ (ℤ≥‘9)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))
132		prmlem2.7	. . . . 5 ⊢ ¬ 7 ∥ 𝑁
133	132	a1i 9	. . . 4 ⊢ (7 ∈ ℙ → ¬ 7 ∥ 𝑁)
134	131, 133, 75	prmlem0 13243	. . 3 ⊢ ((¬ 2 ∥ 7 ∧ 𝑥 ∈ (ℤ≥‘7)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))
135		prmlem2.5	. . . 4 ⊢ ¬ 5 ∥ 𝑁
136	135	a1i 9	. . 3 ⊢ (5 ∈ ℙ → ¬ 5 ∥ 𝑁)
137	134, 136, 36	prmlem0 13243	. 2 ⊢ ((¬ 2 ∥ 5 ∧ 𝑥 ∈ (ℤ≥‘5)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))
138	1, 2, 3, 4, 137	prmlem1a 13244	1 ⊢ 𝑁 ∈ ℙ

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 1009   ∈ wcel 2209   ∖ cdif 3217  {csn 3709   class class class wbr 4130  ‘cfv 5377  (class class class)co 6085  ℝcr 8179  0cc0 8180  1c1 8181   + caddc 8183   · cmul 8185   < clt 8361   ≤ cle 8362  ℕcn 9307  2c2 9358  3c3 9359  4c4 9360  5c5 9361  6c6 9362  7c7 9363  8c8 9364  9c9 9365  ℤcz 9649  ;cdc 9782  ℤ_≥cuz 9931  ↑cexp 10990   ∥ cdvds 12573  ℙcprime 12904

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4246  ax-sep 4249  ax-nul 4259  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-iinf 4735  ax-cnex 8271  ax-resscn 8272  ax-1cn 8273  ax-1re 8274  ax-icn 8275  ax-addcl 8276  ax-addrcl 8277  ax-mulcl 8278  ax-mulrcl 8279  ax-addcom 8280  ax-mulcom 8281  ax-addass 8282  ax-mulass 8283  ax-distr 8284  ax-i2m1 8285  ax-0lt1 8286  ax-1rid 8287  ax-0id 8288  ax-rnegex 8289  ax-precex 8290  ax-cnre 8291  ax-pre-ltirr 8292  ax-pre-ltwlin 8293  ax-pre-lttrn 8294  ax-pre-apti 8295  ax-pre-ltadd 8296  ax-pre-mulgt0 8297  ax-pre-mulext 8298  ax-arch 8299  ax-caucvg 8300

This proof depends on definitions:  df-bi 117  df-stab 843  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-xor 1425  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rmo 2536  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-if 3639  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-br 4131  df-opab 4193  df-mpt 4194  df-tr 4230  df-id 4438  df-po 4441  df-iso 4442  df-iord 4511  df-on 4513  df-ilim 4514  df-suc 4516  df-iom 4738  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384  df-fv 5385  df-riota 6038  df-ov 6088  df-oprab 6089  df-mpo 6090  df-1st 6374  df-2nd 6375  df-recs 6576  df-frec 6662  df-1o 6687  df-2o 6688  df-er 6807  df-en 7023  df-pnf 8363  df-mnf 8364  df-xr 8365  df-ltxr 8366  df-le 8367  df-sub 8501  df-neg 8502  df-reap 8906  df-ap 8913  df-div 9006  df-inn 9308  df-2 9366  df-3 9367  df-4 9368  df-5 9369  df-6 9370  df-7 9371  df-8 9372  df-9 9373  df-n0 9569  df-z 9650  df-dec 9783  df-uz 9932  df-q 10030  df-rp 10066  df-fz 10423  df-fzo 10561  df-fl 10716  df-mod 10775  df-seqfrec 10900  df-exp 10991  df-cj 11623  df-re 11624  df-im 11625  df-rsqrt 11780  df-abs 11781  df-dvds 12574  df-prm 12905

This theorem is used by:  37prm  13258  43prm  13259  83prm  13260  139prm  13261  163prm  13262  317prm  13263  631prm  13264