Metamath Proof Explorer

Theorem nn0sumshdig

Description: A nonnegative integer can be represented as sum of its shifted bits. (Contributed by AV, 7-Jun-2020)

Ref Expression
Assertion nn0sumshdig ⊢A∈ℕ0→A=∑k∈0..^#b ⁡ A kdigit⁡2A⁢2k

Proof

Step Hyp Ref Expression
1 blennn0elnn ⊢A∈ℕ0→#b ⁡ A ∈ ℕ
2 nn0sumshdiglem2 ⊢#b ⁡ A ∈ ℕ → ∀a∈ℕ0#b ⁡a=#b ⁡A→a=∑k∈0..^#b ⁡Akdigit⁡2a⁢2k
3 eqid ⊢#b ⁡ A = #b ⁡A
4 fveqeq2 ⊢a=A→#b ⁡ a = #b ⁡A ↔ #b ⁡A=#b ⁡A
5 id ⊢a=A→a=A
6 oveq2 ⊢a=A→kdigit⁡2a=kdigit⁡2A
7 6 oveq1d ⊢a=A→kdigit⁡2a⁢2k=kdigit⁡2A⁢2k
8 7 adantr ⊢a=A∧k∈0..^#b ⁡ A → kdigit⁡2a⁢2k=kdigit⁡2A⁢2k
9 8 sumeq2dv ⊢a=A→∑k∈0..^#b ⁡ A kdigit⁡2a⁢2k = ∑k∈0..^#b ⁡Akdigit⁡2A⁢2k
10 5 9 eqeq12d ⊢a=A→a=∑k∈0..^#b ⁡ A kdigit⁡2a⁢2k ↔ A=∑k∈0..^#b ⁡Akdigit⁡2A⁢2k
11 4 10 imbi12d ⊢a=A→#b ⁡ a = #b ⁡A → a=∑k∈0..^#b ⁡Akdigit⁡2a⁢2k ↔ #b ⁡A=#b ⁡A→A=∑k∈0..^#b ⁡Akdigit⁡2A⁢2k
12 11 rspcva ⊢A∈ℕ0∧∀a∈ℕ0#b ⁡ a = #b ⁡A → a=∑k∈0..^#b ⁡Akdigit⁡2a⁢2k → #b ⁡A=#b ⁡A→A=∑k∈0..^#b ⁡Akdigit⁡2A⁢2k
13 3 12 mpi ⊢A∈ℕ0∧∀a∈ℕ0#b ⁡ a = #b ⁡A → a=∑k∈0..^#b ⁡Akdigit⁡2a⁢2k → A=∑k∈0..^#b ⁡Akdigit⁡2A⁢2k
14 13 ex ⊢A∈ℕ0→∀a∈ℕ0#b ⁡ a = #b ⁡A → a=∑k∈0..^#b ⁡Akdigit⁡2a⁢2k → A=∑k∈0..^#b ⁡Akdigit⁡2A⁢2k
15 2 14 syl5 ⊢A∈ℕ0→#b ⁡ A ∈ ℕ → A=∑k∈0..^#b ⁡Akdigit⁡2A⁢2k
16 1 15 mpd ⊢A∈ℕ0→A=∑k∈0..^#b ⁡ A kdigit⁡2A⁢2k