Metamath Proof Explorer


Theorem 6nprm

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

Ref Expression
Assertion 6nprm ¬6

Proof

Step Hyp Ref Expression
1 3nn 3
2 2nn 2
3 1lt3 1<3
4 1lt2 1<2
5 3t2e6 32=6
6 1 2 3 4 5 nprmi ¬6