isprm2

Description: The predicate "is a prime number". A prime number is an integer greater than or equal to 2 whose only positive divisors are 1 and itself. Definition in ApostolNT p. 16. (Contributed by Paul Chapman, 26-Oct-2012)

		Ref	Expression
	Assertion	isprm2	$⊢ P \in ℙ \leftrightarrow (P \in ℤ_{\geq 2} \land \forall z \in ℕ (z ∥ P \to (z = 1 \lor z = P)))$

Proof

Step	Hyp	Ref	Expression
1		1nprm	$⊢ \neg 1 \in ℙ$
2		eleq1	$⊢ P = 1 \to (P \in ℙ \leftrightarrow 1 \in ℙ)$
3	2	biimpcd	$⊢ P \in ℙ \to (P = 1 \to 1 \in ℙ)$
4	1 3	mtoi	$⊢ P \in ℙ \to \neg P = 1$
5	4	neqned	$⊢ P \in ℙ \to P \neq 1$
6	5	pm4.71i	$⊢ P \in ℙ \leftrightarrow (P \in ℙ \land P \neq 1)$
7		isprm	$⊢ P \in ℙ \leftrightarrow (P \in ℕ \land \{n \in ℕ \| n ∥ P\} \approx 2_{𝑜})$
8		isprm2lem	$⊢ (P \in ℕ \land P \neq 1) \to (\{n \in ℕ \| n ∥ P\} \approx 2_{𝑜} \leftrightarrow \{n \in ℕ \| n ∥ P\} = \{1, P\})$
9		eqss	$⊢ \{n \in ℕ \| n ∥ P\} = \{1, P\} \leftrightarrow (\{n \in ℕ \| n ∥ P\} \subseteq \{1, P\} \land \{1, P\} \subseteq \{n \in ℕ \| n ∥ P\})$
10	9	imbi2i	$⊢ (P \in ℕ \to \{n \in ℕ \| n ∥ P\} = \{1, P\}) \leftrightarrow (P \in ℕ \to (\{n \in ℕ \| n ∥ P\} \subseteq \{1, P\} \land \{1, P\} \subseteq \{n \in ℕ \| n ∥ P\}))$
11		1idssfct	$⊢ P \in ℕ \to \{1, P\} \subseteq \{n \in ℕ \| n ∥ P\}$
12		jcab	$⊢ (P \in ℕ \to (\{n \in ℕ \| n ∥ P\} \subseteq \{1, P\} \land \{1, P\} \subseteq \{n \in ℕ \| n ∥ P\})) \leftrightarrow ((P \in ℕ \to \{n \in ℕ \| n ∥ P\} \subseteq \{1, P\}) \land (P \in ℕ \to \{1, P\} \subseteq \{n \in ℕ \| n ∥ P\}))$
13	11 12	mpbiran2	$⊢ (P \in ℕ \to (\{n \in ℕ \| n ∥ P\} \subseteq \{1, P\} \land \{1, P\} \subseteq \{n \in ℕ \| n ∥ P\})) \leftrightarrow (P \in ℕ \to \{n \in ℕ \| n ∥ P\} \subseteq \{1, P\})$
14	10 13	bitri	$⊢ (P \in ℕ \to \{n \in ℕ \| n ∥ P\} = \{1, P\}) \leftrightarrow (P \in ℕ \to \{n \in ℕ \| n ∥ P\} \subseteq \{1, P\})$
15	14	pm5.74ri	$⊢ P \in ℕ \to (\{n \in ℕ \| n ∥ P\} = \{1, P\} \leftrightarrow \{n \in ℕ \| n ∥ P\} \subseteq \{1, P\})$
16	15	adantr	$⊢ (P \in ℕ \land P \neq 1) \to (\{n \in ℕ \| n ∥ P\} = \{1, P\} \leftrightarrow \{n \in ℕ \| n ∥ P\} \subseteq \{1, P\})$
17	8 16	bitrd	$⊢ (P \in ℕ \land P \neq 1) \to (\{n \in ℕ \| n ∥ P\} \approx 2_{𝑜} \leftrightarrow \{n \in ℕ \| n ∥ P\} \subseteq \{1, P\})$
18	17	expcom	$⊢ P \neq 1 \to (P \in ℕ \to (\{n \in ℕ \| n ∥ P\} \approx 2_{𝑜} \leftrightarrow \{n \in ℕ \| n ∥ P\} \subseteq \{1, P\}))$
19	18	pm5.32d	$⊢ P \neq 1 \to ((P \in ℕ \land \{n \in ℕ \| n ∥ P\} \approx 2_{𝑜}) \leftrightarrow (P \in ℕ \land \{n \in ℕ \| n ∥ P\} \subseteq \{1, P\}))$
20	7 19	bitrid	$⊢ P \neq 1 \to (P \in ℙ \leftrightarrow (P \in ℕ \land \{n \in ℕ \| n ∥ P\} \subseteq \{1, P\}))$
21	20	pm5.32ri	$⊢ (P \in ℙ \land P \neq 1) \leftrightarrow ((P \in ℕ \land \{n \in ℕ \| n ∥ P\} \subseteq \{1, P\}) \land P \neq 1)$
22		ancom	$⊢ ((P \in ℕ \land \{n \in ℕ \| n ∥ P\} \subseteq \{1, P\}) \land P \neq 1) \leftrightarrow (P \neq 1 \land (P \in ℕ \land \{n \in ℕ \| n ∥ P\} \subseteq \{1, P\}))$
23		anass	$⊢ ((P \neq 1 \land P \in ℕ) \land \{n \in ℕ \| n ∥ P\} \subseteq \{1, P\}) \leftrightarrow (P \neq 1 \land (P \in ℕ \land \{n \in ℕ \| n ∥ P\} \subseteq \{1, P\}))$
24	22 23	bitr4i	$⊢ ((P \in ℕ \land \{n \in ℕ \| n ∥ P\} \subseteq \{1, P\}) \land P \neq 1) \leftrightarrow ((P \neq 1 \land P \in ℕ) \land \{n \in ℕ \| n ∥ P\} \subseteq \{1, P\})$
25		ancom	$⊢ (P \neq 1 \land P \in ℕ) \leftrightarrow (P \in ℕ \land P \neq 1)$
26		eluz2b3	$⊢ P \in ℤ_{\geq 2} \leftrightarrow (P \in ℕ \land P \neq 1)$
27	25 26	bitr4i	$⊢ (P \neq 1 \land P \in ℕ) \leftrightarrow P \in ℤ_{\geq 2}$
28	27	anbi1i	$⊢ ((P \neq 1 \land P \in ℕ) \land \{n \in ℕ \| n ∥ P\} \subseteq \{1, P\}) \leftrightarrow (P \in ℤ_{\geq 2} \land \{n \in ℕ \| n ∥ P\} \subseteq \{1, P\})$
29		dfss2	$⊢ \{n \in ℕ \| n ∥ P\} \subseteq \{1, P\} \leftrightarrow \forall z (z \in \{n \in ℕ \| n ∥ P\} \to z \in \{1, P\})$
30		breq1	$⊢ n = z \to (n ∥ P \leftrightarrow z ∥ P)$
31	30	elrab	$⊢ z \in \{n \in ℕ \| n ∥ P\} \leftrightarrow (z \in ℕ \land z ∥ P)$
32		vex	$⊢ z \in V$
33	32	elpr	$⊢ z \in \{1, P\} \leftrightarrow (z = 1 \lor z = P)$
34	31 33	imbi12i	$⊢ (z \in \{n \in ℕ \| n ∥ P\} \to z \in \{1, P\}) \leftrightarrow ((z \in ℕ \land z ∥ P) \to (z = 1 \lor z = P))$
35		impexp	$⊢ ((z \in ℕ \land z ∥ P) \to (z = 1 \lor z = P)) \leftrightarrow (z \in ℕ \to (z ∥ P \to (z = 1 \lor z = P)))$
36	34 35	bitri	$⊢ (z \in \{n \in ℕ \| n ∥ P\} \to z \in \{1, P\}) \leftrightarrow (z \in ℕ \to (z ∥ P \to (z = 1 \lor z = P)))$
37	36	albii	$⊢ \forall z (z \in \{n \in ℕ \| n ∥ P\} \to z \in \{1, P\}) \leftrightarrow \forall z (z \in ℕ \to (z ∥ P \to (z = 1 \lor z = P)))$
38		df-ral	$⊢ \forall z \in ℕ (z ∥ P \to (z = 1 \lor z = P)) \leftrightarrow \forall z (z \in ℕ \to (z ∥ P \to (z = 1 \lor z = P)))$
39	37 38	bitr4i	$⊢ \forall z (z \in \{n \in ℕ \| n ∥ P\} \to z \in \{1, P\}) \leftrightarrow \forall z \in ℕ (z ∥ P \to (z = 1 \lor z = P))$
40	29 39	bitri	$⊢ \{n \in ℕ \| n ∥ P\} \subseteq \{1, P\} \leftrightarrow \forall z \in ℕ (z ∥ P \to (z = 1 \lor z = P))$
41	40	anbi2i	$⊢ (P \in ℤ_{\geq 2} \land \{n \in ℕ \| n ∥ P\} \subseteq \{1, P\}) \leftrightarrow (P \in ℤ_{\geq 2} \land \forall z \in ℕ (z ∥ P \to (z = 1 \lor z = P)))$
42	24 28 41	3bitri	$⊢ ((P \in ℕ \land \{n \in ℕ \| n ∥ P\} \subseteq \{1, P\}) \land P \neq 1) \leftrightarrow (P \in ℤ_{\geq 2} \land \forall z \in ℕ (z ∥ P \to (z = 1 \lor z = P)))$
43	6 21 42	3bitri	$⊢ P \in ℙ \leftrightarrow (P \in ℤ_{\geq 2} \land \forall z \in ℕ (z ∥ P \to (z = 1 \lor z = P)))$

Metamath Proof Explorer

Theorem isprm2

Proof