Metamath Proof Explorer

Theorem 8nprm

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

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

Proof

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