Step | Hyp | Ref
| Expression |
1 | | nnnn0 12425 |
. . . 4
β’ ((π / 2) β β β
(π / 2) β
β0) |
2 | | blennn0em1 46763 |
. . . 4
β’ ((π β β β§ (π / 2) β
β0) β (#bβ(π / 2)) = ((#bβπ) β 1)) |
3 | 1, 2 | sylan2 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))) |
7 | 6 | oveq1d 7373 |
. . . . . . . . . . . . . 14
β’ (π₯ = (π / 2) β ((π(digitβ2)π₯) Β· (2βπ)) = ((π(digitβ2)(π / 2)) Β· (2βπ))) |
8 | 7 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π₯ = (π / 2) β§ π β (0..^π¦)) β ((π(digitβ2)π₯) Β· (2βπ)) = ((π(digitβ2)(π / 2)) Β· (2βπ))) |
9 | 8 | sumeq2dv 15593 |
. . . . . . . . . . . 12
β’ (π₯ = (π / 2) β Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ)) = Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ))) |
10 | 5, 9 | eqeq12d 2749 |
. . . . . . . . . . 11
β’ (π₯ = (π / 2) β (π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ)) β (π / 2) = Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ)))) |
11 | 4, 10 | imbi12d 345 |
. . . . . . . . . 10
β’ (π₯ = (π / 2) β (((#bβπ₯) = π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))) β ((#bβ(π / 2)) = π¦ β (π / 2) = Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ))))) |
12 | 11 | rspcva 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)) |
14 | 13 | oveq1d 7373 |
. . . . . . . . . . . . . . . 16
β’ ((((π / 2) β β β§ π β β) β§
(#bβπ) =
(π¦ + 1)) β
((#bβπ)
β 1) = ((π¦ + 1)
β 1)) |
15 | | nncn 12166 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β β β π¦ β
β) |
16 | | pncan1 11584 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β β β ((π¦ + 1) β 1) = π¦) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β β ((π¦ + 1) β 1) = π¦) |
18 | 14, 17 | sylan9eq 2793 |
. . . . . . . . . . . . . . 15
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β
((#bβπ)
β 1) = π¦) |
19 | 18 | eqeq2d 2744 |
. . . . . . . . . . . . . 14
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β
((#bβ(π /
2)) = ((#bβπ) β 1) β
(#bβ(π /
2)) = π¦)) |
20 | | nnz 12525 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π¦ β β β π¦ β
β€) |
21 | 20 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β π¦ β β€) |
22 | | fzval3 13647 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π¦ β β€ β
(0...π¦) = (0..^(π¦ + 1))) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β (0...π¦) = (0..^(π¦ + 1))) |
24 | 23 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β (0..^(π¦ + 1)) = (0...π¦)) |
25 | 24 | sumeq1d 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)) |
28 | 26, 27 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ β β β π¦ β
(β€β₯β0)) |
29 | 28 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β π¦ β
(β€β₯β0)) |
30 | | 2nn 12231 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 2 β
β |
31 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0...π¦)) β 2 β β) |
32 | | elfzelz 13447 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (0...π¦) β π β β€) |
33 | 32 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0...π¦)) β π β β€) |
34 | | nnnn0 12425 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β β π β
β0) |
35 | | nn0rp0 13378 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β0
β π β
(0[,)+β)) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β π β
(0[,)+β)) |
37 | 36 | ad4antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0...π¦)) β π β (0[,)+β)) |
38 | | digvalnn0 46771 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((2
β β β§ π
β β€ β§ π
β (0[,)+β)) β (π(digitβ2)π) β
β0) |
39 | 31, 33, 37, 38 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0...π¦)) β (π(digitβ2)π) β
β0) |
40 | 39 | nn0cnd 12480 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0...π¦)) β (π(digitβ2)π) β β) |
41 | | 2nn0 12435 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ 2 β
β0 |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (0...π¦) β 2 β
β0) |
43 | | elfznn0 13540 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (0...π¦) β π β β0) |
44 | 42, 43 | nn0expcld 14155 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (0...π¦) β (2βπ) β
β0) |
45 | 44 | nn0cnd 12480 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (0...π¦) β (2βπ) β β) |
46 | 45 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0...π¦)) β (2βπ) β β) |
47 | 40, 46 | mulcld 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)) |
50 | 48, 49 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = 0 β ((π(digitβ2)π) Β· (2βπ)) = ((0(digitβ2)π) Β· (2β0))) |
51 | | 2cn 12233 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 2 β
β |
52 | | exp0 13977 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (2 β
β β (2β0) = 1) |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(2β0) = 1 |
54 | 53 | oveq2i 7369 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((0(digitβ2)π)
Β· (2β0)) = ((0(digitβ2)π) Β· 1) |
55 | 50, 54 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = 0 β ((π(digitβ2)π) Β· (2βπ)) = ((0(digitβ2)π) Β· 1)) |
56 | 29, 47, 55 | fsum1p 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) |
58 | 34, 1, 57 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π / 2) β β β§ π β β) β
(0(digitβ2)π) =
0) |
59 | 58 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π / 2) β β β§ π β β) β
((0(digitβ2)π)
Β· 1) = (0 Β· 1)) |
60 | | 1re 11160 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ 1 β
β |
61 | | mul02lem2 11337 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (1 β
β β (0 Β· 1) = 0) |
62 | 60, 61 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (0
Β· 1) = 0 |
63 | 59, 62 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π / 2) β β β§ π β β) β
((0(digitβ2)π)
Β· 1) = 0) |
64 | 63 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π / 2) β β β§ π β β) β§
(#bβπ) =
(π¦ + 1)) β
((0(digitβ2)π)
Β· 1) = 0) |
65 | 64 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β
((0(digitβ2)π)
Β· 1) = 0) |
66 | | 1z 12538 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 1 β
β€ |
67 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β 1 β
β€) |
68 | | 0p1e1 12280 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (0 + 1) =
1 |
69 | 68, 66 | eqeltri 2830 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (0 + 1)
β β€ |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β (0 + 1) β
β€) |
71 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β ((0 + 1)...π¦)) β 2 β β) |
72 | | elfzelz 13447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β ((0 + 1)...π¦) β π β β€) |
73 | 72 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β ((0 + 1)...π¦)) β π β β€) |
74 | 36 | ad4antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β ((0 + 1)...π¦)) β π β (0[,)+β)) |
75 | 71, 73, 74, 38 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β ((0 + 1)...π¦)) β (π(digitβ2)π) β
β0) |
76 | 75 | nn0cnd 12480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β ((0 + 1)...π¦)) β (π(digitβ2)π) β β) |
77 | | 2cnd 12236 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β ((0 + 1)...π¦) β 2 β
β) |
78 | | elfznn 13476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (1...π¦) β π β β) |
79 | 78 | nnnn0d 12478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (1...π¦) β π β β0) |
80 | 68 | oveq1i 7368 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((0 +
1)...π¦) = (1...π¦) |
81 | 79, 80 | eleq2s 2852 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β ((0 + 1)...π¦) β π β β0) |
82 | 77, 81 | expcld 14057 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β ((0 + 1)...π¦) β (2βπ) β
β) |
83 | 82 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β ((0 + 1)...π¦)) β (2βπ) β β) |
84 | 76, 83 | mulcld 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))) |
87 | 85, 86 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (π + 1) β ((π(digitβ2)π) Β· (2βπ)) = (((π + 1)(digitβ2)π) Β· (2β(π + 1)))) |
88 | 67, 70, 21, 84, 87 | fsumshftm 15671 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β Ξ£π β ((0 + 1)...π¦)((π(digitβ2)π) Β· (2βπ)) = Ξ£π β (((0 + 1) β 1)...(π¦ β 1))(((π + 1)(digitβ2)π) Β· (2β(π + 1)))) |
89 | 65, 88 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β
(((0(digitβ2)π)
Β· 1) + Ξ£π
β ((0 + 1)...π¦)((π(digitβ2)π) Β· (2βπ))) = (0 + Ξ£π β (((0 + 1) β
1)...(π¦ β 1))(((π + 1)(digitβ2)π) Β· (2β(π + 1))))) |
90 | 1 | ad4antr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0..^π¦)) β (π / 2) β
β0) |
91 | 34 | ad4antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0..^π¦)) β π β β0) |
92 | | elfzonn0 13623 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (0..^π¦) β π β β0) |
93 | 92 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0..^π¦)) β π β β0) |
94 | | dignn0ehalf 46789 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π / 2) β β0
β§ π β
β0 β§ π
β β0) β ((π + 1)(digitβ2)π) = (π(digitβ2)(π / 2))) |
95 | 90, 91, 93, 94 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0..^π¦)) β ((π + 1)(digitβ2)π) = (π(digitβ2)(π / 2))) |
96 | | 2cnd 12236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (0..^π¦) β 2 β β) |
97 | 96, 92 | expp1d 14058 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (0..^π¦) β (2β(π + 1)) = ((2βπ) Β· 2)) |
98 | 97 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0..^π¦)) β (2β(π + 1)) = ((2βπ) Β· 2)) |
99 | 95, 98 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0..^π¦)) β (((π + 1)(digitβ2)π) Β· (2β(π + 1))) = ((π(digitβ2)(π / 2)) Β· ((2βπ) Β· 2))) |
100 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0..^π¦)) β 2 β β) |
101 | | elfzoelz 13578 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (0..^π¦) β π β β€) |
102 | 101 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0..^π¦)) β π β β€) |
103 | | nn0rp0 13378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π / 2) β β0
β (π / 2) β
(0[,)+β)) |
104 | 1, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π / 2) β β β
(π / 2) β
(0[,)+β)) |
105 | 104 | ad4antr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0..^π¦)) β (π / 2) β (0[,)+β)) |
106 | | digvalnn0 46771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((2
β β β§ π
β β€ β§ (π /
2) β (0[,)+β)) β (π(digitβ2)(π / 2)) β
β0) |
107 | 100, 102,
105, 106 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0..^π¦)) β (π(digitβ2)(π / 2)) β
β0) |
108 | 107 | nn0cnd 12480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0..^π¦)) β (π(digitβ2)(π / 2)) β β) |
109 | | 2re 12232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ 2 β
β |
110 | 109 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (0..^π¦) β 2 β β) |
111 | 110, 92 | reexpcld 14074 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (0..^π¦) β (2βπ) β β) |
112 | 111 | recnd 11188 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (0..^π¦) β (2βπ) β β) |
113 | 112 | adantl 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))) |
116 | 115 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π(digitβ2)(π / 2)) β β β§
(2βπ) β β
β§ 2 β β) β ((π(digitβ2)(π / 2)) Β· ((2βπ) Β· 2)) = (((π(digitβ2)(π / 2)) Β· (2βπ)) Β· 2)) |
117 | 108, 113,
114, 116 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0..^π¦)) β ((π(digitβ2)(π / 2)) Β· ((2βπ) Β· 2)) = (((π(digitβ2)(π / 2)) Β· (2βπ)) Β· 2)) |
118 | 99, 117 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0..^π¦)) β (((π + 1)(digitβ2)π) Β· (2β(π + 1))) = (((π(digitβ2)(π / 2)) Β· (2βπ)) Β· 2)) |
119 | 118 | sumeq2dv 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) |
122 | 120, 121 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((0 + 1)
β 1) = 0 |
123 | 122 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π¦ β β β ((0 + 1)
β 1) = 0) |
124 | 123 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π¦ β β β (((0 + 1)
β 1)...(π¦ β 1))
= (0...(π¦ β
1))) |
125 | | fzoval 13579 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π¦ β β€ β
(0..^π¦) = (0...(π¦ β 1))) |
126 | 125 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π¦ β β€ β
(0...(π¦ β 1)) =
(0..^π¦)) |
127 | 20, 126 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π¦ β β β
(0...(π¦ β 1)) =
(0..^π¦)) |
128 | 124, 127 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ β β β (((0 + 1)
β 1)...(π¦ β 1))
= (0..^π¦)) |
129 | 128 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β (((0 + 1) β
1)...(π¦ β 1)) =
(0..^π¦)) |
130 | 129 | sumeq1d 15591 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β Ξ£π β (((0 + 1) β
1)...(π¦ β 1))(((π + 1)(digitβ2)π) Β· (2β(π + 1))) = Ξ£π β (0..^π¦)(((π + 1)(digitβ2)π) Β· (2β(π + 1)))) |
131 | 130 | oveq2d 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 |
133 | 132 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β (0..^π¦) β Fin) |
134 | 101 | peano2zd 12615 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (0..^π¦) β (π + 1) β β€) |
135 | 134 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0..^π¦)) β (π + 1) β β€) |
136 | 36 | ad4antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0..^π¦)) β π β (0[,)+β)) |
137 | | digvalnn0 46771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((2
β β β§ (π +
1) β β€ β§ π
β (0[,)+β)) β ((π + 1)(digitβ2)π) β
β0) |
138 | 100, 135,
136, 137 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0..^π¦)) β ((π + 1)(digitβ2)π) β
β0) |
139 | 138 | nn0cnd 12480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0..^π¦)) β ((π + 1)(digitβ2)π) β β) |
140 | 41 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (0..^π¦) β 2 β
β0) |
141 | | peano2nn0 12458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β β0
β (π + 1) β
β0) |
142 | 92, 141 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (0..^π¦) β (π + 1) β
β0) |
143 | 140, 142 | nn0expcld 14155 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (0..^π¦) β (2β(π + 1)) β
β0) |
144 | 143 | nn0cnd 12480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (0..^π¦) β (2β(π + 1)) β β) |
145 | 144 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0..^π¦)) β (2β(π + 1)) β β) |
146 | 139, 145 | mulcld 11180 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0..^π¦)) β (((π + 1)(digitβ2)π) Β· (2β(π + 1))) β β) |
147 | 133, 146 | fsumcl 15623 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β Ξ£π β (0..^π¦)(((π + 1)(digitβ2)π) Β· (2β(π + 1))) β β) |
148 | 147 | addid2d 11361 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β (0 + Ξ£π β (0..^π¦)(((π + 1)(digitβ2)π) Β· (2β(π + 1)))) = Ξ£π β (0..^π¦)(((π + 1)(digitβ2)π) Β· (2β(π + 1)))) |
149 | 131, 148 | eqtrd 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 β
β) |
151 | 140, 92 | nn0expcld 14155 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (0..^π¦) β (2βπ) β
β0) |
152 | 151 | nn0cnd 12480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (0..^π¦) β (2βπ) β β) |
153 | 152 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0..^π¦)) β (2βπ) β β) |
154 | 108, 153 | mulcld 11180 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β§ π β (0..^π¦)) β ((π(digitβ2)(π / 2)) Β· (2βπ)) β β) |
155 | 133, 150,
154 | fsummulc1 15675 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β (Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ)) Β· 2) = Ξ£π β (0..^π¦)(((π(digitβ2)(π / 2)) Β· (2βπ)) Β· 2)) |
156 | 119, 149,
155 | 3eqtr4d 2783 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β (0 + Ξ£π β (((0 + 1) β
1)...(π¦ β 1))(((π + 1)(digitβ2)π) Β· (2β(π + 1)))) = (Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ)) Β· 2)) |
157 | 89, 156 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β
(((0(digitβ2)π)
Β· 1) + Ξ£π
β ((0 + 1)...π¦)((π(digitβ2)π) Β· (2βπ))) = (Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ)) Β· 2)) |
158 | 25, 56, 157 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ)) = (Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ)) Β· 2)) |
159 | 158 | adantl 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βπ)) |
162 | 160, 161 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π β ((π(digitβ2)(π / 2)) Β· (2βπ)) = ((π(digitβ2)(π / 2)) Β· (2βπ))) |
163 | 162 | cbvsumv 15586 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
Ξ£π β
(0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ)) = Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ)) |
164 | 163 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ)) = Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ))) |
165 | 164 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β ((π / 2) = Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ)) β (π / 2) = Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ)))) |
166 | 165 | biimpac 480 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π / 2) = Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ)) β§ ((((π / 2) β β β§ π β β) β§
(#bβπ) =
(π¦ + 1)) β§ π¦ β β)) β (π / 2) = Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ))) |
167 | 166 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π / 2) = Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ)) β§ ((((π / 2) β β β§ π β β) β§
(#bβπ) =
(π¦ + 1)) β§ π¦ β β)) β
Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ)) = (π / 2)) |
168 | 167 | oveq1d 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 |
172 | 171 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β 2 β
0) |
173 | 169, 170,
172 | divcan1d 11937 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β ((π / 2) Β· 2) = π) |
174 | 173 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β ((π / 2) Β· 2) = π) |
175 | 174 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π / 2) = Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ)) β§ ((((π / 2) β β β§ π β β) β§
(#bβπ) =
(π¦ + 1)) β§ π¦ β β)) β ((π / 2) Β· 2) = π) |
176 | 159, 168,
175 | 3eqtrrd 2778 |
. . . . . . . . . . . . . . . . 17
β’ (((π / 2) = Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ)) β§ ((((π / 2) β β β§ π β β) β§
(#bβπ) =
(π¦ + 1)) β§ π¦ β β)) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))) |
177 | 176 | ex 414 |
. . . . . . . . . . . . . . . 16
β’ ((π / 2) = Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ)) β (((((π / 2) β β β§ π β β) β§
(#bβπ) =
(π¦ + 1)) β§ π¦ β β) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ)))) |
178 | 177 | imim2i 16 |
. . . . . . . . . . . . . . 15
β’
(((#bβ(π / 2)) = π¦ β (π / 2) = Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ))) β ((#bβ(π / 2)) = π¦ β (((((π / 2) β β β§ π β β) β§
(#bβπ) =
(π¦ + 1)) β§ π¦ β β) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))) |
179 | 178 | com13 88 |
. . . . . . . . . . . . . 14
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β
((#bβ(π /
2)) = π¦ β
(((#bβ(π /
2)) = π¦ β (π / 2) = Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ))) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))) |
180 | 19, 179 | sylbid 239 |
. . . . . . . . . . . . 13
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β
((#bβ(π /
2)) = ((#bβπ) β 1) β
(((#bβ(π /
2)) = π¦ β (π / 2) = Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ))) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))) |
181 | 180 | com23 86 |
. . . . . . . . . . . 12
β’
(((((π / 2) β
β β§ π β
β) β§ (#bβπ) = (π¦ + 1)) β§ π¦ β β) β
(((#bβ(π /
2)) = π¦ β (π / 2) = Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ))) β ((#bβ(π / 2)) =
((#bβπ)
β 1) β π =
Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))) |
182 | 181 | exp31 421 |
. . . . . . . . . . 11
β’ (((π / 2) β β β§ π β β) β
((#bβπ) =
(π¦ + 1) β (π¦ β β β
(((#bβ(π /
2)) = π¦ β (π / 2) = Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ))) β ((#bβ(π / 2)) =
((#bβπ)
β 1) β π =
Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))))) |
183 | 182 | com25 99 |
. . . . . . . . . 10
β’ (((π / 2) β β β§ π β β) β
((#bβ(π /
2)) = ((#bβπ) β 1) β (π¦ β β β
(((#bβ(π /
2)) = π¦ β (π / 2) = Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))))) |
184 | 183 | com14 96 |
. . . . . . . . 9
β’
(((#bβ(π / 2)) = π¦ β (π / 2) = Ξ£π β (0..^π¦)((π(digitβ2)(π / 2)) Β· (2βπ))) β ((#bβ(π / 2)) =
((#bβπ)
β 1) β (π¦ β
β β (((π / 2)
β β β§ π
β β) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))))) |
185 | 12, 184 | syl 17 |
. . . . . . . 8
β’ (((π / 2) β β0
β§ βπ₯ β
β0 ((#bβπ₯) = π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ)))) β ((#bβ(π / 2)) =
((#bβπ)
β 1) β (π¦ β
β β (((π / 2)
β β β§ π
β β) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))))) |
186 | 185 | ex 414 |
. . . . . . 7
β’ ((π / 2) β β0
β (βπ₯ β
β0 ((#bβπ₯) = π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))) β ((#bβ(π / 2)) =
((#bβπ)
β 1) β (π¦ β
β β (((π / 2)
β β β§ π
β β) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ)))))))) |
187 | 186 | com25 99 |
. . . . . 6
β’ ((π / 2) β β0
β (((π / 2) β
β β§ π β
β) β ((#bβ(π / 2)) = ((#bβπ) β 1) β (π¦ β β β
(βπ₯ β
β0 ((#bβπ₯) = π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ)))))))) |
188 | 187 | expdcom 416 |
. . . . 5
β’ ((π / 2) β β β
(π β β β
((π / 2) β
β0 β ((#bβ(π / 2)) = ((#bβπ) β 1) β (π¦ β β β
(βπ₯ β
β0 ((#bβπ₯) = π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))))))) |
189 | 1, 188 | mpid 44 |
. . . 4
β’ ((π / 2) β β β
(π β β β
((#bβ(π /
2)) = ((#bβπ) β 1) β (π¦ β β β (βπ₯ β β0
((#bβπ₯) =
π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ)))))))) |
190 | 189 | impcom 409 |
. . 3
β’ ((π β β β§ (π / 2) β β) β
((#bβ(π /
2)) = ((#bβπ) β 1) β (π¦ β β β (βπ₯ β β0
((#bβπ₯) =
π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))))) |
191 | 3, 190 | mpd 15 |
. 2
β’ ((π β β β§ (π / 2) β β) β
(π¦ β β β
(βπ₯ β
β0 ((#bβπ₯) = π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ)))))) |
192 | 191 | imp 408 |
1
β’ (((π β β β§ (π / 2) β β) β§
π¦ β β) β
(βπ₯ β
β0 ((#bβπ₯) = π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))) |