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 ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐼 ∈ ℕ0 ) → ( ( 𝐼 + 1 ) ( digit ‘ 2 ) 𝐴 ) = ( 𝐼 ( digit ‘ 2 ) ( ⌊ ‘ ( 𝐴 / 2 ) ) ) )

Proof

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