Metamath Proof Explorer

Theorem dignn0flhalf

Description: The digits of the rounded half of a nonnegative integer are the digits of the integer shifted by 1. (Contributed by AV, 7-Jun-2010)

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

Proof

Step Hyp Ref Expression
1 eluzge2nn0 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. NN0 )
2 nn0eo 
 |-  ( A e. NN0 -> ( ( A / 2 ) e. NN0 \/ ( ( A + 1 ) / 2 ) e. NN0 ) )
3 1 2 syl 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A / 2 ) e. NN0 \/ ( ( A + 1 ) / 2 ) e. NN0 ) )
4 dignn0ehalf 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> ( ( I + 1 ) ( digit ` 2 ) A ) = ( I ( digit ` 2 ) ( A / 2 ) ) )
5 1 4 syl3an2 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ I e. NN0 ) -> ( ( I + 1 ) ( digit ` 2 ) A ) = ( I ( digit ` 2 ) ( A / 2 ) ) )
6 eluzelz 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. ZZ )
7 nn0z 
 |-  ( ( A / 2 ) e. NN0 -> ( A / 2 ) e. ZZ )
8 zefldiv2 
 |-  ( ( A e. ZZ /\ ( A / 2 ) e. ZZ ) -> ( |_ ` ( A / 2 ) ) = ( A / 2 ) )
9 6 7 8 syl2anr 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( |_ ` ( A / 2 ) ) = ( A / 2 ) )
10 9 eqcomd 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( A / 2 ) = ( |_ ` ( A / 2 ) ) )
11 10 3adant3 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ I e. NN0 ) -> ( A / 2 ) = ( |_ ` ( A / 2 ) ) )
12 11 oveq2d 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ I e. NN0 ) -> ( I ( digit ` 2 ) ( A / 2 ) ) = ( I ( digit ` 2 ) ( |_ ` ( A / 2 ) ) ) )
13 5 12 eqtrd 
 |-  ( ( ( A / 2 ) e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ I e. NN0 ) -> ( ( I + 1 ) ( digit ` 2 ) A ) = ( I ( digit ` 2 ) ( |_ ` ( A / 2 ) ) ) )
14 13 3exp 
 |-  ( ( A / 2 ) e. NN0 -> ( A e. ( ZZ>= ` 2 ) -> ( I e. NN0 -> ( ( I + 1 ) ( digit ` 2 ) A ) = ( I ( digit ` 2 ) ( |_ ` ( A / 2 ) ) ) ) ) )
15 6 3ad2ant2 
 |-  ( ( ( ( A + 1 ) / 2 ) e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ I e. NN0 ) -> A e. ZZ )
16 simp2 
 |-  ( ( ( ( A + 1 ) / 2 ) e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ I e. NN0 ) -> A e. ( ZZ>= ` 2 ) )
17 simp1 
 |-  ( ( ( ( A + 1 ) / 2 ) e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ I e. NN0 ) -> ( ( A + 1 ) / 2 ) e. NN0 )
18 nno 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( ( A + 1 ) / 2 ) e. NN0 ) -> ( ( A - 1 ) / 2 ) e. NN )
19 16 17 18 syl2anc 
 |-  ( ( ( ( A + 1 ) / 2 ) e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ I e. NN0 ) -> ( ( A - 1 ) / 2 ) e. NN )
20 simp3 
 |-  ( ( ( ( A + 1 ) / 2 ) e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ I e. NN0 ) -> I e. NN0 )
21 dignn0flhalflem2 
 |-  ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ I e. NN0 ) -> ( |_ ` ( A / ( 2 ^ ( I + 1 ) ) ) ) = ( |_ ` ( ( |_ ` ( A / 2 ) ) / ( 2 ^ I ) ) ) )
22 15 19 20 21 syl3anc 
 |-  ( ( ( ( A + 1 ) / 2 ) e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ I e. NN0 ) -> ( |_ ` ( A / ( 2 ^ ( I + 1 ) ) ) ) = ( |_ ` ( ( |_ ` ( A / 2 ) ) / ( 2 ^ I ) ) ) )
23 22 oveq1d 
 |-  ( ( ( ( A + 1 ) / 2 ) e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ I e. NN0 ) -> ( ( |_ ` ( A / ( 2 ^ ( I + 1 ) ) ) ) mod 2 ) = ( ( |_ ` ( ( |_ ` ( A / 2 ) ) / ( 2 ^ I ) ) ) mod 2 ) )
24 2nn 
 |-  2 e. NN
25 24 a1i 
 |-  ( ( ( ( A + 1 ) / 2 ) e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ I e. NN0 ) -> 2 e. NN )
26 peano2nn0 
 |-  ( I e. NN0 -> ( I + 1 ) e. NN0 )
27 26 3ad2ant3 
 |-  ( ( ( ( A + 1 ) / 2 ) e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ I e. NN0 ) -> ( I + 1 ) e. NN0 )
