Step | Hyp | Ref
| Expression |
1 | | nn0uz 12812 |
. 2
β’
β0 = (β€β₯β0) |
2 | | 0zd 12518 |
. 2
β’ (π β 0 β
β€) |
3 | | seqex 13915 |
. . 3
β’ seq0( + ,
π») β
V |
4 | 3 | a1i 11 |
. 2
β’ (π β seq0( + , π») β V) |
5 | | mertens.6 |
. . . . 5
β’ ((π β§ π β β0) β (π»βπ) = Ξ£π β (0...π)(π΄ Β· (πΊβ(π β π)))) |
6 | | fzfid 13885 |
. . . . . 6
β’ ((π β§ π β β0) β
(0...π) β
Fin) |
7 | | simpl 484 |
. . . . . . . 8
β’ ((π β§ π β β0) β π) |
8 | | elfznn0 13541 |
. . . . . . . 8
β’ (π β (0...π) β π β β0) |
9 | | mertens.3 |
. . . . . . . 8
β’ ((π β§ π β β0) β π΄ β
β) |
10 | 7, 8, 9 | syl2an 597 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π β (0...π)) β π΄ β β) |
11 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = (π β π) β (πΊβπ) = (πΊβ(π β π))) |
12 | 11 | eleq1d 2823 |
. . . . . . . 8
β’ (π = (π β π) β ((πΊβπ) β β β (πΊβ(π β π)) β β)) |
13 | | mertens.4 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β (πΊβπ) = π΅) |
14 | | mertens.5 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β π΅ β
β) |
15 | 13, 14 | eqeltrd 2838 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β (πΊβπ) β β) |
16 | 15 | ralrimiva 3144 |
. . . . . . . . . 10
β’ (π β βπ β β0 (πΊβπ) β β) |
17 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π β (πΊβπ) = (πΊβπ)) |
18 | 17 | eleq1d 2823 |
. . . . . . . . . . 11
β’ (π = π β ((πΊβπ) β β β (πΊβπ) β β)) |
19 | 18 | cbvralvw 3228 |
. . . . . . . . . 10
β’
(βπ β
β0 (πΊβπ) β β β βπ β β0
(πΊβπ) β β) |
20 | 16, 19 | sylib 217 |
. . . . . . . . 9
β’ (π β βπ β β0 (πΊβπ) β β) |
21 | 20 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ π β (0...π)) β βπ β β0 (πΊβπ) β β) |
22 | | fznn0sub 13480 |
. . . . . . . . 9
β’ (π β (0...π) β (π β π) β
β0) |
23 | 22 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ π β (0...π)) β (π β π) β
β0) |
24 | 12, 21, 23 | rspcdva 3585 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π β (0...π)) β (πΊβ(π β π)) β β) |
25 | 10, 24 | mulcld 11182 |
. . . . . 6
β’ (((π β§ π β β0) β§ π β (0...π)) β (π΄ Β· (πΊβ(π β π))) β β) |
26 | 6, 25 | fsumcl 15625 |
. . . . 5
β’ ((π β§ π β β0) β
Ξ£π β (0...π)(π΄ Β· (πΊβ(π β π))) β β) |
27 | 5, 26 | eqeltrd 2838 |
. . . 4
β’ ((π β§ π β β0) β (π»βπ) β β) |
28 | 1, 2, 27 | serf 13943 |
. . 3
β’ (π β seq0( + , π»):β0βΆβ) |
29 | 28 | ffvelcdmda 7040 |
. 2
β’ ((π β§ π β β0) β (seq0( +
, π»)βπ) β
β) |
30 | | mertens.1 |
. . . . . 6
β’ ((π β§ π β β0) β (πΉβπ) = π΄) |
31 | 30 | adantlr 714 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β β0)
β (πΉβπ) = π΄) |
32 | | mertens.2 |
. . . . . 6
β’ ((π β§ π β β0) β (πΎβπ) = (absβπ΄)) |
33 | 32 | adantlr 714 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β β0)
β (πΎβπ) = (absβπ΄)) |
34 | 9 | adantlr 714 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β β0)
β π΄ β
β) |
35 | 13 | adantlr 714 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β β0)
β (πΊβπ) = π΅) |
36 | 14 | adantlr 714 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β β0)
β π΅ β
β) |
37 | 5 | adantlr 714 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β β0)
β (π»βπ) = Ξ£π β (0...π)(π΄ Β· (πΊβ(π β π)))) |
38 | | mertens.7 |
. . . . . 6
β’ (π β seq0( + , πΎ) β dom β
) |
39 | 38 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β β+) β seq0( + ,
πΎ) β dom β
) |
40 | | mertens.8 |
. . . . . 6
β’ (π β seq0( + , πΊ) β dom β
) |
41 | 40 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β β+) β seq0( + ,
πΊ) β dom β
) |
42 | | simpr 486 |
. . . . 5
β’ ((π β§ π₯ β β+) β π₯ β
β+) |
43 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π β (πΊβπ) = (πΊβπ)) |
44 | 43 | cbvsumv 15588 |
. . . . . . . . . . 11
β’
Ξ£π β
(β€β₯β(π + 1))(πΊβπ) = Ξ£π β (β€β₯β(π + 1))(πΊβπ) |
45 | | fvoveq1 7385 |
. . . . . . . . . . . 12
β’ (π = π β (β€β₯β(π + 1)) =
(β€β₯β(π + 1))) |
46 | 45 | sumeq1d 15593 |
. . . . . . . . . . 11
β’ (π = π β Ξ£π β (β€β₯β(π + 1))(πΊβπ) = Ξ£π β (β€β₯β(π + 1))(πΊβπ)) |
47 | 44, 46 | eqtrid 2789 |
. . . . . . . . . 10
β’ (π = π β Ξ£π β (β€β₯β(π + 1))(πΊβπ) = Ξ£π β (β€β₯β(π + 1))(πΊβπ)) |
48 | 47 | fveq2d 6851 |
. . . . . . . . 9
β’ (π = π β (absβΞ£π β (β€β₯β(π + 1))(πΊβπ)) = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ))) |
49 | 48 | eqeq2d 2748 |
. . . . . . . 8
β’ (π = π β (π’ = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ)) β π’ = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ)))) |
50 | 49 | cbvrexvw 3229 |
. . . . . . 7
β’
(βπ β
(0...(π β 1))π’ = (absβΞ£π β
(β€β₯β(π + 1))(πΊβπ)) β βπ β (0...(π β 1))π’ = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ))) |
51 | | eqeq1 2741 |
. . . . . . . 8
β’ (π’ = π§ β (π’ = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ)) β π§ = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ)))) |
52 | 51 | rexbidv 3176 |
. . . . . . 7
β’ (π’ = π§ β (βπ β (0...(π β 1))π’ = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ)) β βπ β (0...(π β 1))π§ = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ)))) |
53 | 50, 52 | bitrid 283 |
. . . . . 6
β’ (π’ = π§ β (βπ β (0...(π β 1))π’ = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ)) β βπ β (0...(π β 1))π§ = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ)))) |
54 | 53 | cbvabv 2810 |
. . . . 5
β’ {π’ β£ βπ β (0...(π β 1))π’ = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ))} = {π§ β£ βπ β (0...(π β 1))π§ = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ))} |
55 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π β (πΎβπ) = (πΎβπ)) |
56 | 55 | cbvsumv 15588 |
. . . . . . . . . . 11
β’
Ξ£π β
β0 (πΎβπ) = Ξ£π β β0 (πΎβπ) |
57 | 56 | oveq1i 7372 |
. . . . . . . . . 10
β’
(Ξ£π β
β0 (πΎβπ) + 1) = (Ξ£π β β0 (πΎβπ) + 1) |
58 | 57 | oveq2i 7373 |
. . . . . . . . 9
β’ ((π₯ / 2) / (Ξ£π β β0
(πΎβπ) + 1)) = ((π₯ / 2) / (Ξ£π β β0 (πΎβπ) + 1)) |
59 | 58 | breq2i 5118 |
. . . . . . . 8
β’
((absβΞ£π
β (β€β₯β(π’ + 1))(πΊβπ)) < ((π₯ / 2) / (Ξ£π β β0 (πΎβπ) + 1)) β (absβΞ£π β
(β€β₯β(π’ + 1))(πΊβπ)) < ((π₯ / 2) / (Ξ£π β β0 (πΎβπ) + 1))) |
60 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π β (πΊβπ) = (πΊβπ)) |
61 | 60 | cbvsumv 15588 |
. . . . . . . . . . 11
β’
Ξ£π β
(β€β₯β(π’ + 1))(πΊβπ) = Ξ£π β (β€β₯β(π’ + 1))(πΊβπ) |
62 | | fvoveq1 7385 |
. . . . . . . . . . . 12
β’ (π’ = π β (β€β₯β(π’ + 1)) =
(β€β₯β(π + 1))) |
63 | 62 | sumeq1d 15593 |
. . . . . . . . . . 11
β’ (π’ = π β Ξ£π β (β€β₯β(π’ + 1))(πΊβπ) = Ξ£π β (β€β₯β(π + 1))(πΊβπ)) |
64 | 61, 63 | eqtrid 2789 |
. . . . . . . . . 10
β’ (π’ = π β Ξ£π β (β€β₯β(π’ + 1))(πΊβπ) = Ξ£π β (β€β₯β(π + 1))(πΊβπ)) |
65 | 64 | fveq2d 6851 |
. . . . . . . . 9
β’ (π’ = π β (absβΞ£π β (β€β₯β(π’ + 1))(πΊβπ)) = (absβΞ£π β (β€β₯β(π + 1))(πΊβπ))) |
66 | 65 | breq1d 5120 |
. . . . . . . 8
β’ (π’ = π β ((absβΞ£π β (β€β₯β(π’ + 1))(πΊβπ)) < ((π₯ / 2) / (Ξ£π β β0 (πΎβπ) + 1)) β (absβΞ£π β
(β€β₯β(π + 1))(πΊβπ)) < ((π₯ / 2) / (Ξ£π β β0 (πΎβπ) + 1)))) |
67 | 59, 66 | bitrid 283 |
. . . . . . 7
β’ (π’ = π β ((absβΞ£π β (β€β₯β(π’ + 1))(πΊβπ)) < ((π₯ / 2) / (Ξ£π β β0 (πΎβπ) + 1)) β (absβΞ£π β
(β€β₯β(π + 1))(πΊβπ)) < ((π₯ / 2) / (Ξ£π β β0 (πΎβπ) + 1)))) |
68 | 67 | cbvralvw 3228 |
. . . . . 6
β’
(βπ’ β
(β€β₯βπ )(absβΞ£π β (β€β₯β(π’ + 1))(πΊβπ)) < ((π₯ / 2) / (Ξ£π β β0 (πΎβπ) + 1)) β βπ β (β€β₯βπ )(absβΞ£π β
(β€β₯β(π + 1))(πΊβπ)) < ((π₯ / 2) / (Ξ£π β β0 (πΎβπ) + 1))) |
69 | 68 | anbi2i 624 |
. . . . 5
β’ ((π β β β§
βπ’ β
(β€β₯βπ )(absβΞ£π β (β€β₯β(π’ + 1))(πΊβπ)) < ((π₯ / 2) / (Ξ£π β β0 (πΎβπ) + 1))) β (π β β β§ βπ β
(β€β₯βπ )(absβΞ£π β (β€β₯β(π + 1))(πΊβπ)) < ((π₯ / 2) / (Ξ£π β β0 (πΎβπ) + 1)))) |
70 | 31, 33, 34, 35, 36, 37, 39, 41, 42, 54, 69 | mertenslem2 15777 |
. . . 4
β’ ((π β§ π₯ β β+) β
βπ¦ β
β0 βπ β (β€β₯βπ¦)(absβΞ£π β (0...π)(π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅)) < π₯) |
71 | | eluznn0 12849 |
. . . . . . . . 9
β’ ((π¦ β β0
β§ π β
(β€β₯βπ¦)) β π β β0) |
72 | | fzfid 13885 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β0) β
(0...π) β
Fin) |
73 | | simpll 766 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ π β (0...π)) β π) |
74 | | elfznn0 13541 |
. . . . . . . . . . . . . . 15
β’ (π β (0...π) β π β β0) |
75 | 74 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ π β (0...π)) β π β β0) |
76 | 1, 2, 13, 14, 40 | isumcl 15653 |
. . . . . . . . . . . . . . . 16
β’ (π β Ξ£π β β0 π΅ β β) |
77 | 76 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β0) β
Ξ£π β
β0 π΅
β β) |
78 | 30, 9 | eqeltrd 2838 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β0) β (πΉβπ) β β) |
79 | 77, 78 | mulcld 11182 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β0) β
(Ξ£π β
β0 π΅
Β· (πΉβπ)) β
β) |
80 | 73, 75, 79 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ π β (0...π)) β (Ξ£π β β0 π΅ Β· (πΉβπ)) β β) |
81 | | fzfid 13885 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ π β (0...π)) β (0...(π β π)) β Fin) |
82 | | simplll 774 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β β0) β§ π β (0...π)) β§ π β (0...(π β π))) β π) |
83 | 74 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β β0) β§ π β (0...π)) β§ π β (0...(π β π))) β π β β0) |
84 | 82, 83, 9 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β β0) β§ π β (0...π)) β§ π β (0...(π β π))) β π΄ β β) |
85 | | elfznn0 13541 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0...(π β π)) β π β β0) |
86 | 85 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β β0) β§ π β (0...π)) β§ π β (0...(π β π))) β π β β0) |
87 | 82, 86, 15 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β β0) β§ π β (0...π)) β§ π β (0...(π β π))) β (πΊβπ) β β) |
88 | 84, 87 | mulcld 11182 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β0) β§ π β (0...π)) β§ π β (0...(π β π))) β (π΄ Β· (πΊβπ)) β β) |
89 | 81, 88 | fsumcl 15625 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ π β (0...π)) β Ξ£π β (0...(π β π))(π΄ Β· (πΊβπ)) β β) |
90 | 72, 80, 89 | fsumsub 15680 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β
Ξ£π β (0...π)((Ξ£π β β0 π΅ Β· (πΉβπ)) β Ξ£π β (0...(π β π))(π΄ Β· (πΊβπ))) = (Ξ£π β (0...π)(Ξ£π β β0 π΅ Β· (πΉβπ)) β Ξ£π β (0...π)Ξ£π β (0...(π β π))(π΄ Β· (πΊβπ)))) |
91 | 73, 75, 9 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ π β (0...π)) β π΄ β β) |
92 | 76 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ π β (0...π)) β Ξ£π β β0 π΅ β β) |
93 | 81, 87 | fsumcl 15625 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ π β (0...π)) β Ξ£π β (0...(π β π))(πΊβπ) β β) |
94 | 91, 92, 93 | subdid 11618 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ π β (0...π)) β (π΄ Β· (Ξ£π β β0 π΅ β Ξ£π β (0...(π β π))(πΊβπ))) = ((π΄ Β· Ξ£π β β0 π΅) β (π΄ Β· Ξ£π β (0...(π β π))(πΊβπ)))) |
95 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’
(β€β₯β((π β π) + 1)) =
(β€β₯β((π β π) + 1)) |
96 | | fznn0sub 13480 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (0...π) β (π β π) β
β0) |
97 | 96 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β0) β§ π β (0...π)) β (π β π) β
β0) |
98 | | peano2nn0 12460 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β π) β β0 β ((π β π) + 1) β
β0) |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β0) β§ π β (0...π)) β ((π β π) + 1) β
β0) |
100 | 99 | nn0zd 12532 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β0) β§ π β (0...π)) β ((π β π) + 1) β β€) |
101 | | simplll 774 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β β0) β§ π β (0...π)) β§ π β (β€β₯β((π β π) + 1))) β π) |
102 | | eluznn0 12849 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β π) + 1) β β0 β§ π β
(β€β₯β((π β π) + 1))) β π β β0) |
103 | 99, 102 | sylan 581 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β β0) β§ π β (0...π)) β§ π β (β€β₯β((π β π) + 1))) β π β β0) |
104 | 101, 103,
13 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β β0) β§ π β (0...π)) β§ π β (β€β₯β((π β π) + 1))) β (πΊβπ) = π΅) |
105 | 101, 103,
14 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β β0) β§ π β (0...π)) β§ π β (β€β₯β((π β π) + 1))) β π΅ β β) |
106 | 40 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β0) β§ π β (0...π)) β seq0( + , πΊ) β dom β ) |
107 | 73, 13 | sylan 581 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β β0) β§ π β (0...π)) β§ π β β0) β (πΊβπ) = π΅) |
108 | 73, 14 | sylan 581 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β β0) β§ π β (0...π)) β§ π β β0) β π΅ β
β) |
109 | 107, 108 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β β0) β§ π β (0...π)) β§ π β β0) β (πΊβπ) β β) |
110 | 1, 99, 109 | iserex 15548 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β0) β§ π β (0...π)) β (seq0( + , πΊ) β dom β β seq((π β π) + 1)( + , πΊ) β dom β )) |
111 | 106, 110 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β0) β§ π β (0...π)) β seq((π β π) + 1)( + , πΊ) β dom β ) |
112 | 95, 100, 104, 105, 111 | isumcl 15653 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β0) β§ π β (0...π)) β Ξ£π β (β€β₯β((π β π) + 1))π΅ β β) |
113 | 1, 95, 99, 107, 108, 106 | isumsplit 15732 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β0) β§ π β (0...π)) β Ξ£π β β0 π΅ = (Ξ£π β (0...(((π β π) + 1) β 1))π΅ + Ξ£π β (β€β₯β((π β π) + 1))π΅)) |
114 | 97 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β0) β§ π β (0...π)) β (π β π) β β) |
115 | | ax-1cn 11116 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 1 β
β |
116 | | pncan 11414 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β π) β β β§ 1 β β)
β (((π β π) + 1) β 1) = (π β π)) |
117 | 114, 115,
116 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β0) β§ π β (0...π)) β (((π β π) + 1) β 1) = (π β π)) |
118 | 117 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β0) β§ π β (0...π)) β (0...(((π β π) + 1) β 1)) = (0...(π β π))) |
119 | 118 | sumeq1d 15593 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β0) β§ π β (0...π)) β Ξ£π β (0...(((π β π) + 1) β 1))π΅ = Ξ£π β (0...(π β π))π΅) |
120 | 82, 86, 13 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β β0) β§ π β (0...π)) β§ π β (0...(π β π))) β (πΊβπ) = π΅) |
121 | 120 | sumeq2dv 15595 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β0) β§ π β (0...π)) β Ξ£π β (0...(π β π))(πΊβπ) = Ξ£π β (0...(π β π))π΅) |
122 | 119, 121 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β0) β§ π β (0...π)) β Ξ£π β (0...(((π β π) + 1) β 1))π΅ = Ξ£π β (0...(π β π))(πΊβπ)) |
123 | 122 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β0) β§ π β (0...π)) β (Ξ£π β (0...(((π β π) + 1) β 1))π΅ + Ξ£π β (β€β₯β((π β π) + 1))π΅) = (Ξ£π β (0...(π β π))(πΊβπ) + Ξ£π β (β€β₯β((π β π) + 1))π΅)) |
124 | 113, 123 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β0) β§ π β (0...π)) β Ξ£π β β0 π΅ = (Ξ£π β (0...(π β π))(πΊβπ) + Ξ£π β (β€β₯β((π β π) + 1))π΅)) |
125 | 93, 112, 124 | mvrladdd 11575 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ π β (0...π)) β (Ξ£π β β0 π΅ β Ξ£π β (0...(π β π))(πΊβπ)) = Ξ£π β (β€β₯β((π β π) + 1))π΅) |
126 | 125 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ π β (0...π)) β (π΄ Β· (Ξ£π β β0 π΅ β Ξ£π β (0...(π β π))(πΊβπ))) = (π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅)) |
127 | 9, 77 | mulcomd 11183 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β0) β (π΄ Β· Ξ£π β β0
π΅) = (Ξ£π β β0
π΅ Β· π΄)) |
128 | 30 | oveq2d 7378 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β0) β
(Ξ£π β
β0 π΅
Β· (πΉβπ)) = (Ξ£π β β0 π΅ Β· π΄)) |
129 | 127, 128 | eqtr4d 2780 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β0) β (π΄ Β· Ξ£π β β0
π΅) = (Ξ£π β β0
π΅ Β· (πΉβπ))) |
130 | 73, 75, 129 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ π β (0...π)) β (π΄ Β· Ξ£π β β0 π΅) = (Ξ£π β β0 π΅ Β· (πΉβπ))) |
131 | 81, 91, 87 | fsummulc2 15676 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ π β (0...π)) β (π΄ Β· Ξ£π β (0...(π β π))(πΊβπ)) = Ξ£π β (0...(π β π))(π΄ Β· (πΊβπ))) |
132 | 130, 131 | oveq12d 7380 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ π β (0...π)) β ((π΄ Β· Ξ£π β β0 π΅) β (π΄ Β· Ξ£π β (0...(π β π))(πΊβπ))) = ((Ξ£π β β0 π΅ Β· (πΉβπ)) β Ξ£π β (0...(π β π))(π΄ Β· (πΊβπ)))) |
133 | 94, 126, 132 | 3eqtr3rd 2786 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ π β (0...π)) β ((Ξ£π β β0 π΅ Β· (πΉβπ)) β Ξ£π β (0...(π β π))(π΄ Β· (πΊβπ))) = (π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅)) |
134 | 133 | sumeq2dv 15595 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β
Ξ£π β (0...π)((Ξ£π β β0 π΅ Β· (πΉβπ)) β Ξ£π β (0...(π β π))(π΄ Β· (πΊβπ))) = Ξ£π β (0...π)(π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅)) |
135 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (πΉβπ) = (πΉβπ)) |
136 | 135 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (Ξ£π β β0 π΅ Β· (πΉβπ)) = (Ξ£π β β0 π΅ Β· (πΉβπ))) |
137 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β¦ (Ξ£π β
β0 π΅
Β· (πΉβπ))) = (π β β0 β¦
(Ξ£π β
β0 π΅
Β· (πΉβπ))) |
138 | | ovex 7395 |
. . . . . . . . . . . . . . . 16
β’
(Ξ£π β
β0 π΅
Β· (πΉβπ)) β V |
139 | 136, 137,
138 | fvmpt 6953 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β ((π β
β0 β¦ (Ξ£π β β0 π΅ Β· (πΉβπ)))βπ) = (Ξ£π β β0 π΅ Β· (πΉβπ))) |
140 | 75, 139 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ π β (0...π)) β ((π β β0 β¦
(Ξ£π β
β0 π΅
Β· (πΉβπ)))βπ) = (Ξ£π β β0 π΅ Β· (πΉβπ))) |
141 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β0) β π β
β0) |
142 | 141, 1 | eleqtrdi 2848 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β0) β π β
(β€β₯β0)) |
143 | 140, 142,
80 | fsumser 15622 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β0) β
Ξ£π β (0...π)(Ξ£π β β0 π΅ Β· (πΉβπ)) = (seq0( + , (π β β0 β¦
(Ξ£π β
β0 π΅
Β· (πΉβπ))))βπ)) |
144 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (πΊβπ) = (πΊβπ)) |
145 | 144 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π΄ Β· (πΊβπ)) = (π΄ Β· (πΊβπ))) |
146 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’ (π = (π β π) β (πΊβπ) = (πΊβ(π β π))) |
147 | 146 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (π = (π β π) β (π΄ Β· (πΊβπ)) = (π΄ Β· (πΊβ(π β π)))) |
148 | 88 | anasss 468 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (π β (0...π) β§ π β (0...(π β π)))) β (π΄ Β· (πΊβπ)) β β) |
149 | 145, 147,
148 | fsum0diag2 15675 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β0) β
Ξ£π β (0...π)Ξ£π β (0...(π β π))(π΄ Β· (πΊβπ)) = Ξ£π β (0...π)Ξ£π β (0...π)(π΄ Β· (πΊβ(π β π)))) |
150 | | simpll 766 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β0) β§ π β (0...π)) β π) |
151 | | elfznn0 13541 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0...π) β π β β0) |
152 | 151 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β0) β§ π β (0...π)) β π β β0) |
153 | 150, 152,
5 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ π β (0...π)) β (π»βπ) = Ξ£π β (0...π)(π΄ Β· (πΊβ(π β π)))) |
154 | 150, 152,
26 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ π β (0...π)) β Ξ£π β (0...π)(π΄ Β· (πΊβ(π β π))) β β) |
155 | 153, 142,
154 | fsumser 15622 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β0) β
Ξ£π β (0...π)Ξ£π β (0...π)(π΄ Β· (πΊβ(π β π))) = (seq0( + , π»)βπ)) |
156 | 149, 155 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β0) β
Ξ£π β (0...π)Ξ£π β (0...(π β π))(π΄ Β· (πΊβπ)) = (seq0( + , π»)βπ)) |
157 | 143, 156 | oveq12d 7380 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β
(Ξ£π β (0...π)(Ξ£π β β0 π΅ Β· (πΉβπ)) β Ξ£π β (0...π)Ξ£π β (0...(π β π))(π΄ Β· (πΊβπ))) = ((seq0( + , (π β β0 β¦
(Ξ£π β
β0 π΅
Β· (πΉβπ))))βπ) β (seq0( + , π»)βπ))) |
158 | 90, 134, 157 | 3eqtr3rd 2786 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β ((seq0( +
, (π β
β0 β¦ (Ξ£π β β0 π΅ Β· (πΉβπ))))βπ) β (seq0( + , π»)βπ)) = Ξ£π β (0...π)(π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅)) |
159 | 158 | fveq2d 6851 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β
(absβ((seq0( + , (π
β β0 β¦ (Ξ£π β β0 π΅ Β· (πΉβπ))))βπ) β (seq0( + , π»)βπ))) = (absβΞ£π β (0...π)(π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅))) |
160 | 159 | breq1d 5120 |
. . . . . . . . 9
β’ ((π β§ π β β0) β
((absβ((seq0( + , (π
β β0 β¦ (Ξ£π β β0 π΅ Β· (πΉβπ))))βπ) β (seq0( + , π»)βπ))) < π₯ β (absβΞ£π β (0...π)(π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅)) < π₯)) |
161 | 71, 160 | sylan2 594 |
. . . . . . . 8
β’ ((π β§ (π¦ β β0 β§ π β
(β€β₯βπ¦))) β ((absβ((seq0( + , (π β β0
β¦ (Ξ£π β
β0 π΅
Β· (πΉβπ))))βπ) β (seq0( + , π»)βπ))) < π₯ β (absβΞ£π β (0...π)(π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅)) < π₯)) |
162 | 161 | anassrs 469 |
. . . . . . 7
β’ (((π β§ π¦ β β0) β§ π β
(β€β₯βπ¦)) β ((absβ((seq0( + , (π β β0
β¦ (Ξ£π β
β0 π΅
Β· (πΉβπ))))βπ) β (seq0( + , π»)βπ))) < π₯ β (absβΞ£π β (0...π)(π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅)) < π₯)) |
163 | 162 | ralbidva 3173 |
. . . . . 6
β’ ((π β§ π¦ β β0) β
(βπ β
(β€β₯βπ¦)(absβ((seq0( + , (π β β0 β¦
(Ξ£π β
β0 π΅
Β· (πΉβπ))))βπ) β (seq0( + , π»)βπ))) < π₯ β βπ β (β€β₯βπ¦)(absβΞ£π β (0...π)(π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅)) < π₯)) |
164 | 163 | rexbidva 3174 |
. . . . 5
β’ (π β (βπ¦ β β0 βπ β
(β€β₯βπ¦)(absβ((seq0( + , (π β β0 β¦
(Ξ£π β
β0 π΅
Β· (πΉβπ))))βπ) β (seq0( + , π»)βπ))) < π₯ β βπ¦ β β0 βπ β
(β€β₯βπ¦)(absβΞ£π β (0...π)(π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅)) < π₯)) |
165 | 164 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β β+) β
(βπ¦ β
β0 βπ β (β€β₯βπ¦)(absβ((seq0( + , (π β β0
β¦ (Ξ£π β
β0 π΅
Β· (πΉβπ))))βπ) β (seq0( + , π»)βπ))) < π₯ β βπ¦ β β0 βπ β
(β€β₯βπ¦)(absβΞ£π β (0...π)(π΄ Β· Ξ£π β (β€β₯β((π β π) + 1))π΅)) < π₯)) |
166 | 70, 165 | mpbird 257 |
. . 3
β’ ((π β§ π₯ β β+) β
βπ¦ β
β0 βπ β (β€β₯βπ¦)(absβ((seq0( + , (π β β0
β¦ (Ξ£π β
β0 π΅
Β· (πΉβπ))))βπ) β (seq0( + , π»)βπ))) < π₯) |
167 | 166 | ralrimiva 3144 |
. 2
β’ (π β βπ₯ β β+ βπ¦ β β0
βπ β
(β€β₯βπ¦)(absβ((seq0( + , (π β β0 β¦
(Ξ£π β
β0 π΅
Β· (πΉβπ))))βπ) β (seq0( + , π»)βπ))) < π₯) |
168 | 30 | fveq2d 6851 |
. . . . . . 7
β’ ((π β§ π β β0) β
(absβ(πΉβπ)) = (absβπ΄)) |
169 | 32, 168 | eqtr4d 2780 |
. . . . . 6
β’ ((π β§ π β β0) β (πΎβπ) = (absβ(πΉβπ))) |
170 | 1, 2, 169, 78, 38 | abscvgcvg 15711 |
. . . . 5
β’ (π β seq0( + , πΉ) β dom β
) |
171 | 1, 2, 30, 9, 170 | isumclim2 15650 |
. . . 4
β’ (π β seq0( + , πΉ) β Ξ£π β β0
π΄) |
172 | 78 | ralrimiva 3144 |
. . . . 5
β’ (π β βπ β β0 (πΉβπ) β β) |
173 | | fveq2 6847 |
. . . . . . 7
β’ (π = π β (πΉβπ) = (πΉβπ)) |
174 | 173 | eleq1d 2823 |
. . . . . 6
β’ (π = π β ((πΉβπ) β β β (πΉβπ) β β)) |
175 | 174 | rspccva 3583 |
. . . . 5
β’
((βπ β
β0 (πΉβπ) β β β§ π β β0) β (πΉβπ) β β) |
176 | 172, 175 | sylan 581 |
. . . 4
β’ ((π β§ π β β0) β (πΉβπ) β β) |
177 | | fveq2 6847 |
. . . . . . 7
β’ (π = π β (πΉβπ) = (πΉβπ)) |
178 | 177 | oveq2d 7378 |
. . . . . 6
β’ (π = π β (Ξ£π β β0 π΅ Β· (πΉβπ)) = (Ξ£π β β0 π΅ Β· (πΉβπ))) |
179 | | ovex 7395 |
. . . . . 6
β’
(Ξ£π β
β0 π΅
Β· (πΉβπ)) β V |
180 | 178, 137,
179 | fvmpt 6953 |
. . . . 5
β’ (π β β0
β ((π β
β0 β¦ (Ξ£π β β0 π΅ Β· (πΉβπ)))βπ) = (Ξ£π β β0 π΅ Β· (πΉβπ))) |
181 | 180 | adantl 483 |
. . . 4
β’ ((π β§ π β β0) β ((π β β0
β¦ (Ξ£π β
β0 π΅
Β· (πΉβπ)))βπ) = (Ξ£π β β0 π΅ Β· (πΉβπ))) |
182 | 1, 2, 76, 171, 176, 181 | isermulc2 15549 |
. . 3
β’ (π β seq0( + , (π β β0
β¦ (Ξ£π β
β0 π΅
Β· (πΉβπ)))) β (Ξ£π β β0
π΅ Β· Ξ£π β β0
π΄)) |
183 | 1, 2, 30, 9, 170 | isumcl 15653 |
. . . 4
β’ (π β Ξ£π β β0 π΄ β β) |
184 | 76, 183 | mulcomd 11183 |
. . 3
β’ (π β (Ξ£π β β0 π΅ Β· Ξ£π β β0 π΄) = (Ξ£π β β0 π΄ Β· Ξ£π β β0 π΅)) |
185 | 182, 184 | breqtrd 5136 |
. 2
β’ (π β seq0( + , (π β β0
β¦ (Ξ£π β
β0 π΅
Β· (πΉβπ)))) β (Ξ£π β β0
π΄ Β· Ξ£π β β0
π΅)) |
186 | 1, 2, 4, 29, 167, 185 | 2clim 15461 |
1
β’ (π β seq0( + , π») β (Ξ£π β β0
π΄ Β· Ξ£π β β0
π΅)) |