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

Proof

Step Hyp Ref Expression
1 2z 2
2 1lt2 1<2
3 eluz2b1 2221<2
4 1 2 3 mpbir2an 22
5 ral0 z¬z2
6 fzssuz 2212
7 df-ss 22122212=221
8 6 7 mpbi 2212=221
9 uzdisj 2212=
10 8 9 eqtr3i 221=
11 10 raleqi z221¬z2z¬z2
12 5 11 mpbir z221¬z2
13 isprm3 222z221¬z2
14 4 12 13 mpbir2an 2