Metamath Proof Explorer

Theorem nn0sumshdiglem2

Description: Lemma 2 for nn0sumshdig . (Contributed by AV, 7-Jun-2020)

Ref Expression
Assertion nn0sumshdiglem2 ( 𝐿 ∈ ℕ → ∀ 𝑎 ∈ ℕ0 ( ( #b ‘ 𝑎 ) = 𝐿 → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝐿 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 eqeq2 ⊢ ( 𝑥 = 1 → ( ( #b ‘ 𝑎 ) = 𝑥 ↔ ( #b ‘ 𝑎 ) = 1 ) )
2 oveq2 ⊢ ( 𝑥 = 1 → ( 0 ..^ 𝑥 ) = ( 0 ..^ 1 ) )
3 fzo01 ⊢ ( 0 ..^ 1 ) = { 0 }
4 2 3 eqtrdi ⊢ ( 𝑥 = 1 → ( 0 ..^ 𝑥 ) = { 0 } )
5 4 sumeq1d ⊢ ( 𝑥 = 1 → Σ 𝑘 ∈ ( 0 ..^ 𝑥 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) = Σ 𝑘 ∈ { 0 } ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) )
6 5 eqeq2d ⊢ ( 𝑥 = 1 → ( 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝑥 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ↔ 𝑎 = Σ 𝑘 ∈ { 0 } ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) )
7 1 6 imbi12d ⊢ ( 𝑥 = 1 → ( ( ( #b ‘ 𝑎 ) = 𝑥 → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝑥 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ↔ ( ( #b ‘ 𝑎 ) = 1 → 𝑎 = Σ 𝑘 ∈ { 0 } ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) )
8 7 ralbidv ⊢ ( 𝑥 = 1 → ( ∀ 𝑎 ∈ ℕ0 ( ( #b ‘ 𝑎 ) = 𝑥 → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝑥 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ↔ ∀ 𝑎 ∈ ℕ0 ( ( #b ‘ 𝑎 ) = 1 → 𝑎 = Σ 𝑘 ∈ { 0 } ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) )
9 eqeq2 ⊢ ( 𝑥 = 𝑦 → ( ( #b ‘ 𝑎 ) = 𝑥 ↔ ( #b ‘ 𝑎 ) = 𝑦 ) )
10 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 0 ..^ 𝑥 ) = ( 0 ..^ 𝑦 ) )
11 10 sumeq1d ⊢ ( 𝑥 = 𝑦 → Σ 𝑘 ∈ ( 0 ..^ 𝑥 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) )
12 11 eqeq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝑥 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ↔ 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) )
13 9 12 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( #b ‘ 𝑎 ) = 𝑥 → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝑥 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ↔ ( ( #b ‘ 𝑎 ) = 𝑦 → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) )
14 13 ralbidv ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑎 ∈ ℕ0 ( ( #b ‘ 𝑎 ) = 𝑥 → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝑥 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ↔ ∀ 𝑎 ∈ ℕ0 ( ( #b ‘ 𝑎 ) = 𝑦 → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) )
15 eqeq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( #b ‘ 𝑎 ) = 𝑥 ↔ ( #b ‘ 𝑎 ) = ( 𝑦 + 1 ) ) )
16 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 0 ..^ 𝑥 ) = ( 0 ..^ ( 𝑦 + 1 ) ) )
17 16 sumeq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → Σ 𝑘 ∈ ( 0 ..^ 𝑥 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) )
18 17 eqeq2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝑥 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ↔ 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) )
19 15 18 imbi12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( #b ‘ 𝑎 ) = 𝑥 → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝑥 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ↔ ( ( #b ‘ 𝑎 ) = ( 𝑦 + 1 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) )
20 19 ralbidv ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ∀ 𝑎 ∈ ℕ0 ( ( #b ‘ 𝑎 ) = 𝑥 → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝑥 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ↔ ∀ 𝑎 ∈ ℕ0 ( ( #b ‘ 𝑎 ) = ( 𝑦 + 1 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) )
21 eqeq2 ⊢ ( 𝑥 = 𝐿 → ( ( #b ‘ 𝑎 ) = 𝑥 ↔ ( #b ‘ 𝑎 ) = 𝐿 ) )
22 oveq2 ⊢ ( 𝑥 = 𝐿 → ( 0 ..^ 𝑥 ) = ( 0 ..^ 𝐿 ) )
23 22 sumeq1d ⊢ ( 𝑥 = 𝐿 → Σ 𝑘 ∈ ( 0 ..^ 𝑥 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ..^ 𝐿 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) )
24 23 eqeq2d ⊢ ( 𝑥 = 𝐿 → ( 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝑥 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ↔ 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝐿 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) )
25 21 24 imbi12d ⊢ ( 𝑥 = 𝐿 → ( ( ( #b ‘ 𝑎 ) = 𝑥 → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝑥 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ↔ ( ( #b ‘ 𝑎 ) = 𝐿 → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝐿 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) )
26 25 ralbidv ⊢ ( 𝑥 = 𝐿 → ( ∀ 𝑎 ∈ ℕ0 ( ( #b ‘ 𝑎 ) = 𝑥 → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝑥 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ↔ ∀ 𝑎 ∈ ℕ0 ( ( #b ‘ 𝑎 ) = 𝐿 → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝐿 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) )
27 0cnd ⊢ ( 𝑎 ∈ ℕ0 → 0 ∈ ℂ )
28 2nn ⊢ 2 ∈ ℕ
29 28 a1i ⊢ ( 𝑎 ∈ ℕ0 → 2 ∈ ℕ )
30 0zd ⊢ ( 𝑎 ∈ ℕ0 → 0 ∈ ℤ )
31 nn0rp0 ⊢ ( 𝑎 ∈ ℕ0 → 𝑎 ∈ ( 0 [,) +∞ ) )
32 digvalnn0 ⊢ ( ( 2 ∈ ℕ ∧ 0 ∈ ℤ ∧ 𝑎 ∈ ( 0 [,) +∞ ) ) → ( 0 ( digit ‘ 2 ) 𝑎 ) ∈ ℕ0 )
33 29 30 31 32 syl3anc ⊢ ( 𝑎 ∈ ℕ0 → ( 0 ( digit ‘ 2 ) 𝑎 ) ∈ ℕ0 )
34 33 nn0cnd ⊢ ( 𝑎 ∈ ℕ0 → ( 0 ( digit ‘ 2 ) 𝑎 ) ∈ ℂ )
35 1cnd ⊢ ( 𝑎 ∈ ℕ0 → 1 ∈ ℂ )
36 34 35 mulcld ⊢ ( 𝑎 ∈ ℕ0 → ( ( 0 ( digit ‘ 2 ) 𝑎 ) · 1 ) ∈ ℂ )
37 27 36 jca ⊢ ( 𝑎 ∈ ℕ0 → ( 0 ∈ ℂ ∧ ( ( 0 ( digit ‘ 2 ) 𝑎 ) · 1 ) ∈ ℂ ) )
38 37 adantr ⊢ ( ( 𝑎 ∈ ℕ0 ∧ ( #b ‘ 𝑎 ) = 1 ) → ( 0 ∈ ℂ ∧ ( ( 0 ( digit ‘ 2 ) 𝑎 ) · 1 ) ∈ ℂ ) )
39 oveq1 ⊢ ( 𝑘 = 0 → ( 𝑘 ( digit ‘ 2 ) 𝑎 ) = ( 0 ( digit ‘ 2 ) 𝑎 ) )
40 oveq2 ⊢ ( 𝑘 = 0 → ( 2 ↑ 𝑘 ) = ( 2 ↑ 0 ) )
41 2cn ⊢ 2 ∈ ℂ
42 exp0 ⊢ ( 2 ∈ ℂ → ( 2 ↑ 0 ) = 1 )
43 41 42 ax-mp ⊢ ( 2 ↑ 0 ) = 1
44 40 43 eqtrdi ⊢ ( 𝑘 = 0 → ( 2 ↑ 𝑘 ) = 1 )
45 39 44 oveq12d ⊢ ( 𝑘 = 0 → ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) = ( ( 0 ( digit ‘ 2 ) 𝑎 ) · 1 ) )
46 45 sumsn ⊢ ( ( 0 ∈ ℂ ∧ ( ( 0 ( digit ‘ 2 ) 𝑎 ) · 1 ) ∈ ℂ ) → Σ 𝑘 ∈ { 0 } ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) = ( ( 0 ( digit ‘ 2 ) 𝑎 ) · 1 ) )
47 38 46 syl ⊢ ( ( 𝑎 ∈ ℕ0 ∧ ( #b ‘ 𝑎 ) = 1 ) → Σ 𝑘 ∈ { 0 } ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) = ( ( 0 ( digit ‘ 2 ) 𝑎 ) · 1 ) )
48 34 adantr ⊢ ( ( 𝑎 ∈ ℕ0 ∧ ( #b ‘ 𝑎 ) = 1 ) → ( 0 ( digit ‘ 2 ) 𝑎 ) ∈ ℂ )
49 48 mulid1d ⊢ ( ( 𝑎 ∈ ℕ0 ∧ ( #b ‘ 𝑎 ) = 1 ) → ( ( 0 ( digit ‘ 2 ) 𝑎 ) · 1 ) = ( 0 ( digit ‘ 2 ) 𝑎 ) )
50 blen1b ⊢ ( 𝑎 ∈ ℕ0 → ( ( #b ‘ 𝑎 ) = 1 ↔ ( 𝑎 = 0 ∨ 𝑎 = 1 ) ) )
51 50 biimpa ⊢ ( ( 𝑎 ∈ ℕ0 ∧ ( #b ‘ 𝑎 ) = 1 ) → ( 𝑎 = 0 ∨ 𝑎 = 1 ) )
52 vex ⊢ 𝑎 ∈ V
53 52 elpr ⊢ ( 𝑎 ∈ { 0 , 1 } ↔ ( 𝑎 = 0 ∨ 𝑎 = 1 ) )
54 51 53 sylibr ⊢ ( ( 𝑎 ∈ ℕ0 ∧ ( #b ‘ 𝑎 ) = 1 ) → 𝑎 ∈ { 0 , 1 } )
55 0dig2pr01 ⊢ ( 𝑎 ∈ { 0 , 1 } → ( 0 ( digit ‘ 2 ) 𝑎 ) = 𝑎 )
56 54 55 syl ⊢ ( ( 𝑎 ∈ ℕ0 ∧ ( #b ‘ 𝑎 ) = 1 ) → ( 0 ( digit ‘ 2 ) 𝑎 ) = 𝑎 )
57 47 49 56 3eqtrrd ⊢ ( ( 𝑎 ∈ ℕ0 ∧ ( #b ‘ 𝑎 ) = 1 ) → 𝑎 = Σ 𝑘 ∈ { 0 } ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) )
58 57 ex ⊢ ( 𝑎 ∈ ℕ0 → ( ( #b ‘ 𝑎 ) = 1 → 𝑎 = Σ 𝑘 ∈ { 0 } ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) )
59 58 rgen ⊢ ∀ 𝑎 ∈ ℕ0 ( ( #b ‘ 𝑎 ) = 1 → 𝑎 = Σ 𝑘 ∈ { 0 } ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) )
60 nn0sumshdiglem1 ⊢ ( 𝑦 ∈ ℕ → ( ∀ 𝑎 ∈ ℕ0 ( ( #b ‘ 𝑎 ) = 𝑦 → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) → ∀ 𝑎 ∈ ℕ0 ( ( #b ‘ 𝑎 ) = ( 𝑦 + 1 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) )
61 8 14 20 26 59 60 nnind ⊢ ( 𝐿 ∈ ℕ → ∀ 𝑎 ∈ ℕ0 ( ( #b ‘ 𝑎 ) = 𝐿 → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝐿 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) )