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

Theorem nn0sumshdiglemA 46791
Description: Lemma for nn0sumshdig 46795 (induction step, even multiplier). (Contributed by AV, 3-Jun-2020.)
Assertion
Ref Expression
nn0sumshdiglemA (((π‘Ž ∈ β„• ∧ (π‘Ž / 2) ∈ β„•) ∧ 𝑦 ∈ β„•) β†’ (βˆ€π‘₯ ∈ β„•0 ((#bβ€˜π‘₯) = 𝑦 β†’ π‘₯ = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜))) β†’ ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))))
Distinct variable group:   π‘˜,π‘Ž,π‘₯,𝑦

Proof of Theorem nn0sumshdiglemA
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 nnnn0 12425 . . . 4 ((π‘Ž / 2) ∈ β„• β†’ (π‘Ž / 2) ∈ β„•0)
2 blennn0em1 46763 . . . 4 ((π‘Ž ∈ β„• ∧ (π‘Ž / 2) ∈ β„•0) β†’ (#bβ€˜(π‘Ž / 2)) = ((#bβ€˜π‘Ž) βˆ’ 1))
31, 2sylan2 594 . . 3 ((π‘Ž ∈ β„• ∧ (π‘Ž / 2) ∈ β„•) β†’ (#bβ€˜(π‘Ž / 2)) = ((#bβ€˜π‘Ž) βˆ’ 1))
4 fveqeq2 6852 . . . . . . . . . . 11 (π‘₯ = (π‘Ž / 2) β†’ ((#bβ€˜π‘₯) = 𝑦 ↔ (#bβ€˜(π‘Ž / 2)) = 𝑦))
5 id 22 . . . . . . . . . . . 12 (π‘₯ = (π‘Ž / 2) β†’ π‘₯ = (π‘Ž / 2))
6 oveq2 7366 . . . . . . . . . . . . . . 15 (π‘₯ = (π‘Ž / 2) β†’ (π‘˜(digitβ€˜2)π‘₯) = (π‘˜(digitβ€˜2)(π‘Ž / 2)))
76oveq1d 7373 . . . . . . . . . . . . . 14 (π‘₯ = (π‘Ž / 2) β†’ ((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜)) = ((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜)))
87adantr 482 . . . . . . . . . . . . 13 ((π‘₯ = (π‘Ž / 2) ∧ π‘˜ ∈ (0..^𝑦)) β†’ ((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜)) = ((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜)))
98sumeq2dv 15593 . . . . . . . . . . . 12 (π‘₯ = (π‘Ž / 2) β†’ Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜)) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜)))
105, 9eqeq12d 2749 . . . . . . . . . . 11 (π‘₯ = (π‘Ž / 2) β†’ (π‘₯ = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜)) ↔ (π‘Ž / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜))))
114, 10imbi12d 345 . . . . . . . . . 10 (π‘₯ = (π‘Ž / 2) β†’ (((#bβ€˜π‘₯) = 𝑦 β†’ π‘₯ = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜))) ↔ ((#bβ€˜(π‘Ž / 2)) = 𝑦 β†’ (π‘Ž / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜)))))
1211rspcva 3578 . . . . . . . . 9 (((π‘Ž / 2) ∈ β„•0 ∧ βˆ€π‘₯ ∈ β„•0 ((#bβ€˜π‘₯) = 𝑦 β†’ π‘₯ = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜)))) β†’ ((#bβ€˜(π‘Ž / 2)) = 𝑦 β†’ (π‘Ž / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜))))
13 simpr 486 . . . . . . . . . . . . . . . . 17 ((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) β†’ (#bβ€˜π‘Ž) = (𝑦 + 1))
1413oveq1d 7373 . . . . . . . . . . . . . . . 16 ((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) β†’ ((#bβ€˜π‘Ž) βˆ’ 1) = ((𝑦 + 1) βˆ’ 1))
15 nncn 12166 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ β„• β†’ 𝑦 ∈ β„‚)
16 pncan1 11584 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ β„‚ β†’ ((𝑦 + 1) βˆ’ 1) = 𝑦)
1715, 16syl 17 . . . . . . . . . . . . . . . 16 (𝑦 ∈ β„• β†’ ((𝑦 + 1) βˆ’ 1) = 𝑦)
1814, 17sylan9eq 2793 . . . . . . . . . . . . . . 15 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ ((#bβ€˜π‘Ž) βˆ’ 1) = 𝑦)
1918eqeq2d 2744 . . . . . . . . . . . . . 14 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ ((#bβ€˜(π‘Ž / 2)) = ((#bβ€˜π‘Ž) βˆ’ 1) ↔ (#bβ€˜(π‘Ž / 2)) = 𝑦))
20 nnz 12525 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ β„• β†’ 𝑦 ∈ β„€)
2120adantl 483 . . . . . . . . . . . . . . . . . . . . . . 23 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ 𝑦 ∈ β„€)
22 fzval3 13647 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ β„€ β†’ (0...𝑦) = (0..^(𝑦 + 1)))
2321, 22syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ (0...𝑦) = (0..^(𝑦 + 1)))
2423eqcomd 2739 . . . . . . . . . . . . . . . . . . . . 21 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ (0..^(𝑦 + 1)) = (0...𝑦))
2524sumeq1d 15591 . . . . . . . . . . . . . . . . . . . 20 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) = Ξ£π‘˜ ∈ (0...𝑦)((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))
26 nnnn0 12425 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ β„• β†’ 𝑦 ∈ β„•0)
27 elnn0uz 12813 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ β„•0 ↔ 𝑦 ∈ (β„€β‰₯β€˜0))
2826, 27sylib 217 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ β„• β†’ 𝑦 ∈ (β„€β‰₯β€˜0))
2928adantl 483 . . . . . . . . . . . . . . . . . . . . 21 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ 𝑦 ∈ (β„€β‰₯β€˜0))
30 2nn 12231 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ β„•
3130a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ π‘˜ ∈ (0...𝑦)) β†’ 2 ∈ β„•)
32 elfzelz 13447 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘˜ ∈ (0...𝑦) β†’ π‘˜ ∈ β„€)
3332adantl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ π‘˜ ∈ (0...𝑦)) β†’ π‘˜ ∈ β„€)
34 nnnn0 12425 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘Ž ∈ β„• β†’ π‘Ž ∈ β„•0)
35 nn0rp0 13378 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘Ž ∈ β„•0 β†’ π‘Ž ∈ (0[,)+∞))
3634, 35syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘Ž ∈ β„• β†’ π‘Ž ∈ (0[,)+∞))
3736ad4antlr 732 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ π‘˜ ∈ (0...𝑦)) β†’ π‘Ž ∈ (0[,)+∞))
38 digvalnn0 46771 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2 ∈ β„• ∧ π‘˜ ∈ β„€ ∧ π‘Ž ∈ (0[,)+∞)) β†’ (π‘˜(digitβ€˜2)π‘Ž) ∈ β„•0)
3931, 33, 37, 38syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ π‘˜ ∈ (0...𝑦)) β†’ (π‘˜(digitβ€˜2)π‘Ž) ∈ β„•0)
4039nn0cnd 12480 . . . . . . . . . . . . . . . . . . . . . 22 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ π‘˜ ∈ (0...𝑦)) β†’ (π‘˜(digitβ€˜2)π‘Ž) ∈ β„‚)
41 2nn0 12435 . . . . . . . . . . . . . . . . . . . . . . . . . 26 2 ∈ β„•0
4241a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘˜ ∈ (0...𝑦) β†’ 2 ∈ β„•0)
43 elfznn0 13540 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘˜ ∈ (0...𝑦) β†’ π‘˜ ∈ β„•0)
4442, 43nn0expcld 14155 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘˜ ∈ (0...𝑦) β†’ (2β†‘π‘˜) ∈ β„•0)
4544nn0cnd 12480 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘˜ ∈ (0...𝑦) β†’ (2β†‘π‘˜) ∈ β„‚)
4645adantl 483 . . . . . . . . . . . . . . . . . . . . . 22 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ π‘˜ ∈ (0...𝑦)) β†’ (2β†‘π‘˜) ∈ β„‚)
4740, 46mulcld 11180 . . . . . . . . . . . . . . . . . . . . 21 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ π‘˜ ∈ (0...𝑦)) β†’ ((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) ∈ β„‚)
48 oveq1 7365 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘˜ = 0 β†’ (π‘˜(digitβ€˜2)π‘Ž) = (0(digitβ€˜2)π‘Ž))
49 oveq2 7366 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘˜ = 0 β†’ (2β†‘π‘˜) = (2↑0))
5048, 49oveq12d 7376 . . . . . . . . . . . . . . . . . . . . . 22 (π‘˜ = 0 β†’ ((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) = ((0(digitβ€˜2)π‘Ž) Β· (2↑0)))
51 2cn 12233 . . . . . . . . . . . . . . . . . . . . . . . 24 2 ∈ β„‚
52 exp0 13977 . . . . . . . . . . . . . . . . . . . . . . . 24 (2 ∈ β„‚ β†’ (2↑0) = 1)
5351, 52ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (2↑0) = 1
5453oveq2i 7369 . . . . . . . . . . . . . . . . . . . . . 22 ((0(digitβ€˜2)π‘Ž) Β· (2↑0)) = ((0(digitβ€˜2)π‘Ž) Β· 1)
5550, 54eqtrdi 2789 . . . . . . . . . . . . . . . . . . . . 21 (π‘˜ = 0 β†’ ((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) = ((0(digitβ€˜2)π‘Ž) Β· 1))
5629, 47, 55fsum1p 15643 . . . . . . . . . . . . . . . . . . . 20 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ Ξ£π‘˜ ∈ (0...𝑦)((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) = (((0(digitβ€˜2)π‘Ž) Β· 1) + Ξ£π‘˜ ∈ ((0 + 1)...𝑦)((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜))))
57 0dig2nn0e 46784 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((π‘Ž ∈ β„•0 ∧ (π‘Ž / 2) ∈ β„•0) β†’ (0(digitβ€˜2)π‘Ž) = 0)
5834, 1, 57syl2anr 598 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) β†’ (0(digitβ€˜2)π‘Ž) = 0)
5958oveq1d 7373 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) β†’ ((0(digitβ€˜2)π‘Ž) Β· 1) = (0 Β· 1))
60 1re 11160 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ ℝ
61 mul02lem2 11337 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1 ∈ ℝ β†’ (0 Β· 1) = 0)
6260, 61ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 Β· 1) = 0
6359, 62eqtrdi 2789 . . . . . . . . . . . . . . . . . . . . . . . 24 (((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) β†’ ((0(digitβ€˜2)π‘Ž) Β· 1) = 0)
6463adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) β†’ ((0(digitβ€˜2)π‘Ž) Β· 1) = 0)
6564adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ ((0(digitβ€˜2)π‘Ž) Β· 1) = 0)
66 1z 12538 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ∈ β„€
6766a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ 1 ∈ β„€)
68 0p1e1 12280 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 + 1) = 1
6968, 66eqeltri 2830 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 + 1) ∈ β„€
7069a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ (0 + 1) ∈ β„€)
7130a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ π‘˜ ∈ ((0 + 1)...𝑦)) β†’ 2 ∈ β„•)
72 elfzelz 13447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘˜ ∈ ((0 + 1)...𝑦) β†’ π‘˜ ∈ β„€)
7372adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ π‘˜ ∈ ((0 + 1)...𝑦)) β†’ π‘˜ ∈ β„€)
7436ad4antlr 732 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ π‘˜ ∈ ((0 + 1)...𝑦)) β†’ π‘Ž ∈ (0[,)+∞))
7571, 73, 74, 38syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ π‘˜ ∈ ((0 + 1)...𝑦)) β†’ (π‘˜(digitβ€˜2)π‘Ž) ∈ β„•0)
7675nn0cnd 12480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ π‘˜ ∈ ((0 + 1)...𝑦)) β†’ (π‘˜(digitβ€˜2)π‘Ž) ∈ β„‚)
77 2cnd 12236 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘˜ ∈ ((0 + 1)...𝑦) β†’ 2 ∈ β„‚)
78 elfznn 13476 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘˜ ∈ (1...𝑦) β†’ π‘˜ ∈ β„•)
7978nnnn0d 12478 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘˜ ∈ (1...𝑦) β†’ π‘˜ ∈ β„•0)
8068oveq1i 7368 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((0 + 1)...𝑦) = (1...𝑦)
8179, 80eleq2s 2852 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘˜ ∈ ((0 + 1)...𝑦) β†’ π‘˜ ∈ β„•0)
8277, 81expcld 14057 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘˜ ∈ ((0 + 1)...𝑦) β†’ (2β†‘π‘˜) ∈ β„‚)
8382adantl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ π‘˜ ∈ ((0 + 1)...𝑦)) β†’ (2β†‘π‘˜) ∈ β„‚)
8476, 83mulcld 11180 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ π‘˜ ∈ ((0 + 1)...𝑦)) β†’ ((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) ∈ β„‚)
85 oveq1 7365 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘˜ = (𝑖 + 1) β†’ (π‘˜(digitβ€˜2)π‘Ž) = ((𝑖 + 1)(digitβ€˜2)π‘Ž))
86 oveq2 7366 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘˜ = (𝑖 + 1) β†’ (2β†‘π‘˜) = (2↑(𝑖 + 1)))
8785, 86oveq12d 7376 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘˜ = (𝑖 + 1) β†’ ((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) = (((𝑖 + 1)(digitβ€˜2)π‘Ž) Β· (2↑(𝑖 + 1))))
8867, 70, 21, 84, 87fsumshftm 15671 . . . . . . . . . . . . . . . . . . . . . 22 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ Ξ£π‘˜ ∈ ((0 + 1)...𝑦)((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) = Σ𝑖 ∈ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1))(((𝑖 + 1)(digitβ€˜2)π‘Ž) Β· (2↑(𝑖 + 1))))
8965, 88oveq12d 7376 . . . . . . . . . . . . . . . . . . . . 21 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ (((0(digitβ€˜2)π‘Ž) Β· 1) + Ξ£π‘˜ ∈ ((0 + 1)...𝑦)((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜))) = (0 + Σ𝑖 ∈ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1))(((𝑖 + 1)(digitβ€˜2)π‘Ž) Β· (2↑(𝑖 + 1)))))
901ad4antr 731 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ (π‘Ž / 2) ∈ β„•0)
9134ad4antlr 732 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ π‘Ž ∈ β„•0)
92 elfzonn0 13623 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^𝑦) β†’ 𝑖 ∈ β„•0)
9392adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ 𝑖 ∈ β„•0)
94 dignn0ehalf 46789 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((π‘Ž / 2) ∈ β„•0 ∧ π‘Ž ∈ β„•0 ∧ 𝑖 ∈ β„•0) β†’ ((𝑖 + 1)(digitβ€˜2)π‘Ž) = (𝑖(digitβ€˜2)(π‘Ž / 2)))
9590, 91, 93, 94syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ ((𝑖 + 1)(digitβ€˜2)π‘Ž) = (𝑖(digitβ€˜2)(π‘Ž / 2)))
96 2cnd 12236 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^𝑦) β†’ 2 ∈ β„‚)
9796, 92expp1d 14058 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^𝑦) β†’ (2↑(𝑖 + 1)) = ((2↑𝑖) Β· 2))
9897adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ (2↑(𝑖 + 1)) = ((2↑𝑖) Β· 2))
9995, 98oveq12d 7376 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ (((𝑖 + 1)(digitβ€˜2)π‘Ž) Β· (2↑(𝑖 + 1))) = ((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· ((2↑𝑖) Β· 2)))
10030a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ 2 ∈ β„•)
101 elfzoelz 13578 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (0..^𝑦) β†’ 𝑖 ∈ β„€)
102101adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ 𝑖 ∈ β„€)
103 nn0rp0 13378 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((π‘Ž / 2) ∈ β„•0 β†’ (π‘Ž / 2) ∈ (0[,)+∞))
1041, 103syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((π‘Ž / 2) ∈ β„• β†’ (π‘Ž / 2) ∈ (0[,)+∞))
105104ad4antr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ (π‘Ž / 2) ∈ (0[,)+∞))
106 digvalnn0 46771 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2 ∈ β„• ∧ 𝑖 ∈ β„€ ∧ (π‘Ž / 2) ∈ (0[,)+∞)) β†’ (𝑖(digitβ€˜2)(π‘Ž / 2)) ∈ β„•0)
107100, 102, 105, 106syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ (𝑖(digitβ€˜2)(π‘Ž / 2)) ∈ β„•0)
108107nn0cnd 12480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ (𝑖(digitβ€˜2)(π‘Ž / 2)) ∈ β„‚)
109 2re 12232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2 ∈ ℝ
110109a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (0..^𝑦) β†’ 2 ∈ ℝ)
111110, 92reexpcld 14074 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^𝑦) β†’ (2↑𝑖) ∈ ℝ)
112111recnd 11188 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^𝑦) β†’ (2↑𝑖) ∈ β„‚)
113112adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ (2↑𝑖) ∈ β„‚)
114 2cnd 12236 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ 2 ∈ β„‚)
115 mulass 11144 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑖(digitβ€˜2)(π‘Ž / 2)) ∈ β„‚ ∧ (2↑𝑖) ∈ β„‚ ∧ 2 ∈ β„‚) β†’ (((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· (2↑𝑖)) Β· 2) = ((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· ((2↑𝑖) Β· 2)))
116115eqcomd 2739 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑖(digitβ€˜2)(π‘Ž / 2)) ∈ β„‚ ∧ (2↑𝑖) ∈ β„‚ ∧ 2 ∈ β„‚) β†’ ((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· ((2↑𝑖) Β· 2)) = (((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· (2↑𝑖)) Β· 2))
117108, 113, 114, 116syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ ((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· ((2↑𝑖) Β· 2)) = (((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· (2↑𝑖)) Β· 2))
11899, 117eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ (((𝑖 + 1)(digitβ€˜2)π‘Ž) Β· (2↑(𝑖 + 1))) = (((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· (2↑𝑖)) Β· 2))
119118sumeq2dv 15593 . . . . . . . . . . . . . . . . . . . . . 22 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digitβ€˜2)π‘Ž) Β· (2↑(𝑖 + 1))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· (2↑𝑖)) Β· 2))
120 0cn 11152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 0 ∈ β„‚
121 pncan1 11584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (0 ∈ β„‚ β†’ ((0 + 1) βˆ’ 1) = 0)
122120, 121ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((0 + 1) βˆ’ 1) = 0
123122a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ β„• β†’ ((0 + 1) βˆ’ 1) = 0)
124123oveq1d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ β„• β†’ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1)) = (0...(𝑦 βˆ’ 1)))
125 fzoval 13579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ β„€ β†’ (0..^𝑦) = (0...(𝑦 βˆ’ 1)))
126125eqcomd 2739 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ β„€ β†’ (0...(𝑦 βˆ’ 1)) = (0..^𝑦))
12720, 126syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ β„• β†’ (0...(𝑦 βˆ’ 1)) = (0..^𝑦))
128124, 127eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ β„• β†’ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1)) = (0..^𝑦))
129128adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1)) = (0..^𝑦))
130129sumeq1d 15591 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ Σ𝑖 ∈ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1))(((𝑖 + 1)(digitβ€˜2)π‘Ž) Β· (2↑(𝑖 + 1))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digitβ€˜2)π‘Ž) Β· (2↑(𝑖 + 1))))
131130oveq2d 7374 . . . . . . . . . . . . . . . . . . . . . . 23 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ (0 + Σ𝑖 ∈ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1))(((𝑖 + 1)(digitβ€˜2)π‘Ž) Β· (2↑(𝑖 + 1)))) = (0 + Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digitβ€˜2)π‘Ž) Β· (2↑(𝑖 + 1)))))
132 fzofi 13885 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0..^𝑦) ∈ Fin
133132a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ (0..^𝑦) ∈ Fin)
134101peano2zd 12615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝑦) β†’ (𝑖 + 1) ∈ β„€)
135134adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ (𝑖 + 1) ∈ β„€)
13636ad4antlr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ π‘Ž ∈ (0[,)+∞))
137 digvalnn0 46771 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2 ∈ β„• ∧ (𝑖 + 1) ∈ β„€ ∧ π‘Ž ∈ (0[,)+∞)) β†’ ((𝑖 + 1)(digitβ€˜2)π‘Ž) ∈ β„•0)
138100, 135, 136, 137syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ ((𝑖 + 1)(digitβ€˜2)π‘Ž) ∈ β„•0)
139138nn0cnd 12480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ ((𝑖 + 1)(digitβ€˜2)π‘Ž) ∈ β„‚)
14041a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝑦) β†’ 2 ∈ β„•0)
141 peano2nn0 12458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ β„•0 β†’ (𝑖 + 1) ∈ β„•0)
14292, 141syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝑦) β†’ (𝑖 + 1) ∈ β„•0)
143140, 142nn0expcld 14155 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (0..^𝑦) β†’ (2↑(𝑖 + 1)) ∈ β„•0)
144143nn0cnd 12480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^𝑦) β†’ (2↑(𝑖 + 1)) ∈ β„‚)
145144adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ (2↑(𝑖 + 1)) ∈ β„‚)
146139, 145mulcld 11180 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ (((𝑖 + 1)(digitβ€˜2)π‘Ž) Β· (2↑(𝑖 + 1))) ∈ β„‚)
147133, 146fsumcl 15623 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digitβ€˜2)π‘Ž) Β· (2↑(𝑖 + 1))) ∈ β„‚)
148147addid2d 11361 . . . . . . . . . . . . . . . . . . . . . . 23 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ (0 + Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digitβ€˜2)π‘Ž) Β· (2↑(𝑖 + 1)))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digitβ€˜2)π‘Ž) Β· (2↑(𝑖 + 1))))
149131, 148eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . 22 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ (0 + Σ𝑖 ∈ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1))(((𝑖 + 1)(digitβ€˜2)π‘Ž) Β· (2↑(𝑖 + 1)))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digitβ€˜2)π‘Ž) Β· (2↑(𝑖 + 1))))
150 2cnd 12236 . . . . . . . . . . . . . . . . . . . . . . 23 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ 2 ∈ β„‚)
151140, 92nn0expcld 14155 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^𝑦) β†’ (2↑𝑖) ∈ β„•0)
152151nn0cnd 12480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (0..^𝑦) β†’ (2↑𝑖) ∈ β„‚)
153152adantl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ (2↑𝑖) ∈ β„‚)
154108, 153mulcld 11180 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) ∧ 𝑖 ∈ (0..^𝑦)) β†’ ((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· (2↑𝑖)) ∈ β„‚)
155133, 150, 154fsummulc1 15675 . . . . . . . . . . . . . . . . . . . . . 22 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ (Σ𝑖 ∈ (0..^𝑦)((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· (2↑𝑖)) Β· 2) = Σ𝑖 ∈ (0..^𝑦)(((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· (2↑𝑖)) Β· 2))
156119, 149, 1553eqtr4d 2783 . . . . . . . . . . . . . . . . . . . . 21 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ (0 + Σ𝑖 ∈ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1))(((𝑖 + 1)(digitβ€˜2)π‘Ž) Β· (2↑(𝑖 + 1)))) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· (2↑𝑖)) Β· 2))
15789, 156eqtrd 2773 . . . . . . . . . . . . . . . . . . . 20 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ (((0(digitβ€˜2)π‘Ž) Β· 1) + Ξ£π‘˜ ∈ ((0 + 1)...𝑦)((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜))) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· (2↑𝑖)) Β· 2))
15825, 56, 1573eqtrd 2777 . . . . . . . . . . . . . . . . . . 19 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· (2↑𝑖)) Β· 2))
159158adantl 483 . . . . . . . . . . . . . . . . . 18 (((π‘Ž / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜)) ∧ ((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•)) β†’ Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· (2↑𝑖)) Β· 2))
160 oveq1 7365 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘˜ = 𝑖 β†’ (π‘˜(digitβ€˜2)(π‘Ž / 2)) = (𝑖(digitβ€˜2)(π‘Ž / 2)))
161 oveq2 7366 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘˜ = 𝑖 β†’ (2β†‘π‘˜) = (2↑𝑖))
162160, 161oveq12d 7376 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘˜ = 𝑖 β†’ ((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜)) = ((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· (2↑𝑖)))
163162cbvsumv 15586 . . . . . . . . . . . . . . . . . . . . . . 23 Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜)) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· (2↑𝑖))
164163a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜)) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· (2↑𝑖)))
165164eqeq2d 2744 . . . . . . . . . . . . . . . . . . . . 21 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ ((π‘Ž / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜)) ↔ (π‘Ž / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· (2↑𝑖))))
166165biimpac 480 . . . . . . . . . . . . . . . . . . . 20 (((π‘Ž / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜)) ∧ ((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•)) β†’ (π‘Ž / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· (2↑𝑖)))
167166eqcomd 2739 . . . . . . . . . . . . . . . . . . 19 (((π‘Ž / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜)) ∧ ((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•)) β†’ Σ𝑖 ∈ (0..^𝑦)((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· (2↑𝑖)) = (π‘Ž / 2))
168167oveq1d 7373 . . . . . . . . . . . . . . . . . 18 (((π‘Ž / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜)) ∧ ((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•)) β†’ (Σ𝑖 ∈ (0..^𝑦)((𝑖(digitβ€˜2)(π‘Ž / 2)) Β· (2↑𝑖)) Β· 2) = ((π‘Ž / 2) Β· 2))
169 nncn 12166 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž ∈ β„• β†’ π‘Ž ∈ β„‚)
170 2cnd 12236 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž ∈ β„• β†’ 2 ∈ β„‚)
171 2ne0 12262 . . . . . . . . . . . . . . . . . . . . . 22 2 β‰  0
172171a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž ∈ β„• β†’ 2 β‰  0)
173169, 170, 172divcan1d 11937 . . . . . . . . . . . . . . . . . . . 20 (π‘Ž ∈ β„• β†’ ((π‘Ž / 2) Β· 2) = π‘Ž)
174173ad3antlr 730 . . . . . . . . . . . . . . . . . . 19 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ ((π‘Ž / 2) Β· 2) = π‘Ž)
175174adantl 483 . . . . . . . . . . . . . . . . . 18 (((π‘Ž / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜)) ∧ ((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•)) β†’ ((π‘Ž / 2) Β· 2) = π‘Ž)
176159, 168, 1753eqtrrd 2778 . . . . . . . . . . . . . . . . 17 (((π‘Ž / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜)) ∧ ((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•)) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))
177176ex 414 . . . . . . . . . . . . . . . 16 ((π‘Ž / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜)) β†’ (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜))))
178177imim2i 16 . . . . . . . . . . . . . . 15 (((#bβ€˜(π‘Ž / 2)) = 𝑦 β†’ (π‘Ž / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜))) β†’ ((#bβ€˜(π‘Ž / 2)) = 𝑦 β†’ (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))))
179178com13 88 . . . . . . . . . . . . . 14 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ ((#bβ€˜(π‘Ž / 2)) = 𝑦 β†’ (((#bβ€˜(π‘Ž / 2)) = 𝑦 β†’ (π‘Ž / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜))) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))))
18019, 179sylbid 239 . . . . . . . . . . . . 13 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ ((#bβ€˜(π‘Ž / 2)) = ((#bβ€˜π‘Ž) βˆ’ 1) β†’ (((#bβ€˜(π‘Ž / 2)) = 𝑦 β†’ (π‘Ž / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜))) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))))
181180com23 86 . . . . . . . . . . . 12 (((((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) ∧ 𝑦 ∈ β„•) β†’ (((#bβ€˜(π‘Ž / 2)) = 𝑦 β†’ (π‘Ž / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜))) β†’ ((#bβ€˜(π‘Ž / 2)) = ((#bβ€˜π‘Ž) βˆ’ 1) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))))
182181exp31 421 . . . . . . . . . . 11 (((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) β†’ ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ (𝑦 ∈ β„• β†’ (((#bβ€˜(π‘Ž / 2)) = 𝑦 β†’ (π‘Ž / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜))) β†’ ((#bβ€˜(π‘Ž / 2)) = ((#bβ€˜π‘Ž) βˆ’ 1) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))))))
183182com25 99 . . . . . . . . . 10 (((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) β†’ ((#bβ€˜(π‘Ž / 2)) = ((#bβ€˜π‘Ž) βˆ’ 1) β†’ (𝑦 ∈ β„• β†’ (((#bβ€˜(π‘Ž / 2)) = 𝑦 β†’ (π‘Ž / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜))) β†’ ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))))))
184183com14 96 . . . . . . . . 9 (((#bβ€˜(π‘Ž / 2)) = 𝑦 β†’ (π‘Ž / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)(π‘Ž / 2)) Β· (2β†‘π‘˜))) β†’ ((#bβ€˜(π‘Ž / 2)) = ((#bβ€˜π‘Ž) βˆ’ 1) β†’ (𝑦 ∈ β„• β†’ (((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) β†’ ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))))))
18512, 184syl 17 . . . . . . . 8 (((π‘Ž / 2) ∈ β„•0 ∧ βˆ€π‘₯ ∈ β„•0 ((#bβ€˜π‘₯) = 𝑦 β†’ π‘₯ = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜)))) β†’ ((#bβ€˜(π‘Ž / 2)) = ((#bβ€˜π‘Ž) βˆ’ 1) β†’ (𝑦 ∈ β„• β†’ (((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) β†’ ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))))))
186185ex 414 . . . . . . 7 ((π‘Ž / 2) ∈ β„•0 β†’ (βˆ€π‘₯ ∈ β„•0 ((#bβ€˜π‘₯) = 𝑦 β†’ π‘₯ = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜))) β†’ ((#bβ€˜(π‘Ž / 2)) = ((#bβ€˜π‘Ž) βˆ’ 1) β†’ (𝑦 ∈ β„• β†’ (((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) β†’ ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜))))))))
187186com25 99 . . . . . 6 ((π‘Ž / 2) ∈ β„•0 β†’ (((π‘Ž / 2) ∈ β„• ∧ π‘Ž ∈ β„•) β†’ ((#bβ€˜(π‘Ž / 2)) = ((#bβ€˜π‘Ž) βˆ’ 1) β†’ (𝑦 ∈ β„• β†’ (βˆ€π‘₯ ∈ β„•0 ((#bβ€˜π‘₯) = 𝑦 β†’ π‘₯ = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜))) β†’ ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜))))))))
188187expdcom 416 . . . . 5 ((π‘Ž / 2) ∈ β„• β†’ (π‘Ž ∈ β„• β†’ ((π‘Ž / 2) ∈ β„•0 β†’ ((#bβ€˜(π‘Ž / 2)) = ((#bβ€˜π‘Ž) βˆ’ 1) β†’ (𝑦 ∈ β„• β†’ (βˆ€π‘₯ ∈ β„•0 ((#bβ€˜π‘₯) = 𝑦 β†’ π‘₯ = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜))) β†’ ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))))))))
1891, 188mpid 44 . . . 4 ((π‘Ž / 2) ∈ β„• β†’ (π‘Ž ∈ β„• β†’ ((#bβ€˜(π‘Ž / 2)) = ((#bβ€˜π‘Ž) βˆ’ 1) β†’ (𝑦 ∈ β„• β†’ (βˆ€π‘₯ ∈ β„•0 ((#bβ€˜π‘₯) = 𝑦 β†’ π‘₯ = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜))) β†’ ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜))))))))
190189impcom 409 . . 3 ((π‘Ž ∈ β„• ∧ (π‘Ž / 2) ∈ β„•) β†’ ((#bβ€˜(π‘Ž / 2)) = ((#bβ€˜π‘Ž) βˆ’ 1) β†’ (𝑦 ∈ β„• β†’ (βˆ€π‘₯ ∈ β„•0 ((#bβ€˜π‘₯) = 𝑦 β†’ π‘₯ = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜))) β†’ ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))))))
1913, 190mpd 15 . 2 ((π‘Ž ∈ β„• ∧ (π‘Ž / 2) ∈ β„•) β†’ (𝑦 ∈ β„• β†’ (βˆ€π‘₯ ∈ β„•0 ((#bβ€˜π‘₯) = 𝑦 β†’ π‘₯ = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜))) β†’ ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜))))))
192191imp 408 1 (((π‘Ž ∈ β„• ∧ (π‘Ž / 2) ∈ β„•) ∧ 𝑦 ∈ β„•) β†’ (βˆ€π‘₯ ∈ β„•0 ((#bβ€˜π‘₯) = 𝑦 β†’ π‘₯ = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜))) β†’ ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2940  βˆ€wral 3061  β€˜cfv 6497  (class class class)co 7358  Fincfn 8886  β„‚cc 11054  β„cr 11055  0cc0 11056  1c1 11057   + caddc 11059   Β· cmul 11061  +∞cpnf 11191   βˆ’ cmin 11390   / cdiv 11817  β„•cn 12158  2c2 12213  β„•0cn0 12418  β„€cz 12504  β„€β‰₯cuz 12768  [,)cico 13272  ...cfz 13430  ..^cfzo 13573  β†‘cexp 13973  Ξ£csu 15576  #bcblen 46741  digitcdig 46767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9582  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133  ax-pre-sup 11134  ax-addf 11135  ax-mulf 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-iin 4958  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7618  df-om 7804  df-1st 7922  df-2nd 7923  df-supp 8094  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-er 8651  df-map 8770  df-pm 8771  df-ixp 8839  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fsupp 9309  df-fi 9352  df-sup 9383  df-inf 9384  df-oi 9451  df-card 9880  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-div 11818  df-nn 12159  df-2 12221  df-3 12222  df-4 12223  df-5 12224  df-6 12225  df-7 12226  df-8 12227  df-9 12228  df-n0 12419  df-z 12505  df-dec 12624  df-uz 12769  df-q 12879  df-rp 12921  df-xneg 13038  df-xadd 13039  df-xmul 13040  df-ioo 13274  df-ioc 13275  df-ico 13276  df-icc 13277  df-fz 13431  df-fzo 13574  df-fl 13703  df-mod 13781  df-seq 13913  df-exp 13974  df-fac 14180  df-bc 14209  df-hash 14237  df-shft 14958  df-cj 14990  df-re 14991  df-im 14992  df-sqrt 15126  df-abs 15127  df-limsup 15359  df-clim 15376  df-rlim 15377  df-sum 15577  df-ef 15955  df-sin 15957  df-cos 15958  df-pi 15960  df-struct 17024  df-sets 17041  df-slot 17059  df-ndx 17071  df-base 17089  df-ress 17118  df-plusg 17151  df-mulr 17152  df-starv 17153  df-sca 17154  df-vsca 17155  df-ip 17156  df-tset 17157  df-ple 17158  df-ds 17160  df-unif 17161  df-hom 17162  df-cco 17163  df-rest 17309  df-topn 17310  df-0g 17328  df-gsum 17329  df-topgen 17330  df-pt 17331  df-prds 17334  df-xrs 17389  df-qtop 17394  df-imas 17395  df-xps 17397  df-mre 17471  df-mrc 17472  df-acs 17474  df-mgm 18502  df-sgrp 18551  df-mnd 18562  df-submnd 18607  df-mulg 18878  df-cntz 19102  df-cmn 19569  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-haus 22682  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-xms 23689  df-ms 23690  df-tms 23691  df-cncf 24257  df-limc 25246  df-dv 25247  df-log 25928  df-logb 26131  df-blen 46742  df-dig 46768
This theorem is referenced by:  nn0sumshdiglem1  46793
  Copyright terms: Public domain W3C validator