Step | Hyp | Ref
| Expression |
1 | | nnuz 9563 |
. . . . . . 7
β’ β =
(β€β₯β1) |
2 | | 1zzd 9280 |
. . . . . . 7
β’ (π β 1 β
β€) |
3 | | cvgratnn.6 |
. . . . . . 7
β’ ((π β§ π β β) β (πΉβπ) β β) |
4 | 1, 2, 3 | serf 10474 |
. . . . . 6
β’ (π β seq1( + , πΉ):ββΆβ) |
5 | | cvgratnnlemrate.m |
. . . . . . 7
β’ (π β π β β) |
6 | | cvgratnnlemrate.n |
. . . . . . 7
β’ (π β π β (β€β₯βπ)) |
7 | | eluznn 9600 |
. . . . . . 7
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
8 | 5, 6, 7 | syl2anc 411 |
. . . . . 6
β’ (π β π β β) |
9 | 4, 8 | ffvelcdmd 5653 |
. . . . 5
β’ (π β (seq1( + , πΉ)βπ) β β) |
10 | 4, 5 | ffvelcdmd 5653 |
. . . . 5
β’ (π β (seq1( + , πΉ)βπ) β β) |
11 | 9, 10 | subcld 8268 |
. . . 4
β’ (π β ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)βπ)) β β) |
12 | 11 | abscld 11190 |
. . 3
β’ (π β (absβ((seq1( + ,
πΉ)βπ) β (seq1( + , πΉ)βπ))) β β) |
13 | | fveq2 5516 |
. . . . . . 7
β’ (π = π β (πΉβπ) = (πΉβπ)) |
14 | 13 | eleq1d 2246 |
. . . . . 6
β’ (π = π β ((πΉβπ) β β β (πΉβπ) β β)) |
15 | 3 | ralrimiva 2550 |
. . . . . 6
β’ (π β βπ β β (πΉβπ) β β) |
16 | 14, 15, 5 | rspcdva 2847 |
. . . . 5
β’ (π β (πΉβπ) β β) |
17 | 16 | abscld 11190 |
. . . 4
β’ (π β (absβ(πΉβπ)) β β) |
18 | 5 | nnzd 9374 |
. . . . . . 7
β’ (π β π β β€) |
19 | 18 | peano2zd 9378 |
. . . . . 6
β’ (π β (π + 1) β β€) |
20 | | eluzelz 9537 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β π β β€) |
21 | 6, 20 | syl 14 |
. . . . . 6
β’ (π β π β β€) |
22 | 19, 21 | fzfigd 10431 |
. . . . 5
β’ (π β ((π + 1)...π) β Fin) |
23 | | cvgratnn.3 |
. . . . . . 7
β’ (π β π΄ β β) |
24 | 23 | adantr 276 |
. . . . . 6
β’ ((π β§ π β ((π + 1)...π)) β π΄ β β) |
25 | 5 | nnred 8932 |
. . . . . . . . 9
β’ (π β π β β) |
26 | 25 | adantr 276 |
. . . . . . . 8
β’ ((π β§ π β ((π + 1)...π)) β π β β) |
27 | | peano2re 8093 |
. . . . . . . . 9
β’ (π β β β (π + 1) β
β) |
28 | 26, 27 | syl 14 |
. . . . . . . 8
β’ ((π β§ π β ((π + 1)...π)) β (π + 1) β β) |
29 | | elfzelz 10025 |
. . . . . . . . . 10
β’ (π β ((π + 1)...π) β π β β€) |
30 | 29 | adantl 277 |
. . . . . . . . 9
β’ ((π β§ π β ((π + 1)...π)) β π β β€) |
31 | 30 | zred 9375 |
. . . . . . . 8
β’ ((π β§ π β ((π + 1)...π)) β π β β) |
32 | 26 | lep1d 8888 |
. . . . . . . 8
β’ ((π β§ π β ((π + 1)...π)) β π β€ (π + 1)) |
33 | | elfzle1 10027 |
. . . . . . . . 9
β’ (π β ((π + 1)...π) β (π + 1) β€ π) |
34 | 33 | adantl 277 |
. . . . . . . 8
β’ ((π β§ π β ((π + 1)...π)) β (π + 1) β€ π) |
35 | 26, 28, 31, 32, 34 | letrd 8081 |
. . . . . . 7
β’ ((π β§ π β ((π + 1)...π)) β π β€ π) |
36 | | znn0sub 9318 |
. . . . . . . 8
β’ ((π β β€ β§ π β β€) β (π β€ π β (π β π) β
β0)) |
37 | 18, 29, 36 | syl2an 289 |
. . . . . . 7
β’ ((π β§ π β ((π + 1)...π)) β (π β€ π β (π β π) β
β0)) |
38 | 35, 37 | mpbid 147 |
. . . . . 6
β’ ((π β§ π β ((π + 1)...π)) β (π β π) β
β0) |
39 | 24, 38 | reexpcld 10671 |
. . . . 5
β’ ((π β§ π β ((π + 1)...π)) β (π΄β(π β π)) β β) |
40 | 22, 39 | fsumrecl 11409 |
. . . 4
β’ (π β Ξ£π β ((π + 1)...π)(π΄β(π β π)) β β) |
41 | 17, 40 | remulcld 7988 |
. . 3
β’ (π β ((absβ(πΉβπ)) Β· Ξ£π β ((π + 1)...π)(π΄β(π β π))) β β) |
42 | | cvgratnn.4 |
. . . . . . . . . . 11
β’ (π β π΄ < 1) |
43 | | cvgratnn.gt0 |
. . . . . . . . . . . . 13
β’ (π β 0 < π΄) |
44 | 23, 43 | elrpd 9693 |
. . . . . . . . . . . 12
β’ (π β π΄ β
β+) |
45 | 44 | reclt1d 9710 |
. . . . . . . . . . 11
β’ (π β (π΄ < 1 β 1 < (1 / π΄))) |
46 | 42, 45 | mpbid 147 |
. . . . . . . . . 10
β’ (π β 1 < (1 / π΄)) |
47 | | 1re 7956 |
. . . . . . . . . . 11
β’ 1 β
β |
48 | 44 | rprecred 9708 |
. . . . . . . . . . 11
β’ (π β (1 / π΄) β β) |
49 | | difrp 9692 |
. . . . . . . . . . 11
β’ ((1
β β β§ (1 / π΄) β β) β (1 < (1 / π΄) β ((1 / π΄) β 1) β
β+)) |
50 | 47, 48, 49 | sylancr 414 |
. . . . . . . . . 10
β’ (π β (1 < (1 / π΄) β ((1 / π΄) β 1) β
β+)) |
51 | 46, 50 | mpbid 147 |
. . . . . . . . 9
β’ (π β ((1 / π΄) β 1) β
β+) |
52 | 51 | rpreccld 9707 |
. . . . . . . 8
β’ (π β (1 / ((1 / π΄) β 1)) β
β+) |
53 | 52, 44 | rpdivcld 9714 |
. . . . . . 7
β’ (π β ((1 / ((1 / π΄) β 1)) / π΄) β
β+) |
54 | | fveq2 5516 |
. . . . . . . . . . 11
β’ (π = 1 β (πΉβπ) = (πΉβ1)) |
55 | 54 | eleq1d 2246 |
. . . . . . . . . 10
β’ (π = 1 β ((πΉβπ) β β β (πΉβ1) β β)) |
56 | | 1nn 8930 |
. . . . . . . . . . 11
β’ 1 β
β |
57 | 56 | a1i 9 |
. . . . . . . . . 10
β’ (π β 1 β
β) |
58 | 55, 15, 57 | rspcdva 2847 |
. . . . . . . . 9
β’ (π β (πΉβ1) β β) |
59 | 58 | abscld 11190 |
. . . . . . . 8
β’ (π β (absβ(πΉβ1)) β
β) |
60 | 58 | absge0d 11193 |
. . . . . . . 8
β’ (π β 0 β€ (absβ(πΉβ1))) |
61 | 59, 60 | ge0p1rpd 9727 |
. . . . . . 7
β’ (π β ((absβ(πΉβ1)) + 1) β
β+) |
62 | 53, 61 | rpmulcld 9713 |
. . . . . 6
β’ (π β (((1 / ((1 / π΄) β 1)) / π΄) Β· ((absβ(πΉβ1)) + 1)) β
β+) |
63 | 62 | rpred 9696 |
. . . . 5
β’ (π β (((1 / ((1 / π΄) β 1)) / π΄) Β· ((absβ(πΉβ1)) + 1)) β
β) |
64 | 63, 5 | nndivred 8969 |
. . . 4
β’ (π β ((((1 / ((1 / π΄) β 1)) / π΄) Β· ((absβ(πΉβ1)) + 1)) / π) β
β) |
65 | | 1red 7972 |
. . . . . . . 8
β’ (π β 1 β
β) |
66 | 65, 23 | resubcld 8338 |
. . . . . . 7
β’ (π β (1 β π΄) β
β) |
67 | 23, 65 | posdifd 8489 |
. . . . . . . 8
β’ (π β (π΄ < 1 β 0 < (1 β π΄))) |
68 | 42, 67 | mpbid 147 |
. . . . . . 7
β’ (π β 0 < (1 β π΄)) |
69 | 66, 68 | elrpd 9693 |
. . . . . 6
β’ (π β (1 β π΄) β
β+) |
70 | 44, 69 | rpdivcld 9714 |
. . . . 5
β’ (π β (π΄ / (1 β π΄)) β
β+) |
71 | 70 | rpred 9696 |
. . . 4
β’ (π β (π΄ / (1 β π΄)) β β) |
72 | 64, 71 | remulcld 7988 |
. . 3
β’ (π β (((((1 / ((1 / π΄) β 1)) / π΄) Β· ((absβ(πΉβ1)) + 1)) / π) Β· (π΄ / (1 β π΄))) β β) |
73 | | cvgratnn.7 |
. . . . . 6
β’ ((π β§ π β β) β (absβ(πΉβ(π + 1))) β€ (π΄ Β· (absβ(πΉβπ)))) |
74 | 23, 42, 43, 3, 73, 5, 6 | cvgratnnlemseq 11534 |
. . . . 5
β’ (π β ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)βπ)) = Ξ£π β ((π + 1)...π)(πΉβπ)) |
75 | 74 | fveq2d 5520 |
. . . 4
β’ (π β (absβ((seq1( + ,
πΉ)βπ) β (seq1( + , πΉ)βπ))) = (absβΞ£π β ((π + 1)...π)(πΉβπ))) |
76 | 23, 42, 43, 3, 73, 5, 6 | cvgratnnlemabsle 11535 |
. . . 4
β’ (π β (absβΞ£π β ((π + 1)...π)(πΉβπ)) β€ ((absβ(πΉβπ)) Β· Ξ£π β ((π + 1)...π)(π΄β(π β π)))) |
77 | 75, 76 | eqbrtrd 4026 |
. . 3
β’ (π β (absβ((seq1( + ,
πΉ)βπ) β (seq1( + , πΉ)βπ))) β€ ((absβ(πΉβπ)) Β· Ξ£π β ((π + 1)...π)(π΄β(π β π)))) |
78 | 16 | absge0d 11193 |
. . . 4
β’ (π β 0 β€ (absβ(πΉβπ))) |
79 | 23, 42, 43, 3, 73, 5 | cvgratnnlemfm 11537 |
. . . 4
β’ (π β (absβ(πΉβπ)) < ((((1 / ((1 / π΄) β 1)) / π΄) Β· ((absβ(πΉβ1)) + 1)) / π)) |
80 | 44 | adantr 276 |
. . . . . . 7
β’ ((π β§ π β ((π + 1)...π)) β π΄ β
β+) |
81 | 38 | nn0zd 9373 |
. . . . . . 7
β’ ((π β§ π β ((π + 1)...π)) β (π β π) β β€) |
82 | 80, 81 | rpexpcld 10678 |
. . . . . 6
β’ ((π β§ π β ((π + 1)...π)) β (π΄β(π β π)) β
β+) |
83 | 82 | rpge0d 9700 |
. . . . 5
β’ ((π β§ π β ((π + 1)...π)) β 0 β€ (π΄β(π β π))) |
84 | 22, 39, 83 | fsumge0 11467 |
. . . 4
β’ (π β 0 β€ Ξ£π β ((π + 1)...π)(π΄β(π β π))) |
85 | 23, 42, 43, 3, 73, 5, 6 | cvgratnnlemsumlt 11536 |
. . . 4
β’ (π β Ξ£π β ((π + 1)...π)(π΄β(π β π)) < (π΄ / (1 β π΄))) |
86 | 17, 64, 40, 71, 78, 79, 84, 85 | ltmul12ad 8898 |
. . 3
β’ (π β ((absβ(πΉβπ)) Β· Ξ£π β ((π + 1)...π)(π΄β(π β π))) < (((((1 / ((1 / π΄) β 1)) / π΄) Β· ((absβ(πΉβ1)) + 1)) / π) Β· (π΄ / (1 β π΄)))) |
87 | 12, 41, 72, 77, 86 | lelttrd 8082 |
. 2
β’ (π β (absβ((seq1( + ,
πΉ)βπ) β (seq1( + , πΉ)βπ))) < (((((1 / ((1 / π΄) β 1)) / π΄) Β· ((absβ(πΉβ1)) + 1)) / π) Β· (π΄ / (1 β π΄)))) |
88 | 63 | recnd 7986 |
. . 3
β’ (π β (((1 / ((1 / π΄) β 1)) / π΄) Β· ((absβ(πΉβ1)) + 1)) β
β) |
89 | 71 | recnd 7986 |
. . 3
β’ (π β (π΄ / (1 β π΄)) β β) |
90 | 5 | nncnd 8933 |
. . 3
β’ (π β π β β) |
91 | 5 | nnap0d 8965 |
. . 3
β’ (π β π # 0) |
92 | 88, 89, 90, 91 | div23apd 8785 |
. 2
β’ (π β (((((1 / ((1 / π΄) β 1)) / π΄) Β· ((absβ(πΉβ1)) + 1)) Β· (π΄ / (1 β π΄))) / π) = (((((1 / ((1 / π΄) β 1)) / π΄) Β· ((absβ(πΉβ1)) + 1)) / π) Β· (π΄ / (1 β π΄)))) |
93 | 87, 92 | breqtrrd 4032 |
1
β’ (π β (absβ((seq1( + ,
πΉ)βπ) β (seq1( + , πΉ)βπ))) < (((((1 / ((1 / π΄) β 1)) / π΄) Β· ((absβ(πΉβ1)) + 1)) Β· (π΄ / (1 β π΄))) / π)) |