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

Metamath Proof Explorer

Theorem 8nprm

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

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

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