Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . 3
β’
(β€β₯βπ) = (β€β₯βπ) |
2 | | nnz 12527 |
. . 3
β’ (π β β β π β
β€) |
3 | | eqidd 2738 |
. . 3
β’ ((π β β β§ π β
(β€β₯βπ)) β ((πΉβ(β β {π}))βπ) = ((πΉβ(β β {π}))βπ)) |
4 | | eluznn 12850 |
. . . 4
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
5 | | difss 4096 |
. . . . . . 7
β’ (β
β {π}) β
β |
6 | | rpnnen2.1 |
. . . . . . . 8
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) |
7 | 6 | rpnnen2lem2 16104 |
. . . . . . 7
β’ ((β
β {π}) β
β β (πΉβ(β β {π})):ββΆβ) |
8 | 5, 7 | ax-mp 5 |
. . . . . 6
β’ (πΉβ(β β {π})):ββΆβ |
9 | 8 | ffvelcdmi 7039 |
. . . . 5
β’ (π β β β ((πΉβ(β β {π}))βπ) β β) |
10 | 9 | recnd 11190 |
. . . 4
β’ (π β β β ((πΉβ(β β {π}))βπ) β β) |
11 | 4, 10 | syl 17 |
. . 3
β’ ((π β β β§ π β
(β€β₯βπ)) β ((πΉβ(β β {π}))βπ) β β) |
12 | 6 | rpnnen2lem5 16107 |
. . . 4
β’
(((β β {π}) β β β§ π β β) β seqπ( + , (πΉβ(β β {π}))) β dom β ) |
13 | 5, 12 | mpan 689 |
. . 3
β’ (π β β β seqπ( + , (πΉβ(β β {π}))) β dom β ) |
14 | 1, 2, 3, 11, 13 | isum1p 15733 |
. 2
β’ (π β β β
Ξ£π β
(β€β₯βπ)((πΉβ(β β {π}))βπ) = (((πΉβ(β β {π}))βπ) + Ξ£π β (β€β₯β(π + 1))((πΉβ(β β {π}))βπ))) |
15 | 6 | rpnnen2lem1 16103 |
. . . . 5
β’
(((β β {π}) β β β§ π β β) β ((πΉβ(β β {π}))βπ) = if(π β (β β {π}), ((1 / 3)βπ), 0)) |
16 | 5, 15 | mpan 689 |
. . . 4
β’ (π β β β ((πΉβ(β β {π}))βπ) = if(π β (β β {π}), ((1 / 3)βπ), 0)) |
17 | | neldifsnd 4758 |
. . . . 5
β’ (π β β β Β¬
π β (β β
{π})) |
18 | 17 | iffalsed 4502 |
. . . 4
β’ (π β β β if(π β (β β {π}), ((1 / 3)βπ), 0) = 0) |
19 | 16, 18 | eqtrd 2777 |
. . 3
β’ (π β β β ((πΉβ(β β {π}))βπ) = 0) |
20 | | eqid 2737 |
. . . 4
β’
(β€β₯β(π + 1)) =
(β€β₯β(π + 1)) |
21 | | peano2nn 12172 |
. . . . 5
β’ (π β β β (π + 1) β
β) |
22 | 21 | nnzd 12533 |
. . . 4
β’ (π β β β (π + 1) β
β€) |
23 | | eqidd 2738 |
. . . 4
β’ ((π β β β§ π β
(β€β₯β(π + 1))) β ((πΉβ(β β {π}))βπ) = ((πΉβ(β β {π}))βπ)) |
24 | | eluznn 12850 |
. . . . . 6
β’ (((π + 1) β β β§ π β
(β€β₯β(π + 1))) β π β β) |
25 | 21, 24 | sylan 581 |
. . . . 5
β’ ((π β β β§ π β
(β€β₯β(π + 1))) β π β β) |
26 | 25, 10 | syl 17 |
. . . 4
β’ ((π β β β§ π β
(β€β₯β(π + 1))) β ((πΉβ(β β {π}))βπ) β β) |
27 | | 1re 11162 |
. . . . . . . 8
β’ 1 β
β |
28 | | 3nn 12239 |
. . . . . . . 8
β’ 3 β
β |
29 | | nndivre 12201 |
. . . . . . . 8
β’ ((1
β β β§ 3 β β) β (1 / 3) β
β) |
30 | 27, 28, 29 | mp2an 691 |
. . . . . . 7
β’ (1 / 3)
β β |
31 | 30 | recni 11176 |
. . . . . 6
β’ (1 / 3)
β β |
32 | 31 | a1i 11 |
. . . . 5
β’ (π β β β (1 / 3)
β β) |
33 | | 0re 11164 |
. . . . . . . . 9
β’ 0 β
β |
34 | | 3re 12240 |
. . . . . . . . . 10
β’ 3 β
β |
35 | | 3pos 12265 |
. . . . . . . . . 10
β’ 0 <
3 |
36 | 34, 35 | recgt0ii 12068 |
. . . . . . . . 9
β’ 0 < (1
/ 3) |
37 | 33, 30, 36 | ltleii 11285 |
. . . . . . . 8
β’ 0 β€ (1
/ 3) |
38 | | absid 15188 |
. . . . . . . 8
β’ (((1 / 3)
β β β§ 0 β€ (1 / 3)) β (absβ(1 / 3)) = (1 /
3)) |
39 | 30, 37, 38 | mp2an 691 |
. . . . . . 7
β’
(absβ(1 / 3)) = (1 / 3) |
40 | | 1lt3 12333 |
. . . . . . . 8
β’ 1 <
3 |
41 | | recgt1 12058 |
. . . . . . . . 9
β’ ((3
β β β§ 0 < 3) β (1 < 3 β (1 / 3) <
1)) |
42 | 34, 35, 41 | mp2an 691 |
. . . . . . . 8
β’ (1 < 3
β (1 / 3) < 1) |
43 | 40, 42 | mpbi 229 |
. . . . . . 7
β’ (1 / 3)
< 1 |
44 | 39, 43 | eqbrtri 5131 |
. . . . . 6
β’
(absβ(1 / 3)) < 1 |
45 | 44 | a1i 11 |
. . . . 5
β’ (π β β β
(absβ(1 / 3)) < 1) |
46 | 21 | nnnn0d 12480 |
. . . . 5
β’ (π β β β (π + 1) β
β0) |
47 | 6 | rpnnen2lem1 16103 |
. . . . . . . 8
β’
(((β β {π}) β β β§ π β β) β ((πΉβ(β β {π}))βπ) = if(π β (β β {π}), ((1 / 3)βπ), 0)) |
48 | 5, 47 | mpan 689 |
. . . . . . 7
β’ (π β β β ((πΉβ(β β {π}))βπ) = if(π β (β β {π}), ((1 / 3)βπ), 0)) |
49 | 25, 48 | syl 17 |
. . . . . 6
β’ ((π β β β§ π β
(β€β₯β(π + 1))) β ((πΉβ(β β {π}))βπ) = if(π β (β β {π}), ((1 / 3)βπ), 0)) |
50 | | nnre 12167 |
. . . . . . . . . 10
β’ (π β β β π β
β) |
51 | 50 | adantr 482 |
. . . . . . . . 9
β’ ((π β β β§ π β
(β€β₯β(π + 1))) β π β β) |
52 | | eluzle 12783 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β(π + 1)) β (π + 1) β€ π) |
53 | 52 | adantl 483 |
. . . . . . . . . 10
β’ ((π β β β§ π β
(β€β₯β(π + 1))) β (π + 1) β€ π) |
54 | | nnltp1le 12566 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β) β (π < π β (π + 1) β€ π)) |
55 | 25, 54 | syldan 592 |
. . . . . . . . . 10
β’ ((π β β β§ π β
(β€β₯β(π + 1))) β (π < π β (π + 1) β€ π)) |
56 | 53, 55 | mpbird 257 |
. . . . . . . . 9
β’ ((π β β β§ π β
(β€β₯β(π + 1))) β π < π) |
57 | 51, 56 | gtned 11297 |
. . . . . . . 8
β’ ((π β β β§ π β
(β€β₯β(π + 1))) β π β π) |
58 | | eldifsn 4752 |
. . . . . . . 8
β’ (π β (β β {π}) β (π β β β§ π β π)) |
59 | 25, 57, 58 | sylanbrc 584 |
. . . . . . 7
β’ ((π β β β§ π β
(β€β₯β(π + 1))) β π β (β β {π})) |
60 | 59 | iftrued 4499 |
. . . . . 6
β’ ((π β β β§ π β
(β€β₯β(π + 1))) β if(π β (β β {π}), ((1 / 3)βπ), 0) = ((1 / 3)βπ)) |
61 | 49, 60 | eqtrd 2777 |
. . . . 5
β’ ((π β β β§ π β
(β€β₯β(π + 1))) β ((πΉβ(β β {π}))βπ) = ((1 / 3)βπ)) |
62 | 32, 45, 46, 61 | geolim2 15763 |
. . . 4
β’ (π β β β seq(π + 1)( + , (πΉβ(β β {π}))) β (((1 / 3)β(π + 1)) / (1 β (1 /
3)))) |
63 | 20, 22, 23, 26, 62 | isumclim 15649 |
. . 3
β’ (π β β β
Ξ£π β
(β€β₯β(π + 1))((πΉβ(β β {π}))βπ) = (((1 / 3)β(π + 1)) / (1 β (1 /
3)))) |
64 | 19, 63 | oveq12d 7380 |
. 2
β’ (π β β β (((πΉβ(β β {π}))βπ) + Ξ£π β (β€β₯β(π + 1))((πΉβ(β β {π}))βπ)) = (0 + (((1 / 3)β(π + 1)) / (1 β (1 /
3))))) |
65 | 14, 64 | eqtrd 2777 |
1
β’ (π β β β
Ξ£π β
(β€β₯βπ)((πΉβ(β β {π}))βπ) = (0 + (((1 / 3)β(π + 1)) / (1 β (1 /
3))))) |