Metamath Proof Explorer

Theorem 3prm

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

Ref Expression
Assertion 3prm 
|- 3 e. Prime

Proof

Step Hyp Ref Expression
1 3z 
 |-  3 e. ZZ
2 1lt3 
 |-  1 < 3
3 eluz2b1 
 |-  ( 3 e. ( ZZ>= ` 2 ) <-> ( 3 e. ZZ /\ 1 < 3 ) )
4 1 2 3 mpbir2an 
 |-  3 e. ( ZZ>= ` 2 )
5 elfz1eq 
 |-  ( z e. ( 2 ... 2 ) -> z = 2 )
6 n2dvds3 
 |-  -. 2 || 3
7 breq1 
 |-  ( z = 2 -> ( z || 3 <-> 2 || 3 ) )
8 6 7 mtbiri 
 |-  ( z = 2 -> -. z || 3 )
9 5 8 syl 
 |-  ( z e. ( 2 ... 2 ) -> -. z || 3 )
10 3m1e2 
 |-  ( 3 - 1 ) = 2
11 10 oveq2i 
 |-  ( 2 ... ( 3 - 1 ) ) = ( 2 ... 2 )
12 9 11 eleq2s 
 |-  ( z e. ( 2 ... ( 3 - 1 ) ) -> -. z || 3 )
13 12 rgen 
 |-  A. z e. ( 2 ... ( 3 - 1 ) ) -. z || 3
14 isprm3 
 |-  ( 3 e. Prime <-> ( 3 e. ( ZZ>= ` 2 ) /\ A. z e. ( 2 ... ( 3 - 1 ) ) -. z || 3 ) )
15 4 13 14 mpbir2an 
 |-  3 e. Prime