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 k digit ⁡ 2 A ⁢ 2 k

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 ⁡ A k digit ⁡ 2 a ⁢ 2 k
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 → k digit ⁡ 2 a = k digit ⁡ 2 A
7 6 oveq1d ⊢ a = A → k digit ⁡ 2 a ⁢ 2 k = k digit ⁡ 2 A ⁢ 2 k
8 7 adantr ⊢ a = A ∧ k ∈ 0 ..^ # b ⁡ A → k digit ⁡ 2 a ⁢ 2 k = k digit ⁡ 2 A ⁢ 2 k
9 8 sumeq2dv ⊢ a = A → ∑ k ∈ 0 ..^ # b ⁡ A k digit ⁡ 2 a ⁢ 2 k = ∑ k ∈ 0 ..^ # b ⁡ A k digit ⁡ 2 A ⁢ 2 k
10 5 9 eqeq12d ⊢ a = A → a = ∑ k ∈ 0 ..^ # b ⁡ A k digit ⁡ 2 a ⁢ 2 k ↔ A = ∑ k ∈ 0 ..^ # b ⁡ A k digit ⁡ 2 A ⁢ 2 k
11 4 10 imbi12d ⊢ a = A → # b ⁡ a = # b ⁡ A → a = ∑ k ∈ 0 ..^ # b ⁡ A k digit ⁡ 2 a ⁢ 2 k ↔ # b ⁡ A = # b ⁡ A → A = ∑ k ∈ 0 ..^ # b ⁡ A k digit ⁡ 2 A ⁢ 2 k
12 11 rspcva ⊢ A ∈ ℕ 0 ∧ ∀ a ∈ ℕ 0 # b ⁡ a = # b ⁡ A → a = ∑ k ∈ 0 ..^ # b ⁡ A k digit ⁡ 2 a ⁢ 2 k → # b ⁡ A = # b ⁡ A → A = ∑ k ∈ 0 ..^ # b ⁡ A k digit ⁡ 2 A ⁢ 2 k
13 3 12 mpi ⊢ A ∈ ℕ 0 ∧ ∀ a ∈ ℕ 0 # b ⁡ a = # b ⁡ A → a = ∑ k ∈ 0 ..^ # b ⁡ A k digit ⁡ 2 a ⁢ 2 k → A = ∑ k ∈ 0 ..^ # b ⁡ A k digit ⁡ 2 A ⁢ 2 k
14 13 ex ⊢ A ∈ ℕ 0 → ∀ a ∈ ℕ 0 # b ⁡ a = # b ⁡ A → a = ∑ k ∈ 0 ..^ # b ⁡ A k digit ⁡ 2 a ⁢ 2 k → A = ∑ k ∈ 0 ..^ # b ⁡ A k digit ⁡ 2 A ⁢ 2 k
15 2 14 syl5 ⊢ A ∈ ℕ 0 → # b ⁡ A ∈ ℕ → A = ∑ k ∈ 0 ..^ # b ⁡ A k digit ⁡ 2 A ⁢ 2 k
16 1 15 mpd ⊢ A ∈ ℕ 0 → A = ∑ k ∈ 0 ..^ # b ⁡ A k digit ⁡ 2 A ⁢ 2 k