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 2 I 0 I + 1 digit 2 A = I digit 2 A 2

Proof

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