Step | Hyp | Ref
| Expression |
1 | | nnuz 12814 |
. . 3
β’ β =
(β€β₯β1) |
2 | | 1zzd 12542 |
. . 3
β’ (π β 1 β
β€) |
3 | | mertens.9 |
. . . . 5
β’ (π β πΈ β
β+) |
4 | 3 | rphalfcld 12977 |
. . . 4
β’ (π β (πΈ / 2) β
β+) |
5 | | nn0uz 12813 |
. . . . . 6
β’
β0 = (β€β₯β0) |
6 | | 0zd 12519 |
. . . . . 6
β’ (π β 0 β
β€) |
7 | | eqidd 2734 |
. . . . . 6
β’ ((π β§ π β β0) β (πΎβπ) = (πΎβπ)) |
8 | | mertens.2 |
. . . . . . 7
β’ ((π β§ π β β0) β (πΎβπ) = (absβπ΄)) |
9 | | mertens.3 |
. . . . . . . 8
β’ ((π β§ π β β0) β π΄ β
β) |
10 | 9 | abscld 15330 |
. . . . . . 7
β’ ((π β§ π β β0) β
(absβπ΄) β
β) |
11 | 8, 10 | eqeltrd 2834 |
. . . . . 6
β’ ((π β§ π β β0) β (πΎβπ) β β) |
12 | | mertens.7 |
. . . . . 6
β’ (π β seq0( + , πΎ) β dom β
) |
13 | 5, 6, 7, 11, 12 | isumrecl 15658 |
. . . . 5
β’ (π β Ξ£π β β0 (πΎβπ) β β) |
14 | 9 | absge0d 15338 |
. . . . . . 7
β’ ((π β§ π β β0) β 0 β€
(absβπ΄)) |
15 | 14, 8 | breqtrrd 5137 |
. . . . . 6
β’ ((π β§ π β β0) β 0 β€
(πΎβπ)) |
16 | 5, 6, 7, 11, 12, 15 | isumge0 15659 |
. . . . 5
β’ (π β 0 β€ Ξ£π β β0
(πΎβπ)) |
17 | 13, 16 | ge0p1rpd 12995 |
. . . 4
β’ (π β (Ξ£π β β0 (πΎβπ) + 1) β
β+) |
18 | 4, 17 | rpdivcld 12982 |
. . 3
β’ (π β ((πΈ / 2) / (Ξ£π β β0 (πΎβπ) + 1)) β
β+) |
19 | | eqidd 2734 |
. . 3
β’ ((π β§ π β β) β (seq0( + , πΊ)βπ) = (seq0( + , πΊ)βπ)) |
20 | | mertens.4 |
. . . 4
β’ ((π β§ π β β0) β (πΊβπ) = π΅) |
21 | | mertens.5 |
. . . 4
β’ ((π β§ π β β0) β π΅ β
β) |
22 | | mertens.8 |
. . . 4
β’ (π β seq0( + , πΊ) β dom β
) |
23 | 5, 6, 20, 21, 22 | isumclim2 15651 |
. . 3
β’ (π β seq0( + , πΊ) β Ξ£π β β0
π΅) |
24 | 1, 2, 18, 19, 23 | climi2 15402 |
. 2
β’ (π β βπ β β βπ β (β€β₯βπ )(absβ((seq0( + , πΊ)βπ) β Ξ£π β β0 π΅)) < ((πΈ / 2) / (Ξ£π β β0 (πΎβπ) + 1))) |
25 | | eluznn 12851 |
. . . . . . . 8
β’ ((π β β β§ π β
(β€β₯βπ )) β π β β) |
26 | 20, 21 | eqeltrd 2834 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β0) β (πΊβπ) β β) |
27 | 5, 6, 26 | serf 13945 |
. . . . . . . . . . . 12
β’ (π β seq0( + , πΊ):β0βΆβ) |
28 | | nnnn0 12428 |
. . . . . . . . . . . 12
β’ (π β β β π β
β0) |
29 | | ffvelcdm 7036 |
. . . . . . . . . . . 12
β’ ((seq0( +
, πΊ):β0βΆβ β§
π β
β0) β (seq0( + , πΊ)βπ) β β) |
30 | 27, 28, 29 | syl2an 597 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (seq0( + , πΊ)βπ) β β) |
31 | 5, 6, 20, 21, 22 | isumcl 15654 |
. . . . . . . . . . . 12
β’ (π β Ξ£π β β0 π΅ β β) |
32 | 31 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β Ξ£π β β0
π΅ β
β) |
33 | 30, 32 | abssubd 15347 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (absβ((seq0( +
, πΊ)βπ) β Ξ£π β β0
π΅)) =
(absβ(Ξ£π β
β0 π΅
β (seq0( + , πΊ)βπ)))) |
34 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(β€β₯β(π + 1)) = (β€β₯β(π + 1)) |
35 | 28 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β π β β0) |
36 | | peano2nn0 12461 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β (π + 1) β
β0) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (π + 1) β
β0) |
38 | 37 | nn0zd 12533 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (π + 1) β β€) |
39 | | simpll 766 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β (β€β₯β(π + 1))) β π) |
40 | | eluznn0 12850 |
. . . . . . . . . . . . . . . 16
β’ (((π + 1) β β0
β§ π β
(β€β₯β(π + 1))) β π β β0) |
41 | 37, 40 | sylan 581 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β (β€β₯β(π + 1))) β π β
β0) |
42 | 39, 41, 20 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β (β€β₯β(π + 1))) β (πΊβπ) = π΅) |
43 | 39, 41, 21 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β (β€β₯β(π + 1))) β π΅ β β) |
44 | 22 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β seq0( + , πΊ) β dom β
) |
45 | 26 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π β β0) β (πΊβπ) β β) |
46 | 5, 37, 45 | iserex 15550 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (seq0( + , πΊ) β dom β β
seq(π + 1)( + , πΊ) β dom β
)) |
47 | 44, 46 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β seq(π + 1)( + , πΊ) β dom β ) |
48 | 34, 38, 42, 43, 47 | isumcl 15654 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β Ξ£π β
(β€β₯β(π + 1))π΅ β β) |
49 | 30, 48 | pncan2d 11522 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (((seq0( + , πΊ)βπ) + Ξ£π β (β€β₯β(π + 1))π΅) β (seq0( + , πΊ)βπ)) = Ξ£π β (β€β₯β(π + 1))π΅) |
50 | 20 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β β0) β (πΊβπ) = π΅) |
51 | 21 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β β0) β π΅ β
β) |
52 | 5, 34, 37, 50, 51, 44 | isumsplit 15733 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β Ξ£π β β0
π΅ = (Ξ£π β (0...((π + 1) β 1))π΅ + Ξ£π β (β€β₯β(π + 1))π΅)) |
53 | | nncn 12169 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β π β
β) |
54 | 53 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β π β β) |
55 | | ax-1cn 11117 |
. . . . . . . . . . . . . . . . . . 19
β’ 1 β
β |
56 | | pncan 11415 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ 1 β
β) β ((π + 1)
β 1) = π) |
57 | 54, 55, 56 | sylancl 587 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β ((π + 1) β 1) = π) |
58 | 57 | oveq2d 7377 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (0...((π + 1) β 1)) = (0...π)) |
59 | 58 | sumeq1d 15594 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β Ξ£π β (0...((π + 1) β 1))π΅ = Ξ£π β (0...π)π΅) |
60 | | simpl 484 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β π) |
61 | | elfznn0 13543 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0...π) β π β β0) |
62 | 60, 61, 20 | syl2an 597 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ π β (0...π)) β (πΊβπ) = π΅) |
63 | 35, 5 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β π β
(β€β₯β0)) |
64 | 60, 61, 21 | syl2an 597 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ π β (0...π)) β π΅ β β) |
65 | 62, 63, 64 | fsumser 15623 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β Ξ£π β (0...π)π΅ = (seq0( + , πΊ)βπ)) |
66 | 59, 65 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β Ξ£π β (0...((π + 1) β 1))π΅ = (seq0( + , πΊ)βπ)) |
67 | 66 | oveq1d 7376 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (Ξ£π β (0...((π + 1) β 1))π΅ + Ξ£π β (β€β₯β(π + 1))π΅) = ((seq0( + , πΊ)βπ) + Ξ£π β (β€β₯β(π + 1))π΅)) |
68 | 52, 67 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β Ξ£π β β0
π΅ = ((seq0( + , πΊ)βπ) + Ξ£π β (β€β₯β(π + 1))π΅)) |
69 | 68 | oveq1d 7376 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (Ξ£π β β0
π΅ β (seq0( + , πΊ)βπ)) = (((seq0( + , πΊ)βπ) + Ξ£π β (β€β₯β(π + 1))π΅) β (seq0( + , πΊ)βπ))) |
70 | 42 | sumeq2dv 15596 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β Ξ£π β
(β€β₯β(π + 1))(πΊβπ) = Ξ£π β (β€β₯β(π + 1))π΅) |
71 | 49, 69, 70 | 3eqtr4d 2783 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (Ξ£π β β0
π΅ β (seq0( + , πΊ)βπ)) = Ξ£π β (β€β₯β(π + 1))(πΊβπ)) |
72 | 71 | fveq2d 6850 |
. . . . . . . . . 10
β’ ((π β§ π β β) β
(absβ(Ξ£π β
β0 π΅
β (seq0( + , πΊ)βπ))) = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ))) |
73 | 33, 72 | eqtrd 2773 |
. . . . . . . . 9
β’ ((π β§ π β β) β (absβ((seq0( +
, πΊ)βπ) β Ξ£π β β0
π΅)) =
(absβΞ£π β
(β€β₯β(π + 1))(πΊβπ))) |
74 | 73 | breq1d 5119 |
. . . . . . . 8
β’ ((π β§ π β β) β ((absβ((seq0( +
, πΊ)βπ) β Ξ£π β β0
π΅)) < ((πΈ / 2) / (Ξ£π β β0
(πΎβπ) + 1)) β (absβΞ£π β
(β€β₯β(π + 1))(πΊβπ)) < ((πΈ / 2) / (Ξ£π β β0 (πΎβπ) + 1)))) |
75 | 25, 74 | sylan2 594 |
. . . . . . 7
β’ ((π β§ (π β β β§ π β (β€β₯βπ ))) β ((absβ((seq0( +
, πΊ)βπ) β Ξ£π β β0
π΅)) < ((πΈ / 2) / (Ξ£π β β0
(πΎβπ) + 1)) β (absβΞ£π β
(β€β₯β(π + 1))(πΊβπ)) < ((πΈ / 2) / (Ξ£π β β0 (πΎβπ) + 1)))) |
76 | 75 | anassrs 469 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (β€β₯βπ )) β ((absβ((seq0( +
, πΊ)βπ) β Ξ£π β β0
π΅)) < ((πΈ / 2) / (Ξ£π β β0
(πΎβπ) + 1)) β (absβΞ£π β
(β€β₯β(π + 1))(πΊβπ)) < ((πΈ / 2) / (Ξ£π β β0 (πΎβπ) + 1)))) |
77 | 76 | ralbidva 3169 |
. . . . 5
β’ ((π β§ π β β) β (βπ β
(β€β₯βπ )(absβ((seq0( + , πΊ)βπ) β Ξ£π β β0 π΅)) < ((πΈ / 2) / (Ξ£π β β0 (πΎβπ) + 1)) β βπ β (β€β₯βπ )(absβΞ£π β
(β€β₯β(π + 1))(πΊβπ)) < ((πΈ / 2) / (Ξ£π β β0 (πΎβπ) + 1)))) |
78 | | fvoveq1 7384 |
. . . . . . . . 9
β’ (π = π β (β€β₯β(π + 1)) =
(β€β₯β(π + 1))) |
79 | 78 | sumeq1d 15594 |
. . . . . . . 8
β’ (π = π β Ξ£π β (β€β₯β(π + 1))(πΊβπ) = Ξ£π β (β€β₯β(π + 1))(πΊβπ)) |
80 | 79 | fveq2d 6850 |
. . . . . . 7
β’ (π = π β (absβΞ£π β (β€β₯β(π + 1))(πΊβπ)) = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ))) |
81 | 80 | breq1d 5119 |
. . . . . 6
β’ (π = π β ((absβΞ£π β (β€β₯β(π + 1))(πΊβπ)) < ((πΈ / 2) / (Ξ£π β β0 (πΎβπ) + 1)) β (absβΞ£π β
(β€β₯β(π + 1))(πΊβπ)) < ((πΈ / 2) / (Ξ£π β β0 (πΎβπ) + 1)))) |
82 | 81 | cbvralvw 3224 |
. . . . 5
β’
(βπ β
(β€β₯βπ )(absβΞ£π β (β€β₯β(π + 1))(πΊβπ)) < ((πΈ / 2) / (Ξ£π β β0 (πΎβπ) + 1)) β βπ β (β€β₯βπ )(absβΞ£π β
(β€β₯β(π + 1))(πΊβπ)) < ((πΈ / 2) / (Ξ£π β β0 (πΎβπ) + 1))) |
83 | 77, 82 | bitrdi 287 |
. . . 4
β’ ((π β§ π β β) β (βπ β
(β€β₯βπ )(absβ((seq0( + , πΊ)βπ) β Ξ£π β β0 π΅)) < ((πΈ / 2) / (Ξ£π β β0 (πΎβπ) + 1)) β βπ β (β€β₯βπ )(absβΞ£π β
(β€β₯β(π + 1))(πΊβπ)) < ((πΈ / 2) / (Ξ£π β β0 (πΎβπ) + 1)))) |
84 | | mertens.11 |
. . . . . 6
β’ (π β (π β β β§ βπ β
(β€β₯βπ )(absβΞ£π β (β€β₯β(π + 1))(πΊβπ)) < ((πΈ / 2) / (Ξ£π β β0 (πΎβπ) + 1)))) |
85 | | 0zd 12519 |
. . . . . . . . 9
β’ ((π β§ π) β 0 β β€) |
86 | 4 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π) β (πΈ / 2) β
β+) |
87 | 84 | simplbi 499 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
88 | 87 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π) β π β β) |
89 | 88 | nnrpd 12963 |
. . . . . . . . . . 11
β’ ((π β§ π) β π β β+) |
90 | 86, 89 | rpdivcld 12982 |
. . . . . . . . . 10
β’ ((π β§ π) β ((πΈ / 2) / π ) β
β+) |
91 | | mertens.10 |
. . . . . . . . . . . . 13
β’ π = {π§ β£ βπ β (0...(π β 1))π§ = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ))} |
92 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’
(β€β₯β(π + 1)) = (β€β₯β(π + 1)) |
93 | | elfznn0 13543 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0...(π β 1)) β π β β0) |
94 | 93 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π) β§ π β (0...(π β 1))) β π β β0) |
95 | | peano2nn0 12461 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β (π + 1) β
β0) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π) β§ π β (0...(π β 1))) β (π + 1) β
β0) |
97 | 96 | nn0zd 12533 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π) β§ π β (0...(π β 1))) β (π + 1) β β€) |
98 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π) β§ π β (0...(π β 1))) β§ π β (β€β₯β(π + 1))) β (πΊβπ) = (πΊβπ)) |
99 | | simplll 774 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π) β§ π β (0...(π β 1))) β§ π β (β€β₯β(π + 1))) β π) |
100 | | eluznn0 12850 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π + 1) β β0
β§ π β
(β€β₯β(π + 1))) β π β β0) |
101 | 96, 100 | sylan 581 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π) β§ π β (0...(π β 1))) β§ π β (β€β₯β(π + 1))) β π β
β0) |
102 | 99, 101, 26 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π) β§ π β (0...(π β 1))) β§ π β (β€β₯β(π + 1))) β (πΊβπ) β β) |
103 | 22 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π) β§ π β (0...(π β 1))) β seq0( + , πΊ) β dom β
) |
104 | 26 | ad4ant14 751 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π) β§ π β (0...(π β 1))) β§ π β β0) β (πΊβπ) β β) |
105 | 5, 96, 104 | iserex 15550 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π) β§ π β (0...(π β 1))) β (seq0( + , πΊ) β dom β β
seq(π + 1)( + , πΊ) β dom β
)) |
106 | 103, 105 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π) β§ π β (0...(π β 1))) β seq(π + 1)( + , πΊ) β dom β ) |
107 | 92, 97, 98, 102, 106 | isumcl 15654 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π) β§ π β (0...(π β 1))) β Ξ£π β
(β€β₯β(π + 1))(πΊβπ) β β) |
108 | 107 | abscld 15330 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π) β§ π β (0...(π β 1))) β (absβΞ£π β
(β€β₯β(π + 1))(πΊβπ)) β β) |
109 | | eleq1a 2829 |
. . . . . . . . . . . . . . . 16
β’
((absβΞ£π
β (β€β₯β(π + 1))(πΊβπ)) β β β (π§ = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ)) β π§ β β)) |
110 | 108, 109 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π) β§ π β (0...(π β 1))) β (π§ = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ)) β π§ β β)) |
111 | 110 | rexlimdva 3149 |
. . . . . . . . . . . . . 14
β’ ((π β§ π) β (βπ β (0...(π β 1))π§ = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ)) β π§ β β)) |
112 | 111 | abssdv 4029 |
. . . . . . . . . . . . 13
β’ ((π β§ π) β {π§ β£ βπ β (0...(π β 1))π§ = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ))} β β) |
113 | 91, 112 | eqsstrid 3996 |
. . . . . . . . . . . 12
β’ ((π β§ π) β π β β) |
114 | | fzfid 13887 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π) β (0...(π β 1)) β Fin) |
115 | | abrexfi 9302 |
. . . . . . . . . . . . . . 15
β’
((0...(π β 1))
β Fin β {π§
β£ βπ β
(0...(π β 1))π§ = (absβΞ£π β
(β€β₯β(π + 1))(πΊβπ))} β Fin) |
116 | 114, 115 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π) β {π§ β£ βπ β (0...(π β 1))π§ = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ))} β Fin) |
117 | 91, 116 | eqeltrid 2838 |
. . . . . . . . . . . . 13
β’ ((π β§ π) β π β Fin) |
118 | | nnm1nn0 12462 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β (π β 1) β
β0) |
119 | 88, 118 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π) β (π β 1) β
β0) |
120 | 119, 5 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π) β (π β 1) β
(β€β₯β0)) |
121 | | eluzfz1 13457 |
. . . . . . . . . . . . . . . . 17
β’ ((π β 1) β
(β€β₯β0) β 0 β (0...(π β 1))) |
122 | 120, 121 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π) β 0 β (0...(π β 1))) |
123 | | nnnn0 12428 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β π β
β0) |
124 | 123, 20 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β (πΊβπ) = π΅) |
125 | 124 | sumeq2dv 15596 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Ξ£π β β (πΊβπ) = Ξ£π β β π΅) |
126 | 125 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π) β Ξ£π β β (πΊβπ) = Ξ£π β β π΅) |
127 | 126 | fveq2d 6850 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π) β (absβΞ£π β β (πΊβπ)) = (absβΞ£π β β π΅)) |
128 | 127 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π) β (absβΞ£π β β π΅) = (absβΞ£π β β (πΊβπ))) |
129 | | fv0p1e1 12284 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 0 β
(β€β₯β(π + 1)) =
(β€β₯β1)) |
130 | 129, 1 | eqtr4di 2791 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 0 β
(β€β₯β(π + 1)) = β) |
131 | 130 | sumeq1d 15594 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 0 β Ξ£π β
(β€β₯β(π + 1))(πΊβπ) = Ξ£π β β (πΊβπ)) |
132 | 131 | fveq2d 6850 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β
(absβΞ£π β
(β€β₯β(π + 1))(πΊβπ)) = (absβΞ£π β β (πΊβπ))) |
133 | 132 | rspceeqv 3599 |
. . . . . . . . . . . . . . . 16
β’ ((0
β (0...(π β 1))
β§ (absβΞ£π
β β π΅) =
(absβΞ£π β
β (πΊβπ))) β βπ β (0...(π β 1))(absβΞ£π β β π΅) = (absβΞ£π β
(β€β₯β(π + 1))(πΊβπ))) |
134 | 122, 128,
133 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π) β βπ β (0...(π β 1))(absβΞ£π β β π΅) = (absβΞ£π β
(β€β₯β(π + 1))(πΊβπ))) |
135 | | fvex 6859 |
. . . . . . . . . . . . . . . 16
β’
(absβΞ£π
β β π΅) β
V |
136 | | eqeq1 2737 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = (absβΞ£π β β π΅) β (π§ = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ)) β (absβΞ£π β β π΅) = (absβΞ£π β
(β€β₯β(π + 1))(πΊβπ)))) |
137 | 136 | rexbidv 3172 |
. . . . . . . . . . . . . . . 16
β’ (π§ = (absβΞ£π β β π΅) β (βπ β (0...(π β 1))π§ = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ)) β βπ β (0...(π β 1))(absβΞ£π β β π΅) = (absβΞ£π β
(β€β₯β(π + 1))(πΊβπ)))) |
138 | 135, 137,
91 | elab2 3638 |
. . . . . . . . . . . . . . 15
β’
((absβΞ£π
β β π΅) β
π β βπ β (0...(π β 1))(absβΞ£π β β π΅) = (absβΞ£π β
(β€β₯β(π + 1))(πΊβπ))) |
139 | 134, 138 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ ((π β§ π) β (absβΞ£π β β π΅) β π) |
140 | 139 | ne0d 4299 |
. . . . . . . . . . . . 13
β’ ((π β§ π) β π β β
) |
141 | | ltso 11243 |
. . . . . . . . . . . . . 14
β’ < Or
β |
142 | | fisupcl 9413 |
. . . . . . . . . . . . . 14
β’ (( <
Or β β§ (π β
Fin β§ π β β
β§ π β β))
β sup(π, β, <
) β π) |
143 | 141, 142 | mpan 689 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ π β β
β§ π β β) β
sup(π, β, < )
β π) |
144 | 117, 140,
113, 143 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ π) β sup(π, β, < ) β π) |
145 | 113, 144 | sseldd 3949 |
. . . . . . . . . . 11
β’ ((π β§ π) β sup(π, β, < ) β
β) |
146 | | 0red 11166 |
. . . . . . . . . . . 12
β’ ((π β§ π) β 0 β β) |
147 | 123, 21 | sylan2 594 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β π΅ β β) |
148 | | 1nn0 12437 |
. . . . . . . . . . . . . . . . . 18
β’ 1 β
β0 |
149 | 148 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β 1 β
β0) |
150 | 5, 149, 26 | iserex 15550 |
. . . . . . . . . . . . . . . 16
β’ (π β (seq0( + , πΊ) β dom β β
seq1( + , πΊ) β dom
β )) |
151 | 22, 150 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (π β seq1( + , πΊ) β dom β
) |
152 | 1, 2, 124, 147, 151 | isumcl 15654 |
. . . . . . . . . . . . . 14
β’ (π β Ξ£π β β π΅ β β) |
153 | 152 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π) β Ξ£π β β π΅ β β) |
154 | 153 | abscld 15330 |
. . . . . . . . . . . 12
β’ ((π β§ π) β (absβΞ£π β β π΅) β
β) |
155 | 153 | absge0d 15338 |
. . . . . . . . . . . 12
β’ ((π β§ π) β 0 β€ (absβΞ£π β β π΅)) |
156 | | fimaxre2 12108 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β Fin) β βπ§ β β βπ€ β π π€ β€ π§) |
157 | 113, 117,
156 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π) β βπ§ β β βπ€ β π π€ β€ π§) |
158 | 113, 140,
157, 139 | suprubd 12125 |
. . . . . . . . . . . 12
β’ ((π β§ π) β (absβΞ£π β β π΅) β€ sup(π, β, < )) |
159 | 146, 154,
145, 155, 158 | letrd 11320 |
. . . . . . . . . . 11
β’ ((π β§ π) β 0 β€ sup(π, β, < )) |
160 | 145, 159 | ge0p1rpd 12995 |
. . . . . . . . . 10
β’ ((π β§ π) β (sup(π, β, < ) + 1) β
β+) |
161 | 90, 160 | rpdivcld 12982 |
. . . . . . . . 9
β’ ((π β§ π) β (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)) β
β+) |
162 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π = π β (πΎβπ) = (πΎβπ)) |
163 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π β β0
β¦ (πΎβπ)) = (π β β0 β¦ (πΎβπ)) |
164 | | fvex 6859 |
. . . . . . . . . . 11
β’ (πΎβπ) β V |
165 | 162, 163,
164 | fvmpt 6952 |
. . . . . . . . . 10
β’ (π β β0
β ((π β
β0 β¦ (πΎβπ))βπ) = (πΎβπ)) |
166 | 165 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π) β§ π β β0) β ((π β β0
β¦ (πΎβπ))βπ) = (πΎβπ)) |
167 | | nn0ex 12427 |
. . . . . . . . . . . . 13
β’
β0 β V |
168 | 167 | mptex 7177 |
. . . . . . . . . . . 12
β’ (π β β0
β¦ (πΎβπ)) β V |
169 | 168 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (π β β0 β¦ (πΎβπ)) β V) |
170 | | elnn0uz 12816 |
. . . . . . . . . . . . . 14
β’ (π β β0
β π β
(β€β₯β0)) |
171 | | fveq2 6846 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (πΎβπ) = (πΎβπ)) |
172 | | fvex 6859 |
. . . . . . . . . . . . . . . 16
β’ (πΎβπ) β V |
173 | 171, 163,
172 | fvmpt 6952 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β ((π β
β0 β¦ (πΎβπ))βπ) = (πΎβπ)) |
174 | 173 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β0) β ((π β β0
β¦ (πΎβπ))βπ) = (πΎβπ)) |
175 | 170, 174 | sylan2br 596 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β€β₯β0))
β ((π β
β0 β¦ (πΎβπ))βπ) = (πΎβπ)) |
176 | 6, 175 | seqfeq 13942 |
. . . . . . . . . . . 12
β’ (π β seq0( + , (π β β0
β¦ (πΎβπ))) = seq0( + , πΎ)) |
177 | 176, 12 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ (π β seq0( + , (π β β0
β¦ (πΎβπ))) β dom β
) |
178 | 174, 8 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β0) β ((π β β0
β¦ (πΎβπ))βπ) = (absβπ΄)) |
179 | 178, 10 | eqeltrd 2834 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β ((π β β0
β¦ (πΎβπ))βπ) β β) |
180 | 179 | recnd 11191 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β ((π β β0
β¦ (πΎβπ))βπ) β β) |
181 | 5, 6, 169, 177, 180 | serf0 15574 |
. . . . . . . . . 10
β’ (π β (π β β0 β¦ (πΎβπ)) β 0) |
182 | 181 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π) β (π β β0 β¦ (πΎβπ)) β 0) |
183 | 5, 85, 161, 166, 182 | climi0 15403 |
. . . . . . . 8
β’ ((π β§ π) β βπ‘ β β0 βπ β
(β€β₯βπ‘)(absβ(πΎβπ)) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1))) |
184 | | simplll 774 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π) β§ π‘ β β0) β§ π β
(β€β₯βπ‘)) β π) |
185 | | eluznn0 12850 |
. . . . . . . . . . . . . . 15
β’ ((π‘ β β0
β§ π β
(β€β₯βπ‘)) β π β β0) |
186 | 185 | adantll 713 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π) β§ π‘ β β0) β§ π β
(β€β₯βπ‘)) β π β β0) |
187 | 11, 15 | absidd 15316 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β0) β
(absβ(πΎβπ)) = (πΎβπ)) |
188 | 187 | ralrimiva 3140 |
. . . . . . . . . . . . . . 15
β’ (π β βπ β β0 (absβ(πΎβπ)) = (πΎβπ)) |
189 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (πΎβπ) = (πΎβπ)) |
190 | 189 | fveq2d 6850 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (absβ(πΎβπ)) = (absβ(πΎβπ))) |
191 | 190, 189 | eqeq12d 2749 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((absβ(πΎβπ)) = (πΎβπ) β (absβ(πΎβπ)) = (πΎβπ))) |
192 | 191 | rspccva 3582 |
. . . . . . . . . . . . . . 15
β’
((βπ β
β0 (absβ(πΎβπ)) = (πΎβπ) β§ π β β0) β
(absβ(πΎβπ)) = (πΎβπ)) |
193 | 188, 192 | sylan 581 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β0) β
(absβ(πΎβπ)) = (πΎβπ)) |
194 | 184, 186,
193 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π β§ π) β§ π‘ β β0) β§ π β
(β€β₯βπ‘)) β (absβ(πΎβπ)) = (πΎβπ)) |
195 | 194 | breq1d 5119 |
. . . . . . . . . . . 12
β’ ((((π β§ π) β§ π‘ β β0) β§ π β
(β€β₯βπ‘)) β ((absβ(πΎβπ)) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)) β (πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)))) |
196 | 195 | ralbidva 3169 |
. . . . . . . . . . 11
β’ (((π β§ π) β§ π‘ β β0) β
(βπ β
(β€β₯βπ‘)(absβ(πΎβπ)) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)) β βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)))) |
197 | 162 | breq1d 5119 |
. . . . . . . . . . . 12
β’ (π = π β ((πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)) β (πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)))) |
198 | 197 | cbvralvw 3224 |
. . . . . . . . . . 11
β’
(βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)) β βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1))) |
199 | 196, 198 | bitr4di 289 |
. . . . . . . . . 10
β’ (((π β§ π) β§ π‘ β β0) β
(βπ β
(β€β₯βπ‘)(absβ(πΎβπ)) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)) β βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)))) |
200 | | mertens.1 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β0) β (πΉβπ) = π΄) |
201 | 200 | ad4ant14 751 |
. . . . . . . . . . . 12
β’ ((((π β§ π) β§ (π‘ β β0 β§
βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)))) β§ π β β0)
β (πΉβπ) = π΄) |
202 | 8 | ad4ant14 751 |
. . . . . . . . . . . 12
β’ ((((π β§ π) β§ (π‘ β β0 β§
βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)))) β§ π β β0)
β (πΎβπ) = (absβπ΄)) |
203 | 9 | ad4ant14 751 |
. . . . . . . . . . . 12
β’ ((((π β§ π) β§ (π‘ β β0 β§
βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)))) β§ π β β0)
β π΄ β
β) |
204 | 20 | ad4ant14 751 |
. . . . . . . . . . . 12
β’ ((((π β§ π) β§ (π‘ β β0 β§
βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)))) β§ π β β0)
β (πΊβπ) = π΅) |
205 | 21 | ad4ant14 751 |
. . . . . . . . . . . 12
β’ ((((π β§ π) β§ (π‘ β β0 β§
βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)))) β§ π β β0)
β π΅ β
β) |
206 | | mertens.6 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β0) β (π»βπ) = Ξ£π β (0...π)(π΄ Β· (πΊβ(π β π)))) |
207 | 206 | ad4ant14 751 |
. . . . . . . . . . . 12
β’ ((((π β§ π) β§ (π‘ β β0 β§
βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)))) β§ π β β0)
β (π»βπ) = Ξ£π β (0...π)(π΄ Β· (πΊβ(π β π)))) |
208 | 12 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ (π‘ β β0 β§
βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)))) β seq0( + ,
πΎ) β dom β
) |
209 | 22 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ (π‘ β β0 β§
βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)))) β seq0( + ,
πΊ) β dom β
) |
210 | 3 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ (π‘ β β0 β§
βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)))) β πΈ β
β+) |
211 | 198 | anbi2i 624 |
. . . . . . . . . . . . . . 15
β’ ((π‘ β β0
β§ βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1))) β (π‘ β β0
β§ βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)))) |
212 | 211 | anbi2i 624 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π‘ β β0 β§
βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)))) β (π β§ (π‘ β β0 β§
βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1))))) |
213 | 212 | biimpi 215 |
. . . . . . . . . . . . 13
β’ ((π β§ (π‘ β β0 β§
βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)))) β (π β§ (π‘ β β0 β§
βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1))))) |
214 | 213 | adantll 713 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ (π‘ β β0 β§
βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)))) β (π β§ (π‘ β β0 β§
βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1))))) |
215 | 113, 140,
157 | 3jca 1129 |
. . . . . . . . . . . . . 14
β’ ((π β§ π) β (π β β β§ π β β
β§ βπ§ β β βπ€ β π π€ β€ π§)) |
216 | 159, 215 | jca 513 |
. . . . . . . . . . . . 13
β’ ((π β§ π) β (0 β€ sup(π, β, < ) β§ (π β β β§ π β β
β§ βπ§ β β βπ€ β π π€ β€ π§))) |
217 | 216 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ (π‘ β β0 β§
βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)))) β (0 β€
sup(π, β, < )
β§ (π β β
β§ π β β
β§
βπ§ β β
βπ€ β π π€ β€ π§))) |
218 | 201, 202,
203, 204, 205, 207, 208, 209, 210, 91, 84, 214, 217 | mertenslem1 15777 |
. . . . . . . . . . 11
β’ (((π β§ π) β§ (π‘ β β0 β§
βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)))) β
βπ¦ β
β0 βπ β (β€β₯βπ¦)(absβΞ£π β (0...π)(π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅)) < πΈ) |
219 | 218 | expr 458 |
. . . . . . . . . 10
β’ (((π β§ π) β§ π‘ β β0) β
(βπ β
(β€β₯βπ‘)(πΎβπ) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)) β βπ¦ β β0
βπ β
(β€β₯βπ¦)(absβΞ£π β (0...π)(π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅)) < πΈ)) |
220 | 199, 219 | sylbid 239 |
. . . . . . . . 9
β’ (((π β§ π) β§ π‘ β β0) β
(βπ β
(β€β₯βπ‘)(absβ(πΎβπ)) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)) β βπ¦ β β0
βπ β
(β€β₯βπ¦)(absβΞ£π β (0...π)(π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅)) < πΈ)) |
221 | 220 | rexlimdva 3149 |
. . . . . . . 8
β’ ((π β§ π) β (βπ‘ β β0 βπ β
(β€β₯βπ‘)(absβ(πΎβπ)) < (((πΈ / 2) / π ) / (sup(π, β, < ) + 1)) β βπ¦ β β0
βπ β
(β€β₯βπ¦)(absβΞ£π β (0...π)(π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅)) < πΈ)) |
222 | 183, 221 | mpd 15 |
. . . . . . 7
β’ ((π β§ π) β βπ¦ β β0 βπ β
(β€β₯βπ¦)(absβΞ£π β (0...π)(π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅)) < πΈ) |
223 | 222 | ex 414 |
. . . . . 6
β’ (π β (π β βπ¦ β β0 βπ β
(β€β₯βπ¦)(absβΞ£π β (0...π)(π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅)) < πΈ)) |
224 | 84, 223 | biimtrrid 242 |
. . . . 5
β’ (π β ((π β β β§ βπ β
(β€β₯βπ )(absβΞ£π β (β€β₯β(π + 1))(πΊβπ)) < ((πΈ / 2) / (Ξ£π β β0 (πΎβπ) + 1))) β βπ¦ β β0 βπ β
(β€β₯βπ¦)(absβΞ£π β (0...π)(π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅)) < πΈ)) |
225 | 224 | expdimp 454 |
. . . 4
β’ ((π β§ π β β) β (βπ β
(β€β₯βπ )(absβΞ£π β (β€β₯β(π + 1))(πΊβπ)) < ((πΈ / 2) / (Ξ£π β β0 (πΎβπ) + 1)) β βπ¦ β β0 βπ β
(β€β₯βπ¦)(absβΞ£π β (0...π)(π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅)) < πΈ)) |
226 | 83, 225 | sylbid 239 |
. . 3
β’ ((π β§ π β β) β (βπ β
(β€β₯βπ )(absβ((seq0( + , πΊ)βπ) β Ξ£π β β0 π΅)) < ((πΈ / 2) / (Ξ£π β β0 (πΎβπ) + 1)) β βπ¦ β β0 βπ β
(β€β₯βπ¦)(absβΞ£π β (0...π)(π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅)) < πΈ)) |
227 | 226 | rexlimdva 3149 |
. 2
β’ (π β (βπ β β βπ β (β€β₯βπ )(absβ((seq0( + , πΊ)βπ) β Ξ£π β β0 π΅)) < ((πΈ / 2) / (Ξ£π β β0 (πΎβπ) + 1)) β βπ¦ β β0 βπ β
(β€β₯βπ¦)(absβΞ£π β (0...π)(π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅)) < πΈ)) |
228 | 24, 227 | mpd 15 |
1
β’ (π β βπ¦ β β0 βπ β
(β€β₯βπ¦)(absβΞ£π β (0...π)(π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅)) < πΈ) |