Metamath Proof Explorer

Theorem dignn0ehalf

Description: The digits of the half of an even nonnegative integer are the digits of the integer shifted by 1. (Contributed by AV, 3-Jun-2010)

Ref Expression
Assertion dignn0ehalf 
|- ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> ( ( I + 1 ) ( digit ` 2 ) A ) = ( I ( digit ` 2 ) ( A / 2 ) ) )

Proof

Step Hyp Ref Expression
1 nn0cn 
 |-  ( A e. NN0 -> A e. CC )
2 1 3ad2ant2 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> A e. CC )
3 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
4 3 a1i 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> ( 2 e. CC /\ 2 =/= 0 ) )
5 2nn0 
 |-  2 e. NN0
6 5 a1i 
 |-  ( I e. NN0 -> 2 e. NN0 )
7 id 
 |-  ( I e. NN0 -> I e. NN0 )
8 6 7 nn0expcld 
 |-  ( I e. NN0 -> ( 2 ^ I ) e. NN0 )
9 8 nn0cnd 
 |-  ( I e. NN0 -> ( 2 ^ I ) e. CC )
10 2cnd 
 |-  ( I e. NN0 -> 2 e. CC )
11 2ne0 
 |-  2 =/= 0
12 11 a1i 
 |-  ( I e. NN0 -> 2 =/= 0 )
13 nn0z 
 |-  ( I e. NN0 -> I e. ZZ )
14 10 12 13 expne0d 
 |-  ( I e. NN0 -> ( 2 ^ I ) =/= 0 )
15 9 14 jca 
 |-  ( I e. NN0 -> ( ( 2 ^ I ) e. CC /\ ( 2 ^ I ) =/= 0 ) )
16 15 3ad2ant3 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> ( ( 2 ^ I ) e. CC /\ ( 2 ^ I ) =/= 0 ) )
17 divdiv1 
 |-  ( ( A e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( ( 2 ^ I ) e. CC /\ ( 2 ^ I ) =/= 0 ) ) -> ( ( A / 2 ) / ( 2 ^ I ) ) = ( A / ( 2 x. ( 2 ^ I ) ) ) )
18 2 4 16 17 syl3anc 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> ( ( A / 2 ) / ( 2 ^ I ) ) = ( A / ( 2 x. ( 2 ^ I ) ) ) )
19 10 9 mulcomd 
 |-  ( I e. NN0 -> ( 2 x. ( 2 ^ I ) ) = ( ( 2 ^ I ) x. 2 ) )
20 19 3ad2ant3 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> ( 2 x. ( 2 ^ I ) ) = ( ( 2 ^ I ) x. 2 ) )
21 2cnd 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> 2 e. CC )
22 simp3 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> I e. NN0 )
23 21 22 expp1d 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> ( 2 ^ ( I + 1 ) ) = ( ( 2 ^ I ) x. 2 ) )
24 20 23 eqtr4d 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> ( 2 x. ( 2 ^ I ) ) = ( 2 ^ ( I + 1 ) ) )
25 24 oveq2d 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> ( A / ( 2 x. ( 2 ^ I ) ) ) = ( A / ( 2 ^ ( I + 1 ) ) ) )
26 18 25 eqtr2d 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> ( A / ( 2 ^ ( I + 1 ) ) ) = ( ( A / 2 ) / ( 2 ^ I ) ) )
27 26 fveq2d 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> ( |_ ` ( A / ( 2 ^ ( I + 1 ) ) ) ) = ( |_ ` ( ( A / 2 ) / ( 2 ^ I ) ) ) )
28 27 oveq1d 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> ( ( |_ ` ( A / ( 2 ^ ( I + 1 ) ) ) ) mod 2 ) = ( ( |_ ` ( ( A / 2 ) / ( 2 ^ I ) ) ) mod 2 ) )
29 2nn 
 |-  2 e. NN
30 29 a1i 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> 2 e. NN )
31 peano2nn0 
 |-  ( I e. NN0 -> ( I + 1 ) e. NN0 )
32 31 3ad2ant3 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> ( I + 1 ) e. NN0 )
33 nn0rp0 
 |-  ( A e. NN0 -> A e. ( 0 [,) +oo ) )
34 33 3ad2ant2 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> A e. ( 0 [,) +oo ) )
35 nn0digval 
 |-  ( ( 2 e. NN /\ ( I + 1 ) e. NN0 /\ A e. ( 0 [,) +oo ) ) -> ( ( I + 1 ) ( digit ` 2 ) A ) = ( ( |_ ` ( A / ( 2 ^ ( I + 1 ) ) ) ) mod 2 ) )
36 30 32 34 35 syl3anc 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> ( ( I + 1 ) ( digit ` 2 ) A ) = ( ( |_ ` ( A / ( 2 ^ ( I + 1 ) ) ) ) mod 2 ) )
37 nn0rp0 
 |-  ( ( A / 2 ) e. NN0 -> ( A / 2 ) e. ( 0 [,) +oo ) )
38 37 3ad2ant1 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> ( A / 2 ) e. ( 0 [,) +oo ) )
39 nn0digval 
 |-  ( ( 2 e. NN /\ I e. NN0 /\ ( A / 2 ) e. ( 0 [,) +oo ) ) -> ( I ( digit ` 2 ) ( A / 2 ) ) = ( ( |_ ` ( ( A / 2 ) / ( 2 ^ I ) ) ) mod 2 ) )
40 30 22 38 39 syl3anc 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> ( I ( digit ` 2 ) ( A / 2 ) ) = ( ( |_ ` ( ( A / 2 ) / ( 2 ^ I ) ) ) mod 2 ) )
41 28 36 40 3eqtr4d 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> ( ( I + 1 ) ( digit ` 2 ) A ) = ( I ( digit ` 2 ) ( A / 2 ) ) )