Theorem 9nprm

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

	Ref	Expression
Assertion	9nprm	⊢ ¬ 9 ∈ ℙ

Proof

Step	Hyp	Ref	Expression
1		3nn	⊢ 3 ∈ ℕ
2		1lt3	⊢ 1 < 3
3		3t3e9	⊢ ( 3 · 3 ) = 9
4	1 1 2 2 3	nprmi	⊢ ¬ 9 ∈ ℙ