Theorem 31prm 48072

Description: 31 is a prime number. In contrast to 37prm 17082, the proof of this theorem is not based on the "blanket" prmlem2 17081, but on isprm7 16669. 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 17082 (1810 characters compared with 1213 for 37prm 17082). The number of essential steps, however, is much smaller (138 compared with 213 for 37prm 17082). (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 12550	. . 3 ⊢ 2 ∈ ℤ
2		3nn0 12446	. . . . 5 ⊢ 3 ∈ ℕ0
3		1nn0 12444	. . . . 5 ⊢ 1 ∈ ℕ0
4	2, 3	deccl 12650	. . . 4 ⊢ ;31 ∈ ℕ0
5	4	nn0zi 12543	. . 3 ⊢ ;31 ∈ ℤ
6		3nn 12251	. . . 4 ⊢ 3 ∈ ℕ
7		2nn0 12445	. . . 4 ⊢ 2 ∈ ℕ0
8		2re 12246	. . . . 5 ⊢ 2 ∈ ℝ
9		9re 12271	. . . . 5 ⊢ 9 ∈ ℝ
10		2lt9 12372	. . . . 5 ⊢ 2 < 9
11	8, 9, 10	ltleii 11260	. . . 4 ⊢ 2 ≤ 9
12	6, 3, 7, 11	declei 12671	. . 3 ⊢ 2 ≤ ;31
13		eluz2 12785	. . 3 ⊢ (;31 ∈ (ℤ≥‘2) ↔ (2 ∈ ℤ ∧ ;31 ∈ ℤ ∧ 2 ≤ ;31))
14	1, 5, 12, 13	mpbir3an 1343	. 2 ⊢ ;31 ∈ (ℤ≥‘2)
15		elun 4094	. . . . . 6 ⊢ (𝑛 ∈ (({2, 3} ∩ ℙ) ∪ ({4, 5} ∩ ℙ)) ↔ (𝑛 ∈ ({2, 3} ∩ ℙ) ∨ 𝑛 ∈ ({4, 5} ∩ ℙ)))
16		elin 3906	. . . . . . . 8 ⊢ (𝑛 ∈ ({2, 3} ∩ ℙ) ↔ (𝑛 ∈ {2, 3} ∧ 𝑛 ∈ ℙ))
17		vex 3434	. . . . . . . . . . 11 ⊢ 𝑛 ∈ V
18	17	elpr 4593	. . . . . . . . . 10 ⊢ (𝑛 ∈ {2, 3} ↔ (𝑛 = 2 ∨ 𝑛 = 3))
19		0nn0 12443	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
20		2cn 12247	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℂ
21	20	mul02i 11326	. . . . . . . . . . . . 13 ⊢ (0 · 2) = 0
22		1e0p1 12677	. . . . . . . . . . . . 13 ⊢ 1 = (0 + 1)
23	2, 19, 21, 22	dec2dvds 17025	. . . . . . . . . . . 12 ⊢ ¬ 2 ∥ ;31
24		breq1 5089	. . . . . . . . . . . 12 ⊢ (𝑛 = 2 → (𝑛 ∥ ;31 ↔ 2 ∥ ;31))
25	23, 24	mtbiri 327	. . . . . . . . . . 11 ⊢ (𝑛 = 2 → ¬ 𝑛 ∥ ;31)
26		3ndvds4 48070	. . . . . . . . . . . . 13 ⊢ ¬ 3 ∥ 4
27	2, 3	3dvdsdec 16292	. . . . . . . . . . . . . 14 ⊢ (3 ∥ ;31 ↔ 3 ∥ (3 + 1))
28		3p1e4 12312	. . . . . . . . . . . . . . 15 ⊢ (3 + 1) = 4
29	28	breq2i 5094	. . . . . . . . . . . . . 14 ⊢ (3 ∥ (3 + 1) ↔ 3 ∥ 4)
30	27, 29	bitri 275	. . . . . . . . . . . . 13 ⊢ (3 ∥ ;31 ↔ 3 ∥ 4)
31	26, 30	mtbir 323	. . . . . . . . . . . 12 ⊢ ¬ 3 ∥ ;31
32		breq1 5089	. . . . . . . . . . . 12 ⊢ (𝑛 = 3 → (𝑛 ∥ ;31 ↔ 3 ∥ ;31))
33	31, 32	mtbiri 327	. . . . . . . . . . 11 ⊢ (𝑛 = 3 → ¬ 𝑛 ∥ ;31)
34	25, 33	jaoi 858	. . . . . . . . . 10 ⊢ ((𝑛 = 2 ∨ 𝑛 = 3) → ¬ 𝑛 ∥ ;31)
35	18, 34	sylbi 217	. . . . . . . . 9 ⊢ (𝑛 ∈ {2, 3} → ¬ 𝑛 ∥ ;31)
36	35	adantr 480	. . . . . . . 8 ⊢ ((𝑛 ∈ {2, 3} ∧ 𝑛 ∈ ℙ) → ¬ 𝑛 ∥ ;31)
37	16, 36	sylbi 217	. . . . . . 7 ⊢ (𝑛 ∈ ({2, 3} ∩ ℙ) → ¬ 𝑛 ∥ ;31)
38		elin 3906	. . . . . . . 8 ⊢ (𝑛 ∈ ({4, 5} ∩ ℙ) ↔ (𝑛 ∈ {4, 5} ∧ 𝑛 ∈ ℙ))
39	17	elpr 4593	. . . . . . . . . 10 ⊢ (𝑛 ∈ {4, 5} ↔ (𝑛 = 4 ∨ 𝑛 = 5))
40		eleq1 2825	. . . . . . . . . . . 12 ⊢ (𝑛 = 4 → (𝑛 ∈ ℙ ↔ 4 ∈ ℙ))
41		4nprm 16655	. . . . . . . . . . . . 13 ⊢ ¬ 4 ∈ ℙ
42	41	pm2.21i 119	. . . . . . . . . . . 12 ⊢ (4 ∈ ℙ → ¬ 𝑛 ∥ ;31)
43	40, 42	biimtrdi 253	. . . . . . . . . . 11 ⊢ (𝑛 = 4 → (𝑛 ∈ ℙ → ¬ 𝑛 ∥ ;31))
44		1nn 12176	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ
45		1lt5 12347	. . . . . . . . . . . . . 14 ⊢ 1 < 5
46	2, 44, 45	dec5dvds 17026	. . . . . . . . . . . . 13 ⊢ ¬ 5 ∥ ;31
47		breq1 5089	. . . . . . . . . . . . 13 ⊢ (𝑛 = 5 → (𝑛 ∥ ;31 ↔ 5 ∥ ;31))
48	46, 47	mtbiri 327	. . . . . . . . . . . 12 ⊢ (𝑛 = 5 → ¬ 𝑛 ∥ ;31)
49	48	a1d 25	. . . . . . . . . . 11 ⊢ (𝑛 = 5 → (𝑛 ∈ ℙ → ¬ 𝑛 ∥ ;31))
50	43, 49	jaoi 858	. . . . . . . . . 10 ⊢ ((𝑛 = 4 ∨ 𝑛 = 5) → (𝑛 ∈ ℙ → ¬ 𝑛 ∥ ;31))
51	39, 50	sylbi 217	. . . . . . . . 9 ⊢ (𝑛 ∈ {4, 5} → (𝑛 ∈ ℙ → ¬ 𝑛 ∥ ;31))
52	51	imp 406	. . . . . . . 8 ⊢ ((𝑛 ∈ {4, 5} ∧ 𝑛 ∈ ℙ) → ¬ 𝑛 ∥ ;31)
53	38, 52	sylbi 217	. . . . . . 7 ⊢ (𝑛 ∈ ({4, 5} ∩ ℙ) → ¬ 𝑛 ∥ ;31)
54	37, 53	jaoi 858	. . . . . 6 ⊢ ((𝑛 ∈ ({2, 3} ∩ ℙ) ∨ 𝑛 ∈ ({4, 5} ∩ ℙ)) → ¬ 𝑛 ∥ ;31)
55	15, 54	sylbi 217	. . . . 5 ⊢ (𝑛 ∈ (({2, 3} ∩ ℙ) ∪ ({4, 5} ∩ ℙ)) → ¬ 𝑛 ∥ ;31)
56		indir 4227	. . . . 5 ⊢ (({2, 3} ∪ {4, 5}) ∩ ℙ) = (({2, 3} ∩ ℙ) ∪ ({4, 5} ∩ ℙ))
57	55, 56	eleq2s 2855	. . . 4 ⊢ (𝑛 ∈ (({2, 3} ∪ {4, 5}) ∩ ℙ) → ¬ 𝑛 ∥ ;31)
58		5nn0 12448	. . . . . . . . 9 ⊢ 5 ∈ ℕ0
59		5re 12259	. . . . . . . . . 10 ⊢ 5 ∈ ℝ
60		5lt9 12369	. . . . . . . . . 10 ⊢ 5 < 9
61	59, 9, 60	ltleii 11260	. . . . . . . . 9 ⊢ 5 ≤ 9
62		2lt3 12339	. . . . . . . . 9 ⊢ 2 < 3
63	7, 2, 58, 3, 61, 62	decleh 12670	. . . . . . . 8 ⊢ ;25 ≤ ;31
64		6nn 12261	. . . . . . . . 9 ⊢ 6 ∈ ℕ
65		1lt6 12352	. . . . . . . . 9 ⊢ 1 < 6
66	2, 3, 64, 65	declt 12663	. . . . . . . 8 ⊢ ;31 < ;36
67	4	nn0rei 12439	. . . . . . . . . 10 ⊢ ;31 ∈ ℝ
68		0re 11137	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
69		9pos 12285	. . . . . . . . . . . 12 ⊢ 0 < 9
70	68, 9, 69	ltleii 11260	. . . . . . . . . . 11 ⊢ 0 ≤ 9
71	6, 3, 19, 70	declei 12671	. . . . . . . . . 10 ⊢ 0 ≤ ;31
72	67, 71	pm3.2i 470	. . . . . . . . 9 ⊢ (;31 ∈ ℝ ∧ 0 ≤ ;31)
73		flsqrt5 48069	. . . . . . . . . 10 ⊢ ((;31 ∈ ℝ ∧ 0 ≤ ;31) → ((;25 ≤ ;31 ∧ ;31 < ;36) ↔ (⌊‘(√‘;31)) = 5))
74	73	bicomd 223	. . . . . . . . 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 712	. . . . . . 7 ⊢ (⌊‘(√‘;31)) = 5
77	76	oveq2i 7371	. . . . . 6 ⊢ (2...(⌊‘(√‘;31))) = (2...5)
78		5nn 12258	. . . . . . . . . 10 ⊢ 5 ∈ ℕ
79	78	nnzi 12542	. . . . . . . . 9 ⊢ 5 ∈ ℤ
80		3z 12551	. . . . . . . . 9 ⊢ 3 ∈ ℤ
81	1, 79, 80	3pm3.2i 1341	. . . . . . . 8 ⊢ (2 ∈ ℤ ∧ 5 ∈ ℤ ∧ 3 ∈ ℤ)
82		3re 12252	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
83	8, 82, 62	ltleii 11260	. . . . . . . . 9 ⊢ 2 ≤ 3
84		3lt5 12345	. . . . . . . . . 10 ⊢ 3 < 5
85	82, 59, 84	ltleii 11260	. . . . . . . . 9 ⊢ 3 ≤ 5
86	83, 85	pm3.2i 470	. . . . . . . 8 ⊢ (2 ≤ 3 ∧ 3 ≤ 5)
87		elfz2 13459	. . . . . . . 8 ⊢ (3 ∈ (2...5) ↔ ((2 ∈ ℤ ∧ 5 ∈ ℤ ∧ 3 ∈ ℤ) ∧ (2 ≤ 3 ∧ 3 ≤ 5)))
88	81, 86, 87	mpbir2an 712	. . . . . . 7 ⊢ 3 ∈ (2...5)
89		fzsplit 13495	. . . . . . 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 12236	. . . . . . . . 9 ⊢ 3 = (2 + 1)
92	91	oveq2i 7371	. . . . . . . 8 ⊢ (2...3) = (2...(2 + 1))
93		fzpr 13524	. . . . . . . . 9 ⊢ (2 ∈ ℤ → (2...(2 + 1)) = {2, (2 + 1)})
94	1, 93	ax-mp 5	. . . . . . . 8 ⊢ (2...(2 + 1)) = {2, (2 + 1)}
95		2p1e3 12309	. . . . . . . . 9 ⊢ (2 + 1) = 3
96	95	preq2i 4682	. . . . . . . 8 ⊢ {2, (2 + 1)} = {2, 3}
97	92, 94, 96	3eqtri 2764	. . . . . . 7 ⊢ (2...3) = {2, 3}
98	28	oveq1i 7370	. . . . . . . 8 ⊢ ((3 + 1)...5) = (4...5)
99		df-5 12238	. . . . . . . . 9 ⊢ 5 = (4 + 1)
100	99	oveq2i 7371	. . . . . . . 8 ⊢ (4...5) = (4...(4 + 1))
101		4z 12552	. . . . . . . . . 10 ⊢ 4 ∈ ℤ
102		fzpr 13524	. . . . . . . . . 10 ⊢ (4 ∈ ℤ → (4...(4 + 1)) = {4, (4 + 1)})
103	101, 102	ax-mp 5	. . . . . . . . 9 ⊢ (4...(4 + 1)) = {4, (4 + 1)}
104		4p1e5 12313	. . . . . . . . . 10 ⊢ (4 + 1) = 5
105	104	preq2i 4682	. . . . . . . . 9 ⊢ {4, (4 + 1)} = {4, 5}
106	103, 105	eqtri 2760	. . . . . . . 8 ⊢ (4...(4 + 1)) = {4, 5}
107	98, 100, 106	3eqtri 2764	. . . . . . 7 ⊢ ((3 + 1)...5) = {4, 5}
108	97, 107	uneq12i 4107	. . . . . 6 ⊢ ((2...3) ∪ ((3 + 1)...5)) = ({2, 3} ∪ {4, 5})
109	77, 90, 108	3eqtri 2764	. . . . 5 ⊢ (2...(⌊‘(√‘;31))) = ({2, 3} ∪ {4, 5})
110	109	ineq1i 4157	. . . 4 ⊢ ((2...(⌊‘(√‘;31))) ∩ ℙ) = (({2, 3} ∪ {4, 5}) ∩ ℙ)
111	57, 110	eleq2s 2855	. . 3 ⊢ (𝑛 ∈ ((2...(⌊‘(√‘;31))) ∩ ℙ) → ¬ 𝑛 ∥ ;31)
112	111	rgen 3054	. 2 ⊢ ∀𝑛 ∈ ((2...(⌊‘(√‘;31))) ∩ ℙ) ¬ 𝑛 ∥ ;31
113		isprm7 16669	. 2 ⊢ (;31 ∈ ℙ ↔ (;31 ∈ (ℤ≥‘2) ∧ ∀𝑛 ∈ ((2...(⌊‘(√‘;31))) ∩ ℙ) ¬ 𝑛 ∥ ;31))
114	14, 112, 113	mpbir2an 712	1 ⊢ ;31 ∈ ℙ

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3052   ∪ cun 3888   ∩ cin 3889  {cpr 4570   class class class wbr 5086  ‘cfv 6492  (class class class)co 7360  ℝcr 11028  0cc0 11029  1c1 11030   + caddc 11032   < clt 11170   ≤ cle 11171  2c2 12227  3c3 12228  4c4 12229  5c5 12230  6c6 12231  9c9 12234  ℤcz 12515  ;cdc 12635  ℤ_≥cuz 12779  ...cfz 13452  ⌊cfl 13740  √csqrt 15186   ∥ cdvds 16212  ℙcprime 16631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106  ax-pre-sup 11107

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-1st 7935  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-1o 8398  df-2o 8399  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-sup 9348  df-inf 9349  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799  df-nn 12166  df-2 12235  df-3 12236  df-4 12237  df-5 12238  df-6 12239  df-7 12240  df-8 12241  df-9 12242  df-n0 12429  df-z 12516  df-dec 12636  df-uz 12780  df-rp 12934  df-fz 13453  df-fl 13742  df-seq 13955  df-exp 14015  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-dvds 16213  df-prm 16632

This theorem is referenced by:  m5prm  48073