Metamath Proof Explorer

Theorem prmuz2

Description: A prime number is an integer greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012)

Ref Expression
Assertion prmuz2 
|- ( P e. Prime -> P e. ( ZZ>= ` 2 ) )

Proof

Step Hyp Ref Expression
1 isprm4 
 |-  ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. x e. ( ZZ>= ` 2 ) ( x || P -> x = P ) ) )
2 1 simplbi 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )