Metamath Proof Explorer

Theorem dec2dvds

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

Ref Expression
Hypotheses dec2dvds.1 
|- A e. NN0
dec2dvds.2 
|- B e. NN0
dec2dvds.3 
|- ( B x. 2 ) = C
dec2dvds.4 
|- D = ( C + 1 )
Assertion dec2dvds 
|- -. 2 || ; A D

Proof

Step Hyp Ref Expression
1 dec2dvds.1 
 |-  A e. NN0
2 dec2dvds.2 
 |-  B e. NN0
3 dec2dvds.3 
 |-  ( B x. 2 ) = C
4 dec2dvds.4 
 |-  D = ( C + 1 )
5 5nn0 
 |-  5 e. NN0
6 5 nn0zi 
 |-  5 e. ZZ
7 2z 
 |-  2 e. ZZ
8 dvdsmul2 
 |-  ( ( 5 e. ZZ /\ 2 e. ZZ ) -> 2 || ( 5 x. 2 ) )
9 6 7 8 mp2an 
 |-  2 || ( 5 x. 2 )
10 5t2e10 
 |-  ( 5 x. 2 ) = ; 1 0
11 9 10 breqtri 
 |-  2 || ; 1 0
12 10nn0 
 |-  ; 1 0 e. NN0
13 12 nn0zi 
 |-  ; 1 0 e. ZZ
14 1 nn0zi 
 |-  A e. ZZ
15 dvdsmultr1 
 |-  ( ( 2 e. ZZ /\ ; 1 0 e. ZZ /\ A e. ZZ ) -> ( 2 || ; 1 0 -> 2 || ( ; 1 0 x. A ) ) )
16 7 13 14 15 mp3an 
 |-  ( 2 || ; 1 0 -> 2 || ( ; 1 0 x. A ) )
17 11 16 ax-mp 
 |-  2 || ( ; 1 0 x. A )
18 2 nn0zi 
 |-  B e. ZZ
19 dvdsmul2 
 |-  ( ( B e. ZZ /\ 2 e. ZZ ) -> 2 || ( B x. 2 ) )
20 18 7 19 mp2an 
 |-  2 || ( B x. 2 )
21 20 3 breqtri 
 |-  2 || C
22 12 1 nn0mulcli 
 |-  ( ; 1 0 x. A ) e. NN0
23 22 nn0zi 
 |-  ( ; 1 0 x. A ) e. ZZ
24 2nn0 
 |-  2 e. NN0
25 2 24 nn0mulcli 
 |-  ( B x. 2 ) e. NN0
26 3 25 eqeltrri 
 |-  C e. NN0
27 26 nn0zi 
 |-  C e. ZZ
28 dvds2add 
 |-  ( ( 2 e. ZZ /\ ( ; 1 0 x. A ) e. ZZ /\ C e. ZZ ) -> ( ( 2 || ( ; 1 0 x. A ) /\ 2 || C ) -> 2 || ( ( ; 1 0 x. A ) + C ) ) )
29 7 23 27 28 mp3an 
 |-  ( ( 2 || ( ; 1 0 x. A ) /\ 2 || C ) -> 2 || ( ( ; 1 0 x. A ) + C ) )
30 17 21 29 mp2an 
 |-  2 || ( ( ; 1 0 x. A ) + C )
31 dfdec10 
 |-  ; A C = ( ( ; 1 0 x. A ) + C )
32 30 31 breqtrri 
 |-  2 || ; A C
33 1 26 deccl 
 |-  ; A C e. NN0
34 33 nn0zi 
 |-  ; A C e. ZZ
35 2nn 
 |-  2 e. NN
36 1lt2 
 |-  1 < 2
37 ndvdsp1 
 |-  ( ( ; A C e. ZZ /\ 2 e. NN /\ 1 < 2 ) -> ( 2 || ; A C -> -. 2 || ( ; A C + 1 ) ) )
38 34 35 36 37 mp3an 
 |-  ( 2 || ; A C -> -. 2 || ( ; A C + 1 ) )
39 32 38 ax-mp 
 |-  -. 2 || ( ; A C + 1 )
40 4 eqcomi 
 |-  ( C + 1 ) = D
41 eqid 
 |-  ; A C = ; A C
42 1 26 40 41 decsuc 
 |-  ( ; A C + 1 ) = ; A D
43 42 breq2i 
 |-  ( 2 || ( ; A C + 1 ) <-> 2 || ; A D )
44 39 43 mtbi 
 |-  -. 2 || ; A D