28 nn0rp0 
 |-  ( A e. NN0 -> A e. ( 0 [,) +oo ) )
29 1 28 syl 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. ( 0 [,) +oo ) )
30 29 3ad2ant2 
 |-  ( ( ( ( A + 1 ) / 2 ) e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ I e. NN0 ) -> A e. ( 0 [,) +oo ) )
31 nn0digval 
 |-  ( ( 2 e. NN /\ ( I + 1 ) e. NN0 /\ A e. ( 0 [,) +oo ) ) -> ( ( I + 1 ) ( digit ` 2 ) A ) = ( ( |_ ` ( A / ( 2 ^ ( I + 1 ) ) ) ) mod 2 ) )
32 25 27 30 31 syl3anc 
 |-  ( ( ( ( A + 1 ) / 2 ) e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ I e. NN0 ) -> ( ( I + 1 ) ( digit ` 2 ) A ) = ( ( |_ ` ( A / ( 2 ^ ( I + 1 ) ) ) ) mod 2 ) )
33 eluzelre 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. RR )
34 33 rehalfcld 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A / 2 ) e. RR )
35 1 nn0ge0d 
 |-  ( A e. ( ZZ>= ` 2 ) -> 0 <_ A )
36 2re 
 |-  2 e. RR
37 2pos 
 |-  0 < 2
38 36 37 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
39 38 a1i 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( 2 e. RR /\ 0 < 2 ) )
40 divge0 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 <_ ( A / 2 ) )
41 33 35 39 40 syl21anc 
 |-  ( A e. ( ZZ>= ` 2 ) -> 0 <_ ( A / 2 ) )
42 flge0nn0 
 |-  ( ( ( A / 2 ) e. RR /\ 0 <_ ( A / 2 ) ) -> ( |_ ` ( A / 2 ) ) e. NN0 )
43 34 41 42 syl2anc 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( |_ ` ( A / 2 ) ) e. NN0 )
44 43 3ad2ant2 
 |-  ( ( ( ( A + 1 ) / 2 ) e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ I e. NN0 ) -> ( |_ ` ( A / 2 ) ) e. NN0 )
45 nn0rp0 
 |-  ( ( |_ ` ( A / 2 ) ) e. NN0 -> ( |_ ` ( A / 2 ) ) e. ( 0 [,) +oo ) )
46 44 45 syl 
 |-  ( ( ( ( A + 1 ) / 2 ) e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ I e. NN0 ) -> ( |_ ` ( A / 2 ) ) e. ( 0 [,) +oo ) )
47 nn0digval 
 |-  ( ( 2 e. NN /\ I e. NN0 /\ ( |_ ` ( A / 2 ) ) e. ( 0 [,) +oo ) ) -> ( I ( digit ` 2 ) ( |_ ` ( A / 2 ) ) ) = ( ( |_ ` ( ( |_ ` ( A / 2 ) ) / ( 2 ^ I ) ) ) mod 2 ) )
48 25 20 46 47 syl3anc 
 |-  ( ( ( ( A + 1 ) / 2 ) e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ I e. NN0 ) -> ( I ( digit ` 2 ) ( |_ ` ( A / 2 ) ) ) = ( ( |_ ` ( ( |_ ` ( A / 2 ) ) / ( 2 ^ I ) ) ) mod 2 ) )
49 23 32 48 3eqtr4d 
 |-  ( ( ( ( A + 1 ) / 2 ) e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ I e. NN0 ) -> ( ( I + 1 ) ( digit ` 2 ) A ) = ( I ( digit ` 2 ) ( |_ ` ( A / 2 ) ) ) )
50 49 3exp 
 |-  ( ( ( A + 1 ) / 2 ) e. NN0 -> ( A e. ( ZZ>= ` 2 ) -> ( I e. NN0 -> ( ( I + 1 ) ( digit ` 2 ) A ) = ( I ( digit ` 2 ) ( |_ ` ( A / 2 ) ) ) ) ) )
51 14 50 jaoi 
 |-  ( ( ( A / 2 ) e. NN0 \/ ( ( A + 1 ) / 2 ) e. NN0 ) -> ( A e. ( ZZ>= ` 2 ) -> ( I e. NN0 -> ( ( I + 1 ) ( digit ` 2 ) A ) = ( I ( digit ` 2 ) ( |_ ` ( A / 2 ) ) ) ) ) )
52 3 51 mpcom 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( I e. NN0 -> ( ( I + 1 ) ( digit ` 2 ) A ) = ( I ( digit ` 2 ) ( |_ ` ( A / 2 ) ) ) ) )
53 52 imp 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ I e. NN0 ) -> ( ( I + 1 ) ( digit ` 2 ) A ) = ( I ( digit ` 2 ) ( |_ ` ( A / 2 ) ) ) )