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

Proof

Step Hyp Ref Expression
1 nn0cn ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℂ )
2 1 3ad2ant2 ⊢ ( ( ( 𝐴 / 2 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
3 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
4 3 a1i ⊢ ( ( ( 𝐴 / 2 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
5 2nn0 ⊢ 2 ∈ ℕ0
6 5 a1i ⊢ ( 𝐼 ∈ ℕ0 → 2 ∈ ℕ0 )
7 id ⊢ ( 𝐼 ∈ ℕ0 → 𝐼 ∈ ℕ0 )
8 6 7 nn0expcld ⊢ ( 𝐼 ∈ ℕ0 → ( 2 ↑ 𝐼 ) ∈ ℕ0 )
9 8 nn0cnd ⊢ ( 𝐼 ∈ ℕ0 → ( 2 ↑ 𝐼 ) ∈ ℂ )
10 2cnd ⊢ ( 𝐼 ∈ ℕ0 → 2 ∈ ℂ )
11 2ne0 ⊢ 2 ≠ 0
12 11 a1i ⊢ ( 𝐼 ∈ ℕ0 → 2 ≠ 0 )
13 nn0z ⊢ ( 𝐼 ∈ ℕ0 → 𝐼 ∈ ℤ )
14 10 12 13 expne0d ⊢ ( 𝐼 ∈ ℕ0 → ( 2 ↑ 𝐼 ) ≠ 0 )
15 9 14 jca ⊢ ( 𝐼 ∈ ℕ0 → ( ( 2 ↑ 𝐼 ) ∈ ℂ ∧ ( 2 ↑ 𝐼 ) ≠ 0 ) )
16 15 3ad2ant3 ⊢ ( ( ( 𝐴 / 2 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → ( ( 2 ↑ 𝐼 ) ∈ ℂ ∧ ( 2 ↑ 𝐼 ) ≠ 0 ) )
17 divdiv1 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( ( 2 ↑ 𝐼 ) ∈ ℂ ∧ ( 2 ↑ 𝐼 ) ≠ 0 ) ) → ( ( 𝐴 / 2 ) / ( 2 ↑ 𝐼 ) ) = ( 𝐴 / ( 2 · ( 2 ↑ 𝐼 ) ) ) )
18 2 4 16 17 syl3anc ⊢ ( ( ( 𝐴 / 2 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → ( ( 𝐴 / 2 ) / ( 2 ↑ 𝐼 ) ) = ( 𝐴 / ( 2 · ( 2 ↑ 𝐼 ) ) ) )
19 10 9 mulcomd ⊢ ( 𝐼 ∈ ℕ0 → ( 2 · ( 2 ↑ 𝐼 ) ) = ( ( 2 ↑ 𝐼 ) · 2 ) )
20 19 3ad2ant3 ⊢ ( ( ( 𝐴 / 2 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → ( 2 · ( 2 ↑ 𝐼 ) ) = ( ( 2 ↑ 𝐼 ) · 2 ) )
21 2cnd ⊢ ( ( ( 𝐴 / 2 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → 2 ∈ ℂ )
22 simp3 ⊢ ( ( ( 𝐴 / 2 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → 𝐼 ∈ ℕ0 )
23 21 22 expp1d ⊢ ( ( ( 𝐴 / 2 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → ( 2 ↑ ( 𝐼 + 1 ) ) = ( ( 2 ↑ 𝐼 ) · 2 ) )
24 20 23 eqtr4d ⊢ ( ( ( 𝐴 / 2 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → ( 2 · ( 2 ↑ 𝐼 ) ) = ( 2 ↑ ( 𝐼 + 1 ) ) )
25 24 oveq2d ⊢ ( ( ( 𝐴 / 2 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → ( 𝐴 / ( 2 · ( 2 ↑ 𝐼 ) ) ) = ( 𝐴 / ( 2 ↑ ( 𝐼 + 1 ) ) ) )
26 18 25 eqtr2d ⊢ ( ( ( 𝐴 / 2 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → ( 𝐴 / ( 2 ↑ ( 𝐼 + 1 ) ) ) = ( ( 𝐴 / 2 ) / ( 2 ↑ 𝐼 ) ) )
27 26 fveq2d ⊢ ( ( ( 𝐴 / 2 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝐼 + 1 ) ) ) ) = ( ⌊ ‘ ( ( 𝐴 / 2 ) / ( 2 ↑ 𝐼 ) ) ) )
28 27 oveq1d ⊢ ( ( ( 𝐴 / 2 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝐼 + 1 ) ) ) ) mod 2 ) = ( ( ⌊ ‘ ( ( 𝐴 / 2 ) / ( 2 ↑ 𝐼 ) ) ) mod 2 ) )
29 2nn ⊢ 2 ∈ ℕ
30 29 a1i ⊢ ( ( ( 𝐴 / 2 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → 2 ∈ ℕ )
31 peano2nn0 ⊢ ( 𝐼 ∈ ℕ0 → ( 𝐼 + 1 ) ∈ ℕ0 )
32 31 3ad2ant3 ⊢ ( ( ( 𝐴 / 2 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → ( 𝐼 + 1 ) ∈ ℕ0 )
33 nn0rp0 ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ( 0 [,) +∞ ) )
34 33 3ad2ant2 ⊢ ( ( ( 𝐴 / 2 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → 𝐴 ∈ ( 0 [,) +∞ ) )
35 nn0digval ⊢ ( ( 2 ∈ ℕ ∧ ( 𝐼 + 1 ) ∈ ℕ0 ∧ 𝐴 ∈ ( 0 [,) +∞ ) ) → ( ( 𝐼 + 1 ) ( digit ‘ 2 ) 𝐴 ) = ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝐼 + 1 ) ) ) ) mod 2 ) )
36 30 32 34 35 syl3anc ⊢ ( ( ( 𝐴 / 2 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → ( ( 𝐼 + 1 ) ( digit ‘ 2 ) 𝐴 ) = ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝐼 + 1 ) ) ) ) mod 2 ) )
37 nn0rp0 ⊢ ( ( 𝐴 / 2 ) ∈ ℕ0 → ( 𝐴 / 2 ) ∈ ( 0 [,) +∞ ) )
38 37 3ad2ant1 ⊢ ( ( ( 𝐴 / 2 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → ( 𝐴 / 2 ) ∈ ( 0 [,) +∞ ) )
39 nn0digval ⊢ ( ( 2 ∈ ℕ ∧ 𝐼 ∈ ℕ0 ∧ ( 𝐴 / 2 ) ∈ ( 0 [,) +∞ ) ) → ( 𝐼 ( digit ‘ 2 ) ( 𝐴 / 2 ) ) = ( ( ⌊ ‘ ( ( 𝐴 / 2 ) / ( 2 ↑ 𝐼 ) ) ) mod 2 ) )
40 30 22 38 39 syl3anc ⊢ ( ( ( 𝐴 / 2 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → ( 𝐼 ( digit ‘ 2 ) ( 𝐴 / 2 ) ) = ( ( ⌊ ‘ ( ( 𝐴 / 2 ) / ( 2 ↑ 𝐼 ) ) ) mod 2 ) )
41 28 36 40 3eqtr4d ⊢ ( ( ( 𝐴 / 2 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → ( ( 𝐼 + 1 ) ( digit ‘ 2 ) 𝐴 ) = ( 𝐼 ( digit ‘ 2 ) ( 𝐴 / 2 ) ) )