Metamath Proof Explorer

Theorem 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 ℙ$

Proof

Step Hyp Ref Expression
1 2z ${⊢}2\in ℤ$
2 1lt2 ${⊢}1<2$
3 eluz2b1 ${⊢}2\in {ℤ}_{\ge 2}↔\left(2\in ℤ\wedge 1<2\right)$
4 1 2 3 mpbir2an ${⊢}2\in {ℤ}_{\ge 2}$
5 ral0 ${⊢}\forall {z}\in \varnothing \phantom{\rule{.4em}{0ex}}¬{z}\parallel 2$
6 fzssuz ${⊢}\left(2\dots 2-1\right)\subseteq {ℤ}_{\ge 2}$
7 df-ss ${⊢}\left(2\dots 2-1\right)\subseteq {ℤ}_{\ge 2}↔\left(2\dots 2-1\right)\cap {ℤ}_{\ge 2}=\left(2\dots 2-1\right)$
8 6 7 mpbi ${⊢}\left(2\dots 2-1\right)\cap {ℤ}_{\ge 2}=\left(2\dots 2-1\right)$
9 uzdisj ${⊢}\left(2\dots 2-1\right)\cap {ℤ}_{\ge 2}=\varnothing$
10 8 9 eqtr3i ${⊢}\left(2\dots 2-1\right)=\varnothing$
11 10 raleqi ${⊢}\forall {z}\in \left(2\dots 2-1\right)\phantom{\rule{.4em}{0ex}}¬{z}\parallel 2↔\forall {z}\in \varnothing \phantom{\rule{.4em}{0ex}}¬{z}\parallel 2$
12 5 11 mpbir ${⊢}\forall {z}\in \left(2\dots 2-1\right)\phantom{\rule{.4em}{0ex}}¬{z}\parallel 2$
13 isprm3 ${⊢}2\in ℙ↔\left(2\in {ℤ}_{\ge 2}\wedge \forall {z}\in \left(2\dots 2-1\right)\phantom{\rule{.4em}{0ex}}¬{z}\parallel 2\right)$
14 4 12 13 mpbir2an ${⊢}2\in ℙ$