Step | Hyp | Ref
| Expression |
1 | | elnn1uz2 12851 |
. . 3
β’ (π β β β (π = 1 β¨ π β
(β€β₯β2))) |
2 | | 1t1e1 12316 |
. . . . . . . . 9
β’ (1
Β· 1) = 1 |
3 | 2 | eqcomi 2746 |
. . . . . . . 8
β’ 1 = (1
Β· 1) |
4 | | simpl 484 |
. . . . . . . 8
β’ ((π = 1 β§
(#bβπ) =
(π¦ + 1)) β π = 1) |
5 | | oveq2 7366 |
. . . . . . . . . . . 12
β’ ((π¦ + 1) =
(#bβπ)
β (0..^(π¦ + 1)) =
(0..^(#bβπ))) |
6 | 5 | eqcoms 2745 |
. . . . . . . . . . 11
β’
((#bβπ) = (π¦ + 1) β (0..^(π¦ + 1)) = (0..^(#bβπ))) |
7 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π = 1 β
(#bβπ) =
(#bβ1)) |
8 | | blen1 46677 |
. . . . . . . . . . . . . 14
β’
(#bβ1) = 1 |
9 | 7, 8 | eqtrdi 2793 |
. . . . . . . . . . . . 13
β’ (π = 1 β
(#bβπ) =
1) |
10 | 9 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (π = 1 β
(0..^(#bβπ)) = (0..^1)) |
11 | | fzo01 13655 |
. . . . . . . . . . . 12
β’ (0..^1) =
{0} |
12 | 10, 11 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ (π = 1 β
(0..^(#bβπ)) = {0}) |
13 | 6, 12 | sylan9eqr 2799 |
. . . . . . . . . 10
β’ ((π = 1 β§
(#bβπ) =
(π¦ + 1)) β (0..^(π¦ + 1)) = {0}) |
14 | 13 | sumeq1d 15587 |
. . . . . . . . 9
β’ ((π = 1 β§
(#bβπ) =
(π¦ + 1)) β
Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ)) = Ξ£π β {0} ((π(digitβ2)π) Β· (2βπ))) |
15 | | oveq2 7366 |
. . . . . . . . . . . . 13
β’ (π = 1 β (π(digitβ2)π) = (π(digitβ2)1)) |
16 | 15 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ (π = 1 β ((π(digitβ2)π) Β· (2βπ)) = ((π(digitβ2)1) Β· (2βπ))) |
17 | 16 | sumeq2sdv 15590 |
. . . . . . . . . . 11
β’ (π = 1 β Ξ£π β {0} ((π(digitβ2)π) Β· (2βπ)) = Ξ£π β {0} ((π(digitβ2)1) Β· (2βπ))) |
18 | | c0ex 11150 |
. . . . . . . . . . . 12
β’ 0 β
V |
19 | | ax-1cn 11110 |
. . . . . . . . . . . . 13
β’ 1 β
β |
20 | 19, 19 | mulcli 11163 |
. . . . . . . . . . . 12
β’ (1
Β· 1) β β |
21 | | oveq1 7365 |
. . . . . . . . . . . . . . 15
β’ (π = 0 β (π(digitβ2)1) =
(0(digitβ2)1)) |
22 | | 1ex 11152 |
. . . . . . . . . . . . . . . . 17
β’ 1 β
V |
23 | 22 | prid2 4725 |
. . . . . . . . . . . . . . . 16
β’ 1 β
{0, 1} |
24 | | 0dig2pr01 46703 |
. . . . . . . . . . . . . . . 16
β’ (1 β
{0, 1} β (0(digitβ2)1) = 1) |
25 | 23, 24 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’
(0(digitβ2)1) = 1 |
26 | 21, 25 | eqtrdi 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) |
30 | 28, 29 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’
(2β0) = 1 |
31 | 27, 30 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
β’ (π = 0 β (2βπ) = 1) |
32 | 26, 31 | oveq12d 7376 |
. . . . . . . . . . . . 13
β’ (π = 0 β ((π(digitβ2)1) Β· (2βπ)) = (1 Β·
1)) |
33 | 32 | sumsn 15632 |
. . . . . . . . . . . 12
β’ ((0
β V β§ (1 Β· 1) β β) β Ξ£π β {0} ((π(digitβ2)1) Β· (2βπ)) = (1 Β·
1)) |
34 | 18, 20, 33 | mp2an 691 |
. . . . . . . . . . 11
β’
Ξ£π β {0}
((π(digitβ2)1)
Β· (2βπ)) = (1
Β· 1) |
35 | 17, 34 | eqtrdi 2793 |
. . . . . . . . . 10
β’ (π = 1 β Ξ£π β {0} ((π(digitβ2)π) Β· (2βπ)) = (1 Β· 1)) |
36 | 35 | adantr 482 |
. . . . . . . . 9
β’ ((π = 1 β§
(#bβπ) =
(π¦ + 1)) β
Ξ£π β {0} ((π(digitβ2)π) Β· (2βπ)) = (1 Β·
1)) |
37 | 14, 36 | eqtrd 2777 |
. . . . . . . 8
β’ ((π = 1 β§
(#bβπ) =
(π¦ + 1)) β
Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ)) = (1 Β· 1)) |
38 | 3, 4, 37 | 3eqtr4a 2803 |
. . . . . . 7
β’ ((π = 1 β§
(#bβπ) =
(π¦ + 1)) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))) |
39 | 38 | ex 414 |
. . . . . 6
β’ (π = 1 β
((#bβπ) =
(π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ)))) |
40 | 39 | a1d 25 |
. . . . 5
β’ (π = 1 β (βπ₯ β β0
((#bβπ₯) =
π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))) |
41 | 40 | 2a1d 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)) |
44 | 43 | bicomd 222 |
. . . . . . . . 9
β’ (π β β0
β (((π β 1) / 2)
β β0 β ((π + 1) / 2) β
β0)) |
45 | 42, 44 | syl 17 |
. . . . . . . 8
β’ (π β
(β€β₯β2) β (((π β 1) / 2) β β0
β ((π + 1) / 2) β
β0)) |
46 | | blennngt2o2 46685 |
. . . . . . . . 9
β’ ((π β
(β€β₯β2) β§ ((π + 1) / 2) β β0) β
(#bβπ) =
((#bβ((π
β 1) / 2)) + 1)) |
47 | 46 | ex 414 |
. . . . . . . 8
β’ (π β
(β€β₯β2) β (((π + 1) / 2) β β0 β
(#bβπ) =
((#bβ((π
β 1) / 2)) + 1))) |
48 | 45, 47 | sylbid 239 |
. . . . . . 7
β’ (π β
(β€β₯β2) β (((π β 1) / 2) β β0
β (#bβπ) = ((#bβ((π β 1) / 2)) +
1))) |
49 | 48 | imp 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))) |
53 | 52 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
β’ (π₯ = ((π β 1) / 2) β ((π(digitβ2)π₯) Β· (2βπ)) = ((π(digitβ2)((π β 1) / 2)) Β· (2βπ))) |
54 | 53 | sumeq2sdv 15590 |
. . . . . . . . . . . . . 14
β’ (π₯ = ((π β 1) / 2) β Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ)) = Ξ£π β (0..^π¦)((π(digitβ2)((π β 1) / 2)) Β· (2βπ))) |
55 | 51, 54 | eqeq12d 2753 |
. . . . . . . . . . . . 13
β’ (π₯ = ((π β 1) / 2) β (π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ)) β ((π β 1) / 2) = Ξ£π β (0..^π¦)((π(digitβ2)((π β 1) / 2)) Β· (2βπ)))) |
56 | 50, 55 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π₯ = ((π β 1) / 2) β
(((#bβπ₯) =
π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))) β ((#bβ((π β 1) / 2)) = π¦ β ((π β 1) / 2) = Ξ£π β (0..^π¦)((π(digitβ2)((π β 1) / 2)) Β· (2βπ))))) |
57 | 56 | rspcva 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
β’ (π¦ β β β π¦ β
β) |
60 | 59 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β π¦ β β) |
61 | | blennn0elnn 46670 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β 1) / 2) β
β0 β (#bβ((π β 1) / 2)) β
β) |
62 | 61 | nncnd 12170 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β 1) / 2) β
β0 β (#bβ((π β 1) / 2)) β
β) |
63 | 62 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β (#bβ((π β 1) / 2)) β
β) |
64 | 63 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β
(#bβ((π
β 1) / 2)) β β) |
65 | | 1cnd 11151 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β 1 β
β) |
66 | 60, 64, 65 | addcan2d 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
β’ (π¦ β β β π¦ β
β€) |
69 | 68 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β π¦ β β€) |
70 | | fzval3 13642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π¦ β β€ β
(0...π¦) = (0..^(π¦ + 1))) |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β (0...π¦) = (0..^(π¦ + 1))) |
72 | 71 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β (0..^(π¦ + 1)) = (0...π¦)) |
73 | 72 | sumeq1d 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)) |
76 | 74, 75 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π¦ β β β π¦ β
(β€β₯β0)) |
77 | 76 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β π¦ β
(β€β₯β0)) |
78 | | 2nn 12227 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ 2 β
β |
79 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((((π β 1) /
2) β β0 β§ π β (β€β₯β2))
β§ π β (0...π¦)) β 2 β
β) |
80 | | elfzelz 13442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β (0...π¦) β π β β€) |
81 | 80 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((((π β 1) /
2) β β0 β§ π β (β€β₯β2))
β§ π β (0...π¦)) β π β β€) |
82 | | nn0rp0 13373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β β0
β π β
(0[,)+β)) |
83 | 42, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β
(β€β₯β2) β π β (0[,)+β)) |
84 | 83 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β π β (0[,)+β)) |
85 | 84 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((((π β 1) /
2) β β0 β§ π β (β€β₯β2))
β§ π β (0...π¦)) β π β (0[,)+β)) |
86 | | digvalnn0 46692 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((2
β β β§ π
β β€ β§ π
β (0[,)+β)) β (π(digitβ2)π) β
β0) |
87 | 79, 81, 85, 86 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(((((π β 1) /
2) β β0 β§ π β (β€β₯β2))
β§ π β (0...π¦)) β (π(digitβ2)π) β
β0) |
88 | 87 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β (π β (0...π¦) β (π(digitβ2)π) β
β0)) |
89 | 88 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β (π β (0...π¦) β (π(digitβ2)π) β
β0)) |
90 | 89 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β§ π β (0...π¦)) β (π(digitβ2)π) β
β0) |
91 | 90 | nn0cnd 12476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β§ π β (0...π¦)) β (π(digitβ2)π) β β) |
92 | | 2nn0 12431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ 2 β
β0 |
93 | 92 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β (0...π¦) β 2 β
β0) |
94 | | elfznn0 13535 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β (0...π¦) β π β β0) |
95 | 93, 94 | nn0expcld 14150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β (0...π¦) β (2βπ) β
β0) |
96 | 95 | nn0cnd 12476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (0...π¦) β (2βπ) β β) |
97 | 96 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β§ π β (0...π¦)) β (2βπ) β β) |
98 | 91, 97 | mulcld 11176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β§ π β (0...π¦)) β ((π(digitβ2)π) Β· (2βπ)) β β) |
99 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = 0 β (π(digitβ2)π) = (0(digitβ2)π)) |
100 | 99, 27 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = 0 β ((π(digitβ2)π) Β· (2βπ)) = ((0(digitβ2)π) Β· (2β0))) |
101 | 30 | oveq2i 7369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((0(digitβ2)π)
Β· (2β0)) = ((0(digitβ2)π) Β· 1) |
102 | 100, 101 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = 0 β ((π(digitβ2)π) Β· (2βπ)) = ((0(digitβ2)π) Β· 1)) |
103 | 77, 98, 102 | fsum1p 15639 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β Ξ£π β (0...π¦)((π(digitβ2)π) Β· (2βπ)) = (((0(digitβ2)π) Β· 1) + Ξ£π β ((0 + 1)...π¦)((π(digitβ2)π) Β· (2βπ)))) |
104 | 42 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β π β β0) |
105 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β
(β€β₯β2) β (((π + 1) / 2) β β0 β
((π β 1) / 2) β
β0)) |
106 | 105 | biimparc 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β ((π + 1) / 2) β
β0) |
107 | | 0dig2nn0o 46706 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β (0(digitβ2)π) = 1) |
108 | 104, 106,
107 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β (0(digitβ2)π) = 1) |
109 | 108 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β
(0(digitβ2)π) =
1) |
110 | 109 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β
((0(digitβ2)π)
Β· 1) = (1 Β· 1)) |
111 | 110, 2 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β
((0(digitβ2)π)
Β· 1) = 1) |
112 | | 1z 12534 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ 1 β
β€ |
113 | 112 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β 1 β
β€) |
114 | | 0p1e1 12276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (0 + 1) =
1 |
115 | 114, 112 | eqeltri 2834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (0 + 1)
β β€ |
116 | 115 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β (0 + 1) β
β€) |
117 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β
(β€β₯β2) β§ π β ((0 + 1)...π¦)) β 2 β β) |
118 | | elfzelz 13442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β ((0 + 1)...π¦) β π β β€) |
119 | 118 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β
(β€β₯β2) β§ π β ((0 + 1)...π¦)) β π β β€) |
120 | 42 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π β
(β€β₯β2) β§ π β ((0 + 1)...π¦)) β π β β0) |
121 | 120, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β
(β€β₯β2) β§ π β ((0 + 1)...π¦)) β π β (0[,)+β)) |
122 | 117, 119,
121, 86 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β
(β€β₯β2) β§ π β ((0 + 1)...π¦)) β (π(digitβ2)π) β
β0) |
123 | 122 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β
(β€β₯β2) β (π β ((0 + 1)...π¦) β (π(digitβ2)π) β
β0)) |
124 | 123 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β (π β ((0 + 1)...π¦) β (π(digitβ2)π) β
β0)) |
125 | 124 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β (π β ((0 + 1)...π¦) β (π(digitβ2)π) β
β0)) |
126 | 125 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β§ π β ((0 + 1)...π¦)) β (π(digitβ2)π) β
β0) |
127 | 126 | nn0cnd 12476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β§ π β ((0 + 1)...π¦)) β (π(digitβ2)π) β β) |
128 | | 2cnd 12232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β ((0 + 1)...π¦) β 2 β
β) |
129 | | elfznn 13471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β (1...π¦) β π β β) |
130 | 129 | nnnn0d 12474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β (1...π¦) β π β β0) |
131 | 114 | oveq1i 7368 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((0 +
1)...π¦) = (1...π¦) |
132 | 130, 131 | eleq2s 2856 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β ((0 + 1)...π¦) β π β β0) |
133 | 128, 132 | expcld 14052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β ((0 + 1)...π¦) β (2βπ) β
β) |
134 | 133 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β§ π β ((0 + 1)...π¦)) β (2βπ) β β) |
135 | 127, 134 | mulcld 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))) |
138 | 136, 137 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = (π + 1) β ((π(digitβ2)π) Β· (2βπ)) = (((π + 1)(digitβ2)π) Β· (2β(π + 1)))) |
139 | 113, 116,
69, 135, 138 | fsumshftm 15667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β Ξ£π β ((0 + 1)...π¦)((π(digitβ2)π) Β· (2βπ)) = Ξ£π β (((0 + 1) β 1)...(π¦ β 1))(((π + 1)(digitβ2)π) Β· (2β(π + 1)))) |
140 | 111, 139 | oveq12d 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))))) |
141 | 73, 103, 140 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ)) = (1 + Ξ£π β (((0 + 1) β 1)...(π¦ β 1))(((π + 1)(digitβ2)π) Β· (2β(π + 1))))) |
142 | 141 | adantl 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))))) |
143 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
(((((π β 1) /
2) β β0 β§ π β (β€β₯β2))
β§ π β (0..^π¦)) β 2 β
β) |
144 | | elfzoelz 13573 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β (0..^π¦) β π β β€) |
145 | 144 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
(((((π β 1) /
2) β β0 β§ π β (β€β₯β2))
β§ π β (0..^π¦)) β π β β€) |
146 | | nn0rp0 13373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (((π β 1) / 2) β
β0 β ((π β 1) / 2) β
(0[,)+β)) |
147 | 146 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β ((π β 1) / 2) β
(0[,)+β)) |
148 | 147 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
(((((π β 1) /
2) β β0 β§ π β (β€β₯β2))
β§ π β (0..^π¦)) β ((π β 1) / 2) β
(0[,)+β)) |
149 | | digvalnn0 46692 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((2
β β β§ π
β β€ β§ ((π
β 1) / 2) β (0[,)+β)) β (π(digitβ2)((π β 1) / 2)) β
β0) |
150 | 143, 145,
148, 149 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
(((((π β 1) /
2) β β0 β§ π β (β€β₯β2))
β§ π β (0..^π¦)) β (π(digitβ2)((π β 1) / 2)) β
β0) |
151 | 150 | nn0cnd 12476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((((π β 1) /
2) β β0 β§ π β (β€β₯β2))
β§ π β (0..^π¦)) β (π(digitβ2)((π β 1) / 2)) β
β) |
152 | 151 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β (π β (0..^π¦) β (π(digitβ2)((π β 1) / 2)) β
β)) |
153 | 152 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β (π β (0..^π¦) β (π(digitβ2)((π β 1) / 2)) β
β)) |
154 | 153 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β§ π β (0..^π¦)) β (π(digitβ2)((π β 1) / 2)) β
β) |
155 | 92 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β (0..^π¦) β 2 β
β0) |
156 | | elfzonn0 13618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β (0..^π¦) β π β β0) |
157 | 155, 156 | nn0expcld 14150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β (0..^π¦) β (2βπ) β
β0) |
158 | 157 | nn0cnd 12476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β (0..^π¦) β (2βπ) β β) |
159 | 158 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β§ π β (0..^π¦)) β (2βπ) β β) |
160 | | 2cnd 12232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β§ π β (0..^π¦)) β 2 β β) |
161 | 154, 159,
160 | mulassd 11179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β§ π β (0..^π¦)) β (((π(digitβ2)((π β 1) / 2)) Β· (2βπ)) Β· 2) = ((π(digitβ2)((π β 1) / 2)) Β·
((2βπ) Β·
2))) |
162 | 161 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β§ π β (0..^π¦)) β ((π(digitβ2)((π β 1) / 2)) Β· ((2βπ) Β· 2)) = (((π(digitβ2)((π β 1) / 2)) Β·
(2βπ)) Β·
2)) |
163 | 162 | sumeq2dv 15589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β Ξ£π β (0..^π¦)((π(digitβ2)((π β 1) / 2)) Β· ((2βπ) Β· 2)) = Ξ£π β (0..^π¦)(((π(digitβ2)((π β 1) / 2)) Β· (2βπ)) Β· 2)) |
164 | 163 | adantl 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) |
167 | 165, 166 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((0 + 1)
β 1) = 0 |
168 | 167 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π¦ β β β ((0 + 1)
β 1) = 0) |
169 | 168 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π¦ β β β (((0 + 1)
β 1)...(π¦ β 1))
= (0...(π¦ β
1))) |
170 | | fzoval 13574 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π¦ β β€ β
(0..^π¦) = (0...(π¦ β 1))) |
171 | 68, 170 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π¦ β β β
(0..^π¦) = (0...(π¦ β 1))) |
172 | 169, 171 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π¦ β β β (((0 + 1)
β 1)...(π¦ β 1))
= (0..^π¦)) |
173 | 172 | ad2antll 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) |
176 | 167 | oveq1i 7368 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((0 + 1)
β 1)...(π¦ β 1))
= (0...(π¦ β
1)) |
177 | 175, 176 | eleq2s 2856 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β (((0 + 1) β
1)...(π¦ β 1)) β
π β
β0) |
178 | | dignn0flhalf 46711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β
(β€β₯β2) β§ π β β0) β ((π + 1)(digitβ2)π) = (π(digitβ2)(ββ(π / 2)))) |
179 | 174, 177,
178 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β§ π β (((0 + 1) β 1)...(π¦ β 1))) β ((π + 1)(digitβ2)π) = (π(digitβ2)(ββ(π / 2)))) |
180 | | eluzelz 12774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π β
(β€β₯β2) β π β β€) |
181 | 180 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π β
(β€β₯β2) β§ ((π β 1) / 2) β β0)
β π β
β€) |
182 | | nn0z 12525 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (((π β 1) / 2) β
β0 β ((π β 1) / 2) β
β€) |
183 | | zob 16242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π β β€ β (((π + 1) / 2) β β€ β
((π β 1) / 2) β
β€)) |
184 | 180, 183 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π β
(β€β₯β2) β (((π + 1) / 2) β β€ β ((π β 1) / 2) β
β€)) |
185 | 182, 184 | syl5ibr 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π β
(β€β₯β2) β (((π β 1) / 2) β β0
β ((π + 1) / 2) β
β€)) |
186 | 185 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π β
(β€β₯β2) β§ ((π β 1) / 2) β β0)
β ((π + 1) / 2) β
β€) |
187 | 181, 186 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β
(β€β₯β2) β§ ((π β 1) / 2) β β0)
β (π β β€
β§ ((π + 1) / 2) β
β€)) |
188 | 187 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β (π β β€ β§ ((π + 1) / 2) β β€)) |
189 | 188 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β (π β β€ β§ ((π + 1) / 2) β β€)) |
190 | 189 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
((((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β§ π β (((0 + 1) β 1)...(π¦ β 1))) β (π β β€ β§ ((π + 1) / 2) β
β€)) |
191 | | zofldiv2 46624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β β€ β§ ((π + 1) / 2) β β€)
β (ββ(π /
2)) = ((π β 1) /
2)) |
192 | 190, 191 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
((((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β§ π β (((0 + 1) β 1)...(π¦ β 1))) β
(ββ(π / 2)) =
((π β 1) /
2)) |
193 | 192 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β§ π β (((0 + 1) β 1)...(π¦ β 1))) β (π(digitβ2)(ββ(π / 2))) = (π(digitβ2)((π β 1) / 2))) |
194 | 179, 193 | eqtrd 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 β β) |
196 | 195, 177 | expp1d 14053 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β (((0 + 1) β
1)...(π¦ β 1)) β
(2β(π + 1)) =
((2βπ) Β·
2)) |
197 | 196 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β§ π β (((0 + 1) β 1)...(π¦ β 1))) β
(2β(π + 1)) =
((2βπ) Β·
2)) |
198 | 194, 197 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β§ π β (((0 + 1) β 1)...(π¦ β 1))) β (((π + 1)(digitβ2)π) Β· (2β(π + 1))) = ((π(digitβ2)((π β 1) / 2)) Β· ((2βπ) Β· 2))) |
199 | 173, 198 | sumeq12dv 15592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((#bβπ) = (π¦ + 1) β§ ((((π β 1) / 2) β β0
β§ π β
(β€β₯β2)) β§ π¦ β β)) β Ξ£π β (((0 + 1) β
1)...(π¦ β 1))(((π + 1)(digitβ2)π) Β· (2β(π + 1))) = Ξ£π β (0..^π¦)((π(digitβ2)((π β 1) / 2)) Β· ((2βπ) Β· 2))) |
200 | 199 | adantl 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βπ)) |
203 | 201, 202 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π = π β ((π(digitβ2)((π β 1) / 2)) Β· (2βπ)) = ((π(digitβ2)((π β 1) / 2)) Β· (2βπ))) |
204 | 203 | cbvsumv 15582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
Ξ£π β
(0..^π¦)((π(digitβ2)((π β 1) / 2)) Β· (2βπ)) = Ξ£π β (0..^π¦)((π(digitβ2)((π β 1) / 2)) Β· (2βπ)) |
205 | 204 | eqeq2i 2750 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β 1) / 2) = Ξ£π β (0..^π¦)((π(digitβ2)((π β 1) / 2)) Β· (2βπ)) β ((π β 1) / 2) = Ξ£π β (0..^π¦)((π(digitβ2)((π β 1) / 2)) Β· (2βπ))) |
206 | 205 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β 1) / 2) = Ξ£π β (0..^π¦)((π(digitβ2)((π β 1) / 2)) Β· (2βπ)) β ((π β 1) / 2) = Ξ£π β (0..^π¦)((π(digitβ2)((π β 1) / 2)) Β· (2βπ))) |
207 | 206 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β 1) / 2) = Ξ£π β (0..^π¦)((π(digitβ2)((π β 1) / 2)) Β· (2βπ)) β§
((#bβπ) =
(π¦ + 1) β§ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β§ π¦ β β))) β ((π β 1) / 2) = Ξ£π β (0..^π¦)((π(digitβ2)((π β 1) / 2)) Β· (2βπ))) |
208 | 207 | oveq1d 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 |
210 | 209 | a1i 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 β
β) |
212 | 158 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((((π β 1) /
2) β β0 β§ π β (β€β₯β2))
β§ π β (0..^π¦)) β (2βπ) β
β) |
213 | 151, 212 | mulcld 11176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(((((π β 1) /
2) β β0 β§ π β (β€β₯β2))
β§ π β (0..^π¦)) β ((π(digitβ2)((π β 1) / 2)) Β· (2βπ)) β
β) |
214 | 213 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β (π β (0..^π¦) β ((π(digitβ2)((π β 1) / 2)) Β· (2βπ)) β
β)) |
215 | 214 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((π β 1) /
2) β β0 β§ π β (β€β₯β2))
β§ π¦ β β)
β (π β (0..^π¦) β ((π(digitβ2)((π β 1) / 2)) Β· (2βπ)) β
β)) |
216 | 215 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β 1) / 2) = Ξ£π β (0..^π¦)((π(digitβ2)((π β 1) / 2)) Β· (2βπ)) β§
((#bβπ) =
(π¦ + 1) β§ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β§ π¦ β β))) β (π β (0..^π¦) β ((π(digitβ2)((π β 1) / 2)) Β· (2βπ)) β
β)) |
217 | 216 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((((π β 1) /
2) = Ξ£π β
(0..^π¦)((π(digitβ2)((π β 1) / 2)) Β· (2βπ)) β§
((#bβπ) =
(π¦ + 1) β§ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β§ π¦ β β))) β§ π β (0..^π¦)) β ((π(digitβ2)((π β 1) / 2)) Β· (2βπ)) β
β) |
218 | 210, 211,
217 | fsummulc1 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)) |
219 | 208, 218 | eqtrd 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)) |
220 | 164, 200,
219 | 3eqtr4d 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)) |
221 | 220 | oveq2d 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) β
β) |
224 | 222, 223 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β
(β€β₯β2) β (π β 1) β β) |
225 | | 2cnd 12232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β
(β€β₯β2) β 2 β β) |
226 | | 2ne0 12258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ 2 β
0 |
227 | 226 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β
(β€β₯β2) β 2 β 0) |
228 | 224, 225,
227 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β
(β€β₯β2) β ((π β 1) β β β§ 2 β
β β§ 2 β 0)) |
229 | 228 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β ((π β 1) β β β§ 2 β
β β§ 2 β 0)) |
230 | | divcan1 11823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β 1) β β β§
2 β β β§ 2 β 0) β (((π β 1) / 2) Β· 2) = (π β 1)) |
231 | 229, 230 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β (((π β 1) / 2) Β· 2) = (π β 1)) |
232 | 231 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β (1 + (((π β 1) / 2) Β· 2)) = (1 + (π β 1))) |
233 | | 1cnd 11151 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β
(β€β₯β2) β 1 β β) |
234 | 233, 222 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β
(β€β₯β2) β (1 β β β§ π β
β)) |
235 | 234 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β (1 β β β§ π β
β)) |
236 | | pncan3 11410 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((1
β β β§ π
β β) β (1 + (π β 1)) = π) |
237 | 235, 236 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β (1 + (π β 1)) = π) |
238 | 232, 237 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β (1 + (((π β 1) / 2) Β· 2)) = π) |
239 | 238 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β 1) /
2) β β0 β§ π β (β€β₯β2))
β§ π¦ β β)
β (1 + (((π β 1)
/ 2) Β· 2)) = π) |
240 | 239 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β 1) / 2) = Ξ£π β (0..^π¦)((π(digitβ2)((π β 1) / 2)) Β· (2βπ)) β§
((#bβπ) =
(π¦ + 1) β§ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β§ π¦ β β))) β (1 + (((π β 1) / 2) Β· 2)) =
π) |
241 | 142, 221,
240 | 3eqtrrd 2782 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β 1) / 2) = Ξ£π β (0..^π¦)((π(digitβ2)((π β 1) / 2)) Β· (2βπ)) β§
((#bβπ) =
(π¦ + 1) β§ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β§ π¦ β β))) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))) |
242 | 241 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β 1) / 2) = Ξ£π β (0..^π¦)((π(digitβ2)((π β 1) / 2)) Β· (2βπ)) β
(((#bβπ) =
(π¦ + 1) β§ ((((π β 1) / 2) β
β0 β§ π
β (β€β₯β2)) β§ π¦ β β)) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ)))) |
243 | 242 | imim2i 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βπ))))) |
244 | 243 | com13 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βπ))))) |
245 | 67, 244 | biimtrid 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βπ))))) |
246 | 66, 245 | sylbid 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βπ))))) |
247 | 246 | ex 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βπ)))))) |
248 | 247 | com23 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βπ)))))) |
249 | 58, 248 | sylbid 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βπ)))))) |
250 | 249 | com23 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βπ)))))) |
251 | 250 | com14 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βπ)))))) |
252 | 251 | exp4c 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βπ)))))))) |
253 | 252 | com35 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βπ)))))))) |
254 | 57, 253 | syl 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βπ)))))))) |
255 | 254 | ex 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βπ))))))))) |
256 | 255 | pm2.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βπ)))))))) |
257 | 256 | com25 99 |
. . . . . . 7
β’ (((π β 1) / 2) β
β0 β (π β (β€β₯β2)
β ((#bβπ) = ((#bβ((π β 1) / 2)) + 1) β
(π¦ β β β
(βπ₯ β
β0 ((#bβπ₯) = π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ)))))))) |
258 | 257 | impcom 409 |
. . . . . 6
β’ ((π β
(β€β₯β2) β§ ((π β 1) / 2) β β0)
β ((#bβπ) = ((#bβ((π β 1) / 2)) + 1) β
(π¦ β β β
(βπ₯ β
β0 ((#bβπ₯) = π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))))) |
259 | 49, 258 | mpd 15 |
. . . . 5
β’ ((π β
(β€β₯β2) β§ ((π β 1) / 2) β β0)
β (π¦ β β
β (βπ₯ β
β0 ((#bβπ₯) = π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ)))))) |
260 | 259 | ex 414 |
. . . 4
β’ (π β
(β€β₯β2) β (((π β 1) / 2) β β0
β (π¦ β β
β (βπ₯ β
β0 ((#bβπ₯) = π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))))) |
261 | 41, 260 | jaoi 856 |
. . 3
β’ ((π = 1 β¨ π β (β€β₯β2))
β (((π β 1) / 2)
β β0 β (π¦ β β β (βπ₯ β β0
((#bβπ₯) =
π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))))) |
262 | 1, 261 | sylbi 216 |
. 2
β’ (π β β β (((π β 1) / 2) β
β0 β (π¦ β β β (βπ₯ β β0
((#bβπ₯) =
π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))))) |
263 | 262 | imp31 419 |
1
β’ (((π β β β§ ((π β 1) / 2) β
β0) β§ π¦ β β) β (βπ₯ β β0
((#bβπ₯) =
π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))) |