31prm

Description: 31 is a prime number. In contrast to 37prm , the proof of this theorem is not based on the "blanket" prmlem2 , but on isprm7 . 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 (1810 characters compared with 1213 for 37prm ). The number of essential steps, however, is much smaller (138 compared with 213 for 37prm ). (Contributed by AV, 17-Aug-2021) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	31prm	$⊢ 31 \in ℙ$

Proof

Step	Hyp	Ref	Expression
1		2z	$⊢ 2 \in ℤ$
2		3nn0	$⊢ 3 \in ℕ_{0}$
3		1nn0	$⊢ 1 \in ℕ_{0}$
4	2 3	deccl	$⊢ 31 \in ℕ_{0}$
5	4	nn0zi	$⊢ 31 \in ℤ$
6		3nn	$⊢ 3 \in ℕ$
7		2nn0	$⊢ 2 \in ℕ_{0}$
8		2re	$⊢ 2 \in ℝ$
9		9re	$⊢ 9 \in ℝ$
10		2lt9	$⊢ 2 < 9$
11	8 9 10	ltleii	$⊢ 2 \leq 9$
12	6 3 7 11	declei	$⊢ 2 \leq 31$
13		eluz2	$⊢ 31 \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land 31 \in ℤ \land 2 \leq 31)$
14	1 5 12 13	mpbir3an	$⊢ 31 \in ℤ_{\geq 2}$
15		elun	$⊢ n \in ((\{2, 3\} \cap ℙ) \cup (\{4, 5\} \cap ℙ)) \leftrightarrow (n \in (\{2, 3\} \cap ℙ) \lor n \in (\{4, 5\} \cap ℙ))$
16		elin	$⊢ n \in (\{2, 3\} \cap ℙ) \leftrightarrow (n \in \{2, 3\} \land n \in ℙ)$
17		vex	$⊢ n \in V$
18	17	elpr	$⊢ n \in \{2, 3\} \leftrightarrow (n = 2 \lor n = 3)$
19		0nn0	$⊢ 0 \in ℕ_{0}$
20		2cn	$⊢ 2 \in ℂ$
21	20	mul02i	$⊢ 0 \cdot 2 = 0$
22		1e0p1	$⊢ 1 = 0 + 1$
23	2 19 21 22	dec2dvds	$⊢ \neg 2 ∥ 31$
24		breq1	$⊢ n = 2 \to (n ∥ 31 \leftrightarrow 2 ∥ 31)$
25	23 24	mtbiri	$⊢ n = 2 \to \neg n ∥ 31$
26		3ndvds4	$⊢ \neg 3 ∥ 4$
27	2 3	3dvdsdec	$⊢ 3 ∥ 31 \leftrightarrow 3 ∥ (3 + 1)$
28		3p1e4	$⊢ 3 + 1 = 4$
29	28	breq2i	$⊢ 3 ∥ (3 + 1) \leftrightarrow 3 ∥ 4$
30	27 29	bitri	$⊢ 3 ∥ 31 \leftrightarrow 3 ∥ 4$
31	26 30	mtbir	$⊢ \neg 3 ∥ 31$
32		breq1	$⊢ n = 3 \to (n ∥ 31 \leftrightarrow 3 ∥ 31)$
33	31 32	mtbiri	$⊢ n = 3 \to \neg n ∥ 31$
34	25 33	jaoi	$⊢ (n = 2 \lor n = 3) \to \neg n ∥ 31$
35	18 34	sylbi	$⊢ n \in \{2, 3\} \to \neg n ∥ 31$
36	35	adantr	$⊢ (n \in \{2, 3\} \land n \in ℙ) \to \neg n ∥ 31$
37	16 36	sylbi	$⊢ n \in (\{2, 3\} \cap ℙ) \to \neg n ∥ 31$
38		elin	$⊢ n \in (\{4, 5\} \cap ℙ) \leftrightarrow (n \in \{4, 5\} \land n \in ℙ)$
39	17	elpr	$⊢ n \in \{4, 5\} \leftrightarrow (n = 4 \lor n = 5)$
40		eleq1	$⊢ n = 4 \to (n \in ℙ \leftrightarrow 4 \in ℙ)$
41		4nprm	$⊢ \neg 4 \in ℙ$
42	41	pm2.21i	$⊢ 4 \in ℙ \to \neg n ∥ 31$
43	40 42	biimtrdi	$⊢ n = 4 \to (n \in ℙ \to \neg n ∥ 31)$
44		1nn	$⊢ 1 \in ℕ$
45		1lt5	$⊢ 1 < 5$
46	2 44 45	dec5dvds	$⊢ \neg 5 ∥ 31$
47		breq1	$⊢ n = 5 \to (n ∥ 31 \leftrightarrow 5 ∥ 31)$
48	46 47	mtbiri	$⊢ n = 5 \to \neg n ∥ 31$
49	48	a1d	$⊢ n = 5 \to (n \in ℙ \to \neg n ∥ 31)$
50	43 49	jaoi	$⊢ (n = 4 \lor n = 5) \to (n \in ℙ \to \neg n ∥ 31)$
51	39 50	sylbi	$⊢ n \in \{4, 5\} \to (n \in ℙ \to \neg n ∥ 31)$
52	51	imp	$⊢ (n \in \{4, 5\} \land n \in ℙ) \to \neg n ∥ 31$
53	38 52	sylbi	$⊢ n \in (\{4, 5\} \cap ℙ) \to \neg n ∥ 31$
54	37 53	jaoi	$⊢ (n \in (\{2, 3\} \cap ℙ) \lor n \in (\{4, 5\} \cap ℙ)) \to \neg n ∥ 31$
55	15 54	sylbi	$⊢ n \in ((\{2, 3\} \cap ℙ) \cup (\{4, 5\} \cap ℙ)) \to \neg n ∥ 31$
56		indir	$⊢ (\{2, 3\} \cup \{4, 5\}) \cap ℙ = (\{2, 3\} \cap ℙ) \cup (\{4, 5\} \cap ℙ)$
57	55 56	eleq2s	$⊢ n \in ((\{2, 3\} \cup \{4, 5\}) \cap ℙ) \to \neg n ∥ 31$
58		5nn0	$⊢ 5 \in ℕ_{0}$
59		5re	$⊢ 5 \in ℝ$
60		5lt9	$⊢ 5 < 9$
61	59 9 60	ltleii	$⊢ 5 \leq 9$
62		2lt3	$⊢ 2 < 3$
63	7 2 58 3 61 62	decleh	$⊢ 25 \leq 31$
64		6nn	$⊢ 6 \in ℕ$
65		1lt6	$⊢ 1 < 6$
66	2 3 64 65	declt	$⊢ 31 < 36$
67	4	nn0rei	$⊢ 31 \in ℝ$
68		0re	$⊢ 0 \in ℝ$
69		9pos	$⊢ 0 < 9$
70	68 9 69	ltleii	$⊢ 0 \leq 9$
71	6 3 19 70	declei	$⊢ 0 \leq 31$
72	67 71	pm3.2i	$⊢ (31 \in ℝ \land 0 \leq 31)$
73		flsqrt5	$⊢ (31 \in ℝ \land 0 \leq 31) \to ((25 \leq 31 \land 31 < 36) \leftrightarrow ⌊\sqrt{31}⌋ = 5)$
74	73	bicomd	$⊢ (31 \in ℝ \land 0 \leq 31) \to (⌊\sqrt{31}⌋ = 5 \leftrightarrow (25 \leq 31 \land 31 < 36))$
75	72 74	ax-mp	$⊢ ⌊\sqrt{31}⌋ = 5 \leftrightarrow (25 \leq 31 \land 31 < 36)$
76	63 66 75	mpbir2an	$⊢ ⌊\sqrt{31}⌋ = 5$
77	76	oveq2i	$⊢ (2 \dots ⌊\sqrt{31}⌋) = (2 \dots 5)$
78		5nn	$⊢ 5 \in ℕ$
79	78	nnzi	$⊢ 5 \in ℤ$
80		3z	$⊢ 3 \in ℤ$
81	1 79 80	3pm3.2i	$⊢ (2 \in ℤ \land 5 \in ℤ \land 3 \in ℤ)$
82		3re	$⊢ 3 \in ℝ$
83	8 82 62	ltleii	$⊢ 2 \leq 3$
84		3lt5	$⊢ 3 < 5$
85	82 59 84	ltleii	$⊢ 3 \leq 5$
86	83 85	pm3.2i	$⊢ (2 \leq 3 \land 3 \leq 5)$
87		elfz2	$⊢ 3 \in (2 \dots 5) \leftrightarrow ((2 \in ℤ \land 5 \in ℤ \land 3 \in ℤ) \land (2 \leq 3 \land 3 \leq 5))$
88	81 86 87	mpbir2an	$⊢ 3 \in (2 \dots 5)$
89		fzsplit	$⊢ 3 \in (2 \dots 5) \to (2 \dots 5) = (2 \dots 3) \cup (3 + 1 \dots 5)$
90	88 89	ax-mp	$⊢ (2 \dots 5) = (2 \dots 3) \cup (3 + 1 \dots 5)$
91		df-3	$⊢ 3 = 2 + 1$
92	91	oveq2i	$⊢ (2 \dots 3) = (2 \dots 2 + 1)$
93		fzpr	$⊢ 2 \in ℤ \to (2 \dots 2 + 1) = \{2, 2 + 1\}$
94	1 93	ax-mp	$⊢ (2 \dots 2 + 1) = \{2, 2 + 1\}$
95		2p1e3	$⊢ 2 + 1 = 3$
96	95	preq2i	$⊢ \{2, 2 + 1\} = \{2, 3\}$
97	92 94 96	3eqtri	$⊢ (2 \dots 3) = \{2, 3\}$
98	28	oveq1i	$⊢ (3 + 1 \dots 5) = (4 \dots 5)$
99		df-5	$⊢ 5 = 4 + 1$
100	99	oveq2i	$⊢ (4 \dots 5) = (4 \dots 4 + 1)$
101		4z	$⊢ 4 \in ℤ$
102		fzpr	$⊢ 4 \in ℤ \to (4 \dots 4 + 1) = \{4, 4 + 1\}$
103	101 102	ax-mp	$⊢ (4 \dots 4 + 1) = \{4, 4 + 1\}$
104		4p1e5	$⊢ 4 + 1 = 5$
105	104	preq2i	$⊢ \{4, 4 + 1\} = \{4, 5\}$
106	103 105	eqtri	$⊢ (4 \dots 4 + 1) = \{4, 5\}$
107	98 100 106	3eqtri	$⊢ (3 + 1 \dots 5) = \{4, 5\}$
108	97 107	uneq12i	$⊢ (2 \dots 3) \cup (3 + 1 \dots 5) = \{2, 3\} \cup \{4, 5\}$
109	77 90 108	3eqtri	$⊢ (2 \dots ⌊\sqrt{31}⌋) = \{2, 3\} \cup \{4, 5\}$
110	109	ineq1i	$⊢ (2 \dots ⌊\sqrt{31}⌋) \cap ℙ = (\{2, 3\} \cup \{4, 5\}) \cap ℙ$
111	57 110	eleq2s	$⊢ n \in ((2 \dots ⌊\sqrt{31}⌋) \cap ℙ) \to \neg n ∥ 31$
112	111	rgen	$⊢ \forall n \in ((2 \dots ⌊\sqrt{31}⌋) \cap ℙ) \neg n ∥ 31$
113		isprm7	$⊢ 31 \in ℙ \leftrightarrow (31 \in ℤ_{\geq 2} \land \forall n \in ((2 \dots ⌊\sqrt{31}⌋) \cap ℙ) \neg n ∥ 31)$
114	14 112 113	mpbir2an	$⊢ 31 \in ℙ$

Metamath Proof Explorer

Theorem 31prm

Proof