Metamath Proof Explorer

Theorem prmm2nn0

Description: Subtracting 2 from a prime number results in a nonnegative integer. (Contributed by Alexander van der Vekens, 30-Aug-2018)

Ref Expression
Assertion prmm2nn0 
|- ( P e. Prime -> ( P - 2 ) e. NN0 )

Proof

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