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 e. Prime

Proof

Step Hyp Ref Expression
1 2z 
 |-  2 e. ZZ
2 1lt2 
 |-  1 < 2
3 eluz2b1 
 |-  ( 2 e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ 1 < 2 ) )
4 1 2 3 mpbir2an 
 |-  2 e. ( ZZ>= ` 2 )
5 ral0 
 |-  A. z e. (/) -. z || 2
6 fzssuz 
 |-  ( 2 ... ( 2 - 1 ) ) C_ ( ZZ>= ` 2 )
7 df-ss 
 |-  ( ( 2 ... ( 2 - 1 ) ) C_ ( ZZ>= ` 2 ) <-> ( ( 2 ... ( 2 - 1 ) ) i^i ( ZZ>= ` 2 ) ) = ( 2 ... ( 2 - 1 ) ) )
8 6 7 mpbi 
 |-  ( ( 2 ... ( 2 - 1 ) ) i^i ( ZZ>= ` 2 ) ) = ( 2 ... ( 2 - 1 ) )
9 uzdisj 
 |-  ( ( 2 ... ( 2 - 1 ) ) i^i ( ZZ>= ` 2 ) ) = (/)
10 8 9 eqtr3i 
 |-  ( 2 ... ( 2 - 1 ) ) = (/)
11 10 raleqi 
 |-  ( A. z e. ( 2 ... ( 2 - 1 ) ) -. z || 2 <-> A. z e. (/) -. z || 2 )
12 5 11 mpbir 
 |-  A. z e. ( 2 ... ( 2 - 1 ) ) -. z || 2
13 isprm3 
 |-  ( 2 e. Prime <-> ( 2 e. ( ZZ>= ` 2 ) /\ A. z e. ( 2 ... ( 2 - 1 ) ) -. z || 2 ) )
14 4 12 13 mpbir2an 
 |-  2 e. Prime