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

Metamath Proof Explorer

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 ∈ ℙ