Theorem 31prm 48390

Description: 31 is a prime number. In contrast to 37prm 17206, the proof of this theorem is not based on the "blanket" prmlem2 17205, but on isprm7 16792. 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 17206 (1810 characters compared with 1213 for 37prm 17206). The number of essential steps, however, is much smaller (138 compared with 213 for 37prm 17206). (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 12644	. . 3 ⊢ 2 ∈ ℤ
2		3nn0 12540	. . . . 5 ⊢ 3 ∈ ℕ0
3		1nn0 12538	. . . . 5 ⊢ 1 ∈ ℕ0
4	2, 3	deccl 12744	. . . 4 ⊢ ;31 ∈ ℕ0
5	4	nn0zi 12637	. . 3 ⊢ ;31 ∈ ℤ
6		3nn 12338	. . . 4 ⊢ 3 ∈ ℕ
7		2nn0 12539	. . . 4 ⊢ 2 ∈ ℕ0
8		2re 12333	. . . . 5 ⊢ 2 ∈ ℝ
9		9re 12358	. . . . 5 ⊢ 9 ∈ ℝ
10		2lt9 12466	. . . . 5 ⊢ 2 < 9
11	8, 9, 10	ltleii 11351	. . . 4 ⊢ 2 ≤ 9
12	6, 3, 7, 11	declei 12770	. . 3 ⊢ 2 ≤ ;31
13		eluz2 12886	. . 3 ⊢ (;31 ∈ (ℤ≥‘2) ↔ (2 ∈ ℤ ∧ ;31 ∈ ℤ ∧ 2 ≤ ;31))
14	1, 5, 12, 13	mpbir3an 1360	. 2 ⊢ ;31 ∈ (ℤ≥‘2)
15		elun 4110	. . . . . 6 ⊢ (𝑛 ∈ (({2, 3} ∩ ℙ) ∪ ({4, 5} ∩ ℙ)) ↔ (𝑛 ∈ ({2, 3} ∩ ℙ) ∨ 𝑛 ∈ ({4, 5} ∩ ℙ)))
16		elin 3924	. . . . . . . 8 ⊢ (𝑛 ∈ ({2, 3} ∩ ℙ) ↔ (𝑛 ∈ {2, 3} ∧ 𝑛 ∈ ℙ))
17		vex 3462	. . . . . . . . . . 11 ⊢ 𝑛 ∈ V
18	17	elpr 4619	. . . . . . . . . 10 ⊢ (𝑛 ∈ {2, 3} ↔ (𝑛 = 2 ∨ 𝑛 = 3))
19		0nn0 12537	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
20		2cn 12334	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℂ
21	20	mul02i 11417	. . . . . . . . . . . . 13 ⊢ (0 · 2) = 0
22		1e0p1 12776	. . . . . . . . . . . . 13 ⊢ 1 = (0 + 1)
23	2, 19, 21, 22	dec2dvds 17148	. . . . . . . . . . . 12 ⊢ ¬ 2 ∥ ;31
24		breq1 5117	. . . . . . . . . . . 12 ⊢ (𝑛 = 2 → (𝑛 ∥ ;31 ↔ 2 ∥ ;31))
25	23, 24	mtbiri 330	. . . . . . . . . . 11 ⊢ (𝑛 = 2 → ¬ 𝑛 ∥ ;31)
26		3ndvds4 48388	. . . . . . . . . . . . 13 ⊢ ¬ 3 ∥ 4
27	2, 3	3dvdsdec 16415	. . . . . . . . . . . . . 14 ⊢ (3 ∥ ;31 ↔ 3 ∥ (3 + 1))
28		3p1e4 12403	. . . . . . . . . . . . . . 15 ⊢ (3 + 1) = 4
29	28	breq2i 5122	. . . . . . . . . . . . . 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 5117	. . . . . . . . . . . 12 ⊢ (𝑛 = 3 → (𝑛 ∥ ;31 ↔ 3 ∥ ;31))
33	31, 32	mtbiri 330	. . . . . . . . . . 11 ⊢ (𝑛 = 3 → ¬ 𝑛 ∥ ;31)
34	25, 33	jaoi 871	. . . . . . . . . 10 ⊢ ((𝑛 = 2 ∨ 𝑛 = 3) → ¬ 𝑛 ∥ ;31)
35	18, 34	sylbi 220	. . . . . . . . 9 ⊢ (𝑛 ∈ {2, 3} → ¬ 𝑛 ∥ ;31)
36	35	adantr 486	. . . . . . . 8 ⊢ ((𝑛 ∈ {2, 3} ∧ 𝑛 ∈ ℙ) → ¬ 𝑛 ∥ ;31)
37	16, 36	sylbi 220	. . . . . . 7 ⊢ (𝑛 ∈ ({2, 3} ∩ ℙ) → ¬ 𝑛 ∥ ;31)
38		elin 3924	. . . . . . . 8 ⊢ (𝑛 ∈ ({4, 5} ∩ ℙ) ↔ (𝑛 ∈ {4, 5} ∧ 𝑛 ∈ ℙ))
39	17	elpr 4619	. . . . . . . . . 10 ⊢ (𝑛 ∈ {4, 5} ↔ (𝑛 = 4 ∨ 𝑛 = 5))
40		eleq1 2854	. . . . . . . . . . . 12 ⊢ (𝑛 = 4 → (𝑛 ∈ ℙ ↔ 4 ∈ ℙ))
41		4nprm 16778	. . . . . . . . . . . . 13 ⊢ ¬ 4 ∈ ℙ
42	41	pm2.21i 120	. . . . . . . . . . . 12 ⊢ (4 ∈ ℙ → ¬ 𝑛 ∥ ;31)
43	40, 42	biimtrdi 256	. . . . . . . . . . 11 ⊢ (𝑛 = 4 → (𝑛 ∈ ℙ → ¬ 𝑛 ∥ ;31))
44		1nn 12262	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ
45		1lt5 12441	. . . . . . . . . . . . . 14 ⊢ 1 < 5
46	2, 44, 45	dec5dvds 17149	. . . . . . . . . . . . 13 ⊢ ¬ 5 ∥ ;31
47		breq1 5117	. . . . . . . . . . . . 13 ⊢ (𝑛 = 5 → (𝑛 ∥ ;31 ↔ 5 ∥ ;31))
48	46, 47	mtbiri 330	. . . . . . . . . . . 12 ⊢ (𝑛 = 5 → ¬ 𝑛 ∥ ;31)
49	48	a1d 26	. . . . . . . . . . 11 ⊢ (𝑛 = 5 → (𝑛 ∈ ℙ → ¬ 𝑛 ∥ ;31))
50	43, 49	jaoi 871	. . . . . . . . . 10 ⊢ ((𝑛 = 4 ∨ 𝑛 = 5) → (𝑛 ∈ ℙ → ¬ 𝑛 ∥ ;31))
51	39, 50	sylbi 220	. . . . . . . . 9 ⊢ (𝑛 ∈ {4, 5} → (𝑛 ∈ ℙ → ¬ 𝑛 ∥ ;31))
52	51	imp 412	. . . . . . . 8 ⊢ ((𝑛 ∈ {4, 5} ∧ 𝑛 ∈ ℙ) → ¬ 𝑛 ∥ ;31)
53	38, 52	sylbi 220	. . . . . . 7 ⊢ (𝑛 ∈ ({4, 5} ∩ ℙ) → ¬ 𝑛 ∥ ;31)
54	37, 53	jaoi 871	. . . . . 6 ⊢ ((𝑛 ∈ ({2, 3} ∩ ℙ) ∨ 𝑛 ∈ ({4, 5} ∩ ℙ)) → ¬ 𝑛 ∥ ;31)
55	15, 54	sylbi 220	. . . . 5 ⊢ (𝑛 ∈ (({2, 3} ∩ ℙ) ∪ ({4, 5} ∩ ℙ)) → ¬ 𝑛 ∥ ;31)
56		indir 4242	. . . . 5 ⊢ (({2, 3} ∪ {4, 5}) ∩ ℙ) = (({2, 3} ∩ ℙ) ∪ ({4, 5} ∩ ℙ))
57	55, 56	eleq2s 2884	. . . 4 ⊢ (𝑛 ∈ (({2, 3} ∪ {4, 5}) ∩ ℙ) → ¬ 𝑛 ∥ ;31)
58		5nn0 12542	. . . . . . . . 9 ⊢ 5 ∈ ℕ0
59		5re 12346	. . . . . . . . . 10 ⊢ 5 ∈ ℝ
60		5lt9 12463	. . . . . . . . . 10 ⊢ 5 < 9
61	59, 9, 60	ltleii 11351	. . . . . . . . 9 ⊢ 5 ≤ 9
62		2lt3 12432	. . . . . . . . 9 ⊢ 2 < 3
63	7, 2, 58, 3, 61, 62	decleh 12769	. . . . . . . 8 ⊢ ;25 ≤ ;31
64		6nn 12348	. . . . . . . . 9 ⊢ 6 ∈ ℕ
65		1lt6 12446	. . . . . . . . 9 ⊢ 1 < 6
66	2, 3, 64, 65	declt 12762	. . . . . . . 8 ⊢ ;31 < ;36
67	4	nn0rei 12533	. . . . . . . . . 10 ⊢ ;31 ∈ ℝ
68		0re 11228	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
69		9pos 12375	. . . . . . . . . . . 12 ⊢ 0 < 9
70	68, 9, 69	ltleii 11351	. . . . . . . . . . 11 ⊢ 0 ≤ 9
71	6, 3, 19, 70	declei 12770	. . . . . . . . . 10 ⊢ 0 ≤ ;31
72	67, 71	pm3.2i 476	. . . . . . . . 9 ⊢ (;31 ∈ ℝ ∧ 0 ≤ ;31)
73		flsqrt5 48387	. . . . . . . . . 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 724	. . . . . . 7 ⊢ (⌊‘(√‘;31)) = 5
77	76	oveq2i 7434	. . . . . 6 ⊢ (2...(⌊‘(√‘;31))) = (2...5)
78		5nn 12345	. . . . . . . . . 10 ⊢ 5 ∈ ℕ
79	78	nnzi 12636	. . . . . . . . 9 ⊢ 5 ∈ ℤ
80		3z 12645	. . . . . . . . 9 ⊢ 3 ∈ ℤ
81	1, 79, 80	3pm3.2i 1358	. . . . . . . 8 ⊢ (2 ∈ ℤ ∧ 5 ∈ ℤ ∧ 3 ∈ ℤ)
82		3re 12339	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
83	8, 82, 62	ltleii 11351	. . . . . . . . 9 ⊢ 2 ≤ 3
84		3lt5 12439	. . . . . . . . . 10 ⊢ 3 < 5
85	82, 59, 84	ltleii 11351	. . . . . . . . 9 ⊢ 3 ≤ 5
86	83, 85	pm3.2i 476	. . . . . . . 8 ⊢ (2 ≤ 3 ∧ 3 ≤ 5)
87		elfz2 13560	. . . . . . . 8 ⊢ (3 ∈ (2...5) ↔ ((2 ∈ ℤ ∧ 5 ∈ ℤ ∧ 3 ∈ ℤ) ∧ (2 ≤ 3 ∧ 3 ≤ 5)))
88	81, 86, 87	mpbir2an 724	. . . . . . 7 ⊢ 3 ∈ (2...5)
89		fzsplit 13597	. . . . . . 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 12322	. . . . . . . . 9 ⊢ 3 = (2 + 1)
92	91	oveq2i 7434	. . . . . . . 8 ⊢ (2...3) = (2...(2 + 1))
93		fzpr 13626	. . . . . . . . 9 ⊢ (2 ∈ ℤ → (2...(2 + 1)) = {2, (2 + 1)})
94	1, 93	ax-mp 5	. . . . . . . 8 ⊢ (2...(2 + 1)) = {2, (2 + 1)}
95		2p1e3 12400	. . . . . . . . 9 ⊢ (2 + 1) = 3
96	95	preq2i 4708	. . . . . . . 8 ⊢ {2, (2 + 1)} = {2, 3}
97	92, 94, 96	3eqtri 2793	. . . . . . 7 ⊢ (2...3) = {2, 3}
98	28	oveq1i 7433	. . . . . . . 8 ⊢ ((3 + 1)...5) = (4...5)
99		df-5 12324	. . . . . . . . 9 ⊢ 5 = (4 + 1)
100	99	oveq2i 7434	. . . . . . . 8 ⊢ (4...5) = (4...(4 + 1))
101		4z 12646	. . . . . . . . . 10 ⊢ 4 ∈ ℤ
102		fzpr 13626	. . . . . . . . . 10 ⊢ (4 ∈ ℤ → (4...(4 + 1)) = {4, (4 + 1)})
103	101, 102	ax-mp 5	. . . . . . . . 9 ⊢ (4...(4 + 1)) = {4, (4 + 1)}
104		4p1e5 12404	. . . . . . . . . 10 ⊢ (4 + 1) = 5
105	104	preq2i 4708	. . . . . . . . 9 ⊢ {4, (4 + 1)} = {4, 5}
106	103, 105	eqtri 2789	. . . . . . . 8 ⊢ (4...(4 + 1)) = {4, 5}
107	98, 100, 106	3eqtri 2793	. . . . . . 7 ⊢ ((3 + 1)...5) = {4, 5}
108	97, 107	uneq12i 4123	. . . . . 6 ⊢ ((2...3) ∪ ((3 + 1)...5)) = ({2, 3} ∪ {4, 5})
109	77, 90, 108	3eqtri 2793	. . . . 5 ⊢ (2...(⌊‘(√‘;31))) = ({2, 3} ∪ {4, 5})
110	109	ineq1i 4172	. . . 4 ⊢ ((2...(⌊‘(√‘;31))) ∩ ℙ) = (({2, 3} ∪ {4, 5}) ∩ ℙ)
111	57, 110	eleq2s 2884	. . 3 ⊢ (𝑛 ∈ ((2...(⌊‘(√‘;31))) ∩ ℙ) → ¬ 𝑛 ∥ ;31)
112	111	rgen 3084	. 2 ⊢ ∀𝑛 ∈ ((2...(⌊‘(√‘;31))) ∩ ℙ) ¬ 𝑛 ∥ ;31
113		isprm7 16792	. 2 ⊢ (;31 ∈ ℙ ↔ (;31 ∈ (ℤ≥‘2) ∧ ∀𝑛 ∈ ((2...(⌊‘(√‘;31))) ∩ ℙ) ¬ 𝑛 ∥ ;31))
114	14, 112, 113	mpbir2an 724	1 ⊢ ;31 ∈ ℙ

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  ∀wral 3082   ∪ cun 3906   ∩ cin 3907  {cpr 4596   class class class wbr 5114  ‘cfv 6543  (class class class)co 7423  ℝcr 11117  0cc0 11118  1c1 11119   + caddc 11121   < clt 11261   ≤ cle 11262  2c2 12313  3c3 12314  4c4 12315  5c5 12316  6c6 12317  9c9 12320  ℤcz 12609  ;cdc 12729  ℤ_≥cuz 12880  ...cfz 13553  ⌊cfl 13843  √csqrt 15310   ∥ cdvds 16335  ℙcprime 16754

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-cnex 11174  ax-resscn 11175  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-mulcom 11182  ax-addass 11183  ax-mulass 11184  ax-distr 11185  ax-i2m1 11186  ax-1ne0 11187  ax-1rid 11188  ax-rnegex 11189  ax-rrecex 11190  ax-cnre 11191  ax-pre-lttri 11192  ax-pre-lttrn 11193  ax-pre-ltadd 11194  ax-pre-mulgt0 11195  ax-pre-sup 11196

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7380  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7872  df-1st 7995  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-er 8703  df-en 8953  df-dom 8954  df-sdom 8955  df-fin 8956  df-sup 9412  df-inf 9413  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267  df-sub 11461  df-neg 11462  df-div 11890  df-nn 12252  df-2 12321  df-3 12322  df-4 12323  df-5 12324  df-6 12325  df-7 12326  df-8 12327  df-9 12328  df-n0 12523  df-z 12610  df-dec 12730  df-uz 12881  df-rp 13035  df-fz 13554  df-fl 13845  df-seq 14058  df-exp 14118  df-cj 15176  df-re 15177  df-im 15178  df-sqrt 15312  df-abs 15313  df-dvds 16336  df-prm 16755

This theorem is used by:  m5prm  48391