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 e. Prime

Proof

Step Hyp Ref Expression
1 1nn
 |-  1 e. NN
2 0nn0
 |-  0 e. NN0
3 2cn
 |-  2 e. CC
4 3 mul02i
 |-  ( 0 x. 2 ) = 0
5 1 2 4 dec2nprm
 |-  -. ; 1 0 e. Prime