Step | Hyp | Ref
| Expression |
1 | | eqeq2 2748 |
. . . 4
β’ (π₯ = 1 β
((#bβπ) =
π₯ β
(#bβπ) =
1)) |
2 | | oveq2 7365 |
. . . . . . 7
β’ (π₯ = 1 β (0..^π₯) = (0..^1)) |
3 | | fzo01 13654 |
. . . . . . 7
β’ (0..^1) =
{0} |
4 | 2, 3 | eqtrdi 2792 |
. . . . . 6
β’ (π₯ = 1 β (0..^π₯) = {0}) |
5 | 4 | sumeq1d 15586 |
. . . . 5
β’ (π₯ = 1 β Ξ£π β (0..^π₯)((π(digitβ2)π) Β· (2βπ)) = Ξ£π β {0} ((π(digitβ2)π) Β· (2βπ))) |
6 | 5 | eqeq2d 2747 |
. . . 4
β’ (π₯ = 1 β (π = Ξ£π β (0..^π₯)((π(digitβ2)π) Β· (2βπ)) β π = Ξ£π β {0} ((π(digitβ2)π) Β· (2βπ)))) |
7 | 1, 6 | imbi12d 344 |
. . 3
β’ (π₯ = 1 β
(((#bβπ) =
π₯ β π = Ξ£π β (0..^π₯)((π(digitβ2)π) Β· (2βπ))) β ((#bβπ) = 1 β π = Ξ£π β {0} ((π(digitβ2)π) Β· (2βπ))))) |
8 | 7 | ralbidv 3174 |
. 2
β’ (π₯ = 1 β (βπ β β0
((#bβπ) =
π₯ β π = Ξ£π β (0..^π₯)((π(digitβ2)π) Β· (2βπ))) β βπ β β0
((#bβπ) =
1 β π = Ξ£π β {0} ((π(digitβ2)π) Β· (2βπ))))) |
9 | | eqeq2 2748 |
. . . 4
β’ (π₯ = π¦ β ((#bβπ) = π₯ β (#bβπ) = π¦)) |
10 | | oveq2 7365 |
. . . . . 6
β’ (π₯ = π¦ β (0..^π₯) = (0..^π¦)) |
11 | 10 | sumeq1d 15586 |
. . . . 5
β’ (π₯ = π¦ β Ξ£π β (0..^π₯)((π(digitβ2)π) Β· (2βπ)) = Ξ£π β (0..^π¦)((π(digitβ2)π) Β· (2βπ))) |
12 | 11 | eqeq2d 2747 |
. . . 4
β’ (π₯ = π¦ β (π = Ξ£π β (0..^π₯)((π(digitβ2)π) Β· (2βπ)) β π = Ξ£π β (0..^π¦)((π(digitβ2)π) Β· (2βπ)))) |
13 | 9, 12 | imbi12d 344 |
. . 3
β’ (π₯ = π¦ β (((#bβπ) = π₯ β π = Ξ£π β (0..^π₯)((π(digitβ2)π) Β· (2βπ))) β ((#bβπ) = π¦ β π = Ξ£π β (0..^π¦)((π(digitβ2)π) Β· (2βπ))))) |
14 | 13 | ralbidv 3174 |
. 2
β’ (π₯ = π¦ β (βπ β β0
((#bβπ) =
π₯ β π = Ξ£π β (0..^π₯)((π(digitβ2)π) Β· (2βπ))) β βπ β β0
((#bβπ) =
π¦ β π = Ξ£π β (0..^π¦)((π(digitβ2)π) Β· (2βπ))))) |
15 | | eqeq2 2748 |
. . . 4
β’ (π₯ = (π¦ + 1) β ((#bβπ) = π₯ β (#bβπ) = (π¦ + 1))) |
16 | | oveq2 7365 |
. . . . . 6
β’ (π₯ = (π¦ + 1) β (0..^π₯) = (0..^(π¦ + 1))) |
17 | 16 | sumeq1d 15586 |
. . . . 5
β’ (π₯ = (π¦ + 1) β Ξ£π β (0..^π₯)((π(digitβ2)π) Β· (2βπ)) = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))) |
18 | 17 | eqeq2d 2747 |
. . . 4
β’ (π₯ = (π¦ + 1) β (π = Ξ£π β (0..^π₯)((π(digitβ2)π) Β· (2βπ)) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ)))) |
19 | 15, 18 | imbi12d 344 |
. . 3
β’ (π₯ = (π¦ + 1) β (((#bβπ) = π₯ β π = Ξ£π β (0..^π₯)((π(digitβ2)π) Β· (2βπ))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))) |
20 | 19 | ralbidv 3174 |
. 2
β’ (π₯ = (π¦ + 1) β (βπ β β0
((#bβπ) =
π₯ β π = Ξ£π β (0..^π₯)((π(digitβ2)π) Β· (2βπ))) β βπ β β0
((#bβπ) =
(π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))) |
21 | | eqeq2 2748 |
. . . 4
β’ (π₯ = πΏ β ((#bβπ) = π₯ β (#bβπ) = πΏ)) |
22 | | oveq2 7365 |
. . . . . 6
β’ (π₯ = πΏ β (0..^π₯) = (0..^πΏ)) |
23 | 22 | sumeq1d 15586 |
. . . . 5
β’ (π₯ = πΏ β Ξ£π β (0..^π₯)((π(digitβ2)π) Β· (2βπ)) = Ξ£π β (0..^πΏ)((π(digitβ2)π) Β· (2βπ))) |
24 | 23 | eqeq2d 2747 |
. . . 4
β’ (π₯ = πΏ β (π = Ξ£π β (0..^π₯)((π(digitβ2)π) Β· (2βπ)) β π = Ξ£π β (0..^πΏ)((π(digitβ2)π) Β· (2βπ)))) |
25 | 21, 24 | imbi12d 344 |
. . 3
β’ (π₯ = πΏ β (((#bβπ) = π₯ β π = Ξ£π β (0..^π₯)((π(digitβ2)π) Β· (2βπ))) β ((#bβπ) = πΏ β π = Ξ£π β (0..^πΏ)((π(digitβ2)π) Β· (2βπ))))) |
26 | 25 | ralbidv 3174 |
. 2
β’ (π₯ = πΏ β (βπ β β0
((#bβπ) =
π₯ β π = Ξ£π β (0..^π₯)((π(digitβ2)π) Β· (2βπ))) β βπ β β0
((#bβπ) =
πΏ β π = Ξ£π β (0..^πΏ)((π(digitβ2)π) Β· (2βπ))))) |
27 | | 0cnd 11148 |
. . . . . . . 8
β’ (π β β0
β 0 β β) |
28 | | 2nn 12226 |
. . . . . . . . . . . 12
β’ 2 β
β |
29 | 28 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β0
β 2 β β) |
30 | | 0zd 12511 |
. . . . . . . . . . 11
β’ (π β β0
β 0 β β€) |
31 | | nn0rp0 13372 |
. . . . . . . . . . 11
β’ (π β β0
β π β
(0[,)+β)) |
32 | | digvalnn0 46675 |
. . . . . . . . . . 11
β’ ((2
β β β§ 0 β β€ β§ π β (0[,)+β)) β
(0(digitβ2)π) β
β0) |
33 | 29, 30, 31, 32 | syl3anc 1371 |
. . . . . . . . . 10
β’ (π β β0
β (0(digitβ2)π)
β β0) |
34 | 33 | nn0cnd 12475 |
. . . . . . . . 9
β’ (π β β0
β (0(digitβ2)π)
β β) |
35 | | 1cnd 11150 |
. . . . . . . . 9
β’ (π β β0
β 1 β β) |
36 | 34, 35 | mulcld 11175 |
. . . . . . . 8
β’ (π β β0
β ((0(digitβ2)π)
Β· 1) β β) |
37 | 27, 36 | jca 512 |
. . . . . . 7
β’ (π β β0
β (0 β β β§ ((0(digitβ2)π) Β· 1) β
β)) |
38 | 37 | adantr 481 |
. . . . . 6
β’ ((π β β0
β§ (#bβπ) = 1) β (0 β β β§
((0(digitβ2)π)
Β· 1) β β)) |
39 | | oveq1 7364 |
. . . . . . . 8
β’ (π = 0 β (π(digitβ2)π) = (0(digitβ2)π)) |
40 | | oveq2 7365 |
. . . . . . . . 9
β’ (π = 0 β (2βπ) = (2β0)) |
41 | | 2cn 12228 |
. . . . . . . . . 10
β’ 2 β
β |
42 | | exp0 13971 |
. . . . . . . . . 10
β’ (2 β
β β (2β0) = 1) |
43 | 41, 42 | ax-mp 5 |
. . . . . . . . 9
β’
(2β0) = 1 |
44 | 40, 43 | eqtrdi 2792 |
. . . . . . . 8
β’ (π = 0 β (2βπ) = 1) |
45 | 39, 44 | oveq12d 7375 |
. . . . . . 7
β’ (π = 0 β ((π(digitβ2)π) Β· (2βπ)) = ((0(digitβ2)π) Β· 1)) |
46 | 45 | sumsn 15631 |
. . . . . 6
β’ ((0
β β β§ ((0(digitβ2)π) Β· 1) β β) β
Ξ£π β {0} ((π(digitβ2)π) Β· (2βπ)) = ((0(digitβ2)π) Β· 1)) |
47 | 38, 46 | syl 17 |
. . . . 5
β’ ((π β β0
β§ (#bβπ) = 1) β Ξ£π β {0} ((π(digitβ2)π) Β· (2βπ)) = ((0(digitβ2)π) Β· 1)) |
48 | 34 | adantr 481 |
. . . . . 6
β’ ((π β β0
β§ (#bβπ) = 1) β (0(digitβ2)π) β
β) |
49 | 48 | mulid1d 11172 |
. . . . 5
β’ ((π β β0
β§ (#bβπ) = 1) β ((0(digitβ2)π) Β· 1) =
(0(digitβ2)π)) |
50 | | blen1b 46664 |
. . . . . . . 8
β’ (π β β0
β ((#bβπ) = 1 β (π = 0 β¨ π = 1))) |
51 | 50 | biimpa 477 |
. . . . . . 7
β’ ((π β β0
β§ (#bβπ) = 1) β (π = 0 β¨ π = 1)) |
52 | | vex 3449 |
. . . . . . . 8
β’ π β V |
53 | 52 | elpr 4609 |
. . . . . . 7
β’ (π β {0, 1} β (π = 0 β¨ π = 1)) |
54 | 51, 53 | sylibr 233 |
. . . . . 6
β’ ((π β β0
β§ (#bβπ) = 1) β π β {0, 1}) |
55 | | 0dig2pr01 46686 |
. . . . . 6
β’ (π β {0, 1} β
(0(digitβ2)π) = π) |
56 | 54, 55 | syl 17 |
. . . . 5
β’ ((π β β0
β§ (#bβπ) = 1) β (0(digitβ2)π) = π) |
57 | 47, 49, 56 | 3eqtrrd 2781 |
. . . 4
β’ ((π β β0
β§ (#bβπ) = 1) β π = Ξ£π β {0} ((π(digitβ2)π) Β· (2βπ))) |
58 | 57 | ex 413 |
. . 3
β’ (π β β0
β ((#bβπ) = 1 β π = Ξ£π β {0} ((π(digitβ2)π) Β· (2βπ)))) |
59 | 58 | rgen 3066 |
. 2
β’
βπ β
β0 ((#bβπ) = 1 β π = Ξ£π β {0} ((π(digitβ2)π) Β· (2βπ))) |
60 | | nn0sumshdiglem1 46697 |
. 2
β’ (π¦ β β β
(βπ β
β0 ((#bβπ) = π¦ β π = Ξ£π β (0..^π¦)((π(digitβ2)π) Β· (2βπ))) β βπ β β0
((#bβπ) =
(π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))) |
61 | 8, 14, 20, 26, 59, 60 | nnind 12171 |
1
β’ (πΏ β β β
βπ β
β0 ((#bβπ) = πΏ β π = Ξ£π β (0..^πΏ)((π(digitβ2)π) Β· (2βπ)))) |