Metamath Proof Explorer

Theorem dec5nprm

Description: A decimal number greater than 10 and ending with five is not a prime number. (Contributed by Mario Carneiro, 19-Apr-2015)

Ref Expression
Hypothesis dec5nprm.1 
|- A e. NN
Assertion dec5nprm 
|- -. ; A 5 e. Prime

Proof

Step Hyp Ref Expression
1 dec5nprm.1 
 |-  A e. NN
2 2nn 
 |-  2 e. NN
3 2 1 nnmulcli 
 |-  ( 2 x. A ) e. NN
4 peano2nn 
 |-  ( ( 2 x. A ) e. NN -> ( ( 2 x. A ) + 1 ) e. NN )
5 3 4 ax-mp 
 |-  ( ( 2 x. A ) + 1 ) e. NN
6 5nn 
 |-  5 e. NN
7 1nn0 
 |-  1 e. NN0
8 1lt2 
 |-  1 < 2
9 2 1 7 7 8 numlti 
 |-  1 < ( ( 2 x. A ) + 1 )
10 1lt5 
 |-  1 < 5
11 2 nncni 
 |-  2 e. CC
12 1 nncni 
 |-  A e. CC
13 5cn 
 |-  5 e. CC
14 11 12 13 mul32i 
 |-  ( ( 2 x. A ) x. 5 ) = ( ( 2 x. 5 ) x. A )
15 5t2e10 
 |-  ( 5 x. 2 ) = ; 1 0
16 13 11 15 mulcomli 
 |-  ( 2 x. 5 ) = ; 1 0
17 16 oveq1i 
 |-  ( ( 2 x. 5 ) x. A ) = ( ; 1 0 x. A )
18 14 17 eqtri 
 |-  ( ( 2 x. A ) x. 5 ) = ( ; 1 0 x. A )
19 13 mullidi 
 |-  ( 1 x. 5 ) = 5
20 18 19 oveq12i 
 |-  ( ( ( 2 x. A ) x. 5 ) + ( 1 x. 5 ) ) = ( ( ; 1 0 x. A ) + 5 )
21 3 nncni 
 |-  ( 2 x. A ) e. CC
22 ax-1cn 
 |-  1 e. CC
23 21 22 13 adddiri 
 |-  ( ( ( 2 x. A ) + 1 ) x. 5 ) = ( ( ( 2 x. A ) x. 5 ) + ( 1 x. 5 ) )
24 dfdec10 
 |-  ; A 5 = ( ( ; 1 0 x. A ) + 5 )
25 20 23 24 3eqtr4i 
 |-  ( ( ( 2 x. A ) + 1 ) x. 5 ) = ; A 5
26 5 6 9 10 25 nprmi 
 |-  -. ; A 5 e. Prime