Metamath Proof Explorer

Theorem 9nprm

Description: 9 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014)

Ref Expression
Assertion 9nprm 
|- -. 9 e. Prime

Proof

Step Hyp Ref Expression
1 3nn 
 |-  3 e. NN
2 1lt3 
 |-  1 < 3
3 3t3e9 
 |-  ( 3 x. 3 ) = 9
4 1 1 2 2 3 nprmi 
 |-  -. 9 e. Prime