Step | Hyp | Ref
| Expression |
1 | | fveqeq2 6852 |
. . . 4
β’ (π = π₯ β ((#bβπ) = π¦ β (#bβπ₯) = π¦)) |
2 | | id 22 |
. . . . 5
β’ (π = π₯ β π = π₯) |
3 | | oveq2 7366 |
. . . . . . 7
β’ (π = π₯ β (π(digitβ2)π) = (π(digitβ2)π₯)) |
4 | 3 | oveq1d 7373 |
. . . . . 6
β’ (π = π₯ β ((π(digitβ2)π) Β· (2βπ)) = ((π(digitβ2)π₯) Β· (2βπ))) |
5 | 4 | sumeq2sdv 15594 |
. . . . 5
β’ (π = π₯ β Ξ£π β (0..^π¦)((π(digitβ2)π) Β· (2βπ)) = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))) |
6 | 2, 5 | eqeq12d 2749 |
. . . 4
β’ (π = π₯ β (π = Ξ£π β (0..^π¦)((π(digitβ2)π) Β· (2βπ)) β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ)))) |
7 | 1, 6 | imbi12d 345 |
. . 3
β’ (π = π₯ β (((#bβπ) = π¦ β π = Ξ£π β (0..^π¦)((π(digitβ2)π) Β· (2βπ))) β ((#bβπ₯) = π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))))) |
8 | 7 | cbvralvw 3224 |
. 2
β’
(βπ β
β0 ((#bβπ) = π¦ β π = Ξ£π β (0..^π¦)((π(digitβ2)π) Β· (2βπ))) β βπ₯ β β0
((#bβπ₯) =
π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ)))) |
9 | | elnn0 12420 |
. . . . . 6
β’ (π β β0
β (π β β
β¨ π =
0)) |
10 | | nn0sumshdiglemA 46791 |
. . . . . . . . 9
β’ (((π β β β§ (π / 2) β β) β§
π¦ β β) β
(βπ₯ β
β0 ((#bβπ₯) = π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))) |
11 | 10 | expimpd 455 |
. . . . . . . 8
β’ ((π β β β§ (π / 2) β β) β
((π¦ β β β§
βπ₯ β
β0 ((#bβπ₯) = π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ)))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))) |
12 | | nn0sumshdiglemB 46792 |
. . . . . . . . 9
β’ (((π β β β§ ((π β 1) / 2) β
β0) β§ π¦ β β) β (βπ₯ β β0
((#bβπ₯) =
π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))) |
13 | 12 | expimpd 455 |
. . . . . . . 8
β’ ((π β β β§ ((π β 1) / 2) β
β0) β ((π¦ β β β§ βπ₯ β β0
((#bβπ₯) =
π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ)))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))) |
14 | | nneom 46699 |
. . . . . . . 8
β’ (π β β β ((π / 2) β β β¨
((π β 1) / 2) β
β0)) |
15 | 11, 13, 14 | mpjaodan 958 |
. . . . . . 7
β’ (π β β β ((π¦ β β β§
βπ₯ β
β0 ((#bβπ₯) = π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ)))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))) |
16 | | eqcom 2740 |
. . . . . . . . . . . . . 14
β’ (1 =
(π¦ + 1) β (π¦ + 1) = 1) |
17 | 16 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π¦ β β β (1 =
(π¦ + 1) β (π¦ + 1) = 1)) |
18 | | nncn 12166 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β π¦ β
β) |
19 | | 1cnd 11155 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β 1 β
β) |
20 | 18, 19, 19 | addlsub 11576 |
. . . . . . . . . . . . 13
β’ (π¦ β β β ((π¦ + 1) = 1 β π¦ = (1 β
1))) |
21 | | 1m1e0 12230 |
. . . . . . . . . . . . . . 15
β’ (1
β 1) = 0 |
22 | 21 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β (1
β 1) = 0) |
23 | 22 | eqeq2d 2744 |
. . . . . . . . . . . . 13
β’ (π¦ β β β (π¦ = (1 β 1) β π¦ = 0)) |
24 | 17, 20, 23 | 3bitrd 305 |
. . . . . . . . . . . 12
β’ (π¦ β β β (1 =
(π¦ + 1) β π¦ = 0)) |
25 | | oveq1 7365 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = 0 β (π¦ + 1) = (0 + 1)) |
26 | 25 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
β’ (π¦ = 0 β (0..^(π¦ + 1)) = (0..^(0 +
1))) |
27 | | 0p1e1 12280 |
. . . . . . . . . . . . . . . . 17
β’ (0 + 1) =
1 |
28 | 27 | oveq2i 7369 |
. . . . . . . . . . . . . . . 16
β’ (0..^(0 +
1)) = (0..^1) |
29 | | fzo01 13660 |
. . . . . . . . . . . . . . . 16
β’ (0..^1) =
{0} |
30 | 28, 29 | eqtri 2761 |
. . . . . . . . . . . . . . 15
β’ (0..^(0 +
1)) = {0} |
31 | 26, 30 | eqtrdi 2789 |
. . . . . . . . . . . . . 14
β’ (π¦ = 0 β (0..^(π¦ + 1)) = {0}) |
32 | 31 | sumeq1d 15591 |
. . . . . . . . . . . . 13
β’ (π¦ = 0 β Ξ£π β (0..^(π¦ + 1))((π(digitβ2)0) Β· (2βπ)) = Ξ£π β {0} ((π(digitβ2)0) Β· (2βπ))) |
33 | | 0cn 11152 |
. . . . . . . . . . . . . 14
β’ 0 β
β |
34 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 0 β (π(digitβ2)0) =
(0(digitβ2)0)) |
35 | | 2nn 12231 |
. . . . . . . . . . . . . . . . . . 19
β’ 2 β
β |
36 | | 0z 12515 |
. . . . . . . . . . . . . . . . . . 19
β’ 0 β
β€ |
37 | | dig0 46778 |
. . . . . . . . . . . . . . . . . . 19
β’ ((2
β β β§ 0 β β€) β (0(digitβ2)0) =
0) |
38 | 35, 36, 37 | mp2an 691 |
. . . . . . . . . . . . . . . . . 18
β’
(0(digitβ2)0) = 0 |
39 | 34, 38 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β (π(digitβ2)0) = 0) |
40 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 0 β (2βπ) = (2β0)) |
41 | | 2cn 12233 |
. . . . . . . . . . . . . . . . . . 19
β’ 2 β
β |
42 | | exp0 13977 |
. . . . . . . . . . . . . . . . . . 19
β’ (2 β
β β (2β0) = 1) |
43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
β’
(2β0) = 1 |
44 | 40, 43 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β (2βπ) = 1) |
45 | 39, 44 | oveq12d 7376 |
. . . . . . . . . . . . . . . 16
β’ (π = 0 β ((π(digitβ2)0) Β· (2βπ)) = (0 Β·
1)) |
46 | | 1re 11160 |
. . . . . . . . . . . . . . . . 17
β’ 1 β
β |
47 | | mul02lem2 11337 |
. . . . . . . . . . . . . . . . 17
β’ (1 β
β β (0 Β· 1) = 0) |
48 | 46, 47 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ (0
Β· 1) = 0 |
49 | 45, 48 | eqtrdi 2789 |
. . . . . . . . . . . . . . 15
β’ (π = 0 β ((π(digitβ2)0) Β· (2βπ)) = 0) |
50 | 49 | sumsn 15636 |
. . . . . . . . . . . . . 14
β’ ((0
β β β§ 0 β β) β Ξ£π β {0} ((π(digitβ2)0) Β· (2βπ)) = 0) |
51 | 33, 33, 50 | mp2an 691 |
. . . . . . . . . . . . 13
β’
Ξ£π β {0}
((π(digitβ2)0)
Β· (2βπ)) =
0 |
52 | 32, 51 | eqtr2di 2790 |
. . . . . . . . . . . 12
β’ (π¦ = 0 β 0 = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)0) Β· (2βπ))) |
53 | 24, 52 | syl6bi 253 |
. . . . . . . . . . 11
β’ (π¦ β β β (1 =
(π¦ + 1) β 0 =
Ξ£π β (0..^(π¦ + 1))((π(digitβ2)0) Β· (2βπ)))) |
54 | 53 | adantl 483 |
. . . . . . . . . 10
β’ ((π = 0 β§ π¦ β β) β (1 = (π¦ + 1) β 0 = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)0) Β· (2βπ)))) |
55 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π = 0 β
(#bβπ) =
(#bβ0)) |
56 | | blen0 46744 |
. . . . . . . . . . . . . 14
β’
(#bβ0) = 1 |
57 | 55, 56 | eqtrdi 2789 |
. . . . . . . . . . . . 13
β’ (π = 0 β
(#bβπ) =
1) |
58 | 57 | eqeq1d 2735 |
. . . . . . . . . . . 12
β’ (π = 0 β
((#bβπ) =
(π¦ + 1) β 1 = (π¦ + 1))) |
59 | | id 22 |
. . . . . . . . . . . . 13
β’ (π = 0 β π = 0) |
60 | | oveq2 7366 |
. . . . . . . . . . . . . . 15
β’ (π = 0 β (π(digitβ2)π) = (π(digitβ2)0)) |
61 | 60 | oveq1d 7373 |
. . . . . . . . . . . . . 14
β’ (π = 0 β ((π(digitβ2)π) Β· (2βπ)) = ((π(digitβ2)0) Β· (2βπ))) |
62 | 61 | sumeq2sdv 15594 |
. . . . . . . . . . . . 13
β’ (π = 0 β Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ)) = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)0) Β· (2βπ))) |
63 | 59, 62 | eqeq12d 2749 |
. . . . . . . . . . . 12
β’ (π = 0 β (π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ)) β 0 = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)0) Β· (2βπ)))) |
64 | 58, 63 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π = 0 β
(((#bβπ) =
(π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))) β (1 = (π¦ + 1) β 0 = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)0) Β· (2βπ))))) |
65 | 64 | adantr 482 |
. . . . . . . . . 10
β’ ((π = 0 β§ π¦ β β) β
(((#bβπ) =
(π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))) β (1 = (π¦ + 1) β 0 = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)0) Β· (2βπ))))) |
66 | 54, 65 | mpbird 257 |
. . . . . . . . 9
β’ ((π = 0 β§ π¦ β β) β
((#bβπ) =
(π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ)))) |
67 | 66 | a1d 25 |
. . . . . . . 8
β’ ((π = 0 β§ π¦ β β) β (βπ₯ β β0
((#bβπ₯) =
π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))) |
68 | 67 | expimpd 455 |
. . . . . . 7
β’ (π = 0 β ((π¦ β β β§ βπ₯ β β0
((#bβπ₯) =
π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ)))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))) |
69 | 15, 68 | jaoi 856 |
. . . . . 6
β’ ((π β β β¨ π = 0) β ((π¦ β β β§
βπ₯ β
β0 ((#bβπ₯) = π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ)))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))) |
70 | 9, 69 | sylbi 216 |
. . . . 5
β’ (π β β0
β ((π¦ β β
β§ βπ₯ β
β0 ((#bβπ₯) = π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ)))) β ((#bβπ) = (π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))) |
71 | 70 | com12 32 |
. . . 4
β’ ((π¦ β β β§
βπ₯ β
β0 ((#bβπ₯) = π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ)))) β (π β β0 β
((#bβπ) =
(π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))) |
72 | 71 | ralrimiv 3139 |
. . 3
β’ ((π¦ β β β§
βπ₯ β
β0 ((#bβπ₯) = π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ)))) β βπ β β0
((#bβπ) =
(π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ)))) |
73 | 72 | ex 414 |
. 2
β’ (π¦ β β β
(βπ₯ β
β0 ((#bβπ₯) = π¦ β π₯ = Ξ£π β (0..^π¦)((π(digitβ2)π₯) Β· (2βπ))) β βπ β β0
((#bβπ) =
(π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))) |
74 | 8, 73 | biimtrid 241 |
1
β’ (π¦ β β β
(βπ β
β0 ((#bβπ) = π¦ β π = Ξ£π β (0..^π¦)((π(digitβ2)π) Β· (2βπ))) β βπ β β0
((#bβπ) =
(π¦ + 1) β π = Ξ£π β (0..^(π¦ + 1))((π(digitβ2)π) Β· (2βπ))))) |