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 44578
Description: Lemma for nn0sumshdig 44581 (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 12314 . . 3 (𝑎 ∈ ℕ ↔ (𝑎 = 1 ∨ 𝑎 ∈ (ℤ‘2)))
2 1t1e1 11788 . . . . . . . . 9 (1 · 1) = 1
32eqcomi 2830 . . . . . . . 8 1 = (1 · 1)
4 simpl 483 . . . . . . . 8 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → 𝑎 = 1)
5 oveq2 7153 . . . . . . . . . . . 12 ((𝑦 + 1) = (#b𝑎) → (0..^(𝑦 + 1)) = (0..^(#b𝑎)))
65eqcoms 2829 . . . . . . . . . . 11 ((#b𝑎) = (𝑦 + 1) → (0..^(𝑦 + 1)) = (0..^(#b𝑎)))
7 fveq2 6664 . . . . . . . . . . . . . 14 (𝑎 = 1 → (#b𝑎) = (#b‘1))
8 blen1 44542 . . . . . . . . . . . . . 14 (#b‘1) = 1
97, 8syl6eq 2872 . . . . . . . . . . . . 13 (𝑎 = 1 → (#b𝑎) = 1)
109oveq2d 7161 . . . . . . . . . . . 12 (𝑎 = 1 → (0..^(#b𝑎)) = (0..^1))
11 fzo01 13109 . . . . . . . . . . . 12 (0..^1) = {0}
1210, 11syl6eq 2872 . . . . . . . . . . 11 (𝑎 = 1 → (0..^(#b𝑎)) = {0})
136, 12sylan9eqr 2878 . . . . . . . . . 10 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → (0..^(𝑦 + 1)) = {0})
1413sumeq1d 15048 . . . . . . . . 9 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)))
15 oveq2 7153 . . . . . . . . . . . . 13 (𝑎 = 1 → (𝑘(digit‘2)𝑎) = (𝑘(digit‘2)1))
1615oveq1d 7160 . . . . . . . . . . . 12 (𝑎 = 1 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((𝑘(digit‘2)1) · (2↑𝑘)))
1716sumeq2sdv 15051 . . . . . . . . . . 11 (𝑎 = 1 → Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ {0} ((𝑘(digit‘2)1) · (2↑𝑘)))
18 c0ex 10624 . . . . . . . . . . . 12 0 ∈ V
19 ax-1cn 10584 . . . . . . . . . . . . 13 1 ∈ ℂ
2019, 19mulcli 10637 . . . . . . . . . . . 12 (1 · 1) ∈ ℂ
21 oveq1 7152 . . . . . . . . . . . . . . 15 (𝑘 = 0 → (𝑘(digit‘2)1) = (0(digit‘2)1))
22 1ex 10626 . . . . . . . . . . . . . . . . 17 1 ∈ V
2322prid2 4693 . . . . . . . . . . . . . . . 16 1 ∈ {0, 1}
24 0dig2pr01 44568 . . . . . . . . . . . . . . . 16 (1 ∈ {0, 1} → (0(digit‘2)1) = 1)
2523, 24ax-mp 5 . . . . . . . . . . . . . . 15 (0(digit‘2)1) = 1
2621, 25syl6eq 2872 . . . . . . . . . . . . . 14 (𝑘 = 0 → (𝑘(digit‘2)1) = 1)
27 oveq2 7153 . . . . . . . . . . . . . . 15 (𝑘 = 0 → (2↑𝑘) = (2↑0))
28 2cn 11701 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
29 exp0 13423 . . . . . . . . . . . . . . . 16 (2 ∈ ℂ → (2↑0) = 1)
3028, 29ax-mp 5 . . . . . . . . . . . . . . 15 (2↑0) = 1
3127, 30syl6eq 2872 . . . . . . . . . . . . . 14 (𝑘 = 0 → (2↑𝑘) = 1)
3226, 31oveq12d 7163 . . . . . . . . . . . . 13 (𝑘 = 0 → ((𝑘(digit‘2)1) · (2↑𝑘)) = (1 · 1))
3332sumsn 15091 . . . . . . . . . . . 12 ((0 ∈ V ∧ (1 · 1) ∈ ℂ) → Σ𝑘 ∈ {0} ((𝑘(digit‘2)1) · (2↑𝑘)) = (1 · 1))
3418, 20, 33mp2an 688 . . . . . . . . . . 11 Σ𝑘 ∈ {0} ((𝑘(digit‘2)1) · (2↑𝑘)) = (1 · 1)
3517, 34syl6eq 2872 . . . . . . . . . 10 (𝑎 = 1 → Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (1 · 1))
3635adantr 481 . . . . . . . . 9 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (1 · 1))
3714, 36eqtrd 2856 . . . . . . . 8 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (1 · 1))
383, 4, 373eqtr4a 2882 . . . . . . 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 12276 . . . . . . . . 9 (𝑎 ∈ (ℤ‘2) → 𝑎 ∈ ℕ0)
43 nn0ob 15725 . . . . . . . . . 10 (𝑎 ∈ ℕ0 → (((𝑎 + 1) / 2) ∈ ℕ0 ↔ ((𝑎 − 1) / 2) ∈ ℕ0))
4443bicomd 224 . . . . . . . . 9 (𝑎 ∈ ℕ0 → (((𝑎 − 1) / 2) ∈ ℕ0 ↔ ((𝑎 + 1) / 2) ∈ ℕ0))
4542, 44syl 17 . . . . . . . 8 (𝑎 ∈ (ℤ‘2) → (((𝑎 − 1) / 2) ∈ ℕ0 ↔ ((𝑎 + 1) / 2) ∈ ℕ0))
46 blennngt2o2 44550 . . . . . . . . 9 ((𝑎 ∈ (ℤ‘2) ∧ ((𝑎 + 1) / 2) ∈ ℕ0) → (#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1))
4746ex 413 . . . . . . . 8 (𝑎 ∈ (ℤ‘2) → (((𝑎 + 1) / 2) ∈ ℕ0 → (#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1)))
4845, 47sylbid 241 . . . . . . 7 (𝑎 ∈ (ℤ‘2) → (((𝑎 − 1) / 2) ∈ ℕ0 → (#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1)))
4948imp 407 . . . . . 6 ((𝑎 ∈ (ℤ‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0) → (#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1))
50 fveqeq2 6673 . . . . . . . . . . . . 13 (𝑥 = ((𝑎 − 1) / 2) → ((#b𝑥) = 𝑦 ↔ (#b‘((𝑎 − 1) / 2)) = 𝑦))
51 id 22 . . . . . . . . . . . . . 14 (𝑥 = ((𝑎 − 1) / 2) → 𝑥 = ((𝑎 − 1) / 2))
52 oveq2 7153 . . . . . . . . . . . . . . . 16 (𝑥 = ((𝑎 − 1) / 2) → (𝑘(digit‘2)𝑥) = (𝑘(digit‘2)((𝑎 − 1) / 2)))
5352oveq1d 7160 . . . . . . . . . . . . . . 15 (𝑥 = ((𝑎 − 1) / 2) → ((𝑘(digit‘2)𝑥) · (2↑𝑘)) = ((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)))
5453sumeq2sdv 15051 . . . . . . . . . . . . . 14 (𝑥 = ((𝑎 − 1) / 2) → Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)))
5551, 54eqeq12d 2837 . . . . . . . . . . . . 13 (𝑥 = ((𝑎 − 1) / 2) → (𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)) ↔ ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))))
5650, 55imbi12d 346 . . . . . . . . . . . 12 (𝑥 = ((𝑎 − 1) / 2) → (((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) ↔ ((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)))))
5756rspcva 3620 . . . . . . . . . . 11 ((((𝑎 − 1) / 2) ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → ((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))))
58 eqeq1 2825 . . . . . . . . . . . . . . . 16 ((#b𝑎) = (𝑦 + 1) → ((#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1) ↔ (𝑦 + 1) = ((#b‘((𝑎 − 1) / 2)) + 1)))
59 nncn 11635 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
6059ad2antll 725 . . . . . . . . . . . . . . . . . . . 20 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑦 ∈ ℂ)
61 blennn0elnn 44535 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 − 1) / 2) ∈ ℕ0 → (#b‘((𝑎 − 1) / 2)) ∈ ℕ)
6261nncnd 11643 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎 − 1) / 2) ∈ ℕ0 → (#b‘((𝑎 − 1) / 2)) ∈ ℂ)
6362adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (#b‘((𝑎 − 1) / 2)) ∈ ℂ)
6463ad2antrl 724 . . . . . . . . . . . . . . . . . . . 20 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (#b‘((𝑎 − 1) / 2)) ∈ ℂ)
65 1cnd 10625 . . . . . . . . . . . . . . . . . . . 20 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 1 ∈ ℂ)
6660, 64, 65addcan2d 10833 . . . . . . . . . . . . . . . . . . 19 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → ((𝑦 + 1) = ((#b‘((𝑎 − 1) / 2)) + 1) ↔ 𝑦 = (#b‘((𝑎 − 1) / 2))))
67 eqcom 2828 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (#b‘((𝑎 − 1) / 2)) ↔ (#b‘((𝑎 − 1) / 2)) = 𝑦)
68 nnz 11993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
6968ad2antll 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑦 ∈ ℤ)
70 fzval3 13096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ℤ → (0...𝑦) = (0..^(𝑦 + 1)))
7169, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (0...𝑦) = (0..^(𝑦 + 1)))
7271eqcomd 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (0..^(𝑦 + 1)) = (0...𝑦))
7372sumeq1d 15048 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ (0...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)))
74 nnnn0 11893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ℕ → 𝑦 ∈ ℕ0)
75 elnn0uz 12272 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ℕ0𝑦 ∈ (ℤ‘0))
7674, 75sylib 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ‘0))
7776ad2antll 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑦 ∈ (ℤ‘0))
78 2nn 11699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 2 ∈ ℕ
7978a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑘 ∈ (0...𝑦)) → 2 ∈ ℕ)
80 elfzelz 12898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 ∈ (0...𝑦) → 𝑘 ∈ ℤ)
8180adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑘 ∈ (0...𝑦)) → 𝑘 ∈ ℤ)
82 nn0rp0 12833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 44557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((2 ∈ ℕ ∧ 𝑘 ∈ ℤ ∧ 𝑎 ∈ (0[,)+∞)) → (𝑘(digit‘2)𝑎) ∈ ℕ0)
8779, 81, 85, 86syl3anc 1363 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℕ0)
8887ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (𝑘 ∈ (0...𝑦) → (𝑘(digit‘2)𝑎) ∈ ℕ0))
8988ad2antrl 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11946 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℂ)
92 2nn0 11903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2 ∈ ℕ0
9392a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ (0...𝑦) → 2 ∈ ℕ0)
94 elfznn0 12990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ (0...𝑦) → 𝑘 ∈ ℕ0)
9593, 94nn0expcld 13597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ (0...𝑦) → (2↑𝑘) ∈ ℕ0)
9695nn0cnd 11946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 ∈ (0...𝑦) → (2↑𝑘) ∈ ℂ)
9796adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ (0...𝑦)) → (2↑𝑘) ∈ ℂ)
9891, 97mulcld 10650 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ (0...𝑦)) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) ∈ ℂ)
99 oveq1 7152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 0 → (𝑘(digit‘2)𝑎) = (0(digit‘2)𝑎))
10099, 27oveq12d 7163 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = 0 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · (2↑0)))
10130oveq2i 7156 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((0(digit‘2)𝑎) · (2↑0)) = ((0(digit‘2)𝑎) · 1)
102100, 101syl6eq 2872 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 = 0 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · 1))
10377, 98, 102fsum1p 15098 . . . . . . . . . . . . . . . . . . . . . . . . . 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 44571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑎 ∈ ℕ0 ∧ ((𝑎 + 1) / 2) ∈ ℕ0) → (0(digit‘2)𝑎) = 1)
108104, 106, 107syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (0(digit‘2)𝑎) = 1)
109108ad2antrl 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (0(digit‘2)𝑎) = 1)
110109oveq1d 7160 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → ((0(digit‘2)𝑎) · 1) = (1 · 1))
111110, 2syl6eq 2872 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → ((0(digit‘2)𝑎) · 1) = 1)
112 1z 12001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℤ
113112a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 1 ∈ ℤ)
114 0p1e1 11748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (0 + 1) = 1
115114, 112eqeltri 2909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (0 + 1) ∈ ℤ
116115a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (0 + 1) ∈ ℤ)
11778a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎 ∈ (ℤ‘2) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 2 ∈ ℕ)
118 elfzelz 12898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1363 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℂ)
128 2cnd 11704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ ((0 + 1)...𝑦) → 2 ∈ ℂ)
129 elfznn 12926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℕ)
130129nnnn0d 11944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℕ0)
131114oveq1i 7155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((0 + 1)...𝑦) = (1...𝑦)
132130, 131eleq2s 2931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ ((0 + 1)...𝑦) → 𝑘 ∈ ℕ0)
133128, 132expcld 13500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ ((0 + 1)...𝑦) → (2↑𝑘) ∈ ℂ)
134133adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (2↑𝑘) ∈ ℂ)
135127, 134mulcld 10650 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) ∈ ℂ)
136 oveq1 7152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = (𝑖 + 1) → (𝑘(digit‘2)𝑎) = ((𝑖 + 1)(digit‘2)𝑎))
137 oveq2 7153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = (𝑖 + 1) → (2↑𝑘) = (2↑(𝑖 + 1)))
138136, 137oveq12d 7163 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = (𝑖 + 1) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
139113, 116, 69, 135, 138fsumshftm 15126 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
140111, 139oveq12d 7163 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2860 . . . . . . . . . . . . . . . . . . . . . . . . 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 13028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ ℤ)
145144adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑖 ∈ ℤ)
146 nn0rp0 12833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 44557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((2 ∈ ℕ ∧ 𝑖 ∈ ℤ ∧ ((𝑎 − 1) / 2) ∈ (0[,)+∞)) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈ ℕ0)
150143, 145, 148, 149syl3anc 1363 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈ ℕ0)
151150nn0cnd 11946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈ ℂ)
152151ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (𝑖 ∈ (0..^𝑦) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈ ℂ))
153152ad2antrl 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ ℕ0)
157155, 156nn0expcld 13597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℕ0)
158157nn0cnd 11946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℂ)
159158adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑𝑖) ∈ ℂ)
160 2cnd 11704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → 2 ∈ ℂ)
161154, 159, 160mulassd 10653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2) = ((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)))
162161eqcomd 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)) = (((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2))
163162sumeq2dv 15050 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 0 ∈ ℂ
166 pncan1 11053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (0 ∈ ℂ → ((0 + 1) − 1) = 0)
167165, 166ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((0 + 1) − 1) = 0
168167a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ ℕ → ((0 + 1) − 1) = 0)
169168oveq1d 7160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ ℕ → (((0 + 1) − 1)...(𝑦 − 1)) = (0...(𝑦 − 1)))
170 fzoval 13029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ ℤ → (0..^𝑦) = (0...(𝑦 − 1)))
17168, 170syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ ℕ → (0..^𝑦) = (0...(𝑦 − 1)))
172169, 171eqtr4d 2859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ℕ → (((0 + 1) − 1)...(𝑦 − 1)) = (0..^𝑦))
173172ad2antll 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (((0 + 1) − 1)...(𝑦 − 1)) = (0..^𝑦))
174 simprlr 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑎 ∈ (ℤ‘2))
175 elfznn0 12990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 ∈ (0...(𝑦 − 1)) → 𝑖 ∈ ℕ0)
176167oveq1i 7155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((0 + 1) − 1)...(𝑦 − 1)) = (0...(𝑦 − 1))
177175, 176eleq2s 2931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1)) → 𝑖 ∈ ℕ0)
178 dignn0flhalf 44576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑎 ∈ (ℤ‘2) ∧ 𝑖 ∈ ℕ0) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)(⌊‘(𝑎 / 2))))
179174, 177, 178syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)(⌊‘(𝑎 / 2))))
180 eluzelz 12242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑎 ∈ (ℤ‘2) → 𝑎 ∈ ℤ)
181180adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑎 ∈ (ℤ‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0) → 𝑎 ∈ ℤ)
182 nn0z 11994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑎 − 1) / 2) ∈ ℕ0 → ((𝑎 − 1) / 2) ∈ ℤ)
183 zob 15698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎 ∈ ℤ → (((𝑎 + 1) / 2) ∈ ℤ ↔ ((𝑎 − 1) / 2) ∈ ℤ))
184180, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑎 ∈ (ℤ‘2) → (((𝑎 + 1) / 2) ∈ ℤ ↔ ((𝑎 − 1) / 2) ∈ ℤ))
185182, 184syl5ibr 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 44489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑎 ∈ ℤ ∧ ((𝑎 + 1) / 2) ∈ ℤ) → (⌊‘(𝑎 / 2)) = ((𝑎 − 1) / 2))
192190, 191syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → (⌊‘(𝑎 / 2)) = ((𝑎 − 1) / 2))
193192oveq2d 7161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → (𝑖(digit‘2)(⌊‘(𝑎 / 2))) = (𝑖(digit‘2)((𝑎 − 1) / 2)))
194179, 193eqtrd 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)((𝑎 − 1) / 2)))
195 2cnd 11704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1)) → 2 ∈ ℂ)
196195, 177expp1d 13501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7163 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = ((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)))
199173, 198sumeq12dv 15053 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝑖 → (𝑘(digit‘2)((𝑎 − 1) / 2)) = (𝑖(digit‘2)((𝑎 − 1) / 2)))
202 oveq2 7153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝑖 → (2↑𝑘) = (2↑𝑖))
203201, 202oveq12d 7163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝑖 → ((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) = ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)))
204203cbvsumv 15043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖))
205204eqeq2i 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ↔ ((𝑎 − 1) / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)))
206205biimpi 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7160 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (0..^𝑦) ∈ Fin
210209a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → (0..^𝑦) ∈ Fin)
211 2cnd 11704 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 15130 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2856 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2866 . . . . . . . . . . . . . . . . . . . . . . . . 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 7161 . . . . . . . . . . . . . . . . . . . . . . . 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 12244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 ∈ (ℤ‘2) → 𝑎 ∈ ℂ)
223 peano2cnm 10941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 ∈ ℂ → (𝑎 − 1) ∈ ℂ)
224222, 223syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎 ∈ (ℤ‘2) → (𝑎 − 1) ∈ ℂ)
225 2cnd 11704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎 ∈ (ℤ‘2) → 2 ∈ ℂ)
226 2ne0 11730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2 ≠ 0
227226a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎 ∈ (ℤ‘2) → 2 ≠ 0)
228224, 225, 2273jca 1120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 ∈ (ℤ‘2) → ((𝑎 − 1) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0))
229228adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → ((𝑎 − 1) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0))
230 divcan1 11296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑎 − 1) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (((𝑎 − 1) / 2) · 2) = (𝑎 − 1))
231229, 230syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (((𝑎 − 1) / 2) · 2) = (𝑎 − 1))
232231oveq2d 7161 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (1 + (((𝑎 − 1) / 2) · 2)) = (1 + (𝑎 − 1)))
233 1cnd 10625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 ∈ (ℤ‘2) → 1 ∈ ℂ)
234233, 222jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 ∈ (ℤ‘2) → (1 ∈ ℂ ∧ 𝑎 ∈ ℂ))
235234adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (1 ∈ ℂ ∧ 𝑎 ∈ ℂ))
236 pncan3 10883 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((1 ∈ ℂ ∧ 𝑎 ∈ ℂ) → (1 + (𝑎 − 1)) = 𝑎)
237235, 236syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (1 + (𝑎 − 1)) = 𝑎)
238232, 237eqtrd 2856 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (1 + (((𝑎 − 1) / 2) · 2)) = 𝑎)
239238adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ) → (1 + (((𝑎 − 1) / 2) · 2)) = 𝑎)
240239ad2antll 725 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → (1 + (((𝑎 − 1) / 2) · 2)) = 𝑎)
241142, 221, 2403eqtrrd 2861 . . . . . . . . . . . . . . . . . . . . . . 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, 244syl5bi 243 . . . . . . . . . . . . . . . . . . 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 241 . . . . . . . . . . . . . . . . . 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 241 . . . . . . . . . . . . . . 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 851 . . 3 ((𝑎 = 1 ∨ 𝑎 ∈ (ℤ‘2)) → (((𝑎 − 1) / 2) ∈ ℕ0 → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))
2621, 261sylbi 218 . 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 207  wa 396  wo 841  w3a 1079   = wceq 1528  wcel 2105  wne 3016  wral 3138  Vcvv 3495  {csn 4559  {cpr 4561  cfv 6349  (class class class)co 7145  Fincfn 8498  cc 10524  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531  +∞cpnf 10661  cmin 10859   / cdiv 11286  cn 11627  2c2 11681  0cn0 11886  cz 11970  cuz 12232  [,)cico 12730  ...cfz 12882  ..^cfzo 13023  cfl 13150  cexp 13419  Σcsu 15032  #bcblen 44527  digitcdig 44553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-inf2 9093  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604  ax-addf 10605  ax-mulf 10606
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-int 4870  df-iun 4914  df-iin 4915  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-se 5509  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-isom 6358  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7398  df-om 7569  df-1st 7680  df-2nd 7681  df-supp 7822  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-1o 8093  df-2o 8094  df-oadd 8097  df-er 8279  df-map 8398  df-pm 8399  df-ixp 8451  df-en 8499  df-dom 8500  df-sdom 8501  df-fin 8502  df-fsupp 8823  df-fi 8864  df-sup 8895  df-inf 8896  df-oi 8963  df-card 9357  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11628  df-2 11689  df-3 11690  df-4 11691  df-5 11692  df-6 11693  df-7 11694  df-8 11695  df-9 11696  df-n0 11887  df-z 11971  df-dec 12088  df-uz 12233  df-q 12338  df-rp 12380  df-xneg 12497  df-xadd 12498  df-xmul 12499  df-ioo 12732  df-ioc 12733  df-ico 12734  df-icc 12735  df-fz 12883  df-fzo 13024  df-fl 13152  df-mod 13228  df-seq 13360  df-exp 13420  df-fac 13624  df-bc 13653  df-hash 13681  df-shft 14416  df-cj 14448  df-re 14449  df-im 14450  df-sqrt 14584  df-abs 14585  df-limsup 14818  df-clim 14835  df-rlim 14836  df-sum 15033  df-ef 15411  df-sin 15413  df-cos 15414  df-pi 15416  df-dvds 15598  df-struct 16475  df-ndx 16476  df-slot 16477  df-base 16479  df-sets 16480  df-ress 16481  df-plusg 16568  df-mulr 16569  df-starv 16570  df-sca 16571  df-vsca 16572  df-ip 16573  df-tset 16574  df-ple 16575  df-ds 16577  df-unif 16578  df-hom 16579  df-cco 16580  df-rest 16686  df-topn 16687  df-0g 16705  df-gsum 16706  df-topgen 16707  df-pt 16708  df-prds 16711  df-xrs 16765  df-qtop 16770  df-imas 16771  df-xps 16773  df-mre 16847  df-mrc 16848  df-acs 16850  df-mgm 17842  df-sgrp 17891  df-mnd 17902  df-submnd 17947  df-mulg 18165  df-cntz 18387  df-cmn 18839  df-psmet 20467  df-xmet 20468  df-met 20469  df-bl 20470  df-mopn 20471  df-fbas 20472  df-fg 20473  df-cnfld 20476  df-top 21432  df-topon 21449  df-topsp 21471  df-bases 21484  df-cld 21557  df-ntr 21558  df-cls 21559  df-nei 21636  df-lp 21674  df-perf 21675  df-cn 21765  df-cnp 21766  df-haus 21853  df-tx 22100  df-hmeo 22293  df-fil 22384  df-fm 22476  df-flim 22477  df-flf 22478  df-xms 22859  df-ms 22860  df-tms 22861  df-cncf 23415  df-limc 24393  df-dv 24394  df-log 25067  df-cxp 25068  df-logb 25270  df-blen 44528  df-dig 44554
This theorem is referenced by:  nn0sumshdiglem1  44579
  Copyright terms: Public domain W3C validator