Theorem 9nprm

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

	Ref	Expression
Assertion	9nprm	$$⊢\neg 9\in \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		3nn	$$⊢3\in \mathbb{N}$$
2		1lt3	$$⊢1<3$$
3		3t3e9	$$⊢3\cdot 3=9$$
4	1 1 2 2 3	nprmi	$$⊢\neg 9\in \mathbb{P}$$