Metamath Proof Explorer

Theorem dec2nprm

Description: Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015)

Ref Expression
Hypotheses dec5nprm.1 
|- A e. NN
dec2nprm.2 
|- B e. NN0
dec2nprm.3 
|- ( B x. 2 ) = C
Assertion dec2nprm 
|- -. ; A C e. Prime

Proof

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