Metamath Proof Explorer

Theorem nprmdvds1

Description: No prime number divides 1. (Contributed by Paul Chapman, 17-Nov-2012) (Proof shortened by Mario Carneiro, 2-Jul-2015)

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

Proof

Step Hyp Ref Expression
1 1nprm 
 |-  -. 1 e. Prime
2 prmnn 
 |-  ( P e. Prime -> P e. NN )
3 2 nnnn0d 
 |-  ( P e. Prime -> P e. NN0 )
4 dvds1 
 |-  ( P e. NN0 -> ( P || 1 <-> P = 1 ) )
5 3 4 syl 
 |-  ( P e. Prime -> ( P || 1 <-> P = 1 ) )
6 eleq1 
 |-  ( P = 1 -> ( P e. Prime <-> 1 e. Prime ) )
7 6 biimpcd 
 |-  ( P e. Prime -> ( P = 1 -> 1 e. Prime ) )
8 5 7 sylbid 
 |-  ( P e. Prime -> ( P || 1 -> 1 e. Prime ) )
9 1 8 mtoi 
 |-  ( P e. Prime -> -. P || 1 )