2prm

Description: 2 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011) (Proof shortened by Fan Zheng, 16-Jun-2016)

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

Step	Hyp	Ref	Expression
1		2z	$⊢ 2 \in ℤ$
2		1lt2	$⊢ 1 < 2$
3		eluz2b1	$⊢ 2 \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land 1 < 2)$
4	1 2 3	mpbir2an	$⊢ 2 \in ℤ_{\geq 2}$
5		ral0	$⊢ \forall z \in \emptyset \neg z ∥ 2$
6		fzssuz	$⊢ (2 \dots 2 - 1) \subseteq ℤ_{\geq 2}$
7		dfss2	$⊢ (2 \dots 2 - 1) \subseteq ℤ_{\geq 2} \leftrightarrow (2 \dots 2 - 1) \cap ℤ_{\geq 2} = (2 \dots 2 - 1)$
8	6 7	mpbi	$⊢ (2 \dots 2 - 1) \cap ℤ_{\geq 2} = (2 \dots 2 - 1)$
9		uzdisj	$⊢ (2 \dots 2 - 1) \cap ℤ_{\geq 2} = \emptyset$
10	8 9	eqtr3i	$⊢ (2 \dots 2 - 1) = \emptyset$
11	10	raleqi	$⊢ \forall z \in (2 \dots 2 - 1) \neg z ∥ 2 \leftrightarrow \forall z \in \emptyset \neg z ∥ 2$
12	5 11	mpbir	$⊢ \forall z \in (2 \dots 2 - 1) \neg z ∥ 2$
13		isprm3	$⊢ 2 \in ℙ \leftrightarrow (2 \in ℤ_{\geq 2} \land \forall z \in (2 \dots 2 - 1) \neg z ∥ 2)$
14	4 12 13	mpbir2an	$⊢ 2 \in ℙ$

Metamath Proof Explorer