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

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

Proof of Theorem nn0sumshdiglemB
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 elnn1uz2 12850 . . 3 (𝑎 ∈ ℕ ↔ (𝑎 = 1 ∨ 𝑎 ∈ (ℤ‘2)))
2 1t1e1 12315 . . . . . . . . 9 (1 · 1) = 1
32eqcomi 2745 . . . . . . . 8 1 = (1 · 1)
4 simpl 483 . . . . . . . 8 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → 𝑎 = 1)
5 oveq2 7365 . . . . . . . . . . . 12 ((𝑦 + 1) = (#b𝑎) → (0..^(𝑦 + 1)) = (0..^(#b𝑎)))
65eqcoms 2744 . . . . . . . . . . 11 ((#b𝑎) = (𝑦 + 1) → (0..^(𝑦 + 1)) = (0..^(#b𝑎)))
7 fveq2 6842 . . . . . . . . . . . . . 14 (𝑎 = 1 → (#b𝑎) = (#b‘1))
8 blen1 46660 . . . . . . . . . . . . . 14 (#b‘1) = 1
97, 8eqtrdi 2792 . . . . . . . . . . . . 13 (𝑎 = 1 → (#b𝑎) = 1)
109oveq2d 7373 . . . . . . . . . . . 12 (𝑎 = 1 → (0..^(#b𝑎)) = (0..^1))
11 fzo01 13654 . . . . . . . . . . . 12 (0..^1) = {0}
1210, 11eqtrdi 2792 . . . . . . . . . . 11 (𝑎 = 1 → (0..^(#b𝑎)) = {0})
136, 12sylan9eqr 2798 . . . . . . . . . 10 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → (0..^(𝑦 + 1)) = {0})
1413sumeq1d 15586 . . . . . . . . 9 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)))
15 oveq2 7365 . . . . . . . . . . . . 13 (𝑎 = 1 → (𝑘(digit‘2)𝑎) = (𝑘(digit‘2)1))
1615oveq1d 7372 . . . . . . . . . . . 12 (𝑎 = 1 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((𝑘(digit‘2)1) · (2↑𝑘)))
1716sumeq2sdv 15589 . . . . . . . . . . 11 (𝑎 = 1 → Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ {0} ((𝑘(digit‘2)1) · (2↑𝑘)))
18 c0ex 11149 . . . . . . . . . . . 12 0 ∈ V
19 ax-1cn 11109 . . . . . . . . . . . . 13 1 ∈ ℂ
2019, 19mulcli 11162 . . . . . . . . . . . 12 (1 · 1) ∈ ℂ
21 oveq1 7364 . . . . . . . . . . . . . . 15 (𝑘 = 0 → (𝑘(digit‘2)1) = (0(digit‘2)1))
22 1ex 11151 . . . . . . . . . . . . . . . . 17 1 ∈ V
2322prid2 4724 . . . . . . . . . . . . . . . 16 1 ∈ {0, 1}
24 0dig2pr01 46686 . . . . . . . . . . . . . . . 16 (1 ∈ {0, 1} → (0(digit‘2)1) = 1)
2523, 24ax-mp 5 . . . . . . . . . . . . . . 15 (0(digit‘2)1) = 1
2621, 25eqtrdi 2792 . . . . . . . . . . . . . 14 (𝑘 = 0 → (𝑘(digit‘2)1) = 1)
27 oveq2 7365 . . . . . . . . . . . . . . 15 (𝑘 = 0 → (2↑𝑘) = (2↑0))
28 2cn 12228 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
29 exp0 13971 . . . . . . . . . . . . . . . 16 (2 ∈ ℂ → (2↑0) = 1)
3028, 29ax-mp 5 . . . . . . . . . . . . . . 15 (2↑0) = 1
3127, 30eqtrdi 2792 . . . . . . . . . . . . . 14 (𝑘 = 0 → (2↑𝑘) = 1)
3226, 31oveq12d 7375 . . . . . . . . . . . . 13 (𝑘 = 0 → ((𝑘(digit‘2)1) · (2↑𝑘)) = (1 · 1))
3332sumsn 15631 . . . . . . . . . . . 12 ((0 ∈ V ∧ (1 · 1) ∈ ℂ) → Σ𝑘 ∈ {0} ((𝑘(digit‘2)1) · (2↑𝑘)) = (1 · 1))
3418, 20, 33mp2an 690 . . . . . . . . . . 11 Σ𝑘 ∈ {0} ((𝑘(digit‘2)1) · (2↑𝑘)) = (1 · 1)
3517, 34eqtrdi 2792 . . . . . . . . . 10 (𝑎 = 1 → Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (1 · 1))
3635adantr 481 . . . . . . . . 9 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (1 · 1))
3714, 36eqtrd 2776 . . . . . . . 8 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (1 · 1))
383, 4, 373eqtr4a 2802 . . . . . . 7 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))
3938ex 413 . . . . . 6 (𝑎 = 1 → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))
4039a1d 25 . . . . 5 (𝑎 = 1 → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
41402a1d 26 . . . 4 (𝑎 = 1 → (((𝑎 − 1) / 2) ∈ ℕ0 → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))
42 eluzge2nn0 12812 . . . . . . . . 9 (𝑎 ∈ (ℤ‘2) → 𝑎 ∈ ℕ0)
43 nn0ob 16266 . . . . . . . . . 10 (𝑎 ∈ ℕ0 → (((𝑎 + 1) / 2) ∈ ℕ0 ↔ ((𝑎 − 1) / 2) ∈ ℕ0))
4443bicomd 222 . . . . . . . . 9 (𝑎 ∈ ℕ0 → (((𝑎 − 1) / 2) ∈ ℕ0 ↔ ((𝑎 + 1) / 2) ∈ ℕ0))
4542, 44syl 17 . . . . . . . 8 (𝑎 ∈ (ℤ‘2) → (((𝑎 − 1) / 2) ∈ ℕ0 ↔ ((𝑎 + 1) / 2) ∈ ℕ0))
46 blennngt2o2 46668 . . . . . . . . 9 ((𝑎 ∈ (ℤ‘2) ∧ ((𝑎 + 1) / 2) ∈ ℕ0) → (#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1))
4746ex 413 . . . . . . . 8 (𝑎 ∈ (ℤ‘2) → (((𝑎 + 1) / 2) ∈ ℕ0 → (#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1)))
4845, 47sylbid 239 . . . . . . 7 (𝑎 ∈ (ℤ‘2) → (((𝑎 − 1) / 2) ∈ ℕ0 → (#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1)))
4948imp 407 . . . . . 6 ((𝑎 ∈ (ℤ‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0) → (#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1))
50 fveqeq2 6851 . . . . . . . . . . . . 13 (𝑥 = ((𝑎 − 1) / 2) → ((#b𝑥) = 𝑦 ↔ (#b‘((𝑎 − 1) / 2)) = 𝑦))
51 id 22 . . . . . . . . . . . . . 14 (𝑥 = ((𝑎 − 1) / 2) → 𝑥 = ((𝑎 − 1) / 2))
52 oveq2 7365 . . . . . . . . . . . . . . . 16 (𝑥 = ((𝑎 − 1) / 2) → (𝑘(digit‘2)𝑥) = (𝑘(digit‘2)((𝑎 − 1) / 2)))
5352oveq1d 7372 . . . . . . . . . . . . . . 15 (𝑥 = ((𝑎 − 1) / 2) → ((𝑘(digit‘2)𝑥) · (2↑𝑘)) = ((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)))
5453sumeq2sdv 15589 . . . . . . . . . . . . . 14 (𝑥 = ((𝑎 − 1) / 2) → Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)))
5551, 54eqeq12d 2752 . . . . . . . . . . . . 13 (𝑥 = ((𝑎 − 1) / 2) → (𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)) ↔ ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))))
5650, 55imbi12d 344 . . . . . . . . . . . 12 (𝑥 = ((𝑎 − 1) / 2) → (((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) ↔ ((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)))))
5756rspcva 3579 . . . . . . . . . . 11 ((((𝑎 − 1) / 2) ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → ((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))))
58 eqeq1 2740 . . . . . . . . . . . . . . . 16 ((#b𝑎) = (𝑦 + 1) → ((#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1) ↔ (𝑦 + 1) = ((#b‘((𝑎 − 1) / 2)) + 1)))
59 nncn 12161 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
6059ad2antll 727 . . . . . . . . . . . . . . . . . . . 20 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑦 ∈ ℂ)
61 blennn0elnn 46653 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 − 1) / 2) ∈ ℕ0 → (#b‘((𝑎 − 1) / 2)) ∈ ℕ)
6261nncnd 12169 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎 − 1) / 2) ∈ ℕ0 → (#b‘((𝑎 − 1) / 2)) ∈ ℂ)
6362adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (#b‘((𝑎 − 1) / 2)) ∈ ℂ)
6463ad2antrl 726 . . . . . . . . . . . . . . . . . . . 20 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (#b‘((𝑎 − 1) / 2)) ∈ ℂ)
65 1cnd 11150 . . . . . . . . . . . . . . . . . . . 20 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 1 ∈ ℂ)
6660, 64, 65addcan2d 11359 . . . . . . . . . . . . . . . . . . 19 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → ((𝑦 + 1) = ((#b‘((𝑎 − 1) / 2)) + 1) ↔ 𝑦 = (#b‘((𝑎 − 1) / 2))))
67 eqcom 2743 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (#b‘((𝑎 − 1) / 2)) ↔ (#b‘((𝑎 − 1) / 2)) = 𝑦)
68 nnz 12520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
6968ad2antll 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑦 ∈ ℤ)
70 fzval3 13641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ℤ → (0...𝑦) = (0..^(𝑦 + 1)))
7169, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (0...𝑦) = (0..^(𝑦 + 1)))
7271eqcomd 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (0..^(𝑦 + 1)) = (0...𝑦))
7372sumeq1d 15586 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ (0...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)))
74 nnnn0 12420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ℕ → 𝑦 ∈ ℕ0)
75 elnn0uz 12808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ℕ0𝑦 ∈ (ℤ‘0))
7674, 75sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ‘0))
7776ad2antll 727 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑦 ∈ (ℤ‘0))
78 2nn 12226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 2 ∈ ℕ
7978a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑘 ∈ (0...𝑦)) → 2 ∈ ℕ)
80 elfzelz 13441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 ∈ (0...𝑦) → 𝑘 ∈ ℤ)
8180adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑘 ∈ (0...𝑦)) → 𝑘 ∈ ℤ)
82 nn0rp0 13372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑎 ∈ ℕ0𝑎 ∈ (0[,)+∞))
8342, 82syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑎 ∈ (ℤ‘2) → 𝑎 ∈ (0[,)+∞))
8483adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → 𝑎 ∈ (0[,)+∞))
8584adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑘 ∈ (0...𝑦)) → 𝑎 ∈ (0[,)+∞))
86 digvalnn0 46675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((2 ∈ ℕ ∧ 𝑘 ∈ ℤ ∧ 𝑎 ∈ (0[,)+∞)) → (𝑘(digit‘2)𝑎) ∈ ℕ0)
8779, 81, 85, 86syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℕ0)
8887ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (𝑘 ∈ (0...𝑦) → (𝑘(digit‘2)𝑎) ∈ ℕ0))
8988ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (𝑘 ∈ (0...𝑦) → (𝑘(digit‘2)𝑎) ∈ ℕ0))
9089imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℕ0)
9190nn0cnd 12475 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℂ)
92 2nn0 12430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2 ∈ ℕ0
9392a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ (0...𝑦) → 2 ∈ ℕ0)
94 elfznn0 13534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ (0...𝑦) → 𝑘 ∈ ℕ0)
9593, 94nn0expcld 14149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ (0...𝑦) → (2↑𝑘) ∈ ℕ0)
9695nn0cnd 12475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 ∈ (0...𝑦) → (2↑𝑘) ∈ ℂ)
9796adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ (0...𝑦)) → (2↑𝑘) ∈ ℂ)
9891, 97mulcld 11175 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ (0...𝑦)) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) ∈ ℂ)
99 oveq1 7364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 0 → (𝑘(digit‘2)𝑎) = (0(digit‘2)𝑎))
10099, 27oveq12d 7375 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = 0 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · (2↑0)))
10130oveq2i 7368 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((0(digit‘2)𝑎) · (2↑0)) = ((0(digit‘2)𝑎) · 1)
102100, 101eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 = 0 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · 1))
10377, 98, 102fsum1p 15638 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑘 ∈ (0...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (((0(digit‘2)𝑎) · 1) + Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))))
10442adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → 𝑎 ∈ ℕ0)
10542, 43syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 ∈ (ℤ‘2) → (((𝑎 + 1) / 2) ∈ ℕ0 ↔ ((𝑎 − 1) / 2) ∈ ℕ0))
106105biimparc 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → ((𝑎 + 1) / 2) ∈ ℕ0)
107 0dig2nn0o 46689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑎 ∈ ℕ0 ∧ ((𝑎 + 1) / 2) ∈ ℕ0) → (0(digit‘2)𝑎) = 1)
108104, 106, 107syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (0(digit‘2)𝑎) = 1)
109108ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (0(digit‘2)𝑎) = 1)
110109oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → ((0(digit‘2)𝑎) · 1) = (1 · 1))
111110, 2eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → ((0(digit‘2)𝑎) · 1) = 1)
112 1z 12533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℤ
113112a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 1 ∈ ℤ)
114 0p1e1 12275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (0 + 1) = 1
115114, 112eqeltri 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (0 + 1) ∈ ℤ
116115a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (0 + 1) ∈ ℤ)
11778a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎 ∈ (ℤ‘2) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 2 ∈ ℕ)
118 elfzelz 13441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 ∈ ((0 + 1)...𝑦) → 𝑘 ∈ ℤ)
119118adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎 ∈ (ℤ‘2) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 𝑘 ∈ ℤ)
12042adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑎 ∈ (ℤ‘2) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 𝑎 ∈ ℕ0)
121120, 82syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎 ∈ (ℤ‘2) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 𝑎 ∈ (0[,)+∞))
122117, 119, 121, 86syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑎 ∈ (ℤ‘2) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℕ0)
123122ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎 ∈ (ℤ‘2) → (𝑘 ∈ ((0 + 1)...𝑦) → (𝑘(digit‘2)𝑎) ∈ ℕ0))
124123adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (𝑘 ∈ ((0 + 1)...𝑦) → (𝑘(digit‘2)𝑎) ∈ ℕ0))
125124ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (𝑘 ∈ ((0 + 1)...𝑦) → (𝑘(digit‘2)𝑎) ∈ ℕ0))
126125imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℕ0)
127126nn0cnd 12475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℂ)
128 2cnd 12231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ ((0 + 1)...𝑦) → 2 ∈ ℂ)
129 elfznn 13470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℕ)
130129nnnn0d 12473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℕ0)
131114oveq1i 7367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((0 + 1)...𝑦) = (1...𝑦)
132130, 131eleq2s 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ ((0 + 1)...𝑦) → 𝑘 ∈ ℕ0)
133128, 132expcld 14051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ ((0 + 1)...𝑦) → (2↑𝑘) ∈ ℂ)
134133adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (2↑𝑘) ∈ ℂ)
135127, 134mulcld 11175 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) ∈ ℂ)
136 oveq1 7364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = (𝑖 + 1) → (𝑘(digit‘2)𝑎) = ((𝑖 + 1)(digit‘2)𝑎))
137 oveq2 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = (𝑖 + 1) → (2↑𝑘) = (2↑(𝑖 + 1)))
138136, 137oveq12d 7375 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = (𝑖 + 1) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
139113, 116, 69, 135, 138fsumshftm 15666 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
140111, 139oveq12d 7375 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (((0(digit‘2)𝑎) · 1) + Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) = (1 + Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))))
14173, 103, 1403eqtrd 2780 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (1 + Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))))
142141adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (1 + Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))))
14378a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → 2 ∈ ℕ)
144 elfzoelz 13572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ ℤ)
145144adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑖 ∈ ℤ)
146 nn0rp0 13372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑎 − 1) / 2) ∈ ℕ0 → ((𝑎 − 1) / 2) ∈ (0[,)+∞))
147146adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → ((𝑎 − 1) / 2) ∈ (0[,)+∞))
148147adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑎 − 1) / 2) ∈ (0[,)+∞))
149 digvalnn0 46675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((2 ∈ ℕ ∧ 𝑖 ∈ ℤ ∧ ((𝑎 − 1) / 2) ∈ (0[,)+∞)) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈ ℕ0)
150143, 145, 148, 149syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈ ℕ0)
151150nn0cnd 12475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈ ℂ)
152151ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (𝑖 ∈ (0..^𝑦) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈ ℂ))
153152ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (𝑖 ∈ (0..^𝑦) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈ ℂ))
154153imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈ ℂ)
15592a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ (0..^𝑦) → 2 ∈ ℕ0)
156 elfzonn0 13617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ ℕ0)
157155, 156nn0expcld 14149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℕ0)
158157nn0cnd 12475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℂ)
159158adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑𝑖) ∈ ℂ)
160 2cnd 12231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → 2 ∈ ℂ)
161154, 159, 160mulassd 11178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2) = ((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)))
162161eqcomd 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)) = (((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2))
163162sumeq2dv 15588 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)) = Σ𝑖 ∈ (0..^𝑦)(((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2))
164163adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)) = Σ𝑖 ∈ (0..^𝑦)(((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2))
165 0cn 11147 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 0 ∈ ℂ
166 pncan1 11579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (0 ∈ ℂ → ((0 + 1) − 1) = 0)
167165, 166ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((0 + 1) − 1) = 0
168167a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ ℕ → ((0 + 1) − 1) = 0)
169168oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ ℕ → (((0 + 1) − 1)...(𝑦 − 1)) = (0...(𝑦 − 1)))
170 fzoval 13573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ ℤ → (0..^𝑦) = (0...(𝑦 − 1)))
17168, 170syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ ℕ → (0..^𝑦) = (0...(𝑦 − 1)))
172169, 171eqtr4d 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ℕ → (((0 + 1) − 1)...(𝑦 − 1)) = (0..^𝑦))
173172ad2antll 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (((0 + 1) − 1)...(𝑦 − 1)) = (0..^𝑦))
174 simprlr 778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑎 ∈ (ℤ‘2))
175 elfznn0 13534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 ∈ (0...(𝑦 − 1)) → 𝑖 ∈ ℕ0)
176167oveq1i 7367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((0 + 1) − 1)...(𝑦 − 1)) = (0...(𝑦 − 1))
177175, 176eleq2s 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1)) → 𝑖 ∈ ℕ0)
178 dignn0flhalf 46694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑎 ∈ (ℤ‘2) ∧ 𝑖 ∈ ℕ0) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)(⌊‘(𝑎 / 2))))
179174, 177, 178syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)(⌊‘(𝑎 / 2))))
180 eluzelz 12773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑎 ∈ (ℤ‘2) → 𝑎 ∈ ℤ)
181180adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑎 ∈ (ℤ‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0) → 𝑎 ∈ ℤ)
182 nn0z 12524 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑎 − 1) / 2) ∈ ℕ0 → ((𝑎 − 1) / 2) ∈ ℤ)
183 zob 16241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎 ∈ ℤ → (((𝑎 + 1) / 2) ∈ ℤ ↔ ((𝑎 − 1) / 2) ∈ ℤ))
184180, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑎 ∈ (ℤ‘2) → (((𝑎 + 1) / 2) ∈ ℤ ↔ ((𝑎 − 1) / 2) ∈ ℤ))
185182, 184syl5ibr 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑎 ∈ (ℤ‘2) → (((𝑎 − 1) / 2) ∈ ℕ0 → ((𝑎 + 1) / 2) ∈ ℤ))
186185imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑎 ∈ (ℤ‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0) → ((𝑎 + 1) / 2) ∈ ℤ)
187181, 186jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎 ∈ (ℤ‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0) → (𝑎 ∈ ℤ ∧ ((𝑎 + 1) / 2) ∈ ℤ))
188187ancoms 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (𝑎 ∈ ℤ ∧ ((𝑎 + 1) / 2) ∈ ℤ))
189188ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (𝑎 ∈ ℤ ∧ ((𝑎 + 1) / 2) ∈ ℤ))
190189adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → (𝑎 ∈ ℤ ∧ ((𝑎 + 1) / 2) ∈ ℤ))
191 zofldiv2 46607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑎 ∈ ℤ ∧ ((𝑎 + 1) / 2) ∈ ℤ) → (⌊‘(𝑎 / 2)) = ((𝑎 − 1) / 2))
192190, 191syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → (⌊‘(𝑎 / 2)) = ((𝑎 − 1) / 2))
193192oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → (𝑖(digit‘2)(⌊‘(𝑎 / 2))) = (𝑖(digit‘2)((𝑎 − 1) / 2)))
194179, 193eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)((𝑎 − 1) / 2)))
195 2cnd 12231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1)) → 2 ∈ ℂ)
196195, 177expp1d 14052 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1)) → (2↑(𝑖 + 1)) = ((2↑𝑖) · 2))
197196adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → (2↑(𝑖 + 1)) = ((2↑𝑖) · 2))
198194, 197oveq12d 7375 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = ((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)))
199173, 198sumeq12dv 15591 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)))
200199adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)))
201 oveq1 7364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝑖 → (𝑘(digit‘2)((𝑎 − 1) / 2)) = (𝑖(digit‘2)((𝑎 − 1) / 2)))
202 oveq2 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝑖 → (2↑𝑘) = (2↑𝑖))
203201, 202oveq12d 7375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝑖 → ((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) = ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)))
204203cbvsumv 15581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖))
205204eqeq2i 2749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ↔ ((𝑎 − 1) / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)))
206205biimpi 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) → ((𝑎 − 1) / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)))
207206adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → ((𝑎 − 1) / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)))
208207oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → (((𝑎 − 1) / 2) · 2) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2))
209 fzofi 13879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (0..^𝑦) ∈ Fin
210209a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → (0..^𝑦) ∈ Fin)
211 2cnd 12231 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → 2 ∈ ℂ)
212158adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑𝑖) ∈ ℂ)
213151, 212mulcld 11175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) ∈ ℂ)
214213ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (𝑖 ∈ (0..^𝑦) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) ∈ ℂ))
215214adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ) → (𝑖 ∈ (0..^𝑦) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) ∈ ℂ))
216215ad2antll 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → (𝑖 ∈ (0..^𝑦) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) ∈ ℂ))
217216imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) ∈ ℂ)
218210, 211, 217fsummulc1 15670 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2) = Σ𝑖 ∈ (0..^𝑦)(((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2))
219208, 218eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → (((𝑎 − 1) / 2) · 2) = Σ𝑖 ∈ (0..^𝑦)(((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2))
220164, 200, 2193eqtr4d 2786 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = (((𝑎 − 1) / 2) · 2))
221220oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → (1 + Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) = (1 + (((𝑎 − 1) / 2) · 2)))
222 eluzelcn 12775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 ∈ (ℤ‘2) → 𝑎 ∈ ℂ)
223 peano2cnm 11467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 ∈ ℂ → (𝑎 − 1) ∈ ℂ)
224222, 223syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎 ∈ (ℤ‘2) → (𝑎 − 1) ∈ ℂ)
225 2cnd 12231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎 ∈ (ℤ‘2) → 2 ∈ ℂ)
226 2ne0 12257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2 ≠ 0
227226a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎 ∈ (ℤ‘2) → 2 ≠ 0)
228224, 225, 2273jca 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 ∈ (ℤ‘2) → ((𝑎 − 1) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0))
229228adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → ((𝑎 − 1) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0))
230 divcan1 11822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑎 − 1) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (((𝑎 − 1) / 2) · 2) = (𝑎 − 1))
231229, 230syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (((𝑎 − 1) / 2) · 2) = (𝑎 − 1))
232231oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (1 + (((𝑎 − 1) / 2) · 2)) = (1 + (𝑎 − 1)))
233 1cnd 11150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 ∈ (ℤ‘2) → 1 ∈ ℂ)
234233, 222jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 ∈ (ℤ‘2) → (1 ∈ ℂ ∧ 𝑎 ∈ ℂ))
235234adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (1 ∈ ℂ ∧ 𝑎 ∈ ℂ))
236 pncan3 11409 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((1 ∈ ℂ ∧ 𝑎 ∈ ℂ) → (1 + (𝑎 − 1)) = 𝑎)
237235, 236syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (1 + (𝑎 − 1)) = 𝑎)
238232, 237eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (1 + (((𝑎 − 1) / 2) · 2)) = 𝑎)
239238adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ) → (1 + (((𝑎 − 1) / 2) · 2)) = 𝑎)
240239ad2antll 727 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → (1 + (((𝑎 − 1) / 2) · 2)) = 𝑎)
241142, 221, 2403eqtrrd 2781 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))
242241ex 413 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) → (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))
243242imim2i 16 . . . . . . . . . . . . . . . . . . . . 21 (((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) → ((#b‘((𝑎 − 1) / 2)) = 𝑦 → (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
244243com13 88 . . . . . . . . . . . . . . . . . . . 20 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → ((#b‘((𝑎 − 1) / 2)) = 𝑦 → (((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
24567, 244biimtrid 241 . . . . . . . . . . . . . . . . . . 19 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (𝑦 = (#b‘((𝑎 − 1) / 2)) → (((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
24666, 245sylbid 239 . . . . . . . . . . . . . . . . . 18 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → ((𝑦 + 1) = ((#b‘((𝑎 − 1) / 2)) + 1) → (((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
247246ex 413 . . . . . . . . . . . . . . . . 17 ((#b𝑎) = (𝑦 + 1) → (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ) → ((𝑦 + 1) = ((#b‘((𝑎 − 1) / 2)) + 1) → (((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))
248247com23 86 . . . . . . . . . . . . . . . 16 ((#b𝑎) = (𝑦 + 1) → ((𝑦 + 1) = ((#b‘((𝑎 − 1) / 2)) + 1) → (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ) → (((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))
24958, 248sylbid 239 . . . . . . . . . . . . . . 15 ((#b𝑎) = (𝑦 + 1) → ((#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1) → (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ) → (((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))
250249com23 86 . . . . . . . . . . . . . 14 ((#b𝑎) = (𝑦 + 1) → (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ) → ((#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1) → (((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))
251250com14 96 . . . . . . . . . . . . 13 (((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) → (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ) → ((#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))
252251exp4c 433 . . . . . . . . . . . 12 (((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) → (((𝑎 − 1) / 2) ∈ ℕ0 → (𝑎 ∈ (ℤ‘2) → (𝑦 ∈ ℕ → ((#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))))
253252com35 98 . . . . . . . . . . 11 (((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) → (((𝑎 − 1) / 2) ∈ ℕ0 → ((#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1) → (𝑦 ∈ ℕ → (𝑎 ∈ (ℤ‘2) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))))
25457, 253syl 17 . . . . . . . . . 10 ((((𝑎 − 1) / 2) ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → (((𝑎 − 1) / 2) ∈ ℕ0 → ((#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1) → (𝑦 ∈ ℕ → (𝑎 ∈ (ℤ‘2) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))))
255254ex 413 . . . . . . . . 9 (((𝑎 − 1) / 2) ∈ ℕ0 → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → (((𝑎 − 1) / 2) ∈ ℕ0 → ((#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1) → (𝑦 ∈ ℕ → (𝑎 ∈ (ℤ‘2) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))))
256255pm2.43a 54 . . . . . . . 8 (((𝑎 − 1) / 2) ∈ ℕ0 → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1) → (𝑦 ∈ ℕ → (𝑎 ∈ (ℤ‘2) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))))
257256com25 99 . . . . . . 7 (((𝑎 − 1) / 2) ∈ ℕ0 → (𝑎 ∈ (ℤ‘2) → ((#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1) → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))))
258257impcom 408 . . . . . 6 ((𝑎 ∈ (ℤ‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0) → ((#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1) → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))
25949, 258mpd 15 . . . . 5 ((𝑎 ∈ (ℤ‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0) → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))
260259ex 413 . . . 4 (𝑎 ∈ (ℤ‘2) → (((𝑎 − 1) / 2) ∈ ℕ0 → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))
26141, 260jaoi 855 . . 3 ((𝑎 = 1 ∨ 𝑎 ∈ (ℤ‘2)) → (((𝑎 − 1) / 2) ∈ ℕ0 → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))
2621, 261sylbi 216 . 2 (𝑎 ∈ ℕ → (((𝑎 − 1) / 2) ∈ ℕ0 → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))
263262imp31 418 1 (((𝑎 ∈ ℕ ∧ ((𝑎 − 1) / 2) ∈ ℕ0) ∧ 𝑦 ∈ ℕ) → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wral 3064  Vcvv 3445  {csn 4586  {cpr 4588  cfv 6496  (class class class)co 7357  Fincfn 8883  cc 11049  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056  +∞cpnf 11186  cmin 11385   / cdiv 11812  cn 12153  2c2 12208  0cn0 12413  cz 12499  cuz 12763  [,)cico 13266  ...cfz 13424  ..^cfzo 13567  cfl 13695  cexp 13967  Σcsu 15570  #bcblen 46645  digitcdig 46671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-fi 9347  df-sup 9378  df-inf 9379  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ioo 13268  df-ioc 13269  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-fl 13697  df-mod 13775  df-seq 13907  df-exp 13968  df-fac 14174  df-bc 14203  df-hash 14231  df-shft 14952  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-limsup 15353  df-clim 15370  df-rlim 15371  df-sum 15571  df-ef 15950  df-sin 15952  df-cos 15953  df-pi 15955  df-dvds 16137  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-rest 17304  df-topn 17305  df-0g 17323  df-gsum 17324  df-topgen 17325  df-pt 17326  df-prds 17329  df-xrs 17384  df-qtop 17389  df-imas 17390  df-xps 17392  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-mulg 18873  df-cntz 19097  df-cmn 19564  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-fbas 20793  df-fg 20794  df-cnfld 20797  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-cld 22370  df-ntr 22371  df-cls 22372  df-nei 22449  df-lp 22487  df-perf 22488  df-cn 22578  df-cnp 22579  df-haus 22666  df-tx 22913  df-hmeo 23106  df-fil 23197  df-fm 23289  df-flim 23290  df-flf 23291  df-xms 23673  df-ms 23674  df-tms 23675  df-cncf 24241  df-limc 25230  df-dv 25231  df-log 25912  df-cxp 25913  df-logb 26115  df-blen 46646  df-dig 46672
This theorem is referenced by:  nn0sumshdiglem1  46697
  Copyright terms: Public domain W3C validator