Metamath Proof Explorer

Theorem 6nprm

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

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

Proof

Step Hyp Ref Expression
1 3nn 
 |-  3 e. NN
2 2nn 
 |-  2 e. NN
3 1lt3 
 |-  1 < 3
4 1lt2 
 |-  1 < 2
5 3t2e6 
 |-  ( 3 x. 2 ) = 6
6 1 2 3 4 5 nprmi 
 |-  -. 6 e. Prime