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 46713
Description: Lemma for nn0sumshdig 46716 (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 12851 . . 3 (π‘Ž ∈ β„• ↔ (π‘Ž = 1 ∨ π‘Ž ∈ (β„€β‰₯β€˜2)))
2 1t1e1 12316 . . . . . . . . 9 (1 Β· 1) = 1
32eqcomi 2746 . . . . . . . 8 1 = (1 Β· 1)
4 simpl 484 . . . . . . . 8 ((π‘Ž = 1 ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) β†’ π‘Ž = 1)
5 oveq2 7366 . . . . . . . . . . . 12 ((𝑦 + 1) = (#bβ€˜π‘Ž) β†’ (0..^(𝑦 + 1)) = (0..^(#bβ€˜π‘Ž)))
65eqcoms 2745 . . . . . . . . . . 11 ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ (0..^(𝑦 + 1)) = (0..^(#bβ€˜π‘Ž)))
7 fveq2 6843 . . . . . . . . . . . . . 14 (π‘Ž = 1 β†’ (#bβ€˜π‘Ž) = (#bβ€˜1))
8 blen1 46677 . . . . . . . . . . . . . 14 (#bβ€˜1) = 1
97, 8eqtrdi 2793 . . . . . . . . . . . . 13 (π‘Ž = 1 β†’ (#bβ€˜π‘Ž) = 1)
109oveq2d 7374 . . . . . . . . . . . 12 (π‘Ž = 1 β†’ (0..^(#bβ€˜π‘Ž)) = (0..^1))
11 fzo01 13655 . . . . . . . . . . . 12 (0..^1) = {0}
1210, 11eqtrdi 2793 . . . . . . . . . . 11 (π‘Ž = 1 β†’ (0..^(#bβ€˜π‘Ž)) = {0})
136, 12sylan9eqr 2799 . . . . . . . . . 10 ((π‘Ž = 1 ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) β†’ (0..^(𝑦 + 1)) = {0})
1413sumeq1d 15587 . . . . . . . . 9 ((π‘Ž = 1 ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) β†’ Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) = Ξ£π‘˜ ∈ {0} ((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))
15 oveq2 7366 . . . . . . . . . . . . 13 (π‘Ž = 1 β†’ (π‘˜(digitβ€˜2)π‘Ž) = (π‘˜(digitβ€˜2)1))
1615oveq1d 7373 . . . . . . . . . . . 12 (π‘Ž = 1 β†’ ((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) = ((π‘˜(digitβ€˜2)1) Β· (2β†‘π‘˜)))
1716sumeq2sdv 15590 . . . . . . . . . . 11 (π‘Ž = 1 β†’ Ξ£π‘˜ ∈ {0} ((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) = Ξ£π‘˜ ∈ {0} ((π‘˜(digitβ€˜2)1) Β· (2β†‘π‘˜)))
18 c0ex 11150 . . . . . . . . . . . 12 0 ∈ V
19 ax-1cn 11110 . . . . . . . . . . . . 13 1 ∈ β„‚
2019, 19mulcli 11163 . . . . . . . . . . . 12 (1 Β· 1) ∈ β„‚
21 oveq1 7365 . . . . . . . . . . . . . . 15 (π‘˜ = 0 β†’ (π‘˜(digitβ€˜2)1) = (0(digitβ€˜2)1))
22 1ex 11152 . . . . . . . . . . . . . . . . 17 1 ∈ V
2322prid2 4725 . . . . . . . . . . . . . . . 16 1 ∈ {0, 1}
24 0dig2pr01 46703 . . . . . . . . . . . . . . . 16 (1 ∈ {0, 1} β†’ (0(digitβ€˜2)1) = 1)
2523, 24ax-mp 5 . . . . . . . . . . . . . . 15 (0(digitβ€˜2)1) = 1
2621, 25eqtrdi 2793 . . . . . . . . . . . . . 14 (π‘˜ = 0 β†’ (π‘˜(digitβ€˜2)1) = 1)
27 oveq2 7366 . . . . . . . . . . . . . . 15 (π‘˜ = 0 β†’ (2β†‘π‘˜) = (2↑0))
28 2cn 12229 . . . . . . . . . . . . . . . 16 2 ∈ β„‚
29 exp0 13972 . . . . . . . . . . . . . . . 16 (2 ∈ β„‚ β†’ (2↑0) = 1)
3028, 29ax-mp 5 . . . . . . . . . . . . . . 15 (2↑0) = 1
3127, 30eqtrdi 2793 . . . . . . . . . . . . . 14 (π‘˜ = 0 β†’ (2β†‘π‘˜) = 1)
3226, 31oveq12d 7376 . . . . . . . . . . . . 13 (π‘˜ = 0 β†’ ((π‘˜(digitβ€˜2)1) Β· (2β†‘π‘˜)) = (1 Β· 1))
3332sumsn 15632 . . . . . . . . . . . 12 ((0 ∈ V ∧ (1 Β· 1) ∈ β„‚) β†’ Ξ£π‘˜ ∈ {0} ((π‘˜(digitβ€˜2)1) Β· (2β†‘π‘˜)) = (1 Β· 1))
3418, 20, 33mp2an 691 . . . . . . . . . . 11 Ξ£π‘˜ ∈ {0} ((π‘˜(digitβ€˜2)1) Β· (2β†‘π‘˜)) = (1 Β· 1)
3517, 34eqtrdi 2793 . . . . . . . . . 10 (π‘Ž = 1 β†’ Ξ£π‘˜ ∈ {0} ((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) = (1 Β· 1))
3635adantr 482 . . . . . . . . 9 ((π‘Ž = 1 ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) β†’ Ξ£π‘˜ ∈ {0} ((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) = (1 Β· 1))
3714, 36eqtrd 2777 . . . . . . . 8 ((π‘Ž = 1 ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) β†’ Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) = (1 Β· 1))
383, 4, 373eqtr4a 2803 . . . . . . 7 ((π‘Ž = 1 ∧ (#bβ€˜π‘Ž) = (𝑦 + 1)) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))
3938ex 414 . . . . . 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 12813 . . . . . . . . 9 (π‘Ž ∈ (β„€β‰₯β€˜2) β†’ π‘Ž ∈ β„•0)
43 nn0ob 16267 . . . . . . . . . 10 (π‘Ž ∈ β„•0 β†’ (((π‘Ž + 1) / 2) ∈ β„•0 ↔ ((π‘Ž βˆ’ 1) / 2) ∈ β„•0))
4443bicomd 222 . . . . . . . . 9 (π‘Ž ∈ β„•0 β†’ (((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ↔ ((π‘Ž + 1) / 2) ∈ β„•0))
4542, 44syl 17 . . . . . . . 8 (π‘Ž ∈ (β„€β‰₯β€˜2) β†’ (((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ↔ ((π‘Ž + 1) / 2) ∈ β„•0))
46 blennngt2o2 46685 . . . . . . . . 9 ((π‘Ž ∈ (β„€β‰₯β€˜2) ∧ ((π‘Ž + 1) / 2) ∈ β„•0) β†’ (#bβ€˜π‘Ž) = ((#bβ€˜((π‘Ž βˆ’ 1) / 2)) + 1))
4746ex 414 . . . . . . . 8 (π‘Ž ∈ (β„€β‰₯β€˜2) β†’ (((π‘Ž + 1) / 2) ∈ β„•0 β†’ (#bβ€˜π‘Ž) = ((#bβ€˜((π‘Ž βˆ’ 1) / 2)) + 1)))
4845, 47sylbid 239 . . . . . . 7 (π‘Ž ∈ (β„€β‰₯β€˜2) β†’ (((π‘Ž βˆ’ 1) / 2) ∈ β„•0 β†’ (#bβ€˜π‘Ž) = ((#bβ€˜((π‘Ž βˆ’ 1) / 2)) + 1)))
4948imp 408 . . . . . 6 ((π‘Ž ∈ (β„€β‰₯β€˜2) ∧ ((π‘Ž βˆ’ 1) / 2) ∈ β„•0) β†’ (#bβ€˜π‘Ž) = ((#bβ€˜((π‘Ž βˆ’ 1) / 2)) + 1))
50 fveqeq2 6852 . . . . . . . . . . . . 13 (π‘₯ = ((π‘Ž βˆ’ 1) / 2) β†’ ((#bβ€˜π‘₯) = 𝑦 ↔ (#bβ€˜((π‘Ž βˆ’ 1) / 2)) = 𝑦))
51 id 22 . . . . . . . . . . . . . 14 (π‘₯ = ((π‘Ž βˆ’ 1) / 2) β†’ π‘₯ = ((π‘Ž βˆ’ 1) / 2))
52 oveq2 7366 . . . . . . . . . . . . . . . 16 (π‘₯ = ((π‘Ž βˆ’ 1) / 2) β†’ (π‘˜(digitβ€˜2)π‘₯) = (π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)))
5352oveq1d 7373 . . . . . . . . . . . . . . 15 (π‘₯ = ((π‘Ž βˆ’ 1) / 2) β†’ ((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜)) = ((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜)))
5453sumeq2sdv 15590 . . . . . . . . . . . . . 14 (π‘₯ = ((π‘Ž βˆ’ 1) / 2) β†’ Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜)) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜)))
5551, 54eqeq12d 2753 . . . . . . . . . . . . 13 (π‘₯ = ((π‘Ž βˆ’ 1) / 2) β†’ (π‘₯ = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜)) ↔ ((π‘Ž βˆ’ 1) / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜))))
5650, 55imbi12d 345 . . . . . . . . . . . 12 (π‘₯ = ((π‘Ž βˆ’ 1) / 2) β†’ (((#bβ€˜π‘₯) = 𝑦 β†’ π‘₯ = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜))) ↔ ((#bβ€˜((π‘Ž βˆ’ 1) / 2)) = 𝑦 β†’ ((π‘Ž βˆ’ 1) / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜)))))
5756rspcva 3580 . . . . . . . . . . 11 ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ βˆ€π‘₯ ∈ β„•0 ((#bβ€˜π‘₯) = 𝑦 β†’ π‘₯ = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜)))) β†’ ((#bβ€˜((π‘Ž βˆ’ 1) / 2)) = 𝑦 β†’ ((π‘Ž βˆ’ 1) / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜))))
58 eqeq1 2741 . . . . . . . . . . . . . . . 16 ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ ((#bβ€˜π‘Ž) = ((#bβ€˜((π‘Ž βˆ’ 1) / 2)) + 1) ↔ (𝑦 + 1) = ((#bβ€˜((π‘Ž βˆ’ 1) / 2)) + 1)))
59 nncn 12162 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ β„• β†’ 𝑦 ∈ β„‚)
6059ad2antll 728 . . . . . . . . . . . . . . . . . . . 20 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ 𝑦 ∈ β„‚)
61 blennn0elnn 46670 . . . . . . . . . . . . . . . . . . . . . . 23 (((π‘Ž βˆ’ 1) / 2) ∈ β„•0 β†’ (#bβ€˜((π‘Ž βˆ’ 1) / 2)) ∈ β„•)
6261nncnd 12170 . . . . . . . . . . . . . . . . . . . . . 22 (((π‘Ž βˆ’ 1) / 2) ∈ β„•0 β†’ (#bβ€˜((π‘Ž βˆ’ 1) / 2)) ∈ β„‚)
6362adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) β†’ (#bβ€˜((π‘Ž βˆ’ 1) / 2)) ∈ β„‚)
6463ad2antrl 727 . . . . . . . . . . . . . . . . . . . 20 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ (#bβ€˜((π‘Ž βˆ’ 1) / 2)) ∈ β„‚)
65 1cnd 11151 . . . . . . . . . . . . . . . . . . . 20 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ 1 ∈ β„‚)
6660, 64, 65addcan2d 11360 . . . . . . . . . . . . . . . . . . 19 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ ((𝑦 + 1) = ((#bβ€˜((π‘Ž βˆ’ 1) / 2)) + 1) ↔ 𝑦 = (#bβ€˜((π‘Ž βˆ’ 1) / 2))))
67 eqcom 2744 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (#bβ€˜((π‘Ž βˆ’ 1) / 2)) ↔ (#bβ€˜((π‘Ž βˆ’ 1) / 2)) = 𝑦)
68 nnz 12521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ β„• β†’ 𝑦 ∈ β„€)
6968ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ 𝑦 ∈ β„€)
70 fzval3 13642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ β„€ β†’ (0...𝑦) = (0..^(𝑦 + 1)))
7169, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ (0...𝑦) = (0..^(𝑦 + 1)))
7271eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ (0..^(𝑦 + 1)) = (0...𝑦))
7372sumeq1d 15587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) = Ξ£π‘˜ ∈ (0...𝑦)((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))
74 nnnn0 12421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ β„• β†’ 𝑦 ∈ β„•0)
75 elnn0uz 12809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ β„•0 ↔ 𝑦 ∈ (β„€β‰₯β€˜0))
7674, 75sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ β„• β†’ 𝑦 ∈ (β„€β‰₯β€˜0))
7776ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ 𝑦 ∈ (β„€β‰₯β€˜0))
78 2nn 12227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 2 ∈ β„•
7978a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ π‘˜ ∈ (0...𝑦)) β†’ 2 ∈ β„•)
80 elfzelz 13442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (π‘˜ ∈ (0...𝑦) β†’ π‘˜ ∈ β„€)
8180adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ π‘˜ ∈ (0...𝑦)) β†’ π‘˜ ∈ β„€)
82 nn0rp0 13373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (π‘Ž ∈ β„•0 β†’ π‘Ž ∈ (0[,)+∞))
8342, 82syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (π‘Ž ∈ (β„€β‰₯β€˜2) β†’ π‘Ž ∈ (0[,)+∞))
8483adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) β†’ π‘Ž ∈ (0[,)+∞))
8584adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ π‘˜ ∈ (0...𝑦)) β†’ π‘Ž ∈ (0[,)+∞))
86 digvalnn0 46692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((2 ∈ β„• ∧ π‘˜ ∈ β„€ ∧ π‘Ž ∈ (0[,)+∞)) β†’ (π‘˜(digitβ€˜2)π‘Ž) ∈ β„•0)
8779, 81, 85, 86syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ π‘˜ ∈ (0...𝑦)) β†’ (π‘˜(digitβ€˜2)π‘Ž) ∈ β„•0)
8887ex 414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) β†’ (π‘˜ ∈ (0...𝑦) β†’ (π‘˜(digitβ€˜2)π‘Ž) ∈ β„•0))
8988ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ (π‘˜ ∈ (0...𝑦) β†’ (π‘˜(digitβ€˜2)π‘Ž) ∈ β„•0))
9089imp 408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) ∧ π‘˜ ∈ (0...𝑦)) β†’ (π‘˜(digitβ€˜2)π‘Ž) ∈ β„•0)
9190nn0cnd 12476 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) ∧ π‘˜ ∈ (0...𝑦)) β†’ (π‘˜(digitβ€˜2)π‘Ž) ∈ β„‚)
92 2nn0 12431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2 ∈ β„•0
9392a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (π‘˜ ∈ (0...𝑦) β†’ 2 ∈ β„•0)
94 elfznn0 13535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (π‘˜ ∈ (0...𝑦) β†’ π‘˜ ∈ β„•0)
9593, 94nn0expcld 14150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (π‘˜ ∈ (0...𝑦) β†’ (2β†‘π‘˜) ∈ β„•0)
9695nn0cnd 12476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (π‘˜ ∈ (0...𝑦) β†’ (2β†‘π‘˜) ∈ β„‚)
9796adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) ∧ π‘˜ ∈ (0...𝑦)) β†’ (2β†‘π‘˜) ∈ β„‚)
9891, 97mulcld 11176 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) ∧ π‘˜ ∈ (0...𝑦)) β†’ ((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) ∈ β„‚)
99 oveq1 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (π‘˜ = 0 β†’ (π‘˜(digitβ€˜2)π‘Ž) = (0(digitβ€˜2)π‘Ž))
10099, 27oveq12d 7376 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘˜ = 0 β†’ ((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) = ((0(digitβ€˜2)π‘Ž) Β· (2↑0)))
10130oveq2i 7369 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((0(digitβ€˜2)π‘Ž) Β· (2↑0)) = ((0(digitβ€˜2)π‘Ž) Β· 1)
102100, 101eqtrdi 2793 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘˜ = 0 β†’ ((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) = ((0(digitβ€˜2)π‘Ž) Β· 1))
10377, 98, 102fsum1p 15639 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ Ξ£π‘˜ ∈ (0...𝑦)((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) = (((0(digitβ€˜2)π‘Ž) Β· 1) + Ξ£π‘˜ ∈ ((0 + 1)...𝑦)((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜))))
10442adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) β†’ π‘Ž ∈ β„•0)
10542, 43syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (π‘Ž ∈ (β„€β‰₯β€˜2) β†’ (((π‘Ž + 1) / 2) ∈ β„•0 ↔ ((π‘Ž βˆ’ 1) / 2) ∈ β„•0))
106105biimparc 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) β†’ ((π‘Ž + 1) / 2) ∈ β„•0)
107 0dig2nn0o 46706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((π‘Ž ∈ β„•0 ∧ ((π‘Ž + 1) / 2) ∈ β„•0) β†’ (0(digitβ€˜2)π‘Ž) = 1)
108104, 106, 107syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) β†’ (0(digitβ€˜2)π‘Ž) = 1)
109108ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ (0(digitβ€˜2)π‘Ž) = 1)
110109oveq1d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ ((0(digitβ€˜2)π‘Ž) Β· 1) = (1 Β· 1))
111110, 2eqtrdi 2793 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ ((0(digitβ€˜2)π‘Ž) Β· 1) = 1)
112 1z 12534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ β„€
113112a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ 1 ∈ β„€)
114 0p1e1 12276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (0 + 1) = 1
115114, 112eqeltri 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (0 + 1) ∈ β„€
116115a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ (0 + 1) ∈ β„€)
11778a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((π‘Ž ∈ (β„€β‰₯β€˜2) ∧ π‘˜ ∈ ((0 + 1)...𝑦)) β†’ 2 ∈ β„•)
118 elfzelz 13442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (π‘˜ ∈ ((0 + 1)...𝑦) β†’ π‘˜ ∈ β„€)
119118adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((π‘Ž ∈ (β„€β‰₯β€˜2) ∧ π‘˜ ∈ ((0 + 1)...𝑦)) β†’ π‘˜ ∈ β„€)
12042adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((π‘Ž ∈ (β„€β‰₯β€˜2) ∧ π‘˜ ∈ ((0 + 1)...𝑦)) β†’ π‘Ž ∈ β„•0)
121120, 82syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((π‘Ž ∈ (β„€β‰₯β€˜2) ∧ π‘˜ ∈ ((0 + 1)...𝑦)) β†’ π‘Ž ∈ (0[,)+∞))
122117, 119, 121, 86syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((π‘Ž ∈ (β„€β‰₯β€˜2) ∧ π‘˜ ∈ ((0 + 1)...𝑦)) β†’ (π‘˜(digitβ€˜2)π‘Ž) ∈ β„•0)
123122ex 414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (π‘Ž ∈ (β„€β‰₯β€˜2) β†’ (π‘˜ ∈ ((0 + 1)...𝑦) β†’ (π‘˜(digitβ€˜2)π‘Ž) ∈ β„•0))
124123adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) β†’ (π‘˜ ∈ ((0 + 1)...𝑦) β†’ (π‘˜(digitβ€˜2)π‘Ž) ∈ β„•0))
125124ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ (π‘˜ ∈ ((0 + 1)...𝑦) β†’ (π‘˜(digitβ€˜2)π‘Ž) ∈ β„•0))
126125imp 408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) ∧ π‘˜ ∈ ((0 + 1)...𝑦)) β†’ (π‘˜(digitβ€˜2)π‘Ž) ∈ β„•0)
127126nn0cnd 12476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) ∧ π‘˜ ∈ ((0 + 1)...𝑦)) β†’ (π‘˜(digitβ€˜2)π‘Ž) ∈ β„‚)
128 2cnd 12232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (π‘˜ ∈ ((0 + 1)...𝑦) β†’ 2 ∈ β„‚)
129 elfznn 13471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (π‘˜ ∈ (1...𝑦) β†’ π‘˜ ∈ β„•)
130129nnnn0d 12474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (π‘˜ ∈ (1...𝑦) β†’ π‘˜ ∈ β„•0)
131114oveq1i 7368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((0 + 1)...𝑦) = (1...𝑦)
132130, 131eleq2s 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (π‘˜ ∈ ((0 + 1)...𝑦) β†’ π‘˜ ∈ β„•0)
133128, 132expcld 14052 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (π‘˜ ∈ ((0 + 1)...𝑦) β†’ (2β†‘π‘˜) ∈ β„‚)
134133adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) ∧ π‘˜ ∈ ((0 + 1)...𝑦)) β†’ (2β†‘π‘˜) ∈ β„‚)
135127, 134mulcld 11176 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) ∧ π‘˜ ∈ ((0 + 1)...𝑦)) β†’ ((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) ∈ β„‚)
136 oveq1 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (π‘˜ = (𝑖 + 1) β†’ (π‘˜(digitβ€˜2)π‘Ž) = ((𝑖 + 1)(digitβ€˜2)π‘Ž))
137 oveq2 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (π‘˜ = (𝑖 + 1) β†’ (2β†‘π‘˜) = (2↑(𝑖 + 1)))
138136, 137oveq12d 7376 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘˜ = (𝑖 + 1) β†’ ((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) = (((𝑖 + 1)(digitβ€˜2)π‘Ž) Β· (2↑(𝑖 + 1))))
139113, 116, 69, 135, 138fsumshftm 15667 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ Ξ£π‘˜ ∈ ((0 + 1)...𝑦)((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) = Σ𝑖 ∈ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1))(((𝑖 + 1)(digitβ€˜2)π‘Ž) Β· (2↑(𝑖 + 1))))
140111, 139oveq12d 7376 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2781 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)) = (1 + Σ𝑖 ∈ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1))(((𝑖 + 1)(digitβ€˜2)π‘Ž) Β· (2↑(𝑖 + 1)))))
142141adantl 483 . . . . . . . . . . . . . . . . . . . . . . . 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 13573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑖 ∈ (0..^𝑦) β†’ 𝑖 ∈ β„€)
145144adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑖 ∈ (0..^𝑦)) β†’ 𝑖 ∈ β„€)
146 nn0rp0 13373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((π‘Ž βˆ’ 1) / 2) ∈ β„•0 β†’ ((π‘Ž βˆ’ 1) / 2) ∈ (0[,)+∞))
147146adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) β†’ ((π‘Ž βˆ’ 1) / 2) ∈ (0[,)+∞))
148147adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑖 ∈ (0..^𝑦)) β†’ ((π‘Ž βˆ’ 1) / 2) ∈ (0[,)+∞))
149 digvalnn0 46692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((2 ∈ β„• ∧ 𝑖 ∈ β„€ ∧ ((π‘Ž βˆ’ 1) / 2) ∈ (0[,)+∞)) β†’ (𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) ∈ β„•0)
150143, 145, 148, 149syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑖 ∈ (0..^𝑦)) β†’ (𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) ∈ β„•0)
151150nn0cnd 12476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑖 ∈ (0..^𝑦)) β†’ (𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) ∈ β„‚)
152151ex 414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) β†’ (𝑖 ∈ (0..^𝑦) β†’ (𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) ∈ β„‚))
153152ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ (𝑖 ∈ (0..^𝑦) β†’ (𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) ∈ β„‚))
154153imp 408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) ∧ 𝑖 ∈ (0..^𝑦)) β†’ (𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) ∈ β„‚)
15592a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ (0..^𝑦) β†’ 2 ∈ β„•0)
156 elfzonn0 13618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ (0..^𝑦) β†’ 𝑖 ∈ β„•0)
157155, 156nn0expcld 14150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 ∈ (0..^𝑦) β†’ (2↑𝑖) ∈ β„•0)
158157nn0cnd 12476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (0..^𝑦) β†’ (2↑𝑖) ∈ β„‚)
159158adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) ∧ 𝑖 ∈ (0..^𝑦)) β†’ (2↑𝑖) ∈ β„‚)
160 2cnd 12232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) ∧ 𝑖 ∈ (0..^𝑦)) β†’ 2 ∈ β„‚)
161154, 159, 160mulassd 11179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) ∧ 𝑖 ∈ (0..^𝑦)) β†’ (((𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2↑𝑖)) Β· 2) = ((𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· ((2↑𝑖) Β· 2)))
162161eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) ∧ 𝑖 ∈ (0..^𝑦)) β†’ ((𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· ((2↑𝑖) Β· 2)) = (((𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2↑𝑖)) Β· 2))
163162sumeq2dv 15589 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ Σ𝑖 ∈ (0..^𝑦)((𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· ((2↑𝑖) Β· 2)) = Σ𝑖 ∈ (0..^𝑦)(((𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2↑𝑖)) Β· 2))
164163adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . 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 11148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 0 ∈ β„‚
166 pncan1 11580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (0 ∈ β„‚ β†’ ((0 + 1) βˆ’ 1) = 0)
167165, 166ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((0 + 1) βˆ’ 1) = 0
168167a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ β„• β†’ ((0 + 1) βˆ’ 1) = 0)
169168oveq1d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ β„• β†’ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1)) = (0...(𝑦 βˆ’ 1)))
170 fzoval 13574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ β„€ β†’ (0..^𝑦) = (0...(𝑦 βˆ’ 1)))
17168, 170syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ β„• β†’ (0..^𝑦) = (0...(𝑦 βˆ’ 1)))
172169, 171eqtr4d 2780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ β„• β†’ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1)) = (0..^𝑦))
173172ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1)) = (0..^𝑦))
174 simprlr 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ π‘Ž ∈ (β„€β‰₯β€˜2))
175 elfznn0 13535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 ∈ (0...(𝑦 βˆ’ 1)) β†’ 𝑖 ∈ β„•0)
176167oveq1i 7368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1)) = (0...(𝑦 βˆ’ 1))
177175, 176eleq2s 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1)) β†’ 𝑖 ∈ β„•0)
178 dignn0flhalf 46711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((π‘Ž ∈ (β„€β‰₯β€˜2) ∧ 𝑖 ∈ β„•0) β†’ ((𝑖 + 1)(digitβ€˜2)π‘Ž) = (𝑖(digitβ€˜2)(βŒŠβ€˜(π‘Ž / 2))))
179174, 177, 178syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) ∧ 𝑖 ∈ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1))) β†’ ((𝑖 + 1)(digitβ€˜2)π‘Ž) = (𝑖(digitβ€˜2)(βŒŠβ€˜(π‘Ž / 2))))
180 eluzelz 12774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (π‘Ž ∈ (β„€β‰₯β€˜2) β†’ π‘Ž ∈ β„€)
181180adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((π‘Ž ∈ (β„€β‰₯β€˜2) ∧ ((π‘Ž βˆ’ 1) / 2) ∈ β„•0) β†’ π‘Ž ∈ β„€)
182 nn0z 12525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((π‘Ž βˆ’ 1) / 2) ∈ β„•0 β†’ ((π‘Ž βˆ’ 1) / 2) ∈ β„€)
183 zob 16242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (π‘Ž ∈ β„€ β†’ (((π‘Ž + 1) / 2) ∈ β„€ ↔ ((π‘Ž βˆ’ 1) / 2) ∈ β„€))
184180, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (π‘Ž ∈ (β„€β‰₯β€˜2) β†’ (((π‘Ž + 1) / 2) ∈ β„€ ↔ ((π‘Ž βˆ’ 1) / 2) ∈ β„€))
185182, 184syl5ibr 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (π‘Ž ∈ (β„€β‰₯β€˜2) β†’ (((π‘Ž βˆ’ 1) / 2) ∈ β„•0 β†’ ((π‘Ž + 1) / 2) ∈ β„€))
186185imp 408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((π‘Ž ∈ (β„€β‰₯β€˜2) ∧ ((π‘Ž βˆ’ 1) / 2) ∈ β„•0) β†’ ((π‘Ž + 1) / 2) ∈ β„€)
187181, 186jca 513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((π‘Ž ∈ (β„€β‰₯β€˜2) ∧ ((π‘Ž βˆ’ 1) / 2) ∈ β„•0) β†’ (π‘Ž ∈ β„€ ∧ ((π‘Ž + 1) / 2) ∈ β„€))
188187ancoms 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) β†’ (π‘Ž ∈ β„€ ∧ ((π‘Ž + 1) / 2) ∈ β„€))
189188ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ (π‘Ž ∈ β„€ ∧ ((π‘Ž + 1) / 2) ∈ β„€))
190189adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) ∧ 𝑖 ∈ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1))) β†’ (π‘Ž ∈ β„€ ∧ ((π‘Ž + 1) / 2) ∈ β„€))
191 zofldiv2 46624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((π‘Ž ∈ β„€ ∧ ((π‘Ž + 1) / 2) ∈ β„€) β†’ (βŒŠβ€˜(π‘Ž / 2)) = ((π‘Ž βˆ’ 1) / 2))
192190, 191syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) ∧ 𝑖 ∈ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1))) β†’ (βŒŠβ€˜(π‘Ž / 2)) = ((π‘Ž βˆ’ 1) / 2))
193192oveq2d 7374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) ∧ 𝑖 ∈ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1))) β†’ (𝑖(digitβ€˜2)(βŒŠβ€˜(π‘Ž / 2))) = (𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)))
194179, 193eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) ∧ 𝑖 ∈ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1))) β†’ ((𝑖 + 1)(digitβ€˜2)π‘Ž) = (𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)))
195 2cnd 12232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1)) β†’ 2 ∈ β„‚)
196195, 177expp1d 14053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1)) β†’ (2↑(𝑖 + 1)) = ((2↑𝑖) Β· 2))
197196adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) ∧ 𝑖 ∈ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1))) β†’ (2↑(𝑖 + 1)) = ((2↑𝑖) Β· 2))
198194, 197oveq12d 7376 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) ∧ 𝑖 ∈ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1))) β†’ (((𝑖 + 1)(digitβ€˜2)π‘Ž) Β· (2↑(𝑖 + 1))) = ((𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· ((2↑𝑖) Β· 2)))
199173, 198sumeq12dv 15592 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ Σ𝑖 ∈ (((0 + 1) βˆ’ 1)...(𝑦 βˆ’ 1))(((𝑖 + 1)(digitβ€˜2)π‘Ž) Β· (2↑(𝑖 + 1))) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· ((2↑𝑖) Β· 2)))
200199adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . 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 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (π‘˜ = 𝑖 β†’ (π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) = (𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)))
202 oveq2 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (π‘˜ = 𝑖 β†’ (2β†‘π‘˜) = (2↑𝑖))
203201, 202oveq12d 7376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (π‘˜ = 𝑖 β†’ ((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜)) = ((𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2↑𝑖)))
204203cbvsumv 15582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜)) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2↑𝑖))
205204eqeq2i 2750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((π‘Ž βˆ’ 1) / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜)) ↔ ((π‘Ž βˆ’ 1) / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2↑𝑖)))
206205biimpi 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((π‘Ž βˆ’ 1) / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜)) β†’ ((π‘Ž βˆ’ 1) / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2↑𝑖)))
207206adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((π‘Ž βˆ’ 1) / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜)) ∧ ((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•))) β†’ ((π‘Ž βˆ’ 1) / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2↑𝑖)))
208207oveq1d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (0..^𝑦) ∈ Fin
210209a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((π‘Ž βˆ’ 1) / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜)) ∧ ((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•))) β†’ (0..^𝑦) ∈ Fin)
211 2cnd 12232 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((π‘Ž βˆ’ 1) / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜)) ∧ ((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•))) β†’ 2 ∈ β„‚)
212158adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑖 ∈ (0..^𝑦)) β†’ (2↑𝑖) ∈ β„‚)
213151, 212mulcld 11176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑖 ∈ (0..^𝑦)) β†’ ((𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2↑𝑖)) ∈ β„‚)
214213ex 414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) β†’ (𝑖 ∈ (0..^𝑦) β†’ ((𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2↑𝑖)) ∈ β„‚))
215214adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•) β†’ (𝑖 ∈ (0..^𝑦) β†’ ((𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2↑𝑖)) ∈ β„‚))
216215ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((π‘Ž βˆ’ 1) / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜)) ∧ ((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•))) β†’ (𝑖 ∈ (0..^𝑦) β†’ ((𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2↑𝑖)) ∈ β„‚))
217216imp 408 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((π‘Ž βˆ’ 1) / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜)) ∧ ((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•))) ∧ 𝑖 ∈ (0..^𝑦)) β†’ ((𝑖(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2↑𝑖)) ∈ β„‚)
218210, 211, 217fsummulc1 15671 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2777 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2787 . . . . . . . . . . . . . . . . . . . . . . . . 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 7374 . . . . . . . . . . . . . . . . . . . . . . . 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 12776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (π‘Ž ∈ (β„€β‰₯β€˜2) β†’ π‘Ž ∈ β„‚)
223 peano2cnm 11468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (π‘Ž ∈ β„‚ β†’ (π‘Ž βˆ’ 1) ∈ β„‚)
224222, 223syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (π‘Ž ∈ (β„€β‰₯β€˜2) β†’ (π‘Ž βˆ’ 1) ∈ β„‚)
225 2cnd 12232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (π‘Ž ∈ (β„€β‰₯β€˜2) β†’ 2 ∈ β„‚)
226 2ne0 12258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2 β‰  0
227226a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (π‘Ž ∈ (β„€β‰₯β€˜2) β†’ 2 β‰  0)
228224, 225, 2273jca 1129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (π‘Ž ∈ (β„€β‰₯β€˜2) β†’ ((π‘Ž βˆ’ 1) ∈ β„‚ ∧ 2 ∈ β„‚ ∧ 2 β‰  0))
229228adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) β†’ ((π‘Ž βˆ’ 1) ∈ β„‚ ∧ 2 ∈ β„‚ ∧ 2 β‰  0))
230 divcan1 11823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((π‘Ž βˆ’ 1) ∈ β„‚ ∧ 2 ∈ β„‚ ∧ 2 β‰  0) β†’ (((π‘Ž βˆ’ 1) / 2) Β· 2) = (π‘Ž βˆ’ 1))
231229, 230syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) β†’ (((π‘Ž βˆ’ 1) / 2) Β· 2) = (π‘Ž βˆ’ 1))
232231oveq2d 7374 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) β†’ (1 + (((π‘Ž βˆ’ 1) / 2) Β· 2)) = (1 + (π‘Ž βˆ’ 1)))
233 1cnd 11151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (π‘Ž ∈ (β„€β‰₯β€˜2) β†’ 1 ∈ β„‚)
234233, 222jca 513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (π‘Ž ∈ (β„€β‰₯β€˜2) β†’ (1 ∈ β„‚ ∧ π‘Ž ∈ β„‚))
235234adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) β†’ (1 ∈ β„‚ ∧ π‘Ž ∈ β„‚))
236 pncan3 11410 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((1 ∈ β„‚ ∧ π‘Ž ∈ β„‚) β†’ (1 + (π‘Ž βˆ’ 1)) = π‘Ž)
237235, 236syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) β†’ (1 + (π‘Ž βˆ’ 1)) = π‘Ž)
238232, 237eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) β†’ (1 + (((π‘Ž βˆ’ 1) / 2) Β· 2)) = π‘Ž)
239238adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•) β†’ (1 + (((π‘Ž βˆ’ 1) / 2) Β· 2)) = π‘Ž)
240239ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((π‘Ž βˆ’ 1) / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜)) ∧ ((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•))) β†’ (1 + (((π‘Ž βˆ’ 1) / 2) Β· 2)) = π‘Ž)
241142, 221, 2403eqtrrd 2782 . . . . . . . . . . . . . . . . . . . . . . 23 ((((π‘Ž βˆ’ 1) / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜)) ∧ ((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•))) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))
242241ex 414 . . . . . . . . . . . . . . . . . . . . . 22 (((π‘Ž βˆ’ 1) / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜)) β†’ (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜))))
243242imim2i 16 . . . . . . . . . . . . . . . . . . . . 21 (((#bβ€˜((π‘Ž βˆ’ 1) / 2)) = 𝑦 β†’ ((π‘Ž βˆ’ 1) / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜))) β†’ ((#bβ€˜((π‘Ž βˆ’ 1) / 2)) = 𝑦 β†’ (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))))
244243com13 88 . . . . . . . . . . . . . . . . . . . 20 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ ((#bβ€˜((π‘Ž βˆ’ 1) / 2)) = 𝑦 β†’ (((#bβ€˜((π‘Ž βˆ’ 1) / 2)) = 𝑦 β†’ ((π‘Ž βˆ’ 1) / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜))) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))))
24567, 244biimtrid 241 . . . . . . . . . . . . . . . . . . 19 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ (𝑦 = (#bβ€˜((π‘Ž βˆ’ 1) / 2)) β†’ (((#bβ€˜((π‘Ž βˆ’ 1) / 2)) = 𝑦 β†’ ((π‘Ž βˆ’ 1) / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜))) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))))
24666, 245sylbid 239 . . . . . . . . . . . . . . . . . 18 (((#bβ€˜π‘Ž) = (𝑦 + 1) ∧ ((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•)) β†’ ((𝑦 + 1) = ((#bβ€˜((π‘Ž βˆ’ 1) / 2)) + 1) β†’ (((#bβ€˜((π‘Ž βˆ’ 1) / 2)) = 𝑦 β†’ ((π‘Ž βˆ’ 1) / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜))) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))))
247246ex 414 . . . . . . . . . . . . . . . . 17 ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ (((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•) β†’ ((𝑦 + 1) = ((#bβ€˜((π‘Ž βˆ’ 1) / 2)) + 1) β†’ (((#bβ€˜((π‘Ž βˆ’ 1) / 2)) = 𝑦 β†’ ((π‘Ž βˆ’ 1) / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜))) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜))))))
248247com23 86 . . . . . . . . . . . . . . . 16 ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ ((𝑦 + 1) = ((#bβ€˜((π‘Ž βˆ’ 1) / 2)) + 1) β†’ (((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•) β†’ (((#bβ€˜((π‘Ž βˆ’ 1) / 2)) = 𝑦 β†’ ((π‘Ž βˆ’ 1) / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜))) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜))))))
24958, 248sylbid 239 . . . . . . . . . . . . . . 15 ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ ((#bβ€˜π‘Ž) = ((#bβ€˜((π‘Ž βˆ’ 1) / 2)) + 1) β†’ (((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•) β†’ (((#bβ€˜((π‘Ž βˆ’ 1) / 2)) = 𝑦 β†’ ((π‘Ž βˆ’ 1) / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜))) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜))))))
250249com23 86 . . . . . . . . . . . . . 14 ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ (((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•) β†’ ((#bβ€˜π‘Ž) = ((#bβ€˜((π‘Ž βˆ’ 1) / 2)) + 1) β†’ (((#bβ€˜((π‘Ž βˆ’ 1) / 2)) = 𝑦 β†’ ((π‘Ž βˆ’ 1) / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜))) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜))))))
251250com14 96 . . . . . . . . . . . . 13 (((#bβ€˜((π‘Ž βˆ’ 1) / 2)) = 𝑦 β†’ ((π‘Ž βˆ’ 1) / 2) = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)((π‘Ž βˆ’ 1) / 2)) Β· (2β†‘π‘˜))) β†’ (((((π‘Ž βˆ’ 1) / 2) ∈ β„•0 ∧ π‘Ž ∈ (β„€β‰₯β€˜2)) ∧ 𝑦 ∈ β„•) β†’ ((#bβ€˜π‘Ž) = ((#bβ€˜((π‘Ž βˆ’ 1) / 2)) + 1) β†’ ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜))))))
252251exp4c 434 . . . . . . . . . . . 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 414 . . . . . . . . 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 409 . . . . . 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 414 . . . 4 (π‘Ž ∈ (β„€β‰₯β€˜2) β†’ (((π‘Ž βˆ’ 1) / 2) ∈ β„•0 β†’ (𝑦 ∈ β„• β†’ (βˆ€π‘₯ ∈ β„•0 ((#bβ€˜π‘₯) = 𝑦 β†’ π‘₯ = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜))) β†’ ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))))))
26141, 260jaoi 856 . . 3 ((π‘Ž = 1 ∨ π‘Ž ∈ (β„€β‰₯β€˜2)) β†’ (((π‘Ž βˆ’ 1) / 2) ∈ β„•0 β†’ (𝑦 ∈ β„• β†’ (βˆ€π‘₯ ∈ β„•0 ((#bβ€˜π‘₯) = 𝑦 β†’ π‘₯ = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜))) β†’ ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))))))
2621, 261sylbi 216 . 2 (π‘Ž ∈ β„• β†’ (((π‘Ž βˆ’ 1) / 2) ∈ β„•0 β†’ (𝑦 ∈ β„• β†’ (βˆ€π‘₯ ∈ β„•0 ((#bβ€˜π‘₯) = 𝑦 β†’ π‘₯ = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜))) β†’ ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))))))
263262imp31 419 1 (((π‘Ž ∈ β„• ∧ ((π‘Ž βˆ’ 1) / 2) ∈ β„•0) ∧ 𝑦 ∈ β„•) β†’ (βˆ€π‘₯ ∈ β„•0 ((#bβ€˜π‘₯) = 𝑦 β†’ π‘₯ = Ξ£π‘˜ ∈ (0..^𝑦)((π‘˜(digitβ€˜2)π‘₯) Β· (2β†‘π‘˜))) β†’ ((#bβ€˜π‘Ž) = (𝑦 + 1) β†’ π‘Ž = Ξ£π‘˜ ∈ (0..^(𝑦 + 1))((π‘˜(digitβ€˜2)π‘Ž) Β· (2β†‘π‘˜)))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  Vcvv 3446  {csn 4587  {cpr 4589  β€˜cfv 6497  (class class class)co 7358  Fincfn 8884  β„‚cc 11050  0cc0 11052  1c1 11053   + caddc 11055   Β· cmul 11057  +∞cpnf 11187   βˆ’ cmin 11386   / cdiv 11813  β„•cn 12154  2c2 12209  β„•0cn0 12414  β„€cz 12500  β„€β‰₯cuz 12764  [,)cico 13267  ...cfz 13425  ..^cfzo 13568  βŒŠcfl 13696  β†‘cexp 13968  Ξ£csu 15571  #bcblen 46662  digitcdig 46688
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 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9578  ax-cnex 11108  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-mulcom 11116  ax-addass 11117  ax-mulass 11118  ax-distr 11119  ax-i2m1 11120  ax-1ne0 11121  ax-1rid 11122  ax-rnegex 11123  ax-rrecex 11124  ax-cnre 11125  ax-pre-lttri 11126  ax-pre-lttrn 11127  ax-pre-ltadd 11128  ax-pre-mulgt0 11129  ax-pre-sup 11130  ax-addf 11131  ax-mulf 11132
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3354  df-reu 3355  df-rab 3409  df-v 3448  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 8649  df-map 8768  df-pm 8769  df-ixp 8837  df-en 8885  df-dom 8886  df-sdom 8887  df-fin 8888  df-fsupp 9307  df-fi 9348  df-sup 9379  df-inf 9380  df-oi 9447  df-card 9876  df-pnf 11192  df-mnf 11193  df-xr 11194  df-ltxr 11195  df-le 11196  df-sub 11388  df-neg 11389  df-div 11814  df-nn 12155  df-2 12217  df-3 12218  df-4 12219  df-5 12220  df-6 12221  df-7 12222  df-8 12223  df-9 12224  df-n0 12415  df-z 12501  df-dec 12620  df-uz 12765  df-q 12875  df-rp 12917  df-xneg 13034  df-xadd 13035  df-xmul 13036  df-ioo 13269  df-ioc 13270  df-ico 13271  df-icc 13272  df-fz 13426  df-fzo 13569  df-fl 13698  df-mod 13776  df-seq 13908  df-exp 13969  df-fac 14175  df-bc 14204  df-hash 14232  df-shft 14953  df-cj 14985  df-re 14986  df-im 14987  df-sqrt 15121  df-abs 15122  df-limsup 15354  df-clim 15371  df-rlim 15372  df-sum 15572  df-ef 15951  df-sin 15953  df-cos 15954  df-pi 15956  df-dvds 16138  df-struct 17020  df-sets 17037  df-slot 17055  df-ndx 17067  df-base 17085  df-ress 17114  df-plusg 17147  df-mulr 17148  df-starv 17149  df-sca 17150  df-vsca 17151  df-ip 17152  df-tset 17153  df-ple 17154  df-ds 17156  df-unif 17157  df-hom 17158  df-cco 17159  df-rest 17305  df-topn 17306  df-0g 17324  df-gsum 17325  df-topgen 17326  df-pt 17327  df-prds 17330  df-xrs 17385  df-qtop 17390  df-imas 17391  df-xps 17393  df-mre 17467  df-mrc 17468  df-acs 17470  df-mgm 18498  df-sgrp 18547  df-mnd 18558  df-submnd 18603  df-mulg 18874  df-cntz 19098  df-cmn 19565  df-psmet 20791  df-xmet 20792  df-met 20793  df-bl 20794  df-mopn 20795  df-fbas 20796  df-fg 20797  df-cnfld 20800  df-top 22246  df-topon 22263  df-topsp 22285  df-bases 22299  df-cld 22373  df-ntr 22374  df-cls 22375  df-nei 22452  df-lp 22490  df-perf 22491  df-cn 22581  df-cnp 22582  df-haus 22669  df-tx 22916  df-hmeo 23109  df-fil 23200  df-fm 23292  df-flim 23293  df-flf 23294  df-xms 23676  df-ms 23677  df-tms 23678  df-cncf 24244  df-limc 25233  df-dv 25234  df-log 25915  df-cxp 25916  df-logb 26118  df-blen 46663  df-dig 46689
This theorem is referenced by:  nn0sumshdiglem1  46714
  Copyright terms: Public domain W3C validator