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 ( 𝐴 ∈ ℕ0 → 𝐴 = Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝐴 ) · ( 2 ↑ 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 blennn0elnn ⊢ ( 𝐴 ∈ ℕ0 → ( #b ‘ 𝐴 ) ∈ ℕ )
2 nn0sumshdiglem2 ⊢ ( ( #b ‘ 𝐴 ) ∈ ℕ → ∀ 𝑎 ∈ ℕ0 ( ( #b ‘ 𝑎 ) = ( #b ‘ 𝐴 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) )
3 eqid ⊢ ( #b ‘ 𝐴 ) = ( #b ‘ 𝐴 )
4 fveqeq2 ⊢ ( 𝑎 = 𝐴 → ( ( #b ‘ 𝑎 ) = ( #b ‘ 𝐴 ) ↔ ( #b ‘ 𝐴 ) = ( #b ‘ 𝐴 ) ) )
5 id ⊢ ( 𝑎 = 𝐴 → 𝑎 = 𝐴 )
6 oveq2 ⊢ ( 𝑎 = 𝐴 → ( 𝑘 ( digit ‘ 2 ) 𝑎 ) = ( 𝑘 ( digit ‘ 2 ) 𝐴 ) )
7 6 oveq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) = ( ( 𝑘 ( digit ‘ 2 ) 𝐴 ) · ( 2 ↑ 𝑘 ) ) )
8 7 adantr ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ) → ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) = ( ( 𝑘 ( digit ‘ 2 ) 𝐴 ) · ( 2 ↑ 𝑘 ) ) )
9 8 sumeq2dv ⊢ ( 𝑎 = 𝐴 → Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝐴 ) · ( 2 ↑ 𝑘 ) ) )
10 5 9 eqeq12d ⊢ ( 𝑎 = 𝐴 → ( 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ↔ 𝐴 = Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝐴 ) · ( 2 ↑ 𝑘 ) ) ) )
11 4 10 imbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ( #b ‘ 𝑎 ) = ( #b ‘ 𝐴 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ↔ ( ( #b ‘ 𝐴 ) = ( #b ‘ 𝐴 ) → 𝐴 = Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝐴 ) · ( 2 ↑ 𝑘 ) ) ) ) )
12 11 rspcva ⊢ ( ( 𝐴 ∈ ℕ0 ∧ ∀ 𝑎 ∈ ℕ0 ( ( #b ‘ 𝑎 ) = ( #b ‘ 𝐴 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) → ( ( #b ‘ 𝐴 ) = ( #b ‘ 𝐴 ) → 𝐴 = Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝐴 ) · ( 2 ↑ 𝑘 ) ) ) )
13 3 12 mpi ⊢ ( ( 𝐴 ∈ ℕ0 ∧ ∀ 𝑎 ∈ ℕ0 ( ( #b ‘ 𝑎 ) = ( #b ‘ 𝐴 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) → 𝐴 = Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝐴 ) · ( 2 ↑ 𝑘 ) ) )
14 13 ex ⊢ ( 𝐴 ∈ ℕ0 → ( ∀ 𝑎 ∈ ℕ0 ( ( #b ‘ 𝑎 ) = ( #b ‘ 𝐴 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) → 𝐴 = Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝐴 ) · ( 2 ↑ 𝑘 ) ) ) )
15 2 14 syl5 ⊢ ( 𝐴 ∈ ℕ0 → ( ( #b ‘ 𝐴 ) ∈ ℕ → 𝐴 = Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝐴 ) · ( 2 ↑ 𝑘 ) ) ) )
16 1 15 mpd ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 = Σ 𝑘 ∈ ( 0 ..^ ( #b ‘ 𝐴 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝐴 ) · ( 2 ↑ 𝑘 ) ) )