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 43015
Description: Lemma for nn0sumshdig 43018 (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 11966 . . 3 (𝑎 ∈ ℕ ↔ (𝑎 = 1 ∨ 𝑎 ∈ (ℤ‘2)))
2 1t1e1 11440 . . . . . . . . 9 (1 · 1) = 1
32eqcomi 2774 . . . . . . . 8 1 = (1 · 1)
4 simpl 474 . . . . . . . 8 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → 𝑎 = 1)
5 oveq2 6850 . . . . . . . . . . . 12 ((𝑦 + 1) = (#b𝑎) → (0..^(𝑦 + 1)) = (0..^(#b𝑎)))
65eqcoms 2773 . . . . . . . . . . 11 ((#b𝑎) = (𝑦 + 1) → (0..^(𝑦 + 1)) = (0..^(#b𝑎)))
7 fveq2 6375 . . . . . . . . . . . . . 14 (𝑎 = 1 → (#b𝑎) = (#b‘1))
8 blen1 42979 . . . . . . . . . . . . . 14 (#b‘1) = 1
97, 8syl6eq 2815 . . . . . . . . . . . . 13 (𝑎 = 1 → (#b𝑎) = 1)
109oveq2d 6858 . . . . . . . . . . . 12 (𝑎 = 1 → (0..^(#b𝑎)) = (0..^1))
11 fzo01 12758 . . . . . . . . . . . 12 (0..^1) = {0}
1210, 11syl6eq 2815 . . . . . . . . . . 11 (𝑎 = 1 → (0..^(#b𝑎)) = {0})
136, 12sylan9eqr 2821 . . . . . . . . . 10 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → (0..^(𝑦 + 1)) = {0})
1413sumeq1d 14718 . . . . . . . . 9 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)))
15 oveq2 6850 . . . . . . . . . . . . 13 (𝑎 = 1 → (𝑘(digit‘2)𝑎) = (𝑘(digit‘2)1))
1615oveq1d 6857 . . . . . . . . . . . 12 (𝑎 = 1 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((𝑘(digit‘2)1) · (2↑𝑘)))
1716sumeq2sdv 14722 . . . . . . . . . . 11 (𝑎 = 1 → Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ {0} ((𝑘(digit‘2)1) · (2↑𝑘)))
18 c0ex 10287 . . . . . . . . . . . 12 0 ∈ V
19 ax-1cn 10247 . . . . . . . . . . . . 13 1 ∈ ℂ
2019, 19mulcli 10301 . . . . . . . . . . . 12 (1 · 1) ∈ ℂ
21 oveq1 6849 . . . . . . . . . . . . . . 15 (𝑘 = 0 → (𝑘(digit‘2)1) = (0(digit‘2)1))
22 1ex 10289 . . . . . . . . . . . . . . . . 17 1 ∈ V
2322prid2 4453 . . . . . . . . . . . . . . . 16 1 ∈ {0, 1}
24 0dig2pr01 43005 . . . . . . . . . . . . . . . 16 (1 ∈ {0, 1} → (0(digit‘2)1) = 1)
2523, 24ax-mp 5 . . . . . . . . . . . . . . 15 (0(digit‘2)1) = 1
2621, 25syl6eq 2815 . . . . . . . . . . . . . 14 (𝑘 = 0 → (𝑘(digit‘2)1) = 1)
27 oveq2 6850 . . . . . . . . . . . . . . 15 (𝑘 = 0 → (2↑𝑘) = (2↑0))
28 2cn 11347 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
29 exp0 13071 . . . . . . . . . . . . . . . 16 (2 ∈ ℂ → (2↑0) = 1)
3028, 29ax-mp 5 . . . . . . . . . . . . . . 15 (2↑0) = 1
3127, 30syl6eq 2815 . . . . . . . . . . . . . 14 (𝑘 = 0 → (2↑𝑘) = 1)
3226, 31oveq12d 6860 . . . . . . . . . . . . 13 (𝑘 = 0 → ((𝑘(digit‘2)1) · (2↑𝑘)) = (1 · 1))
3332sumsn 14762 . . . . . . . . . . . 12 ((0 ∈ V ∧ (1 · 1) ∈ ℂ) → Σ𝑘 ∈ {0} ((𝑘(digit‘2)1) · (2↑𝑘)) = (1 · 1))
3418, 20, 33mp2an 683 . . . . . . . . . . 11 Σ𝑘 ∈ {0} ((𝑘(digit‘2)1) · (2↑𝑘)) = (1 · 1)
3517, 34syl6eq 2815 . . . . . . . . . 10 (𝑎 = 1 → Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (1 · 1))
3635adantr 472 . . . . . . . . 9 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (1 · 1))
3714, 36eqtrd 2799 . . . . . . . 8 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (1 · 1))
383, 4, 373eqtr4a 2825 . . . . . . 7 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))
3938ex 401 . . . . . 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 11927 . . . . . . . . 9 (𝑎 ∈ (ℤ‘2) → 𝑎 ∈ ℕ0)
43 nn0ob 15384 . . . . . . . . . 10 (𝑎 ∈ ℕ0 → (((𝑎 + 1) / 2) ∈ ℕ0 ↔ ((𝑎 − 1) / 2) ∈ ℕ0))
4443bicomd 214 . . . . . . . . 9 (𝑎 ∈ ℕ0 → (((𝑎 − 1) / 2) ∈ ℕ0 ↔ ((𝑎 + 1) / 2) ∈ ℕ0))
4542, 44syl 17 . . . . . . . 8 (𝑎 ∈ (ℤ‘2) → (((𝑎 − 1) / 2) ∈ ℕ0 ↔ ((𝑎 + 1) / 2) ∈ ℕ0))
46 blennngt2o2 42987 . . . . . . . . 9 ((𝑎 ∈ (ℤ‘2) ∧ ((𝑎 + 1) / 2) ∈ ℕ0) → (#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1))
4746ex 401 . . . . . . . 8 (𝑎 ∈ (ℤ‘2) → (((𝑎 + 1) / 2) ∈ ℕ0 → (#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1)))
4845, 47sylbid 231 . . . . . . 7 (𝑎 ∈ (ℤ‘2) → (((𝑎 − 1) / 2) ∈ ℕ0 → (#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1)))
4948imp 395 . . . . . 6 ((𝑎 ∈ (ℤ‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0) → (#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1))
50 fveqeq2 6384 . . . . . . . . . . . . 13 (𝑥 = ((𝑎 − 1) / 2) → ((#b𝑥) = 𝑦 ↔ (#b‘((𝑎 − 1) / 2)) = 𝑦))
51 id 22 . . . . . . . . . . . . . 14 (𝑥 = ((𝑎 − 1) / 2) → 𝑥 = ((𝑎 − 1) / 2))
52 oveq2 6850 . . . . . . . . . . . . . . . 16 (𝑥 = ((𝑎 − 1) / 2) → (𝑘(digit‘2)𝑥) = (𝑘(digit‘2)((𝑎 − 1) / 2)))
5352oveq1d 6857 . . . . . . . . . . . . . . 15 (𝑥 = ((𝑎 − 1) / 2) → ((𝑘(digit‘2)𝑥) · (2↑𝑘)) = ((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)))
5453sumeq2sdv 14722 . . . . . . . . . . . . . 14 (𝑥 = ((𝑎 − 1) / 2) → Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)))
5551, 54eqeq12d 2780 . . . . . . . . . . . . 13 (𝑥 = ((𝑎 − 1) / 2) → (𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)) ↔ ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))))
5650, 55imbi12d 335 . . . . . . . . . . . 12 (𝑥 = ((𝑎 − 1) / 2) → (((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) ↔ ((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)))))
5756rspcva 3459 . . . . . . . . . . 11 ((((𝑎 − 1) / 2) ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → ((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))))
58 eqeq1 2769 . . . . . . . . . . . . . . . 16 ((#b𝑎) = (𝑦 + 1) → ((#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1) ↔ (𝑦 + 1) = ((#b‘((𝑎 − 1) / 2)) + 1)))
59 nncn 11283 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
6059ad2antll 720 . . . . . . . . . . . . . . . . . . . 20 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑦 ∈ ℂ)
61 blennn0elnn 42972 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 − 1) / 2) ∈ ℕ0 → (#b‘((𝑎 − 1) / 2)) ∈ ℕ)
6261nncnd 11292 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎 − 1) / 2) ∈ ℕ0 → (#b‘((𝑎 − 1) / 2)) ∈ ℂ)
6362adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (#b‘((𝑎 − 1) / 2)) ∈ ℂ)
6463ad2antrl 719 . . . . . . . . . . . . . . . . . . . 20 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (#b‘((𝑎 − 1) / 2)) ∈ ℂ)
65 1cnd 10288 . . . . . . . . . . . . . . . . . . . 20 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 1 ∈ ℂ)
6660, 64, 65addcan2d 10494 . . . . . . . . . . . . . . . . . . 19 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → ((𝑦 + 1) = ((#b‘((𝑎 − 1) / 2)) + 1) ↔ 𝑦 = (#b‘((𝑎 − 1) / 2))))
67 eqcom 2772 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (#b‘((𝑎 − 1) / 2)) ↔ (#b‘((𝑎 − 1) / 2)) = 𝑦)
68 nnz 11646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
6968ad2antll 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑦 ∈ ℤ)
70 fzval3 12745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ℤ → (0...𝑦) = (0..^(𝑦 + 1)))
7169, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (0...𝑦) = (0..^(𝑦 + 1)))
7271eqcomd 2771 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (0..^(𝑦 + 1)) = (0...𝑦))
7372sumeq1d 14718 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ (0...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)))
74 nnnn0 11546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ℕ → 𝑦 ∈ ℕ0)
75 elnn0uz 11925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ℕ0𝑦 ∈ (ℤ‘0))
7674, 75sylib 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ‘0))
7776ad2antll 720 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑦 ∈ (ℤ‘0))
78 2nn 11345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 2 ∈ ℕ
7978a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑘 ∈ (0...𝑦)) → 2 ∈ ℕ)
80 elfzelz 12549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 ∈ (0...𝑦) → 𝑘 ∈ ℤ)
8180adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑘 ∈ (0...𝑦)) → 𝑘 ∈ ℤ)
82 nn0rp0 12483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑎 ∈ ℕ0𝑎 ∈ (0[,)+∞))
8342, 82syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑎 ∈ (ℤ‘2) → 𝑎 ∈ (0[,)+∞))
8483adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → 𝑎 ∈ (0[,)+∞))
8584adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑘 ∈ (0...𝑦)) → 𝑎 ∈ (0[,)+∞))
86 digvalnn0 42994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((2 ∈ ℕ ∧ 𝑘 ∈ ℤ ∧ 𝑎 ∈ (0[,)+∞)) → (𝑘(digit‘2)𝑎) ∈ ℕ0)
8779, 81, 85, 86syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℕ0)
8887ex 401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (𝑘 ∈ (0...𝑦) → (𝑘(digit‘2)𝑎) ∈ ℕ0))
8988ad2antrl 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (𝑘 ∈ (0...𝑦) → (𝑘(digit‘2)𝑎) ∈ ℕ0))
9089imp 395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℕ0)
9190nn0cnd 11600 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℂ)
92 2nn0 11557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2 ∈ ℕ0
9392a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ (0...𝑦) → 2 ∈ ℕ0)
94 elfznn0 12640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ (0...𝑦) → 𝑘 ∈ ℕ0)
9593, 94nn0expcld 13238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ (0...𝑦) → (2↑𝑘) ∈ ℕ0)
9695nn0cnd 11600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 ∈ (0...𝑦) → (2↑𝑘) ∈ ℂ)
9796adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ (0...𝑦)) → (2↑𝑘) ∈ ℂ)
9891, 97mulcld 10314 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ (0...𝑦)) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) ∈ ℂ)
99 oveq1 6849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 0 → (𝑘(digit‘2)𝑎) = (0(digit‘2)𝑎))
10099, 27oveq12d 6860 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = 0 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · (2↑0)))
10130oveq2i 6853 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((0(digit‘2)𝑎) · (2↑0)) = ((0(digit‘2)𝑎) · 1)
102100, 101syl6eq 2815 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 = 0 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · 1))
10377, 98, 102fsum1p 14769 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑘 ∈ (0...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (((0(digit‘2)𝑎) · 1) + Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))))
10442adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → 𝑎 ∈ ℕ0)
10542, 43syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 ∈ (ℤ‘2) → (((𝑎 + 1) / 2) ∈ ℕ0 ↔ ((𝑎 − 1) / 2) ∈ ℕ0))
106105biimparc 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → ((𝑎 + 1) / 2) ∈ ℕ0)
107 0dig2nn0o 43008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑎 ∈ ℕ0 ∧ ((𝑎 + 1) / 2) ∈ ℕ0) → (0(digit‘2)𝑎) = 1)
108104, 106, 107syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (0(digit‘2)𝑎) = 1)
109108ad2antrl 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (0(digit‘2)𝑎) = 1)
110109oveq1d 6857 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → ((0(digit‘2)𝑎) · 1) = (1 · 1))
111110, 2syl6eq 2815 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → ((0(digit‘2)𝑎) · 1) = 1)
112 1z 11654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℤ
113112a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 1 ∈ ℤ)
114 0p1e1 11401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (0 + 1) = 1
115114, 112eqeltri 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (0 + 1) ∈ ℤ
116115a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (0 + 1) ∈ ℤ)
11778a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎 ∈ (ℤ‘2) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 2 ∈ ℕ)
118 elfzelz 12549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 ∈ ((0 + 1)...𝑦) → 𝑘 ∈ ℤ)
119118adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎 ∈ (ℤ‘2) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 𝑘 ∈ ℤ)
12042adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑎 ∈ (ℤ‘2) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 𝑎 ∈ ℕ0)
121120, 82syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎 ∈ (ℤ‘2) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 𝑎 ∈ (0[,)+∞))
122117, 119, 121, 86syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑎 ∈ (ℤ‘2) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℕ0)
123122ex 401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎 ∈ (ℤ‘2) → (𝑘 ∈ ((0 + 1)...𝑦) → (𝑘(digit‘2)𝑎) ∈ ℕ0))
124123adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (𝑘 ∈ ((0 + 1)...𝑦) → (𝑘(digit‘2)𝑎) ∈ ℕ0))
125124ad2antrl 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (𝑘 ∈ ((0 + 1)...𝑦) → (𝑘(digit‘2)𝑎) ∈ ℕ0))
126125imp 395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℕ0)
127126nn0cnd 11600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℂ)
128 2cnd 11350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ ((0 + 1)...𝑦) → 2 ∈ ℂ)
129 elfznn 12577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℕ)
130129nnnn0d 11598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℕ0)
131114oveq1i 6852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((0 + 1)...𝑦) = (1...𝑦)
132130, 131eleq2s 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ ((0 + 1)...𝑦) → 𝑘 ∈ ℕ0)
133128, 132expcld 13215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ ((0 + 1)...𝑦) → (2↑𝑘) ∈ ℂ)
134133adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (2↑𝑘) ∈ ℂ)
135127, 134mulcld 10314 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) ∈ ℂ)
136 oveq1 6849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = (𝑖 + 1) → (𝑘(digit‘2)𝑎) = ((𝑖 + 1)(digit‘2)𝑎))
137 oveq2 6850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = (𝑖 + 1) → (2↑𝑘) = (2↑(𝑖 + 1)))
138136, 137oveq12d 6860 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = (𝑖 + 1) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
139113, 116, 69, 135, 138fsumshftm 14799 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
140111, 139oveq12d 6860 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2803 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (1 + Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))))
142141adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 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 12678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ ℤ)
145144adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑖 ∈ ℤ)
146 nn0rp0 12483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑎 − 1) / 2) ∈ ℕ0 → ((𝑎 − 1) / 2) ∈ (0[,)+∞))
147146adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → ((𝑎 − 1) / 2) ∈ (0[,)+∞))
148147adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑎 − 1) / 2) ∈ (0[,)+∞))
149 digvalnn0 42994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((2 ∈ ℕ ∧ 𝑖 ∈ ℤ ∧ ((𝑎 − 1) / 2) ∈ (0[,)+∞)) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈ ℕ0)
150143, 145, 148, 149syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈ ℕ0)
151150nn0cnd 11600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈ ℂ)
152151ex 401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (𝑖 ∈ (0..^𝑦) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈ ℂ))
153152ad2antrl 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (𝑖 ∈ (0..^𝑦) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈ ℂ))
154153imp 395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈ ℂ)
15592a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ (0..^𝑦) → 2 ∈ ℕ0)
156 elfzonn0 12721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ ℕ0)
157155, 156nn0expcld 13238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℕ0)
158157nn0cnd 11600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℂ)
159158adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑𝑖) ∈ ℂ)
160 2cnd 11350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → 2 ∈ ℂ)
161154, 159, 160mulassd 10317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2) = ((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)))
162161eqcomd 2771 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)) = (((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2))
163162sumeq2dv 14720 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)) = Σ𝑖 ∈ (0..^𝑦)(((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2))
164163adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 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 10285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 0 ∈ ℂ
166 pncan1 10708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (0 ∈ ℂ → ((0 + 1) − 1) = 0)
167165, 166ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((0 + 1) − 1) = 0
168167a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ ℕ → ((0 + 1) − 1) = 0)
169168oveq1d 6857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ ℕ → (((0 + 1) − 1)...(𝑦 − 1)) = (0...(𝑦 − 1)))
170 fzoval 12679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ ℤ → (0..^𝑦) = (0...(𝑦 − 1)))
17168, 170syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ ℕ → (0..^𝑦) = (0...(𝑦 − 1)))
172169, 171eqtr4d 2802 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ℕ → (((0 + 1) − 1)...(𝑦 − 1)) = (0..^𝑦))
173172ad2antll 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (((0 + 1) − 1)...(𝑦 − 1)) = (0..^𝑦))
174 simprlr 798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑎 ∈ (ℤ‘2))
175 elfznn0 12640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 ∈ (0...(𝑦 − 1)) → 𝑖 ∈ ℕ0)
176167oveq1i 6852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((0 + 1) − 1)...(𝑦 − 1)) = (0...(𝑦 − 1))
177175, 176eleq2s 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1)) → 𝑖 ∈ ℕ0)
178 dignn0flhalf 43013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑎 ∈ (ℤ‘2) ∧ 𝑖 ∈ ℕ0) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)(⌊‘(𝑎 / 2))))
179174, 177, 178syl2an 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)(⌊‘(𝑎 / 2))))
180 eluzelz 11896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑎 ∈ (ℤ‘2) → 𝑎 ∈ ℤ)
181180adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑎 ∈ (ℤ‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0) → 𝑎 ∈ ℤ)
182 nn0z 11647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑎 − 1) / 2) ∈ ℕ0 → ((𝑎 − 1) / 2) ∈ ℤ)
183 zob 15367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎 ∈ ℤ → (((𝑎 + 1) / 2) ∈ ℤ ↔ ((𝑎 − 1) / 2) ∈ ℤ))
184180, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑎 ∈ (ℤ‘2) → (((𝑎 + 1) / 2) ∈ ℤ ↔ ((𝑎 − 1) / 2) ∈ ℤ))
185182, 184syl5ibr 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑎 ∈ (ℤ‘2) → (((𝑎 − 1) / 2) ∈ ℕ0 → ((𝑎 + 1) / 2) ∈ ℤ))
186185imp 395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑎 ∈ (ℤ‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0) → ((𝑎 + 1) / 2) ∈ ℤ)
187181, 186jca 507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎 ∈ (ℤ‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0) → (𝑎 ∈ ℤ ∧ ((𝑎 + 1) / 2) ∈ ℤ))
188187ancoms 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (𝑎 ∈ ℤ ∧ ((𝑎 + 1) / 2) ∈ ℤ))
189188ad2antrl 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (𝑎 ∈ ℤ ∧ ((𝑎 + 1) / 2) ∈ ℤ))
190189adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → (𝑎 ∈ ℤ ∧ ((𝑎 + 1) / 2) ∈ ℤ))
191 zofldiv2 42926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑎 ∈ ℤ ∧ ((𝑎 + 1) / 2) ∈ ℤ) → (⌊‘(𝑎 / 2)) = ((𝑎 − 1) / 2))
192190, 191syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → (⌊‘(𝑎 / 2)) = ((𝑎 − 1) / 2))
193192oveq2d 6858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → (𝑖(digit‘2)(⌊‘(𝑎 / 2))) = (𝑖(digit‘2)((𝑎 − 1) / 2)))
194179, 193eqtrd 2799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)((𝑎 − 1) / 2)))
195 2cnd 11350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1)) → 2 ∈ ℂ)
196195, 177expp1d 13216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1)) → (2↑(𝑖 + 1)) = ((2↑𝑖) · 2))
197196adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → (2↑(𝑖 + 1)) = ((2↑𝑖) · 2))
198194, 197oveq12d 6860 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = ((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)))
199173, 198sumeq12dv 14724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)))
200199adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 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 6849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝑖 → (𝑘(digit‘2)((𝑎 − 1) / 2)) = (𝑖(digit‘2)((𝑎 − 1) / 2)))
202 oveq2 6850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝑖 → (2↑𝑘) = (2↑𝑖))
203201, 202oveq12d 6860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝑖 → ((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) = ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)))
204203cbvsumv 14713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖))
205204eqeq2i 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ↔ ((𝑎 − 1) / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)))
206205biimpi 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) → ((𝑎 − 1) / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)))
207206adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → ((𝑎 − 1) / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)))
208207oveq1d 6857 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (0..^𝑦) ∈ Fin
210209a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → (0..^𝑦) ∈ Fin)
211 2cnd 11350 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → 2 ∈ ℂ)
212158adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑𝑖) ∈ ℂ)
213151, 212mulcld 10314 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) ∈ ℂ)
214213ex 401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (𝑖 ∈ (0..^𝑦) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) ∈ ℂ))
215214adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ) → (𝑖 ∈ (0..^𝑦) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) ∈ ℂ))
216215ad2antll 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → (𝑖 ∈ (0..^𝑦) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) ∈ ℂ))
217216imp 395 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) ∈ ℂ)
218210, 211, 217fsummulc1 14803 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2799 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2809 . . . . . . . . . . . . . . . . . . . . . . . . 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 6858 . . . . . . . . . . . . . . . . . . . . . . . 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 11898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 ∈ (ℤ‘2) → 𝑎 ∈ ℂ)
223 peano2cnm 10601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 ∈ ℂ → (𝑎 − 1) ∈ ℂ)
224222, 223syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎 ∈ (ℤ‘2) → (𝑎 − 1) ∈ ℂ)
225 2cnd 11350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎 ∈ (ℤ‘2) → 2 ∈ ℂ)
226 2ne0 11383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2 ≠ 0
227226a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎 ∈ (ℤ‘2) → 2 ≠ 0)
228224, 225, 2273jca 1158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 ∈ (ℤ‘2) → ((𝑎 − 1) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0))
229228adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → ((𝑎 − 1) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0))
230 divcan1 10948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑎 − 1) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (((𝑎 − 1) / 2) · 2) = (𝑎 − 1))
231229, 230syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (((𝑎 − 1) / 2) · 2) = (𝑎 − 1))
232231oveq2d 6858 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (1 + (((𝑎 − 1) / 2) · 2)) = (1 + (𝑎 − 1)))
233 1cnd 10288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 ∈ (ℤ‘2) → 1 ∈ ℂ)
234233, 222jca 507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 ∈ (ℤ‘2) → (1 ∈ ℂ ∧ 𝑎 ∈ ℂ))
235234adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (1 ∈ ℂ ∧ 𝑎 ∈ ℂ))
236 pncan3 10543 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((1 ∈ ℂ ∧ 𝑎 ∈ ℂ) → (1 + (𝑎 − 1)) = 𝑎)
237235, 236syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (1 + (𝑎 − 1)) = 𝑎)
238232, 237eqtrd 2799 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (1 + (((𝑎 − 1) / 2) · 2)) = 𝑎)
239238adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ) → (1 + (((𝑎 − 1) / 2) · 2)) = 𝑎)
240239ad2antll 720 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → (1 + (((𝑎 − 1) / 2) · 2)) = 𝑎)
241142, 221, 2403eqtrrd 2804 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))
242241ex 401 . . . . . . . . . . . . . . . . . . . . . 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 233 . . . . . . . . . . . . . . . . . . 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 231 . . . . . . . . . . . . . . . . . 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 401 . . . . . . . . . . . . . . . . 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 231 . . . . . . . . . . . . . . 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 423 . . . . . . . . . . . 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 401 . . . . . . . . 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 396 . . . . . 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 401 . . . 4 (𝑎 ∈ (ℤ‘2) → (((𝑎 − 1) / 2) ∈ ℕ0 → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))
26141, 260jaoi 883 . . 3 ((𝑎 = 1 ∨ 𝑎 ∈ (ℤ‘2)) → (((𝑎 − 1) / 2) ∈ ℕ0 → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))
2621, 261sylbi 208 . 2 (𝑎 ∈ ℕ → (((𝑎 − 1) / 2) ∈ ℕ0 → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))
263262imp31 408 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 197  wa 384  wo 873  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055  Vcvv 3350  {csn 4334  {cpr 4336  cfv 6068  (class class class)co 6842  Fincfn 8160  cc 10187  0cc0 10189  1c1 10190   + caddc 10192   · cmul 10194  +∞cpnf 10325  cmin 10520   / cdiv 10938  cn 11274  2c2 11327  0cn0 11538  cz 11624  cuz 11886  [,)cico 12379  ...cfz 12533  ..^cfzo 12673  cfl 12799  cexp 13067  Σcsu 14703  #bcblen 42964  digitcdig 42990
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 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267  ax-addf 10268  ax-mulf 10269
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 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-of 7095  df-om 7264  df-1st 7366  df-2nd 7367  df-supp 7498  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-map 8062  df-pm 8063  df-ixp 8114  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fsupp 8483  df-fi 8524  df-sup 8555  df-inf 8556  df-oi 8622  df-card 9016  df-cda 9243  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-dec 11741  df-uz 11887  df-q 11990  df-rp 12029  df-xneg 12146  df-xadd 12147  df-xmul 12148  df-ioo 12381  df-ioc 12382  df-ico 12383  df-icc 12384  df-fz 12534  df-fzo 12674  df-fl 12801  df-mod 12877  df-seq 13009  df-exp 13068  df-fac 13265  df-bc 13294  df-hash 13322  df-shft 14094  df-cj 14126  df-re 14127  df-im 14128  df-sqrt 14262  df-abs 14263  df-limsup 14489  df-clim 14506  df-rlim 14507  df-sum 14704  df-ef 15082  df-sin 15084  df-cos 15085  df-pi 15087  df-dvds 15268  df-struct 16134  df-ndx 16135  df-slot 16136  df-base 16138  df-sets 16139  df-ress 16140  df-plusg 16229  df-mulr 16230  df-starv 16231  df-sca 16232  df-vsca 16233  df-ip 16234  df-tset 16235  df-ple 16236  df-ds 16238  df-unif 16239  df-hom 16240  df-cco 16241  df-rest 16351  df-topn 16352  df-0g 16370  df-gsum 16371  df-topgen 16372  df-pt 16373  df-prds 16376  df-xrs 16430  df-qtop 16435  df-imas 16436  df-xps 16438  df-mre 16514  df-mrc 16515  df-acs 16517  df-mgm 17510  df-sgrp 17552  df-mnd 17563  df-submnd 17604  df-mulg 17810  df-cntz 18015  df-cmn 18461  df-psmet 20011  df-xmet 20012  df-met 20013  df-bl 20014  df-mopn 20015  df-fbas 20016  df-fg 20017  df-cnfld 20020  df-top 20978  df-topon 20995  df-topsp 21017  df-bases 21030  df-cld 21103  df-ntr 21104  df-cls 21105  df-nei 21182  df-lp 21220  df-perf 21221  df-cn 21311  df-cnp 21312  df-haus 21399  df-tx 21645  df-hmeo 21838  df-fil 21929  df-fm 22021  df-flim 22022  df-flf 22023  df-xms 22404  df-ms 22405  df-tms 22406  df-cncf 22960  df-limc 23921  df-dv 23922  df-log 24594  df-cxp 24595  df-logb 24794  df-blen 42965  df-dig 42991
This theorem is referenced by:  nn0sumshdiglem1  43016
  Copyright terms: Public domain W3C validator