isprm3

Description: The predicate "is a prime number". A prime number is an integer greater than or equal to 2 with no divisors strictly between 1 and itself. (Contributed by Paul Chapman, 26-Oct-2012)

		Ref	Expression
	Assertion	isprm3	$⊢ P \in ℙ \leftrightarrow (P \in ℤ_{\geq 2} \land \forall z \in (2 \dots P - 1) \neg z ∥ P)$

Proof

Step	Hyp	Ref	Expression
1		isprm2	$⊢ P \in ℙ \leftrightarrow (P \in ℤ_{\geq 2} \land \forall z \in ℕ (z ∥ P \to (z = 1 \lor z = P)))$
2		iman	$⊢ (z \in ℕ \to (z = 1 \lor z = P)) \leftrightarrow \neg (z \in ℕ \land \neg (z = 1 \lor z = P))$
3		eluz2nn	$⊢ P \in ℤ_{\geq 2} \to P \in ℕ$
4		nnz	$⊢ z \in ℕ \to z \in ℤ$
5		dvdsle	$⊢ (z \in ℤ \land P \in ℕ) \to (z ∥ P \to z \leq P)$
6	4 5	sylan	$⊢ (z \in ℕ \land P \in ℕ) \to (z ∥ P \to z \leq P)$
7		nnge1	$⊢ z \in ℕ \to 1 \leq z$
8	7	adantr	$⊢ (z \in ℕ \land P \in ℕ) \to 1 \leq z$
9	6 8	jctild	$⊢ (z \in ℕ \land P \in ℕ) \to (z ∥ P \to (1 \leq z \land z \leq P))$
10	3 9	sylan2	$⊢ (z \in ℕ \land P \in ℤ_{\geq 2}) \to (z ∥ P \to (1 \leq z \land z \leq P))$
11		zre	$⊢ z \in ℤ \to z \in ℝ$
12		nnre	$⊢ P \in ℕ \to P \in ℝ$
13		1re	$⊢ 1 \in ℝ$
14		leltne	$⊢ (1 \in ℝ \land z \in ℝ \land 1 \leq z) \to (1 < z \leftrightarrow z \neq 1)$
15	13 14	mp3an1	$⊢ (z \in ℝ \land 1 \leq z) \to (1 < z \leftrightarrow z \neq 1)$
16	15	3adant2	$⊢ (z \in ℝ \land P \in ℝ \land 1 \leq z) \to (1 < z \leftrightarrow z \neq 1)$
17	16	3expia	$⊢ (z \in ℝ \land P \in ℝ) \to (1 \leq z \to (1 < z \leftrightarrow z \neq 1))$
18		leltne	$⊢ (z \in ℝ \land P \in ℝ \land z \leq P) \to (z < P \leftrightarrow P \neq z)$
19	18	3expia	$⊢ (z \in ℝ \land P \in ℝ) \to (z \leq P \to (z < P \leftrightarrow P \neq z))$
20	17 19	anim12d	$⊢ (z \in ℝ \land P \in ℝ) \to ((1 \leq z \land z \leq P) \to ((1 < z \leftrightarrow z \neq 1) \land (z < P \leftrightarrow P \neq z)))$
21	11 12 20	syl2an	$⊢ (z \in ℤ \land P \in ℕ) \to ((1 \leq z \land z \leq P) \to ((1 < z \leftrightarrow z \neq 1) \land (z < P \leftrightarrow P \neq z)))$
22		pm4.38	$⊢ ((1 < z \leftrightarrow z \neq 1) \land (z < P \leftrightarrow P \neq z)) \to ((1 < z \land z < P) \leftrightarrow (z \neq 1 \land P \neq z))$
23		df-ne	$⊢ z \neq 1 \leftrightarrow \neg z = 1$
24		nesym	$⊢ P \neq z \leftrightarrow \neg z = P$
25	23 24	anbi12i	$⊢ (z \neq 1 \land P \neq z) \leftrightarrow (\neg z = 1 \land \neg z = P)$
26		ioran	$⊢ \neg (z = 1 \lor z = P) \leftrightarrow (\neg z = 1 \land \neg z = P)$
27	25 26	bitr4i	$⊢ (z \neq 1 \land P \neq z) \leftrightarrow \neg (z = 1 \lor z = P)$
28	22 27	bitrdi	$⊢ ((1 < z \leftrightarrow z \neq 1) \land (z < P \leftrightarrow P \neq z)) \to ((1 < z \land z < P) \leftrightarrow \neg (z = 1 \lor z = P))$
29	21 28	syl6	$⊢ (z \in ℤ \land P \in ℕ) \to ((1 \leq z \land z \leq P) \to ((1 < z \land z < P) \leftrightarrow \neg (z = 1 \lor z = P)))$
30	4 3 29	syl2an	$⊢ (z \in ℕ \land P \in ℤ_{\geq 2}) \to ((1 \leq z \land z \leq P) \to ((1 < z \land z < P) \leftrightarrow \neg (z = 1 \lor z = P)))$
31	10 30	syld	$⊢ (z \in ℕ \land P \in ℤ_{\geq 2}) \to (z ∥ P \to ((1 < z \land z < P) \leftrightarrow \neg (z = 1 \lor z = P)))$
32	31	imp	$⊢ ((z \in ℕ \land P \in ℤ_{\geq 2}) \land z ∥ P) \to ((1 < z \land z < P) \leftrightarrow \neg (z = 1 \lor z = P))$
33		eluzelz	$⊢ P \in ℤ_{\geq 2} \to P \in ℤ$
34		1z	$⊢ 1 \in ℤ$
35		zltp1le	$⊢ (1 \in ℤ \land z \in ℤ) \to (1 < z \leftrightarrow 1 + 1 \leq z)$
36	34 35	mpan	$⊢ z \in ℤ \to (1 < z \leftrightarrow 1 + 1 \leq z)$
37		df-2	$⊢ 2 = 1 + 1$
38	37	breq1i	$⊢ 2 \leq z \leftrightarrow 1 + 1 \leq z$
39	36 38	bitr4di	$⊢ z \in ℤ \to (1 < z \leftrightarrow 2 \leq z)$
40	39	adantr	$⊢ (z \in ℤ \land P \in ℤ) \to (1 < z \leftrightarrow 2 \leq z)$
41		zltlem1	$⊢ (z \in ℤ \land P \in ℤ) \to (z < P \leftrightarrow z \leq P - 1)$
42	40 41	anbi12d	$⊢ (z \in ℤ \land P \in ℤ) \to ((1 < z \land z < P) \leftrightarrow (2 \leq z \land z \leq P - 1))$
43		peano2zm	$⊢ P \in ℤ \to P - 1 \in ℤ$
44		2z	$⊢ 2 \in ℤ$
45		elfz	$⊢ (z \in ℤ \land 2 \in ℤ \land P - 1 \in ℤ) \to (z \in (2 \dots P - 1) \leftrightarrow (2 \leq z \land z \leq P - 1))$
46	44 45	mp3an2	$⊢ (z \in ℤ \land P - 1 \in ℤ) \to (z \in (2 \dots P - 1) \leftrightarrow (2 \leq z \land z \leq P - 1))$
47	43 46	sylan2	$⊢ (z \in ℤ \land P \in ℤ) \to (z \in (2 \dots P - 1) \leftrightarrow (2 \leq z \land z \leq P - 1))$
48	42 47	bitr4d	$⊢ (z \in ℤ \land P \in ℤ) \to ((1 < z \land z < P) \leftrightarrow z \in (2 \dots P - 1))$
49	4 33 48	syl2an	$⊢ (z \in ℕ \land P \in ℤ_{\geq 2}) \to ((1 < z \land z < P) \leftrightarrow z \in (2 \dots P - 1))$
50	49	adantr	$⊢ ((z \in ℕ \land P \in ℤ_{\geq 2}) \land z ∥ P) \to ((1 < z \land z < P) \leftrightarrow z \in (2 \dots P - 1))$
51	32 50	bitr3d	$⊢ ((z \in ℕ \land P \in ℤ_{\geq 2}) \land z ∥ P) \to (\neg (z = 1 \lor z = P) \leftrightarrow z \in (2 \dots P - 1))$
52	51	anasss	$⊢ (z \in ℕ \land (P \in ℤ_{\geq 2} \land z ∥ P)) \to (\neg (z = 1 \lor z = P) \leftrightarrow z \in (2 \dots P - 1))$
53	52	expcom	$⊢ (P \in ℤ_{\geq 2} \land z ∥ P) \to (z \in ℕ \to (\neg (z = 1 \lor z = P) \leftrightarrow z \in (2 \dots P - 1)))$
54	53	pm5.32d	$⊢ (P \in ℤ_{\geq 2} \land z ∥ P) \to ((z \in ℕ \land \neg (z = 1 \lor z = P)) \leftrightarrow (z \in ℕ \land z \in (2 \dots P - 1)))$
55		fzssuz	$⊢ (2 \dots P - 1) \subseteq ℤ_{\geq 2}$
56		2eluzge1	$⊢ 2 \in ℤ_{\geq 1}$
57		uzss	$⊢ 2 \in ℤ_{\geq 1} \to ℤ_{\geq 2} \subseteq ℤ_{\geq 1}$
58	56 57	ax-mp	$⊢ ℤ_{\geq 2} \subseteq ℤ_{\geq 1}$
59	55 58	sstri	$⊢ (2 \dots P - 1) \subseteq ℤ_{\geq 1}$
60		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
61	59 60	sseqtrri	$⊢ (2 \dots P - 1) \subseteq ℕ$
62	61	sseli	$⊢ z \in (2 \dots P - 1) \to z \in ℕ$
63	62	pm4.71ri	$⊢ z \in (2 \dots P - 1) \leftrightarrow (z \in ℕ \land z \in (2 \dots P - 1))$
64	54 63	bitr4di	$⊢ (P \in ℤ_{\geq 2} \land z ∥ P) \to ((z \in ℕ \land \neg (z = 1 \lor z = P)) \leftrightarrow z \in (2 \dots P - 1))$
65	64	notbid	$⊢ (P \in ℤ_{\geq 2} \land z ∥ P) \to (\neg (z \in ℕ \land \neg (z = 1 \lor z = P)) \leftrightarrow \neg z \in (2 \dots P - 1))$
66	2 65	bitrid	$⊢ (P \in ℤ_{\geq 2} \land z ∥ P) \to ((z \in ℕ \to (z = 1 \lor z = P)) \leftrightarrow \neg z \in (2 \dots P - 1))$
67	66	pm5.74da	$⊢ P \in ℤ_{\geq 2} \to ((z ∥ P \to (z \in ℕ \to (z = 1 \lor z = P))) \leftrightarrow (z ∥ P \to \neg z \in (2 \dots P - 1)))$
68		bi2.04	$⊢ (z ∥ P \to (z \in ℕ \to (z = 1 \lor z = P))) \leftrightarrow (z \in ℕ \to (z ∥ P \to (z = 1 \lor z = P)))$
69		con2b	$⊢ (z ∥ P \to \neg z \in (2 \dots P - 1)) \leftrightarrow (z \in (2 \dots P - 1) \to \neg z ∥ P)$
70	67 68 69	3bitr3g	$⊢ P \in ℤ_{\geq 2} \to ((z \in ℕ \to (z ∥ P \to (z = 1 \lor z = P))) \leftrightarrow (z \in (2 \dots P - 1) \to \neg z ∥ P))$
71	70	ralbidv2	$⊢ P \in ℤ_{\geq 2} \to (\forall z \in ℕ (z ∥ P \to (z = 1 \lor z = P)) \leftrightarrow \forall z \in (2 \dots P - 1) \neg z ∥ P)$
72	71	pm5.32i	$⊢ (P \in ℤ_{\geq 2} \land \forall z \in ℕ (z ∥ P \to (z = 1 \lor z = P))) \leftrightarrow (P \in ℤ_{\geq 2} \land \forall z \in (2 \dots P - 1) \neg z ∥ P)$
73	1 72	bitri	$⊢ P \in ℙ \leftrightarrow (P \in ℤ_{\geq 2} \land \forall z \in (2 \dots P - 1) \neg z ∥ P)$

Metamath Proof Explorer

Theorem isprm3

Proof