Step | Hyp | Ref
| Expression |
1 | | oveq2 7417 |
. . . . . . . . . . 11
β’ (π₯ = 0 β (0..^π₯) = (0..^0)) |
2 | | fzo0 13656 |
. . . . . . . . . . 11
β’ (0..^0) =
β
|
3 | 1, 2 | eqtrdi 2789 |
. . . . . . . . . 10
β’ (π₯ = 0 β (0..^π₯) = β
) |
4 | 3 | ineq2d 4213 |
. . . . . . . . 9
β’ (π₯ = 0 β ((bitsβπ) β© (0..^π₯)) = ((bitsβπ) β© β
)) |
5 | | in0 4392 |
. . . . . . . . 9
β’
((bitsβπ)
β© β
) = β
|
6 | 4, 5 | eqtrdi 2789 |
. . . . . . . 8
β’ (π₯ = 0 β ((bitsβπ) β© (0..^π₯)) = β
) |
7 | 6 | sumeq1d 15647 |
. . . . . . 7
β’ (π₯ = 0 β Ξ£π β ((bitsβπ) β© (0..^π₯))(2βπ) = Ξ£π β β
(2βπ)) |
8 | | sum0 15667 |
. . . . . . 7
β’
Ξ£π β
β
(2βπ) =
0 |
9 | 7, 8 | eqtrdi 2789 |
. . . . . 6
β’ (π₯ = 0 β Ξ£π β ((bitsβπ) β© (0..^π₯))(2βπ) = 0) |
10 | | oveq2 7417 |
. . . . . . . 8
β’ (π₯ = 0 β (2βπ₯) = (2β0)) |
11 | | 2cn 12287 |
. . . . . . . . 9
β’ 2 β
β |
12 | | exp0 14031 |
. . . . . . . . 9
β’ (2 β
β β (2β0) = 1) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . 8
β’
(2β0) = 1 |
14 | 10, 13 | eqtrdi 2789 |
. . . . . . 7
β’ (π₯ = 0 β (2βπ₯) = 1) |
15 | 14 | oveq2d 7425 |
. . . . . 6
β’ (π₯ = 0 β (π mod (2βπ₯)) = (π mod 1)) |
16 | 9, 15 | eqeq12d 2749 |
. . . . 5
β’ (π₯ = 0 β (Ξ£π β ((bitsβπ) β© (0..^π₯))(2βπ) = (π mod (2βπ₯)) β 0 = (π mod 1))) |
17 | 16 | imbi2d 341 |
. . . 4
β’ (π₯ = 0 β ((π β β0 β
Ξ£π β
((bitsβπ) β©
(0..^π₯))(2βπ) = (π mod (2βπ₯))) β (π β β0 β 0 =
(π mod
1)))) |
18 | | oveq2 7417 |
. . . . . . . 8
β’ (π₯ = π β (0..^π₯) = (0..^π)) |
19 | 18 | ineq2d 4213 |
. . . . . . 7
β’ (π₯ = π β ((bitsβπ) β© (0..^π₯)) = ((bitsβπ) β© (0..^π))) |
20 | 19 | sumeq1d 15647 |
. . . . . 6
β’ (π₯ = π β Ξ£π β ((bitsβπ) β© (0..^π₯))(2βπ) = Ξ£π β ((bitsβπ) β© (0..^π))(2βπ)) |
21 | | oveq2 7417 |
. . . . . . 7
β’ (π₯ = π β (2βπ₯) = (2βπ)) |
22 | 21 | oveq2d 7425 |
. . . . . 6
β’ (π₯ = π β (π mod (2βπ₯)) = (π mod (2βπ))) |
23 | 20, 22 | eqeq12d 2749 |
. . . . 5
β’ (π₯ = π β (Ξ£π β ((bitsβπ) β© (0..^π₯))(2βπ) = (π mod (2βπ₯)) β Ξ£π β ((bitsβπ) β© (0..^π))(2βπ) = (π mod (2βπ)))) |
24 | 23 | imbi2d 341 |
. . . 4
β’ (π₯ = π β ((π β β0 β
Ξ£π β
((bitsβπ) β©
(0..^π₯))(2βπ) = (π mod (2βπ₯))) β (π β β0 β
Ξ£π β
((bitsβπ) β©
(0..^π))(2βπ) = (π mod (2βπ))))) |
25 | | oveq2 7417 |
. . . . . . . 8
β’ (π₯ = (π + 1) β (0..^π₯) = (0..^(π + 1))) |
26 | 25 | ineq2d 4213 |
. . . . . . 7
β’ (π₯ = (π + 1) β ((bitsβπ) β© (0..^π₯)) = ((bitsβπ) β© (0..^(π + 1)))) |
27 | 26 | sumeq1d 15647 |
. . . . . 6
β’ (π₯ = (π + 1) β Ξ£π β ((bitsβπ) β© (0..^π₯))(2βπ) = Ξ£π β ((bitsβπ) β© (0..^(π + 1)))(2βπ)) |
28 | | oveq2 7417 |
. . . . . . 7
β’ (π₯ = (π + 1) β (2βπ₯) = (2β(π + 1))) |
29 | 28 | oveq2d 7425 |
. . . . . 6
β’ (π₯ = (π + 1) β (π mod (2βπ₯)) = (π mod (2β(π + 1)))) |
30 | 27, 29 | eqeq12d 2749 |
. . . . 5
β’ (π₯ = (π + 1) β (Ξ£π β ((bitsβπ) β© (0..^π₯))(2βπ) = (π mod (2βπ₯)) β Ξ£π β ((bitsβπ) β© (0..^(π + 1)))(2βπ) = (π mod (2β(π + 1))))) |
31 | 30 | imbi2d 341 |
. . . 4
β’ (π₯ = (π + 1) β ((π β β0 β
Ξ£π β
((bitsβπ) β©
(0..^π₯))(2βπ) = (π mod (2βπ₯))) β (π β β0 β
Ξ£π β
((bitsβπ) β©
(0..^(π + 1)))(2βπ) = (π mod (2β(π + 1)))))) |
32 | | oveq2 7417 |
. . . . . . . 8
β’ (π₯ = π β (0..^π₯) = (0..^π)) |
33 | 32 | ineq2d 4213 |
. . . . . . 7
β’ (π₯ = π β ((bitsβπ) β© (0..^π₯)) = ((bitsβπ) β© (0..^π))) |
34 | 33 | sumeq1d 15647 |
. . . . . 6
β’ (π₯ = π β Ξ£π β ((bitsβπ) β© (0..^π₯))(2βπ) = Ξ£π β ((bitsβπ) β© (0..^π))(2βπ)) |
35 | | oveq2 7417 |
. . . . . . 7
β’ (π₯ = π β (2βπ₯) = (2βπ)) |
36 | 35 | oveq2d 7425 |
. . . . . 6
β’ (π₯ = π β (π mod (2βπ₯)) = (π mod (2βπ))) |
37 | 34, 36 | eqeq12d 2749 |
. . . . 5
β’ (π₯ = π β (Ξ£π β ((bitsβπ) β© (0..^π₯))(2βπ) = (π mod (2βπ₯)) β Ξ£π β ((bitsβπ) β© (0..^π))(2βπ) = (π mod (2βπ)))) |
38 | 37 | imbi2d 341 |
. . . 4
β’ (π₯ = π β ((π β β0 β
Ξ£π β
((bitsβπ) β©
(0..^π₯))(2βπ) = (π mod (2βπ₯))) β (π β β0 β
Ξ£π β
((bitsβπ) β©
(0..^π))(2βπ) = (π mod (2βπ))))) |
39 | | nn0z 12583 |
. . . . . 6
β’ (π β β0
β π β
β€) |
40 | | zmod10 13852 |
. . . . . 6
β’ (π β β€ β (π mod 1) = 0) |
41 | 39, 40 | syl 17 |
. . . . 5
β’ (π β β0
β (π mod 1) =
0) |
42 | 41 | eqcomd 2739 |
. . . 4
β’ (π β β0
β 0 = (π mod
1)) |
43 | | oveq1 7416 |
. . . . . . 7
β’
(Ξ£π β
((bitsβπ) β©
(0..^π))(2βπ) = (π mod (2βπ)) β (Ξ£π β ((bitsβπ) β© (0..^π))(2βπ) + Ξ£π β ((bitsβπ) β© {π})(2βπ)) = ((π mod (2βπ)) + Ξ£π β ((bitsβπ) β© {π})(2βπ))) |
44 | | fzonel 13646 |
. . . . . . . . . . . . 13
β’ Β¬
π β (0..^π) |
45 | 44 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π β
β0) β Β¬ π β (0..^π)) |
46 | | disjsn 4716 |
. . . . . . . . . . . 12
β’
(((0..^π) β©
{π}) = β
β Β¬
π β (0..^π)) |
47 | 45, 46 | sylibr 233 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π β
β0) β ((0..^π) β© {π}) = β
) |
48 | 47 | ineq2d 4213 |
. . . . . . . . . 10
β’ ((π β β0
β§ π β
β0) β ((bitsβπ) β© ((0..^π) β© {π})) = ((bitsβπ) β© β
)) |
49 | | inindi 4227 |
. . . . . . . . . 10
β’
((bitsβπ)
β© ((0..^π) β© {π})) = (((bitsβπ) β© (0..^π)) β© ((bitsβπ) β© {π})) |
50 | 48, 49, 5 | 3eqtr3g 2796 |
. . . . . . . . 9
β’ ((π β β0
β§ π β
β0) β (((bitsβπ) β© (0..^π)) β© ((bitsβπ) β© {π})) = β
) |
51 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π β
β0) β π β β0) |
52 | | nn0uz 12864 |
. . . . . . . . . . . . 13
β’
β0 = (β€β₯β0) |
53 | 51, 52 | eleqtrdi 2844 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π β
β0) β π β
(β€β₯β0)) |
54 | | fzosplitsn 13740 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯β0) β (0..^(π + 1)) = ((0..^π) βͺ {π})) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π β
β0) β (0..^(π + 1)) = ((0..^π) βͺ {π})) |
56 | 55 | ineq2d 4213 |
. . . . . . . . . 10
β’ ((π β β0
β§ π β
β0) β ((bitsβπ) β© (0..^(π + 1))) = ((bitsβπ) β© ((0..^π) βͺ {π}))) |
57 | | indi 4274 |
. . . . . . . . . 10
β’
((bitsβπ)
β© ((0..^π) βͺ {π})) = (((bitsβπ) β© (0..^π)) βͺ ((bitsβπ) β© {π})) |
58 | 56, 57 | eqtrdi 2789 |
. . . . . . . . 9
β’ ((π β β0
β§ π β
β0) β ((bitsβπ) β© (0..^(π + 1))) = (((bitsβπ) β© (0..^π)) βͺ ((bitsβπ) β© {π}))) |
59 | | fzofi 13939 |
. . . . . . . . . . 11
β’
(0..^(π + 1)) β
Fin |
60 | | inss2 4230 |
. . . . . . . . . . 11
β’
((bitsβπ)
β© (0..^(π + 1)))
β (0..^(π +
1)) |
61 | | ssfi 9173 |
. . . . . . . . . . 11
β’
(((0..^(π + 1))
β Fin β§ ((bitsβπ) β© (0..^(π + 1))) β (0..^(π + 1))) β ((bitsβπ) β© (0..^(π + 1))) β Fin) |
62 | 59, 60, 61 | mp2an 691 |
. . . . . . . . . 10
β’
((bitsβπ)
β© (0..^(π + 1))) β
Fin |
63 | 62 | a1i 11 |
. . . . . . . . 9
β’ ((π β β0
β§ π β
β0) β ((bitsβπ) β© (0..^(π + 1))) β Fin) |
64 | | 2nn 12285 |
. . . . . . . . . . . 12
β’ 2 β
β |
65 | 64 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β β0
β§ π β
β0) β§ π β ((bitsβπ) β© (0..^(π + 1)))) β 2 β
β) |
66 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π β β0
β§ π β
β0) β§ π β ((bitsβπ) β© (0..^(π + 1)))) β π β ((bitsβπ) β© (0..^(π + 1)))) |
67 | 66 | elin2d 4200 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ π β
β0) β§ π β ((bitsβπ) β© (0..^(π + 1)))) β π β (0..^(π + 1))) |
68 | | elfzouz 13636 |
. . . . . . . . . . . . 13
β’ (π β (0..^(π + 1)) β π β
(β€β₯β0)) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ π β
β0) β§ π β ((bitsβπ) β© (0..^(π + 1)))) β π β
(β€β₯β0)) |
70 | 69, 52 | eleqtrrdi 2845 |
. . . . . . . . . . 11
β’ (((π β β0
β§ π β
β0) β§ π β ((bitsβπ) β© (0..^(π + 1)))) β π β β0) |
71 | 65, 70 | nnexpcld 14208 |
. . . . . . . . . 10
β’ (((π β β0
β§ π β
β0) β§ π β ((bitsβπ) β© (0..^(π + 1)))) β (2βπ) β β) |
72 | 71 | nncnd 12228 |
. . . . . . . . 9
β’ (((π β β0
β§ π β
β0) β§ π β ((bitsβπ) β© (0..^(π + 1)))) β (2βπ) β β) |
73 | 50, 58, 63, 72 | fsumsplit 15687 |
. . . . . . . 8
β’ ((π β β0
β§ π β
β0) β Ξ£π β ((bitsβπ) β© (0..^(π + 1)))(2βπ) = (Ξ£π β ((bitsβπ) β© (0..^π))(2βπ) + Ξ£π β ((bitsβπ) β© {π})(2βπ))) |
74 | | bitsinv1lem 16382 |
. . . . . . . . . 10
β’ ((π β β€ β§ π β β0)
β (π mod
(2β(π + 1))) = ((π mod (2βπ)) + if(π β (bitsβπ), (2βπ), 0))) |
75 | 39, 74 | sylan 581 |
. . . . . . . . 9
β’ ((π β β0
β§ π β
β0) β (π mod (2β(π + 1))) = ((π mod (2βπ)) + if(π β (bitsβπ), (2βπ), 0))) |
76 | | eqeq2 2745 |
. . . . . . . . . . 11
β’
((2βπ) =
if(π β
(bitsβπ),
(2βπ), 0) β
(Ξ£π β
((bitsβπ) β©
{π})(2βπ) = (2βπ) β Ξ£π β ((bitsβπ) β© {π})(2βπ) = if(π β (bitsβπ), (2βπ), 0))) |
77 | | eqeq2 2745 |
. . . . . . . . . . 11
β’ (0 =
if(π β
(bitsβπ),
(2βπ), 0) β
(Ξ£π β
((bitsβπ) β©
{π})(2βπ) = 0 β Ξ£π β ((bitsβπ) β© {π})(2βπ) = if(π β (bitsβπ), (2βπ), 0))) |
78 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ (((π β β0
β§ π β
β0) β§ π β (bitsβπ)) β π β (bitsβπ)) |
79 | 78 | snssd 4813 |
. . . . . . . . . . . . . 14
β’ (((π β β0
β§ π β
β0) β§ π β (bitsβπ)) β {π} β (bitsβπ)) |
80 | | sseqin2 4216 |
. . . . . . . . . . . . . 14
β’ ({π} β (bitsβπ) β ((bitsβπ) β© {π}) = {π}) |
81 | 79, 80 | sylib 217 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ π β
β0) β§ π β (bitsβπ)) β ((bitsβπ) β© {π}) = {π}) |
82 | 81 | sumeq1d 15647 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ π β
β0) β§ π β (bitsβπ)) β Ξ£π β ((bitsβπ) β© {π})(2βπ) = Ξ£π β {π} (2βπ)) |
83 | | simplr 768 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ π β
β0) β§ π β (bitsβπ)) β π β β0) |
84 | 64 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((π β β0
β§ π β
β0) β§ π β (bitsβπ)) β 2 β β) |
85 | 84, 83 | nnexpcld 14208 |
. . . . . . . . . . . . . 14
β’ (((π β β0
β§ π β
β0) β§ π β (bitsβπ)) β (2βπ) β β) |
86 | 85 | nncnd 12228 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ π β
β0) β§ π β (bitsβπ)) β (2βπ) β β) |
87 | | oveq2 7417 |
. . . . . . . . . . . . . 14
β’ (π = π β (2βπ) = (2βπ)) |
88 | 87 | sumsn 15692 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ (2βπ) β
β) β Ξ£π
β {π} (2βπ) = (2βπ)) |
89 | 83, 86, 88 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ π β
β0) β§ π β (bitsβπ)) β Ξ£π β {π} (2βπ) = (2βπ)) |
90 | 82, 89 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (((π β β0
β§ π β
β0) β§ π β (bitsβπ)) β Ξ£π β ((bitsβπ) β© {π})(2βπ) = (2βπ)) |
91 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π β β0
β§ π β
β0) β§ Β¬ π β (bitsβπ)) β Β¬ π β (bitsβπ)) |
92 | | disjsn 4716 |
. . . . . . . . . . . . . 14
β’
(((bitsβπ)
β© {π}) = β
β
Β¬ π β
(bitsβπ)) |
93 | 91, 92 | sylibr 233 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ π β
β0) β§ Β¬ π β (bitsβπ)) β ((bitsβπ) β© {π}) = β
) |
94 | 93 | sumeq1d 15647 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ π β
β0) β§ Β¬ π β (bitsβπ)) β Ξ£π β ((bitsβπ) β© {π})(2βπ) = Ξ£π β β
(2βπ)) |
95 | 94, 8 | eqtrdi 2789 |
. . . . . . . . . . 11
β’ (((π β β0
β§ π β
β0) β§ Β¬ π β (bitsβπ)) β Ξ£π β ((bitsβπ) β© {π})(2βπ) = 0) |
96 | 76, 77, 90, 95 | ifbothda 4567 |
. . . . . . . . . 10
β’ ((π β β0
β§ π β
β0) β Ξ£π β ((bitsβπ) β© {π})(2βπ) = if(π β (bitsβπ), (2βπ), 0)) |
97 | 96 | oveq2d 7425 |
. . . . . . . . 9
β’ ((π β β0
β§ π β
β0) β ((π mod (2βπ)) + Ξ£π β ((bitsβπ) β© {π})(2βπ)) = ((π mod (2βπ)) + if(π β (bitsβπ), (2βπ), 0))) |
98 | 75, 97 | eqtr4d 2776 |
. . . . . . . 8
β’ ((π β β0
β§ π β
β0) β (π mod (2β(π + 1))) = ((π mod (2βπ)) + Ξ£π β ((bitsβπ) β© {π})(2βπ))) |
99 | 73, 98 | eqeq12d 2749 |
. . . . . . 7
β’ ((π β β0
β§ π β
β0) β (Ξ£π β ((bitsβπ) β© (0..^(π + 1)))(2βπ) = (π mod (2β(π + 1))) β (Ξ£π β ((bitsβπ) β© (0..^π))(2βπ) + Ξ£π β ((bitsβπ) β© {π})(2βπ)) = ((π mod (2βπ)) + Ξ£π β ((bitsβπ) β© {π})(2βπ)))) |
100 | 43, 99 | imbitrrid 245 |
. . . . . 6
β’ ((π β β0
β§ π β
β0) β (Ξ£π β ((bitsβπ) β© (0..^π))(2βπ) = (π mod (2βπ)) β Ξ£π β ((bitsβπ) β© (0..^(π + 1)))(2βπ) = (π mod (2β(π + 1))))) |
101 | 100 | expcom 415 |
. . . . 5
β’ (π β β0
β (π β
β0 β (Ξ£π β ((bitsβπ) β© (0..^π))(2βπ) = (π mod (2βπ)) β Ξ£π β ((bitsβπ) β© (0..^(π + 1)))(2βπ) = (π mod (2β(π + 1)))))) |
102 | 101 | a2d 29 |
. . . 4
β’ (π β β0
β ((π β
β0 β Ξ£π β ((bitsβπ) β© (0..^π))(2βπ) = (π mod (2βπ))) β (π β β0 β
Ξ£π β
((bitsβπ) β©
(0..^(π + 1)))(2βπ) = (π mod (2β(π + 1)))))) |
103 | 17, 24, 31, 38, 42, 102 | nn0ind 12657 |
. . 3
β’ (π β β0
β (π β
β0 β Ξ£π β ((bitsβπ) β© (0..^π))(2βπ) = (π mod (2βπ)))) |
104 | 103 | pm2.43i 52 |
. 2
β’ (π β β0
β Ξ£π β
((bitsβπ) β©
(0..^π))(2βπ) = (π mod (2βπ))) |
105 | | id 22 |
. . . . . . 7
β’ (π β β0
β π β
β0) |
106 | 105, 52 | eleqtrdi 2844 |
. . . . . 6
β’ (π β β0
β π β
(β€β₯β0)) |
107 | 64 | a1i 11 |
. . . . . . . 8
β’ (π β β0
β 2 β β) |
108 | 107, 105 | nnexpcld 14208 |
. . . . . . 7
β’ (π β β0
β (2βπ) β
β) |
109 | 108 | nnzd 12585 |
. . . . . 6
β’ (π β β0
β (2βπ) β
β€) |
110 | | 2z 12594 |
. . . . . . . 8
β’ 2 β
β€ |
111 | | uzid 12837 |
. . . . . . . 8
β’ (2 β
β€ β 2 β (β€β₯β2)) |
112 | 110, 111 | ax-mp 5 |
. . . . . . 7
β’ 2 β
(β€β₯β2) |
113 | | bernneq3 14194 |
. . . . . . 7
β’ ((2
β (β€β₯β2) β§ π β β0) β π < (2βπ)) |
114 | 112, 113 | mpan 689 |
. . . . . 6
β’ (π β β0
β π < (2βπ)) |
115 | | elfzo2 13635 |
. . . . . 6
β’ (π β (0..^(2βπ)) β (π β (β€β₯β0)
β§ (2βπ) β
β€ β§ π <
(2βπ))) |
116 | 106, 109,
114, 115 | syl3anbrc 1344 |
. . . . 5
β’ (π β β0
β π β
(0..^(2βπ))) |
117 | | bitsfzo 16376 |
. . . . . 6
β’ ((π β β€ β§ π β β0)
β (π β
(0..^(2βπ)) β
(bitsβπ) β
(0..^π))) |
118 | 39, 105, 117 | syl2anc 585 |
. . . . 5
β’ (π β β0
β (π β
(0..^(2βπ)) β
(bitsβπ) β
(0..^π))) |
119 | 116, 118 | mpbid 231 |
. . . 4
β’ (π β β0
β (bitsβπ)
β (0..^π)) |
120 | | df-ss 3966 |
. . . 4
β’
((bitsβπ)
β (0..^π) β
((bitsβπ) β©
(0..^π)) =
(bitsβπ)) |
121 | 119, 120 | sylib 217 |
. . 3
β’ (π β β0
β ((bitsβπ)
β© (0..^π)) =
(bitsβπ)) |
122 | 121 | sumeq1d 15647 |
. 2
β’ (π β β0
β Ξ£π β
((bitsβπ) β©
(0..^π))(2βπ) = Ξ£π β (bitsβπ)(2βπ)) |
123 | | nn0re 12481 |
. . 3
β’ (π β β0
β π β
β) |
124 | | 2rp 12979 |
. . . . 5
β’ 2 β
β+ |
125 | 124 | a1i 11 |
. . . 4
β’ (π β β0
β 2 β β+) |
126 | 125, 39 | rpexpcld 14210 |
. . 3
β’ (π β β0
β (2βπ) β
β+) |
127 | | nn0ge0 12497 |
. . 3
β’ (π β β0
β 0 β€ π) |
128 | | modid 13861 |
. . 3
β’ (((π β β β§
(2βπ) β
β+) β§ (0 β€ π β§ π < (2βπ))) β (π mod (2βπ)) = π) |
129 | 123, 126,
127, 114, 128 | syl22anc 838 |
. 2
β’ (π β β0
β (π mod (2βπ)) = π) |
130 | 104, 122,
129 | 3eqtr3d 2781 |
1
β’ (π β β0
β Ξ£π β
(bitsβπ)(2βπ) = π) |