Metamath Proof Explorer

Theorem prmgt1

Description: A prime number is an integer greater than 1. (Contributed by Alexander van der Vekens, 17-May-2018)

Ref Expression
Assertion prmgt1 
|- ( P e. Prime -> 1 < P )

Proof

Step Hyp Ref Expression
1 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
2 eluz2gt1 
 |-  ( P e. ( ZZ>= ` 2 ) -> 1 < P )
3 1 2 syl 
 |-  ( P e. Prime -> 1 < P )