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 42212
 Description: Lemma for nn0sumshdig 42215 (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 11641 . . 3 (𝑎 ∈ ℕ ↔ (𝑎 = 1 ∨ 𝑎 ∈ (ℤ‘2)))
2 1t1e1 11052 . . . . . . . . 9 (1 · 1) = 1
32eqcomi 2619 . . . . . . . 8 1 = (1 · 1)
4 simpl 472 . . . . . . . 8 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → 𝑎 = 1)
5 oveq2 6557 . . . . . . . . . . . 12 ((𝑦 + 1) = (#b𝑎) → (0..^(𝑦 + 1)) = (0..^(#b𝑎)))
65eqcoms 2618 . . . . . . . . . . 11 ((#b𝑎) = (𝑦 + 1) → (0..^(𝑦 + 1)) = (0..^(#b𝑎)))
7 fveq2 6103 . . . . . . . . . . . . . 14 (𝑎 = 1 → (#b𝑎) = (#b‘1))
8 blen1 42176 . . . . . . . . . . . . . 14 (#b‘1) = 1
97, 8syl6eq 2660 . . . . . . . . . . . . 13 (𝑎 = 1 → (#b𝑎) = 1)
109oveq2d 6565 . . . . . . . . . . . 12 (𝑎 = 1 → (0..^(#b𝑎)) = (0..^1))
11 fzo01 12417 . . . . . . . . . . . 12 (0..^1) = {0}
1210, 11syl6eq 2660 . . . . . . . . . . 11 (𝑎 = 1 → (0..^(#b𝑎)) = {0})
136, 12sylan9eqr 2666 . . . . . . . . . 10 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → (0..^(𝑦 + 1)) = {0})
1413sumeq1d 14279 . . . . . . . . 9 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)))
15 oveq2 6557 . . . . . . . . . . . . 13 (𝑎 = 1 → (𝑘(digit‘2)𝑎) = (𝑘(digit‘2)1))
1615oveq1d 6564 . . . . . . . . . . . 12 (𝑎 = 1 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((𝑘(digit‘2)1) · (2↑𝑘)))
1716sumeq2sdv 14282 . . . . . . . . . . 11 (𝑎 = 1 → Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ {0} ((𝑘(digit‘2)1) · (2↑𝑘)))
18 c0ex 9913 . . . . . . . . . . . 12 0 ∈ V
19 ax-1cn 9873 . . . . . . . . . . . . 13 1 ∈ ℂ
2019, 19mulcli 9924 . . . . . . . . . . . 12 (1 · 1) ∈ ℂ
21 oveq1 6556 . . . . . . . . . . . . . . 15 (𝑘 = 0 → (𝑘(digit‘2)1) = (0(digit‘2)1))
22 1ex 9914 . . . . . . . . . . . . . . . . 17 1 ∈ V
2322prid2 4242 . . . . . . . . . . . . . . . 16 1 ∈ {0, 1}
24 0dig2pr01 42202 . . . . . . . . . . . . . . . 16 (1 ∈ {0, 1} → (0(digit‘2)1) = 1)
2523, 24ax-mp 5 . . . . . . . . . . . . . . 15 (0(digit‘2)1) = 1
2621, 25syl6eq 2660 . . . . . . . . . . . . . 14 (𝑘 = 0 → (𝑘(digit‘2)1) = 1)
27 oveq2 6557 . . . . . . . . . . . . . . 15 (𝑘 = 0 → (2↑𝑘) = (2↑0))
28 2cn 10968 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
29 exp0 12726 . . . . . . . . . . . . . . . 16 (2 ∈ ℂ → (2↑0) = 1)
3028, 29ax-mp 5 . . . . . . . . . . . . . . 15 (2↑0) = 1
3127, 30syl6eq 2660 . . . . . . . . . . . . . 14 (𝑘 = 0 → (2↑𝑘) = 1)
3226, 31oveq12d 6567 . . . . . . . . . . . . 13 (𝑘 = 0 → ((𝑘(digit‘2)1) · (2↑𝑘)) = (1 · 1))
3332sumsn 14319 . . . . . . . . . . . 12 ((0 ∈ V ∧ (1 · 1) ∈ ℂ) → Σ𝑘 ∈ {0} ((𝑘(digit‘2)1) · (2↑𝑘)) = (1 · 1))
3418, 20, 33mp2an 704 . . . . . . . . . . 11 Σ𝑘 ∈ {0} ((𝑘(digit‘2)1) · (2↑𝑘)) = (1 · 1)
3517, 34syl6eq 2660 . . . . . . . . . 10 (𝑎 = 1 → Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (1 · 1))
3635adantr 480 . . . . . . . . 9 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (1 · 1))
3714, 36eqtrd 2644 . . . . . . . 8 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (1 · 1))
383, 4, 373eqtr4a 2670 . . . . . . 7 ((𝑎 = 1 ∧ (#b𝑎) = (𝑦 + 1)) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))
3938ex 449 . . . . . 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 11603 . . . . . . . . 9 (𝑎 ∈ (ℤ‘2) → 𝑎 ∈ ℕ0)
43 nn0ob 14938 . . . . . . . . . 10 (𝑎 ∈ ℕ0 → (((𝑎 + 1) / 2) ∈ ℕ0 ↔ ((𝑎 − 1) / 2) ∈ ℕ0))
4443bicomd 212 . . . . . . . . 9 (𝑎 ∈ ℕ0 → (((𝑎 − 1) / 2) ∈ ℕ0 ↔ ((𝑎 + 1) / 2) ∈ ℕ0))
4542, 44syl 17 . . . . . . . 8 (𝑎 ∈ (ℤ‘2) → (((𝑎 − 1) / 2) ∈ ℕ0 ↔ ((𝑎 + 1) / 2) ∈ ℕ0))
46 blennngt2o2 42184 . . . . . . . . 9 ((𝑎 ∈ (ℤ‘2) ∧ ((𝑎 + 1) / 2) ∈ ℕ0) → (#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1))
4746ex 449 . . . . . . . 8 (𝑎 ∈ (ℤ‘2) → (((𝑎 + 1) / 2) ∈ ℕ0 → (#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1)))
4845, 47sylbid 229 . . . . . . 7 (𝑎 ∈ (ℤ‘2) → (((𝑎 − 1) / 2) ∈ ℕ0 → (#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1)))
4948imp 444 . . . . . 6 ((𝑎 ∈ (ℤ‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0) → (#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1))
50 fveq2 6103 . . . . . . . . . . . . . 14 (𝑥 = ((𝑎 − 1) / 2) → (#b𝑥) = (#b‘((𝑎 − 1) / 2)))
5150eqeq1d 2612 . . . . . . . . . . . . 13 (𝑥 = ((𝑎 − 1) / 2) → ((#b𝑥) = 𝑦 ↔ (#b‘((𝑎 − 1) / 2)) = 𝑦))
52 id 22 . . . . . . . . . . . . . 14 (𝑥 = ((𝑎 − 1) / 2) → 𝑥 = ((𝑎 − 1) / 2))
53 oveq2 6557 . . . . . . . . . . . . . . . 16 (𝑥 = ((𝑎 − 1) / 2) → (𝑘(digit‘2)𝑥) = (𝑘(digit‘2)((𝑎 − 1) / 2)))
5453oveq1d 6564 . . . . . . . . . . . . . . 15 (𝑥 = ((𝑎 − 1) / 2) → ((𝑘(digit‘2)𝑥) · (2↑𝑘)) = ((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)))
5554sumeq2sdv 14282 . . . . . . . . . . . . . 14 (𝑥 = ((𝑎 − 1) / 2) → Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)))
5652, 55eqeq12d 2625 . . . . . . . . . . . . 13 (𝑥 = ((𝑎 − 1) / 2) → (𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)) ↔ ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))))
5751, 56imbi12d 333 . . . . . . . . . . . 12 (𝑥 = ((𝑎 − 1) / 2) → (((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) ↔ ((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)))))
5857rspcva 3280 . . . . . . . . . . 11 ((((𝑎 − 1) / 2) ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → ((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))))
59 eqeq1 2614 . . . . . . . . . . . . . . . 16 ((#b𝑎) = (𝑦 + 1) → ((#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1) ↔ (𝑦 + 1) = ((#b‘((𝑎 − 1) / 2)) + 1)))
60 nncn 10905 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
6160ad2antll 761 . . . . . . . . . . . . . . . . . . . 20 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑦 ∈ ℂ)
62 blennn0elnn 42169 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 − 1) / 2) ∈ ℕ0 → (#b‘((𝑎 − 1) / 2)) ∈ ℕ)
6362nncnd 10913 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎 − 1) / 2) ∈ ℕ0 → (#b‘((𝑎 − 1) / 2)) ∈ ℂ)
6463adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (#b‘((𝑎 − 1) / 2)) ∈ ℂ)
6564ad2antrl 760 . . . . . . . . . . . . . . . . . . . 20 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (#b‘((𝑎 − 1) / 2)) ∈ ℂ)
66 1cnd 9935 . . . . . . . . . . . . . . . . . . . 20 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 1 ∈ ℂ)
6761, 65, 66addcan2d 10119 . . . . . . . . . . . . . . . . . . 19 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → ((𝑦 + 1) = ((#b‘((𝑎 − 1) / 2)) + 1) ↔ 𝑦 = (#b‘((𝑎 − 1) / 2))))
68 eqcom 2617 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (#b‘((𝑎 − 1) / 2)) ↔ (#b‘((𝑎 − 1) / 2)) = 𝑦)
69 nnz 11276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
7069ad2antll 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑦 ∈ ℤ)
71 fzval3 12404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ℤ → (0...𝑦) = (0..^(𝑦 + 1)))
7270, 71syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (0...𝑦) = (0..^(𝑦 + 1)))
7372eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (0..^(𝑦 + 1)) = (0...𝑦))
7473sumeq1d 14279 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ (0...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)))
75 nnnn0 11176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ℕ → 𝑦 ∈ ℕ0)
76 elnn0uz 11601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ℕ0𝑦 ∈ (ℤ‘0))
7775, 76sylib 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ‘0))
7877ad2antll 761 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑦 ∈ (ℤ‘0))
79 2nn 11062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 2 ∈ ℕ
8079a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑘 ∈ (0...𝑦)) → 2 ∈ ℕ)
81 elfzelz 12213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 ∈ (0...𝑦) → 𝑘 ∈ ℤ)
8281adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑘 ∈ (0...𝑦)) → 𝑘 ∈ ℤ)
83 nn0rp0 12150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑎 ∈ ℕ0𝑎 ∈ (0[,)+∞))
8442, 83syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑎 ∈ (ℤ‘2) → 𝑎 ∈ (0[,)+∞))
8584adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → 𝑎 ∈ (0[,)+∞))
8685adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑘 ∈ (0...𝑦)) → 𝑎 ∈ (0[,)+∞))
87 digvalnn0 42191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((2 ∈ ℕ ∧ 𝑘 ∈ ℤ ∧ 𝑎 ∈ (0[,)+∞)) → (𝑘(digit‘2)𝑎) ∈ ℕ0)
8880, 82, 86, 87syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℕ0)
8988ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (𝑘 ∈ (0...𝑦) → (𝑘(digit‘2)𝑎) ∈ ℕ0))
9089ad2antrl 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (𝑘 ∈ (0...𝑦) → (𝑘(digit‘2)𝑎) ∈ ℕ0))
9190imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℕ0)
9291nn0cnd 11230 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℂ)
93 2nn0 11186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2 ∈ ℕ0
9493a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ (0...𝑦) → 2 ∈ ℕ0)
95 elfznn0 12302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ (0...𝑦) → 𝑘 ∈ ℕ0)
9694, 95nn0expcld 12893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ (0...𝑦) → (2↑𝑘) ∈ ℕ0)
9796nn0cnd 11230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 ∈ (0...𝑦) → (2↑𝑘) ∈ ℂ)
9897adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ (0...𝑦)) → (2↑𝑘) ∈ ℂ)
9992, 98mulcld 9939 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ (0...𝑦)) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) ∈ ℂ)
100 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 0 → (𝑘(digit‘2)𝑎) = (0(digit‘2)𝑎))
101100, 27oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = 0 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · (2↑0)))
10230oveq2i 6560 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((0(digit‘2)𝑎) · (2↑0)) = ((0(digit‘2)𝑎) · 1)
103101, 102syl6eq 2660 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 = 0 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · 1))
10478, 99, 103fsum1p 14326 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑘 ∈ (0...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (((0(digit‘2)𝑎) · 1) + Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))))
10542adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → 𝑎 ∈ ℕ0)
10642, 43syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 ∈ (ℤ‘2) → (((𝑎 + 1) / 2) ∈ ℕ0 ↔ ((𝑎 − 1) / 2) ∈ ℕ0))
107106biimparc 503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → ((𝑎 + 1) / 2) ∈ ℕ0)
108 0dig2nn0o 42205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑎 ∈ ℕ0 ∧ ((𝑎 + 1) / 2) ∈ ℕ0) → (0(digit‘2)𝑎) = 1)
109105, 107, 108syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (0(digit‘2)𝑎) = 1)
110109ad2antrl 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (0(digit‘2)𝑎) = 1)
111110oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → ((0(digit‘2)𝑎) · 1) = (1 · 1))
112111, 2syl6eq 2660 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → ((0(digit‘2)𝑎) · 1) = 1)
113 1z 11284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℤ
114113a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 1 ∈ ℤ)
115 0p1e1 11009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (0 + 1) = 1
116115, 113eqeltri 2684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (0 + 1) ∈ ℤ
117116a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (0 + 1) ∈ ℤ)
11879a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎 ∈ (ℤ‘2) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 2 ∈ ℕ)
119 elfzelz 12213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 ∈ ((0 + 1)...𝑦) → 𝑘 ∈ ℤ)
120119adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎 ∈ (ℤ‘2) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 𝑘 ∈ ℤ)
12142adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑎 ∈ (ℤ‘2) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 𝑎 ∈ ℕ0)
122121, 83syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎 ∈ (ℤ‘2) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 𝑎 ∈ (0[,)+∞))
123118, 120, 122, 87syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑎 ∈ (ℤ‘2) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℕ0)
124123ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎 ∈ (ℤ‘2) → (𝑘 ∈ ((0 + 1)...𝑦) → (𝑘(digit‘2)𝑎) ∈ ℕ0))
125124adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (𝑘 ∈ ((0 + 1)...𝑦) → (𝑘(digit‘2)𝑎) ∈ ℕ0))
126125ad2antrl 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (𝑘 ∈ ((0 + 1)...𝑦) → (𝑘(digit‘2)𝑎) ∈ ℕ0))
127126imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℕ0)
128127nn0cnd 11230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℂ)
129 2cnd 10970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ ((0 + 1)...𝑦) → 2 ∈ ℂ)
130 elfznn 12241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℕ)
131130nnnn0d 11228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℕ0)
132115oveq1i 6559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((0 + 1)...𝑦) = (1...𝑦)
133131, 132eleq2s 2706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ ((0 + 1)...𝑦) → 𝑘 ∈ ℕ0)
134129, 133expcld 12870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ ((0 + 1)...𝑦) → (2↑𝑘) ∈ ℂ)
135134adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (2↑𝑘) ∈ ℂ)
136128, 135mulcld 9939 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) ∈ ℂ)
137 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = (𝑖 + 1) → (𝑘(digit‘2)𝑎) = ((𝑖 + 1)(digit‘2)𝑎))
138 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = (𝑖 + 1) → (2↑𝑘) = (2↑(𝑖 + 1)))
139137, 138oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = (𝑖 + 1) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
140114, 117, 70, 136, 139fsumshftm 14355 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
141112, 140oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . . . . . 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)))))
14274, 104, 1413eqtrd 2648 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (1 + Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))))
143142adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 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)))))
14479a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → 2 ∈ ℕ)
145 elfzoelz 12339 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ ℤ)
146145adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑖 ∈ ℤ)
147 nn0rp0 12150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑎 − 1) / 2) ∈ ℕ0 → ((𝑎 − 1) / 2) ∈ (0[,)+∞))
148147adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → ((𝑎 − 1) / 2) ∈ (0[,)+∞))
149148adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑎 − 1) / 2) ∈ (0[,)+∞))
150 digvalnn0 42191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((2 ∈ ℕ ∧ 𝑖 ∈ ℤ ∧ ((𝑎 − 1) / 2) ∈ (0[,)+∞)) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈ ℕ0)
151144, 146, 149, 150syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈ ℕ0)
152151nn0cnd 11230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈ ℂ)
153152ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (𝑖 ∈ (0..^𝑦) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈ ℂ))
154153ad2antrl 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (𝑖 ∈ (0..^𝑦) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈ ℂ))
155154imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈ ℂ)
15693a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ (0..^𝑦) → 2 ∈ ℕ0)
157 elfzonn0 12380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ ℕ0)
158156, 157nn0expcld 12893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℕ0)
159158nn0cnd 11230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℂ)
160159adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑𝑖) ∈ ℂ)
161 2cnd 10970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → 2 ∈ ℂ)
162155, 160, 161mulassd 9942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2) = ((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)))
163162eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)) = (((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2))
164163sumeq2dv 14281 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)) = Σ𝑖 ∈ (0..^𝑦)(((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2))
165164adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 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))
166 0cn 9911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 0 ∈ ℂ
167 pncan1 10333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (0 ∈ ℂ → ((0 + 1) − 1) = 0)
168166, 167ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((0 + 1) − 1) = 0
169168a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ ℕ → ((0 + 1) − 1) = 0)
170169oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ ℕ → (((0 + 1) − 1)...(𝑦 − 1)) = (0...(𝑦 − 1)))
171 fzoval 12340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ ℤ → (0..^𝑦) = (0...(𝑦 − 1)))
17269, 171syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ ℕ → (0..^𝑦) = (0...(𝑦 − 1)))
173170, 172eqtr4d 2647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ℕ → (((0 + 1) − 1)...(𝑦 − 1)) = (0..^𝑦))
174173ad2antll 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (((0 + 1) − 1)...(𝑦 − 1)) = (0..^𝑦))
175 simprlr 799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑎 ∈ (ℤ‘2))
176 elfznn0 12302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 ∈ (0...(𝑦 − 1)) → 𝑖 ∈ ℕ0)
177168oveq1i 6559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((0 + 1) − 1)...(𝑦 − 1)) = (0...(𝑦 − 1))
178176, 177eleq2s 2706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1)) → 𝑖 ∈ ℕ0)
179 dignn0flhalf 42210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑎 ∈ (ℤ‘2) ∧ 𝑖 ∈ ℕ0) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)(⌊‘(𝑎 / 2))))
180175, 178, 179syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)(⌊‘(𝑎 / 2))))
181 eluzelz 11573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑎 ∈ (ℤ‘2) → 𝑎 ∈ ℤ)
182181adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑎 ∈ (ℤ‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0) → 𝑎 ∈ ℤ)
183 nn0z 11277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑎 − 1) / 2) ∈ ℕ0 → ((𝑎 − 1) / 2) ∈ ℤ)
184 zob 14921 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎 ∈ ℤ → (((𝑎 + 1) / 2) ∈ ℤ ↔ ((𝑎 − 1) / 2) ∈ ℤ))
185181, 184syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑎 ∈ (ℤ‘2) → (((𝑎 + 1) / 2) ∈ ℤ ↔ ((𝑎 − 1) / 2) ∈ ℤ))
186183, 185syl5ibr 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑎 ∈ (ℤ‘2) → (((𝑎 − 1) / 2) ∈ ℕ0 → ((𝑎 + 1) / 2) ∈ ℤ))
187186imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑎 ∈ (ℤ‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0) → ((𝑎 + 1) / 2) ∈ ℤ)
188182, 187jca 553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎 ∈ (ℤ‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0) → (𝑎 ∈ ℤ ∧ ((𝑎 + 1) / 2) ∈ ℤ))
189188ancoms 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (𝑎 ∈ ℤ ∧ ((𝑎 + 1) / 2) ∈ ℤ))
190189ad2antrl 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → (𝑎 ∈ ℤ ∧ ((𝑎 + 1) / 2) ∈ ℤ))
191190adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → (𝑎 ∈ ℤ ∧ ((𝑎 + 1) / 2) ∈ ℤ))
192 zofldiv2 42119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑎 ∈ ℤ ∧ ((𝑎 + 1) / 2) ∈ ℤ) → (⌊‘(𝑎 / 2)) = ((𝑎 − 1) / 2))
193191, 192syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → (⌊‘(𝑎 / 2)) = ((𝑎 − 1) / 2))
194193oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → (𝑖(digit‘2)(⌊‘(𝑎 / 2))) = (𝑖(digit‘2)((𝑎 − 1) / 2)))
195180, 194eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)((𝑎 − 1) / 2)))
196 2cnd 10970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1)) → 2 ∈ ℂ)
197196, 178expp1d 12871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1)) → (2↑(𝑖 + 1)) = ((2↑𝑖) · 2))
198197adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → (2↑(𝑖 + 1)) = ((2↑𝑖) · 2))
199195, 198oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = ((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)))
200174, 199sumeq12dv 14284 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)))
201200adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 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)))
202 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝑖 → (𝑘(digit‘2)((𝑎 − 1) / 2)) = (𝑖(digit‘2)((𝑎 − 1) / 2)))
203 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝑖 → (2↑𝑘) = (2↑𝑖))
204202, 203oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝑖 → ((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) = ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)))
205204cbvsumv 14274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖))
206205eqeq2i 2622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ↔ ((𝑎 − 1) / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)))
207206biimpi 205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) → ((𝑎 − 1) / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)))
208207adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → ((𝑎 − 1) / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)))
209208oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . . . 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))
210 fzofi 12635 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (0..^𝑦) ∈ Fin
211210a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → (0..^𝑦) ∈ Fin)
212 2cnd 10970 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → 2 ∈ ℂ)
213159adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑𝑖) ∈ ℂ)
214152, 213mulcld 9939 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) ∈ ℂ)
215214ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (𝑖 ∈ (0..^𝑦) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) ∈ ℂ))
216215adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ) → (𝑖 ∈ (0..^𝑦) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) ∈ ℂ))
217216ad2antll 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → (𝑖 ∈ (0..^𝑦) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) ∈ ℂ))
218217imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) ∈ ℂ)
219211, 212, 218fsummulc1 14359 . . . . . . . . . . . . . . . . . . . . . . . . . . 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))
220209, 219eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . . 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))
221165, 201, 2203eqtr4d 2654 . . . . . . . . . . . . . . . . . . . . . . . . 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))
222221oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . 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)))
223 eluzelcn 11575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 ∈ (ℤ‘2) → 𝑎 ∈ ℂ)
224 peano2cnm 10226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 ∈ ℂ → (𝑎 − 1) ∈ ℂ)
225223, 224syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎 ∈ (ℤ‘2) → (𝑎 − 1) ∈ ℂ)
226 2cnd 10970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎 ∈ (ℤ‘2) → 2 ∈ ℂ)
227 2ne0 10990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2 ≠ 0
228227a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎 ∈ (ℤ‘2) → 2 ≠ 0)
229225, 226, 2283jca 1235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 ∈ (ℤ‘2) → ((𝑎 − 1) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0))
230229adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → ((𝑎 − 1) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0))
231 divcan1 10573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑎 − 1) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (((𝑎 − 1) / 2) · 2) = (𝑎 − 1))
232230, 231syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (((𝑎 − 1) / 2) · 2) = (𝑎 − 1))
233232oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (1 + (((𝑎 − 1) / 2) · 2)) = (1 + (𝑎 − 1)))
234 1cnd 9935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 ∈ (ℤ‘2) → 1 ∈ ℂ)
235234, 223jca 553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 ∈ (ℤ‘2) → (1 ∈ ℂ ∧ 𝑎 ∈ ℂ))
236235adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (1 ∈ ℂ ∧ 𝑎 ∈ ℂ))
237 pncan3 10168 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((1 ∈ ℂ ∧ 𝑎 ∈ ℂ) → (1 + (𝑎 − 1)) = 𝑎)
238236, 237syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (1 + (𝑎 − 1)) = 𝑎)
239233, 238eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) → (1 + (((𝑎 − 1) / 2) · 2)) = 𝑎)
240239adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ) → (1 + (((𝑎 − 1) / 2) · 2)) = 𝑎)
241240ad2antll 761 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → (1 + (((𝑎 − 1) / 2) · 2)) = 𝑎)
242143, 222, 2413eqtrrd 2649 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧ ((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))
243242ex 449 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) → (((#b𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0𝑎 ∈ (ℤ‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))
244243imim2i 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↑𝑘)))))
245244com13 86 . . . . . . . . . . . . . . . . . . . 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↑𝑘)))))
24668, 245syl5bi 231 . . . . . . . . . . . . . . . . . . 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↑𝑘)))))
24767, 246sylbid 229 . . . . . . . . . . . . . . . . . 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↑𝑘)))))
248247ex 449 . . . . . . . . . . . . . . . . 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↑𝑘))))))
249248com23 84 . . . . . . . . . . . . . . . 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↑𝑘))))))
25059, 249sylbid 229 . . . . . . . . . . . . . . 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↑𝑘))))))
251250com23 84 . . . . . . . . . . . . . 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↑𝑘))))))
252251com14 94 . . . . . . . . . . . . 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↑𝑘))))))
253252exp4c 634 . . . . . . . . . . . 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↑𝑘))))))))
254253com35 96 . . . . . . . . . . 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↑𝑘))))))))
25558, 254syl 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↑𝑘))))))))
256255ex 449 . . . . . . . . 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↑𝑘)))))))))
257256pm2.43a 52 . . . . . . . 8 (((𝑎 − 1) / 2) ∈ ℕ0 → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1) → (𝑦 ∈ ℕ → (𝑎 ∈ (ℤ‘2) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))))
258257com25 97 . . . . . . 7 (((𝑎 − 1) / 2) ∈ ℕ0 → (𝑎 ∈ (ℤ‘2) → ((#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1) → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))))
259258impcom 445 . . . . . 6 ((𝑎 ∈ (ℤ‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0) → ((#b𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1) → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))
26049, 259mpd 15 . . . . 5 ((𝑎 ∈ (ℤ‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0) → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))
261260ex 449 . . . 4 (𝑎 ∈ (ℤ‘2) → (((𝑎 − 1) / 2) ∈ ℕ0 → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))
26241, 261jaoi 393 . . 3 ((𝑎 = 1 ∨ 𝑎 ∈ (ℤ‘2)) → (((𝑎 − 1) / 2) ∈ ℕ0 → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))
2631, 262sylbi 206 . 2 (𝑎 ∈ ℕ → (((𝑎 − 1) / 2) ∈ ℕ0 → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))
264263imp31 447 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 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  Vcvv 3173  {csn 4125  {cpr 4127  ‘cfv 5804  (class class class)co 6549  Fincfn 7841  ℂcc 9813  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  +∞cpnf 9950   − cmin 10145   / cdiv 10563  ℕcn 10897  2c2 10947  ℕ0cn0 11169  ℤcz 11254  ℤ≥cuz 11563  [,)cico 12048  ...cfz 12197  ..^cfzo 12334  ⌊cfl 12453  ↑cexp 12722  Σcsu 14264  #bcblen 42161  digitcdig 42187 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894  ax-mulf 9895 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ioc 12051  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-mod 12531  df-seq 12664  df-exp 12723  df-fac 12923  df-bc 12952  df-hash 12980  df-shft 13655  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-limsup 14050  df-clim 14067  df-rlim 14068  df-sum 14265  df-ef 14637  df-sin 14639  df-cos 14640  df-pi 14642  df-dvds 14822  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-starv 15783  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-hom 15793  df-cco 15794  df-rest 15906  df-topn 15907  df-0g 15925  df-gsum 15926  df-topgen 15927  df-pt 15928  df-prds 15931  df-xrs 15985  df-qtop 15990  df-imas 15991  df-xps 15993  df-mre 16069  df-mrc 16070  df-acs 16072  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-mulg 17364  df-cntz 17573  df-cmn 18018  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-fbas 19564  df-fg 19565  df-cnfld 19568  df-top 20521  df-bases 20522  df-topon 20523  df-topsp 20524  df-cld 20633  df-ntr 20634  df-cls 20635  df-nei 20712  df-lp 20750  df-perf 20751  df-cn 20841  df-cnp 20842  df-haus 20929  df-tx 21175  df-hmeo 21368  df-fil 21460  df-fm 21552  df-flim 21553  df-flf 21554  df-xms 21935  df-ms 21936  df-tms 21937  df-cncf 22489  df-limc 23436  df-dv 23437  df-log 24107  df-cxp 24108  df-logb 24303  df-blen 42162  df-dig 42188 This theorem is referenced by:  nn0sumshdiglem1  42213
 Copyright terms: Public domain W3C validator