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) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026)

Ref Expression
Assertion 10nprm ¬ 1 0 ∈ ℙ

Proof

Step Hyp Ref Expression
1 1nn 1 ∈ ℕ
2 0nn0 0 ∈ ℕ0
3 2cn 2 ∈ ℂ
4 3 mul02i ( 0 · 2 ) = 0
5 1 2 4 dec2nprm ¬ 1 0 ∈ ℙ