Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nn0sumshdiglemA Structured version   Visualization version   GIF version

Theorem nn0sumshdiglemA 43085
Description: Lemma for nn0sumshdig 43089 (induction step, even multiplier). (Contributed by AV, 3-Jun-2020.)
Assertion
Ref Expression
nn0sumshdiglemA (((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ) ∧ 𝑦 ∈ ℕ) → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
Distinct variable group:   𝑘,𝑎,𝑥,𝑦

Proof of Theorem nn0sumshdiglemA
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 nnnn0 11548 . . . 4 ((𝑎 / 2) ∈ ℕ → (𝑎 / 2) ∈ ℕ0)
2 blennn0em1 43057 . . . 4 ((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ0) → (#b‘(𝑎 / 2)) = ((#b𝑎) − 1))
31, 2sylan2 586 . . 3 ((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ) → (#b‘(𝑎 / 2)) = ((#b𝑎) − 1))
4 fveqeq2 6386 . . . . . . . . . . 11 (𝑥 = (𝑎 / 2) → ((#b𝑥) = 𝑦 ↔ (#b‘(𝑎 / 2)) = 𝑦))
5 id 22 . . . . . . . . . . . 12 (𝑥 = (𝑎 / 2) → 𝑥 = (𝑎 / 2))
6 oveq2 6852 . . . . . . . . . . . . . . 15 (𝑥 = (𝑎 / 2) → (𝑘(digit‘2)𝑥) = (𝑘(digit‘2)(𝑎 / 2)))
76oveq1d 6859 . . . . . . . . . . . . . 14 (𝑥 = (𝑎 / 2) → ((𝑘(digit‘2)𝑥) · (2↑𝑘)) = ((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)))
87adantr 472 . . . . . . . . . . . . 13 ((𝑥 = (𝑎 / 2) ∧ 𝑘 ∈ (0..^𝑦)) → ((𝑘(digit‘2)𝑥) · (2↑𝑘)) = ((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)))
98sumeq2dv 14721 . . . . . . . . . . . 12 (𝑥 = (𝑎 / 2) → Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)))
105, 9eqeq12d 2780 . . . . . . . . . . 11 (𝑥 = (𝑎 / 2) → (𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)) ↔ (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))))
114, 10imbi12d 335 . . . . . . . . . 10 (𝑥 = (𝑎 / 2) → (((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) ↔ ((#b‘(𝑎 / 2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)))))
1211rspcva 3460 . . . . . . . . 9 (((𝑎 / 2) ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → ((#b‘(𝑎 / 2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))))
13 simpr 477 . . . . . . . . . . . . . . . . 17 ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) → (#b𝑎) = (𝑦 + 1))
1413oveq1d 6859 . . . . . . . . . . . . . . . 16 ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) → ((#b𝑎) − 1) = ((𝑦 + 1) − 1))
15 nncn 11285 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
16 pncan1 10710 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℂ → ((𝑦 + 1) − 1) = 𝑦)
1715, 16syl 17 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → ((𝑦 + 1) − 1) = 𝑦)
1814, 17sylan9eq 2819 . . . . . . . . . . . . . . 15 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → ((#b𝑎) − 1) = 𝑦)
1918eqeq2d 2775 . . . . . . . . . . . . . 14 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → ((#b‘(𝑎 / 2)) = ((#b𝑎) − 1) ↔ (#b‘(𝑎 / 2)) = 𝑦))
20 nnz 11649 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
2120adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℤ)
22 fzval3 12748 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℤ → (0...𝑦) = (0..^(𝑦 + 1)))
2321, 22syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0...𝑦) = (0..^(𝑦 + 1)))
2423eqcomd 2771 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0..^(𝑦 + 1)) = (0...𝑦))
2524sumeq1d 14719 . . . . . . . . . . . . . . . . . . . 20 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ (0...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)))
26 nnnn0 11548 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℕ → 𝑦 ∈ ℕ0)
27 elnn0uz 11928 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℕ0𝑦 ∈ (ℤ‘0))
2826, 27sylib 209 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ‘0))
2928adantl 473 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ (ℤ‘0))
30 2nn 11347 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℕ
3130a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → 2 ∈ ℕ)
32 elfzelz 12552 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (0...𝑦) → 𝑘 ∈ ℤ)
3332adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → 𝑘 ∈ ℤ)
34 nnnn0 11548 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 ∈ ℕ → 𝑎 ∈ ℕ0)
35 nn0rp0 12486 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 ∈ ℕ0𝑎 ∈ (0[,)+∞))
3634, 35syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ ℕ → 𝑎 ∈ (0[,)+∞))
3736ad4antlr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → 𝑎 ∈ (0[,)+∞))
38 digvalnn0 43065 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2 ∈ ℕ ∧ 𝑘 ∈ ℤ ∧ 𝑎 ∈ (0[,)+∞)) → (𝑘(digit‘2)𝑎) ∈ ℕ0)
3931, 33, 37, 38syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℕ0)
4039nn0cnd 11602 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℂ)
41 2nn0 11559 . . . . . . . . . . . . . . . . . . . . . . . . . 26 2 ∈ ℕ0
4241a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (0...𝑦) → 2 ∈ ℕ0)
43 elfznn0 12643 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (0...𝑦) → 𝑘 ∈ ℕ0)
4442, 43nn0expcld 13241 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (0...𝑦) → (2↑𝑘) ∈ ℕ0)
4544nn0cnd 11602 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ (0...𝑦) → (2↑𝑘) ∈ ℂ)
4645adantl 473 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → (2↑𝑘) ∈ ℂ)
4740, 46mulcld 10316 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) ∈ ℂ)
48 oveq1 6851 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 0 → (𝑘(digit‘2)𝑎) = (0(digit‘2)𝑎))
49 oveq2 6852 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 0 → (2↑𝑘) = (2↑0))
5048, 49oveq12d 6862 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 0 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · (2↑0)))
51 2cn 11349 . . . . . . . . . . . . . . . . . . . . . . . 24 2 ∈ ℂ
52 exp0 13074 . . . . . . . . . . . . . . . . . . . . . . . 24 (2 ∈ ℂ → (2↑0) = 1)
5351, 52ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (2↑0) = 1
5453oveq2i 6855 . . . . . . . . . . . . . . . . . . . . . 22 ((0(digit‘2)𝑎) · (2↑0)) = ((0(digit‘2)𝑎) · 1)
5550, 54syl6eq 2815 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 0 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · 1))
5629, 47, 55fsum1p 14770 . . . . . . . . . . . . . . . . . . . 20 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ (0...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (((0(digit‘2)𝑎) · 1) + Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))))
57 0dig2nn0e 43078 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 ∈ ℕ0 ∧ (𝑎 / 2) ∈ ℕ0) → (0(digit‘2)𝑎) = 0)
5834, 1, 57syl2anr 590 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) → (0(digit‘2)𝑎) = 0)
5958oveq1d 6859 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) → ((0(digit‘2)𝑎) · 1) = (0 · 1))
60 1re 10295 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ ℝ
61 mul02lem2 10469 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1 ∈ ℝ → (0 · 1) = 0)
6260, 61ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 · 1) = 0
6359, 62syl6eq 2815 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) → ((0(digit‘2)𝑎) · 1) = 0)
6463adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) → ((0(digit‘2)𝑎) · 1) = 0)
6564adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → ((0(digit‘2)𝑎) · 1) = 0)
66 1z 11657 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ∈ ℤ
6766a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 1 ∈ ℤ)
68 0p1e1 11403 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 + 1) = 1
6968, 66eqeltri 2840 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 + 1) ∈ ℤ
7069a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + 1) ∈ ℤ)
7130a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 2 ∈ ℕ)
72 elfzelz 12552 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 ∈ ((0 + 1)...𝑦) → 𝑘 ∈ ℤ)
7372adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 𝑘 ∈ ℤ)
7436ad4antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 𝑎 ∈ (0[,)+∞))
7571, 73, 74, 38syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℕ0)
7675nn0cnd 11602 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℂ)
77 2cnd 11352 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 ∈ ((0 + 1)...𝑦) → 2 ∈ ℂ)
78 elfznn 12580 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℕ)
7978nnnn0d 11600 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℕ0)
8068oveq1i 6854 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((0 + 1)...𝑦) = (1...𝑦)
8179, 80eleq2s 2862 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 ∈ ((0 + 1)...𝑦) → 𝑘 ∈ ℕ0)
8277, 81expcld 13218 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ ((0 + 1)...𝑦) → (2↑𝑘) ∈ ℂ)
8382adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (2↑𝑘) ∈ ℂ)
8476, 83mulcld 10316 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) ∈ ℂ)
85 oveq1 6851 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = (𝑖 + 1) → (𝑘(digit‘2)𝑎) = ((𝑖 + 1)(digit‘2)𝑎))
86 oveq2 6852 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = (𝑖 + 1) → (2↑𝑘) = (2↑(𝑖 + 1)))
8785, 86oveq12d 6862 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑖 + 1) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
8867, 70, 21, 84, 87fsumshftm 14800 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
8965, 88oveq12d 6862 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (((0(digit‘2)𝑎) · 1) + Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) = (0 + Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))))
901ad4antr 724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑎 / 2) ∈ ℕ0)
9134ad4antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑎 ∈ ℕ0)
92 elfzonn0 12724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ ℕ0)
9392adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑖 ∈ ℕ0)
94 dignn0ehalf 43083 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑎 / 2) ∈ ℕ0𝑎 ∈ ℕ0𝑖 ∈ ℕ0) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)(𝑎 / 2)))
9590, 91, 93, 94syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)(𝑎 / 2)))
96 2cnd 11352 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^𝑦) → 2 ∈ ℂ)
9796, 92expp1d 13219 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^𝑦) → (2↑(𝑖 + 1)) = ((2↑𝑖) · 2))
9897adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑(𝑖 + 1)) = ((2↑𝑖) · 2))
9995, 98oveq12d 6862 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = ((𝑖(digit‘2)(𝑎 / 2)) · ((2↑𝑖) · 2)))
10030a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 2 ∈ ℕ)
101 elfzoelz 12681 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ ℤ)
102101adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑖 ∈ ℤ)
103 nn0rp0 12486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎 / 2) ∈ ℕ0 → (𝑎 / 2) ∈ (0[,)+∞))
1041, 103syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 / 2) ∈ ℕ → (𝑎 / 2) ∈ (0[,)+∞))
105104ad4antr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑎 / 2) ∈ (0[,)+∞))
106 digvalnn0 43065 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2 ∈ ℕ ∧ 𝑖 ∈ ℤ ∧ (𝑎 / 2) ∈ (0[,)+∞)) → (𝑖(digit‘2)(𝑎 / 2)) ∈ ℕ0)
107100, 102, 105, 106syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)(𝑎 / 2)) ∈ ℕ0)
108107nn0cnd 11602 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)(𝑎 / 2)) ∈ ℂ)
109 2re 11348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2 ∈ ℝ
110109a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (0..^𝑦) → 2 ∈ ℝ)
111110, 92reexpcld 13235 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℝ)
112111recnd 10324 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℂ)
113112adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑𝑖) ∈ ℂ)
114 2cnd 11352 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 2 ∈ ℂ)
115 mulass 10279 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑖(digit‘2)(𝑎 / 2)) ∈ ℂ ∧ (2↑𝑖) ∈ ℂ ∧ 2 ∈ ℂ) → (((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2) = ((𝑖(digit‘2)(𝑎 / 2)) · ((2↑𝑖) · 2)))
116115eqcomd 2771 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑖(digit‘2)(𝑎 / 2)) ∈ ℂ ∧ (2↑𝑖) ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑖(digit‘2)(𝑎 / 2)) · ((2↑𝑖) · 2)) = (((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
117108, 113, 114, 116syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)(𝑎 / 2)) · ((2↑𝑖) · 2)) = (((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
11899, 117eqtrd 2799 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = (((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
119118sumeq2dv 14721 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
120 0cn 10287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 0 ∈ ℂ
121 pncan1 10710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (0 ∈ ℂ → ((0 + 1) − 1) = 0)
122120, 121ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((0 + 1) − 1) = 0
123122a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ ℕ → ((0 + 1) − 1) = 0)
124123oveq1d 6859 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ℕ → (((0 + 1) − 1)...(𝑦 − 1)) = (0...(𝑦 − 1)))
125 fzoval 12682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ℤ → (0..^𝑦) = (0...(𝑦 − 1)))
126125eqcomd 2771 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ ℤ → (0...(𝑦 − 1)) = (0..^𝑦))
12720, 126syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ℕ → (0...(𝑦 − 1)) = (0..^𝑦))
128124, 127eqtrd 2799 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ℕ → (((0 + 1) − 1)...(𝑦 − 1)) = (0..^𝑦))
129128adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (((0 + 1) − 1)...(𝑦 − 1)) = (0..^𝑦))
130129sumeq1d 14719 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
131130oveq2d 6860 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) = (0 + Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))))
132 fzofi 12984 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0..^𝑦) ∈ Fin
133132a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0..^𝑦) ∈ Fin)
134101peano2zd 11735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝑦) → (𝑖 + 1) ∈ ℤ)
135134adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖 + 1) ∈ ℤ)
13636ad4antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑎 ∈ (0[,)+∞))
137 digvalnn0 43065 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2 ∈ ℕ ∧ (𝑖 + 1) ∈ ℤ ∧ 𝑎 ∈ (0[,)+∞)) → ((𝑖 + 1)(digit‘2)𝑎) ∈ ℕ0)
138100, 135, 136, 137syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖 + 1)(digit‘2)𝑎) ∈ ℕ0)
139138nn0cnd 11602 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖 + 1)(digit‘2)𝑎) ∈ ℂ)
14041a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝑦) → 2 ∈ ℕ0)
141 peano2nn0 11582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ ℕ0 → (𝑖 + 1) ∈ ℕ0)
14292, 141syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝑦) → (𝑖 + 1) ∈ ℕ0)
143140, 142nn0expcld 13241 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (0..^𝑦) → (2↑(𝑖 + 1)) ∈ ℕ0)
144143nn0cnd 11602 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^𝑦) → (2↑(𝑖 + 1)) ∈ ℂ)
145144adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑(𝑖 + 1)) ∈ ℂ)
146139, 145mulcld 10316 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) ∈ ℂ)
147133, 146fsumcl 14752 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) ∈ ℂ)
148147addid2d 10493 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
149131, 148eqtrd 2799 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
150 2cnd 11352 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 2 ∈ ℂ)
151140, 92nn0expcld 13241 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℕ0)
152151nn0cnd 11602 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℂ)
153152adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑𝑖) ∈ ℂ)
154108, 153mulcld 10316 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) ∈ ℂ)
155133, 150, 154fsummulc1 14804 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2) = Σ𝑖 ∈ (0..^𝑦)(((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
156119, 149, 1553eqtr4d 2809 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
15789, 156eqtrd 2799 . . . . . . . . . . . . . . . . . . . 20 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (((0(digit‘2)𝑎) · 1) + Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
15825, 56, 1573eqtrd 2803 . . . . . . . . . . . . . . . . . . 19 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
159158adantl 473 . . . . . . . . . . . . . . . . . 18 (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
160 oveq1 6851 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = 𝑖 → (𝑘(digit‘2)(𝑎 / 2)) = (𝑖(digit‘2)(𝑎 / 2)))
161 oveq2 6852 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = 𝑖 → (2↑𝑘) = (2↑𝑖))
162160, 161oveq12d 6862 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑖 → ((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) = ((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)))
163162cbvsumv 14714 . . . . . . . . . . . . . . . . . . . . . . 23 Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖))
164163a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)))
165164eqeq2d 2775 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → ((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ↔ (𝑎 / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖))))
166165biimpac 470 . . . . . . . . . . . . . . . . . . . 20 (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → (𝑎 / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)))
167166eqcomd 2771 . . . . . . . . . . . . . . . . . . 19 (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) = (𝑎 / 2))
168167oveq1d 6859 . . . . . . . . . . . . . . . . . 18 (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2) = ((𝑎 / 2) · 2))
169 nncn 11285 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ∈ ℕ → 𝑎 ∈ ℂ)
170 2cnd 11352 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ∈ ℕ → 2 ∈ ℂ)
171 2ne0 11385 . . . . . . . . . . . . . . . . . . . . . 22 2 ≠ 0
172171a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ∈ ℕ → 2 ≠ 0)
173169, 170, 172divcan1d 11058 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ ℕ → ((𝑎 / 2) · 2) = 𝑎)
174173ad3antlr 722 . . . . . . . . . . . . . . . . . . 19 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → ((𝑎 / 2) · 2) = 𝑎)
175174adantl 473 . . . . . . . . . . . . . . . . . 18 (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → ((𝑎 / 2) · 2) = 𝑎)
176159, 168, 1753eqtrrd 2804 . . . . . . . . . . . . . . . . 17 (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))
177176ex 401 . . . . . . . . . . . . . . . 16 ((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) → (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))
178177imim2i 16 . . . . . . . . . . . . . . 15 (((#b‘(𝑎 / 2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) → ((#b‘(𝑎 / 2)) = 𝑦 → (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
179178com13 88 . . . . . . . . . . . . . 14 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → ((#b‘(𝑎 / 2)) = 𝑦 → (((#b‘(𝑎 / 2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
18019, 179sylbid 231 . . . . . . . . . . . . 13 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → ((#b‘(𝑎 / 2)) = ((#b𝑎) − 1) → (((#b‘(𝑎 / 2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
181180com23 86 . . . . . . . . . . . 12 (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#b𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (((#b‘(𝑎 / 2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) → ((#b‘(𝑎 / 2)) = ((#b𝑎) − 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
182181exp31 410 . . . . . . . . . . 11 (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) → ((#b𝑎) = (𝑦 + 1) → (𝑦 ∈ ℕ → (((#b‘(𝑎 / 2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) → ((#b‘(𝑎 / 2)) = ((#b𝑎) − 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))
183182com25 99 . . . . . . . . . 10 (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) → ((#b‘(𝑎 / 2)) = ((#b𝑎) − 1) → (𝑦 ∈ ℕ → (((#b‘(𝑎 / 2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))
184183com14 96 . . . . . . . . 9 (((#b‘(𝑎 / 2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) → ((#b‘(𝑎 / 2)) = ((#b𝑎) − 1) → (𝑦 ∈ ℕ → (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))
18512, 184syl 17 . . . . . . . 8 (((𝑎 / 2) ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → ((#b‘(𝑎 / 2)) = ((#b𝑎) − 1) → (𝑦 ∈ ℕ → (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))
186185ex 401 . . . . . . 7 ((𝑎 / 2) ∈ ℕ0 → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘(𝑎 / 2)) = ((#b𝑎) − 1) → (𝑦 ∈ ℕ → (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))))
187186com25 99 . . . . . 6 ((𝑎 / 2) ∈ ℕ0 → (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) → ((#b‘(𝑎 / 2)) = ((#b𝑎) − 1) → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))))
188187expdcom 403 . . . . 5 ((𝑎 / 2) ∈ ℕ → (𝑎 ∈ ℕ → ((𝑎 / 2) ∈ ℕ0 → ((#b‘(𝑎 / 2)) = ((#b𝑎) − 1) → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))))
1891, 188mpid 44 . . . 4 ((𝑎 / 2) ∈ ℕ → (𝑎 ∈ ℕ → ((#b‘(𝑎 / 2)) = ((#b𝑎) − 1) → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))))
190189impcom 396 . . 3 ((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ) → ((#b‘(𝑎 / 2)) = ((#b𝑎) − 1) → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))
1913, 190mpd 15 . 2 ((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ) → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))
192191imp 395 1 (((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ) ∧ 𝑦 ∈ ℕ) → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055  cfv 6070  (class class class)co 6844  Fincfn 8162  cc 10189  cr 10190  0cc0 10191  1c1 10192   + caddc 10194   · cmul 10196  +∞cpnf 10327  cmin 10522   / cdiv 10940  cn 11276  2c2 11329  0cn0 11540  cz 11626  cuz 11889  [,)cico 12382  ...cfz 12536  ..^cfzo 12676  cexp 13070  Σcsu 14704  #bcblen 43035  digitcdig 43061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149  ax-inf2 8755  ax-cnex 10247  ax-resscn 10248  ax-1cn 10249  ax-icn 10250  ax-addcl 10251  ax-addrcl 10252  ax-mulcl 10253  ax-mulrcl 10254  ax-mulcom 10255  ax-addass 10256  ax-mulass 10257  ax-distr 10258  ax-i2m1 10259  ax-1ne0 10260  ax-1rid 10261  ax-rnegex 10262  ax-rrecex 10263  ax-cnre 10264  ax-pre-lttri 10265  ax-pre-lttrn 10266  ax-pre-ltadd 10267  ax-pre-mulgt0 10268  ax-pre-sup 10269  ax-addf 10270  ax-mulf 10271
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-iin 4681  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-se 5239  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-isom 6079  df-riota 6805  df-ov 6847  df-oprab 6848  df-mpt2 6849  df-of 7097  df-om 7266  df-1st 7368  df-2nd 7369  df-supp 7500  df-wrecs 7612  df-recs 7674  df-rdg 7712  df-1o 7766  df-2o 7767  df-oadd 7770  df-er 7949  df-map 8064  df-pm 8065  df-ixp 8116  df-en 8163  df-dom 8164  df-sdom 8165  df-fin 8166  df-fsupp 8485  df-fi 8526  df-sup 8557  df-inf 8558  df-oi 8624  df-card 9018  df-cda 9245  df-pnf 10332  df-mnf 10333  df-xr 10334  df-ltxr 10335  df-le 10336  df-sub 10524  df-neg 10525  df-div 10941  df-nn 11277  df-2 11337  df-3 11338  df-4 11339  df-5 11340  df-6 11341  df-7 11342  df-8 11343  df-9 11344  df-n0 11541  df-z 11627  df-dec 11744  df-uz 11890  df-q 11993  df-rp 12032  df-xneg 12149  df-xadd 12150  df-xmul 12151  df-ioo 12384  df-ioc 12385  df-ico 12386  df-icc 12387  df-fz 12537  df-fzo 12677  df-fl 12804  df-mod 12880  df-seq 13012  df-exp 13071  df-fac 13268  df-bc 13297  df-hash 13325  df-shft 14095  df-cj 14127  df-re 14128  df-im 14129  df-sqrt 14263  df-abs 14264  df-limsup 14490  df-clim 14507  df-rlim 14508  df-sum 14705  df-ef 15083  df-sin 15085  df-cos 15086  df-pi 15088  df-struct 16135  df-ndx 16136  df-slot 16137  df-base 16139  df-sets 16140  df-ress 16141  df-plusg 16230  df-mulr 16231  df-starv 16232  df-sca 16233  df-vsca 16234  df-ip 16235  df-tset 16236  df-ple 16237  df-ds 16239  df-unif 16240  df-hom 16241  df-cco 16242  df-rest 16352  df-topn 16353  df-0g 16371  df-gsum 16372  df-topgen 16373  df-pt 16374  df-prds 16377  df-xrs 16431  df-qtop 16436  df-imas 16437  df-xps 16439  df-mre 16515  df-mrc 16516  df-acs 16518  df-mgm 17511  df-sgrp 17553  df-mnd 17564  df-submnd 17605  df-mulg 17811  df-cntz 18016  df-cmn 18464  df-psmet 20014  df-xmet 20015  df-met 20016  df-bl 20017  df-mopn 20018  df-fbas 20019  df-fg 20020  df-cnfld 20023  df-top 20981  df-topon 20998  df-topsp 21020  df-bases 21033  df-cld 21106  df-ntr 21107  df-cls 21108  df-nei 21185  df-lp 21223  df-perf 21224  df-cn 21314  df-cnp 21315  df-haus 21402  df-tx 21648  df-hmeo 21841  df-fil 21932  df-fm 22024  df-flim 22025  df-flf 22026  df-xms 22407  df-ms 22408  df-tms 22409  df-cncf 22963  df-limc 23924  df-dv 23925  df-log 24597  df-logb 24797  df-blen 43036  df-dig 43062
This theorem is referenced by:  nn0sumshdiglem1  43087
  Copyright terms: Public domain W3C validator