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 
|- -. ; 1 0 e. Prime

Proof

Step Hyp Ref Expression
1 5nn 
 |-  5 e. NN
2 2nn 
 |-  2 e. NN
3 1lt5 
 |-  1 < 5
4 1lt2 
 |-  1 < 2
5 5t2e10 
 |-  ( 5 x. 2 ) = ; 1 0
6 1 2 3 4 5 nprmi 
 |-  -. ; 1 0 e. Prime