3prm

Description: 3 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011)

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

Step	Hyp	Ref	Expression
1		3z	$⊢ 3 \in ℤ$
2		1lt3	$⊢ 1 < 3$
3		eluz2b1	$⊢ 3 \in ℤ_{\geq 2} \leftrightarrow (3 \in ℤ \land 1 < 3)$
4	1 2 3	mpbir2an	$⊢ 3 \in ℤ_{\geq 2}$
5		elfz1eq	$⊢ z \in (2 \dots 2) \to z = 2$
6		n2dvds3	$⊢ \neg 2 ∥ 3$
7		breq1	$⊢ z = 2 \to (z ∥ 3 \leftrightarrow 2 ∥ 3)$
8	6 7	mtbiri	$⊢ z = 2 \to \neg z ∥ 3$
9	5 8	syl	$⊢ z \in (2 \dots 2) \to \neg z ∥ 3$
10		3m1e2	$⊢ 3 - 1 = 2$
11	10	oveq2i	$⊢ (2 \dots 3 - 1) = (2 \dots 2)$
12	9 11	eleq2s	$⊢ z \in (2 \dots 3 - 1) \to \neg z ∥ 3$
13	12	rgen	$⊢ \forall z \in (2 \dots 3 - 1) \neg z ∥ 3$
14		isprm3	$⊢ 3 \in ℙ \leftrightarrow (3 \in ℤ_{\geq 2} \land \forall z \in (2 \dots 3 - 1) \neg z ∥ 3)$
15	4 13 14	mpbir2an	$⊢ 3 \in ℙ$

Metamath Proof Explorer