This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 6nprm

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

		Ref	Expression
	Assertion	6nprm	$⊢ \neg 6 \in ℙ$

Step	Hyp	Ref	Expression
1		3nn	$⊢ 3 \in ℕ$
2		2nn	$⊢ 2 \in ℕ$
3		1lt3	$⊢ 1 < 3$
4		1lt2	$⊢ 1 < 2$
5		3t2e6	$⊢ 3 \cdot 2 = 6$
6	1 2 3 4 5	nprmi	$⊢ \neg 6 \in ℙ$