Theorem 31prm 48205

Description: 31 is a prime number. In contrast to 37prm 17169, the proof of this theorem is not based on the "blanket" prmlem2 17168, but on isprm7 16755. Although the checks for non-divisibility by the primes 7 to 23 are not needed, the proof is much longer (regarding size) than the proof of 37prm 17169 (1810 characters compared with 1213 for 37prm 17169). The number of essential steps, however, is much smaller (138 compared with 213 for 37prm 17169). (Contributed by AV, 17-Aug-2021.) (Proof modification is discouraged.)

Assertion

Ref	Expression
31prm	⊢ ;31 ∈ ℙ

Proof of Theorem 31prm

Step	Hyp	Ref	Expression
1		2z 12614	. . 3 ⊢ 2 ∈ ℤ
2		3nn0 12510	. . . . 5 ⊢ 3 ∈ ℕ0
3		1nn0 12508	. . . . 5 ⊢ 1 ∈ ℕ0
4	2, 3	deccl 12714	. . . 4 ⊢ ;31 ∈ ℕ0
5	4	nn0zi 12607	. . 3 ⊢ ;31 ∈ ℤ
6		3nn 12308	. . . 4 ⊢ 3 ∈ ℕ
7		2nn0 12509	. . . 4 ⊢ 2 ∈ ℕ0
8		2re 12303	. . . . 5 ⊢ 2 ∈ ℝ
9		9re 12328	. . . . 5 ⊢ 9 ∈ ℝ
10		2lt9 12436	. . . . 5 ⊢ 2 < 9
11	8, 9, 10	ltleii 11321	. . . 4 ⊢ 2 ≤ 9
12	6, 3, 7, 11	declei 12740	. . 3 ⊢ 2 ≤ ;31
13		eluz2 12856	. . 3 ⊢ (;31 ∈ (ℤ≥‘2) ↔ (2 ∈ ℤ ∧ ;31 ∈ ℤ ∧ 2 ≤ ;31))
14	1, 5, 12, 13	mpbir3an 1358	. 2 ⊢ ;31 ∈ (ℤ≥‘2)
15		elun 4109	. . . . . 6 ⊢ (𝑛 ∈ (({2, 3} ∩ ℙ) ∪ ({4, 5} ∩ ℙ)) ↔ (𝑛 ∈ ({2, 3} ∩ ℙ) ∨ 𝑛 ∈ ({4, 5} ∩ ℙ)))
16		elin 3923	. . . . . . . 8 ⊢ (𝑛 ∈ ({2, 3} ∩ ℙ) ↔ (𝑛 ∈ {2, 3} ∧ 𝑛 ∈ ℙ))
17		vex 3461	. . . . . . . . . . 11 ⊢ 𝑛 ∈ V
18	17	elpr 4610	. . . . . . . . . 10 ⊢ (𝑛 ∈ {2, 3} ↔ (𝑛 = 2 ∨ 𝑛 = 3))
19		0nn0 12507	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
20		2cn 12304	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℂ
21	20	mul02i 11387	. . . . . . . . . . . . 13 ⊢ (0 · 2) = 0
22		1e0p1 12746	. . . . . . . . . . . . 13 ⊢ 1 = (0 + 1)
23	2, 19, 21, 22	dec2dvds 17111	. . . . . . . . . . . 12 ⊢ ¬ 2 ∥ ;31
24		breq1 5107	. . . . . . . . . . . 12 ⊢ (𝑛 = 2 → (𝑛 ∥ ;31 ↔ 2 ∥ ;31))
25	23, 24	mtbiri 330	. . . . . . . . . . 11 ⊢ (𝑛 = 2 → ¬ 𝑛 ∥ ;31)
26		3ndvds4 48203	. . . . . . . . . . . . 13 ⊢ ¬ 3 ∥ 4
27	2, 3	3dvdsdec 16378	. . . . . . . . . . . . . 14 ⊢ (3 ∥ ;31 ↔ 3 ∥ (3 + 1))
28		3p1e4 12373	. . . . . . . . . . . . . . 15 ⊢ (3 + 1) = 4
29	28	breq2i 5112	. . . . . . . . . . . . . 14 ⊢ (3 ∥ (3 + 1) ↔ 3 ∥ 4)
30	27, 29	bitri 278	. . . . . . . . . . . . 13 ⊢ (3 ∥ ;31 ↔ 3 ∥ 4)
31	26, 30	mtbir 326	. . . . . . . . . . . 12 ⊢ ¬ 3 ∥ ;31
32		breq1 5107	. . . . . . . . . . . 12 ⊢ (𝑛 = 3 → (𝑛 ∥ ;31 ↔ 3 ∥ ;31))
33	31, 32	mtbiri 330	. . . . . . . . . . 11 ⊢ (𝑛 = 3 → ¬ 𝑛 ∥ ;31)
34	25, 33	jaoi 870	. . . . . . . . . 10 ⊢ ((𝑛 = 2 ∨ 𝑛 = 3) → ¬ 𝑛 ∥ ;31)
35	18, 34	sylbi 220	. . . . . . . . 9 ⊢ (𝑛 ∈ {2, 3} → ¬ 𝑛 ∥ ;31)
36	35	adantr 485	. . . . . . . 8 ⊢ ((𝑛 ∈ {2, 3} ∧ 𝑛 ∈ ℙ) → ¬ 𝑛 ∥ ;31)
37	16, 36	sylbi 220	. . . . . . 7 ⊢ (𝑛 ∈ ({2, 3} ∩ ℙ) → ¬ 𝑛 ∥ ;31)
38		elin 3923	. . . . . . . 8 ⊢ (𝑛 ∈ ({4, 5} ∩ ℙ) ↔ (𝑛 ∈ {4, 5} ∧ 𝑛 ∈ ℙ))
39	17	elpr 4610	. . . . . . . . . 10 ⊢ (𝑛 ∈ {4, 5} ↔ (𝑛 = 4 ∨ 𝑛 = 5))
40		eleq1 2853	. . . . . . . . . . . 12 ⊢ (𝑛 = 4 → (𝑛 ∈ ℙ ↔ 4 ∈ ℙ))
41		4nprm 16741	. . . . . . . . . . . . 13 ⊢ ¬ 4 ∈ ℙ
42	41	pm2.21i 120	. . . . . . . . . . . 12 ⊢ (4 ∈ ℙ → ¬ 𝑛 ∥ ;31)
43	40, 42	biimtrdi 256	. . . . . . . . . . 11 ⊢ (𝑛 = 4 → (𝑛 ∈ ℙ → ¬ 𝑛 ∥ ;31))
44		1nn 12232	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ
45		1lt5 12411	. . . . . . . . . . . . . 14 ⊢ 1 < 5
46	2, 44, 45	dec5dvds 17112	. . . . . . . . . . . . 13 ⊢ ¬ 5 ∥ ;31
47		breq1 5107	. . . . . . . . . . . . 13 ⊢ (𝑛 = 5 → (𝑛 ∥ ;31 ↔ 5 ∥ ;31))
48	46, 47	mtbiri 330	. . . . . . . . . . . 12 ⊢ (𝑛 = 5 → ¬ 𝑛 ∥ ;31)
49	48	a1d 26	. . . . . . . . . . 11 ⊢ (𝑛 = 5 → (𝑛 ∈ ℙ → ¬ 𝑛 ∥ ;31))
50	43, 49	jaoi 870	. . . . . . . . . 10 ⊢ ((𝑛 = 4 ∨ 𝑛 = 5) → (𝑛 ∈ ℙ → ¬ 𝑛 ∥ ;31))
51	39, 50	sylbi 220	. . . . . . . . 9 ⊢ (𝑛 ∈ {4, 5} → (𝑛 ∈ ℙ → ¬ 𝑛 ∥ ;31))
52	51	imp 411	. . . . . . . 8 ⊢ ((𝑛 ∈ {4, 5} ∧ 𝑛 ∈ ℙ) → ¬ 𝑛 ∥ ;31)
53	38, 52	sylbi 220	. . . . . . 7 ⊢ (𝑛 ∈ ({4, 5} ∩ ℙ) → ¬ 𝑛 ∥ ;31)
54	37, 53	jaoi 870	. . . . . 6 ⊢ ((𝑛 ∈ ({2, 3} ∩ ℙ) ∨ 𝑛 ∈ ({4, 5} ∩ ℙ)) → ¬ 𝑛 ∥ ;31)
55	15, 54	sylbi 220	. . . . 5 ⊢ (𝑛 ∈ (({2, 3} ∩ ℙ) ∪ ({4, 5} ∩ ℙ)) → ¬ 𝑛 ∥ ;31)
56		indir 4241	. . . . 5 ⊢ (({2, 3} ∪ {4, 5}) ∩ ℙ) = (({2, 3} ∩ ℙ) ∪ ({4, 5} ∩ ℙ))
57	55, 56	eleq2s 2883	. . . 4 ⊢ (𝑛 ∈ (({2, 3} ∪ {4, 5}) ∩ ℙ) → ¬ 𝑛 ∥ ;31)
58		5nn0 12512	. . . . . . . . 9 ⊢ 5 ∈ ℕ0
59		5re 12316	. . . . . . . . . 10 ⊢ 5 ∈ ℝ
60		5lt9 12433	. . . . . . . . . 10 ⊢ 5 < 9
61	59, 9, 60	ltleii 11321	. . . . . . . . 9 ⊢ 5 ≤ 9
62		2lt3 12402	. . . . . . . . 9 ⊢ 2 < 3
63	7, 2, 58, 3, 61, 62	decleh 12739	. . . . . . . 8 ⊢ ;25 ≤ ;31
64		6nn 12318	. . . . . . . . 9 ⊢ 6 ∈ ℕ
65		1lt6 12416	. . . . . . . . 9 ⊢ 1 < 6
66	2, 3, 64, 65	declt 12732	. . . . . . . 8 ⊢ ;31 < ;36
67	4	nn0rei 12503	. . . . . . . . . 10 ⊢ ;31 ∈ ℝ
68		0re 11198	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
69		9pos 12345	. . . . . . . . . . . 12 ⊢ 0 < 9
70	68, 9, 69	ltleii 11321	. . . . . . . . . . 11 ⊢ 0 ≤ 9
71	6, 3, 19, 70	declei 12740	. . . . . . . . . 10 ⊢ 0 ≤ ;31
72	67, 71	pm3.2i 475	. . . . . . . . 9 ⊢ (;31 ∈ ℝ ∧ 0 ≤ ;31)
73		flsqrt5 48202	. . . . . . . . . 10 ⊢ ((;31 ∈ ℝ ∧ 0 ≤ ;31) → ((;25 ≤ ;31 ∧ ;31 < ;36) ↔ (⌊‘(√‘;31)) = 5))
74	73	bicomd 226	. . . . . . . . 9 ⊢ ((;31 ∈ ℝ ∧ 0 ≤ ;31) → ((⌊‘(√‘;31)) = 5 ↔ (;25 ≤ ;31 ∧ ;31 < ;36)))
75	72, 74	ax-mp 5	. . . . . . . 8 ⊢ ((⌊‘(√‘;31)) = 5 ↔ (;25 ≤ ;31 ∧ ;31 < ;36))
76	63, 66, 75	mpbir2an 723	. . . . . . 7 ⊢ (⌊‘(√‘;31)) = 5
77	76	oveq2i 7411	. . . . . 6 ⊢ (2...(⌊‘(√‘;31))) = (2...5)
78		5nn 12315	. . . . . . . . . 10 ⊢ 5 ∈ ℕ
79	78	nnzi 12606	. . . . . . . . 9 ⊢ 5 ∈ ℤ
80		3z 12615	. . . . . . . . 9 ⊢ 3 ∈ ℤ
81	1, 79, 80	3pm3.2i 1356	. . . . . . . 8 ⊢ (2 ∈ ℤ ∧ 5 ∈ ℤ ∧ 3 ∈ ℤ)
82		3re 12309	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
83	8, 82, 62	ltleii 11321	. . . . . . . . 9 ⊢ 2 ≤ 3
84		3lt5 12409	. . . . . . . . . 10 ⊢ 3 < 5
85	82, 59, 84	ltleii 11321	. . . . . . . . 9 ⊢ 3 ≤ 5
86	83, 85	pm3.2i 475	. . . . . . . 8 ⊢ (2 ≤ 3 ∧ 3 ≤ 5)
87		elfz2 13530	. . . . . . . 8 ⊢ (3 ∈ (2...5) ↔ ((2 ∈ ℤ ∧ 5 ∈ ℤ ∧ 3 ∈ ℤ) ∧ (2 ≤ 3 ∧ 3 ≤ 5)))
88	81, 86, 87	mpbir2an 723	. . . . . . 7 ⊢ 3 ∈ (2...5)
89		fzsplit 13566	. . . . . . 7 ⊢ (3 ∈ (2...5) → (2...5) = ((2...3) ∪ ((3 + 1)...5)))
90	88, 89	ax-mp 5	. . . . . 6 ⊢ (2...5) = ((2...3) ∪ ((3 + 1)...5))
91		df-3 12292	. . . . . . . . 9 ⊢ 3 = (2 + 1)
92	91	oveq2i 7411	. . . . . . . 8 ⊢ (2...3) = (2...(2 + 1))
93		fzpr 13595	. . . . . . . . 9 ⊢ (2 ∈ ℤ → (2...(2 + 1)) = {2, (2 + 1)})
94	1, 93	ax-mp 5	. . . . . . . 8 ⊢ (2...(2 + 1)) = {2, (2 + 1)}
95		2p1e3 12370	. . . . . . . . 9 ⊢ (2 + 1) = 3
96	95	preq2i 4699	. . . . . . . 8 ⊢ {2, (2 + 1)} = {2, 3}
97	92, 94, 96	3eqtri 2792	. . . . . . 7 ⊢ (2...3) = {2, 3}
98	28	oveq1i 7410	. . . . . . . 8 ⊢ ((3 + 1)...5) = (4...5)
99		df-5 12294	. . . . . . . . 9 ⊢ 5 = (4 + 1)
100	99	oveq2i 7411	. . . . . . . 8 ⊢ (4...5) = (4...(4 + 1))
101		4z 12616	. . . . . . . . . 10 ⊢ 4 ∈ ℤ
102		fzpr 13595	. . . . . . . . . 10 ⊢ (4 ∈ ℤ → (4...(4 + 1)) = {4, (4 + 1)})
103	101, 102	ax-mp 5	. . . . . . . . 9 ⊢ (4...(4 + 1)) = {4, (4 + 1)}
104		4p1e5 12374	. . . . . . . . . 10 ⊢ (4 + 1) = 5
105	104	preq2i 4699	. . . . . . . . 9 ⊢ {4, (4 + 1)} = {4, 5}
106	103, 105	eqtri 2788	. . . . . . . 8 ⊢ (4...(4 + 1)) = {4, 5}
107	98, 100, 106	3eqtri 2792	. . . . . . 7 ⊢ ((3 + 1)...5) = {4, 5}
108	97, 107	uneq12i 4122	. . . . . 6 ⊢ ((2...3) ∪ ((3 + 1)...5)) = ({2, 3} ∪ {4, 5})
109	77, 90, 108	3eqtri 2792	. . . . 5 ⊢ (2...(⌊‘(√‘;31))) = ({2, 3} ∪ {4, 5})
110	109	ineq1i 4171	. . . 4 ⊢ ((2...(⌊‘(√‘;31))) ∩ ℙ) = (({2, 3} ∪ {4, 5}) ∩ ℙ)
111	57, 110	eleq2s 2883	. . 3 ⊢ (𝑛 ∈ ((2...(⌊‘(√‘;31))) ∩ ℙ) → ¬ 𝑛 ∥ ;31)
112	111	rgen 3081	. 2 ⊢ ∀𝑛 ∈ ((2...(⌊‘(√‘;31))) ∩ ℙ) ¬ 𝑛 ∥ ;31
113		isprm7 16755	. 2 ⊢ (;31 ∈ ℙ ↔ (;31 ∈ (ℤ≥‘2) ∧ ∀𝑛 ∈ ((2...(⌊‘(√‘;31))) ∩ ℙ) ¬ 𝑛 ∥ ;31))
114	14, 112, 113	mpbir2an 723	1 ⊢ ;31 ∈ ℙ

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145  ∀wral 3079   ∪ cun 3905   ∩ cin 3906  {cpr 4587   class class class wbr 5104  ‘cfv 6525  (class class class)co 7400  ℝcr 11087  0cc0 11088  1c1 11089   + caddc 11091   < clt 11231   ≤ cle 11232  2c2 12283  3c3 12284  4c4 12285  5c5 12286  6c6 12287  9c9 12290  ℤcz 12579  ;cdc 12699  ℤ_≥cuz 12850  ...cfz 13523  ⌊cfl 13811  √csqrt 15272   ∥ cdvds 16298  ℙcprime 16717

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pow 5326  ax-pr 5394  ax-un 7722  ax-cnex 11144  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164  ax-pre-mulgt0 11165  ax-pre-sup 11166

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3370  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5105  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6291  df-ord 6352  df-on 6353  df-lim 6354  df-suc 6355  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-om 7851  df-1st 7974  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-1o 8441  df-2o 8442  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-fin 8935  df-sup 9390  df-inf 9391  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-sub 11431  df-neg 11432  df-div 11860  df-nn 12222  df-2 12291  df-3 12292  df-4 12293  df-5 12294  df-6 12295  df-7 12296  df-8 12297  df-9 12298  df-n0 12493  df-z 12580  df-dec 12700  df-uz 12851  df-rp 13005  df-fz 13524  df-fl 13813  df-seq 14026  df-exp 14086  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-dvds 16299  df-prm 16718

This theorem is referenced by:  m5prm  48206