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

Metamath Proof Explorer

Theorem 10nprm

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

Ref Expression
Assertion 10nprm ⊢ ¬ 10 ∈ ℙ

Proof

Step Hyp Ref Expression
1 5nn ⊢ 5 ∈ ℕ
2 2nn ⊢ 2 ∈ ℕ
3 1lt5 ⊢ 1 < 5
4 1lt2 ⊢ 1 < 2
5 5t2e10 ⊢ 5 ⋅ 2 = 10
6 1 2 3 4 5 nprmi ⊢ ¬ 10 ∈ ℙ