# Metamath Proof Explorer

## Theorem 3prm

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

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

### Proof

Step Hyp Ref Expression
1 3z ${⊢}3\in ℤ$
2 1lt3 ${⊢}1<3$
3 eluz2b1 ${⊢}3\in {ℤ}_{\ge 2}↔\left(3\in ℤ\wedge 1<3\right)$
4 1 2 3 mpbir2an ${⊢}3\in {ℤ}_{\ge 2}$
5 elfz1eq ${⊢}{z}\in \left(2\dots 2\right)\to {z}=2$
6 n2dvds3 ${⊢}¬2\parallel 3$
7 breq1 ${⊢}{z}=2\to \left({z}\parallel 3↔2\parallel 3\right)$
8 6 7 mtbiri ${⊢}{z}=2\to ¬{z}\parallel 3$
9 5 8 syl ${⊢}{z}\in \left(2\dots 2\right)\to ¬{z}\parallel 3$
10 3m1e2 ${⊢}3-1=2$
11 10 oveq2i ${⊢}\left(2\dots 3-1\right)=\left(2\dots 2\right)$
12 9 11 eleq2s ${⊢}{z}\in \left(2\dots 3-1\right)\to ¬{z}\parallel 3$
13 12 rgen ${⊢}\forall {z}\in \left(2\dots 3-1\right)\phantom{\rule{.4em}{0ex}}¬{z}\parallel 3$
14 isprm3 ${⊢}3\in ℙ↔\left(3\in {ℤ}_{\ge 2}\wedge \forall {z}\in \left(2\dots 3-1\right)\phantom{\rule{.4em}{0ex}}¬{z}\parallel 3\right)$
15 4 13 14 mpbir2an ${⊢}3\in ℙ$