Step | Hyp | Ref
| Expression |
1 | | dvfsum.s |
. . . . . . 7
β’ π = (π(,)+β) |
2 | | ioossre 13385 |
. . . . . . 7
β’ (π(,)+β) β
β |
3 | 1, 2 | eqsstri 4017 |
. . . . . 6
β’ π β
β |
4 | | dvfsumrlim2.1 |
. . . . . 6
β’ (π β π β π) |
5 | 3, 4 | sselid 3981 |
. . . . 5
β’ (π β π β β) |
6 | 5 | rexrd 11264 |
. . . 4
β’ (π β π β
β*) |
7 | 5 | renepnfd 11265 |
. . . 4
β’ (π β π β +β) |
8 | | icopnfsup 13830 |
. . . 4
β’ ((π β β*
β§ π β +β)
β sup((π[,)+β),
β*, < ) = +β) |
9 | 6, 7, 8 | syl2anc 585 |
. . 3
β’ (π β sup((π[,)+β), β*, < ) =
+β) |
10 | 9 | adantr 482 |
. 2
β’ ((π β§ πΊ βπ πΏ) β sup((π[,)+β), β*, < ) =
+β) |
11 | | dvfsum.z |
. . . . . . . 8
β’ π =
(β€β₯βπ) |
12 | | dvfsum.m |
. . . . . . . 8
β’ (π β π β β€) |
13 | | dvfsum.d |
. . . . . . . 8
β’ (π β π· β β) |
14 | | dvfsum.md |
. . . . . . . 8
β’ (π β π β€ (π· + 1)) |
15 | | dvfsum.t |
. . . . . . . 8
β’ (π β π β β) |
16 | | dvfsum.a |
. . . . . . . 8
β’ ((π β§ π₯ β π) β π΄ β β) |
17 | | dvfsum.b1 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β π΅ β π) |
18 | | dvfsum.b2 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β π΅ β β) |
19 | | dvfsum.b3 |
. . . . . . . 8
β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) |
20 | | dvfsum.c |
. . . . . . . 8
β’ (π₯ = π β π΅ = πΆ) |
21 | | dvfsumrlim.g |
. . . . . . . 8
β’ πΊ = (π₯ β π β¦ (Ξ£π β (π...(ββπ₯))πΆ β π΄)) |
22 | 1, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21 | dvfsumrlimf 25542 |
. . . . . . 7
β’ (π β πΊ:πβΆβ) |
23 | 22 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ πΊ βπ πΏ) β§ π¦ β (π[,)+β)) β πΊ:πβΆβ) |
24 | 4 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ πΊ βπ πΏ) β§ π¦ β (π[,)+β)) β π β π) |
25 | 23, 24 | ffvelcdmd 7088 |
. . . . 5
β’ (((π β§ πΊ βπ πΏ) β§ π¦ β (π[,)+β)) β (πΊβπ) β β) |
26 | 25 | recnd 11242 |
. . . 4
β’ (((π β§ πΊ βπ πΏ) β§ π¦ β (π[,)+β)) β (πΊβπ) β β) |
27 | 15 | rexrd 11264 |
. . . . . . . . . 10
β’ (π β π β
β*) |
28 | 4, 1 | eleqtrdi 2844 |
. . . . . . . . . . . 12
β’ (π β π β (π(,)+β)) |
29 | | elioopnf 13420 |
. . . . . . . . . . . . 13
β’ (π β β*
β (π β (π(,)+β) β (π β β β§ π < π))) |
30 | 27, 29 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π β (π(,)+β) β (π β β β§ π < π))) |
31 | 28, 30 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β (π β β β§ π < π)) |
32 | 31 | simprd 497 |
. . . . . . . . . 10
β’ (π β π < π) |
33 | | df-ioo 13328 |
. . . . . . . . . . 11
β’ (,) =
(π’ β
β*, π£
β β* β¦ {π€ β β* β£ (π’ < π€ β§ π€ < π£)}) |
34 | | df-ico 13330 |
. . . . . . . . . . 11
β’ [,) =
(π’ β
β*, π£
β β* β¦ {π€ β β* β£ (π’ β€ π€ β§ π€ < π£)}) |
35 | | xrltletr 13136 |
. . . . . . . . . . 11
β’ ((π β β*
β§ π β
β* β§ π§
β β*) β ((π < π β§ π β€ π§) β π < π§)) |
36 | 33, 34, 35 | ixxss1 13342 |
. . . . . . . . . 10
β’ ((π β β*
β§ π < π) β (π[,)+β) β (π(,)+β)) |
37 | 27, 32, 36 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π[,)+β) β (π(,)+β)) |
38 | 37, 1 | sseqtrrdi 4034 |
. . . . . . . 8
β’ (π β (π[,)+β) β π) |
39 | 38 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΊ βπ πΏ) β (π[,)+β) β π) |
40 | 39 | sselda 3983 |
. . . . . 6
β’ (((π β§ πΊ βπ πΏ) β§ π¦ β (π[,)+β)) β π¦ β π) |
41 | 23, 40 | ffvelcdmd 7088 |
. . . . 5
β’ (((π β§ πΊ βπ πΏ) β§ π¦ β (π[,)+β)) β (πΊβπ¦) β β) |
42 | 41 | recnd 11242 |
. . . 4
β’ (((π β§ πΊ βπ πΏ) β§ π¦ β (π[,)+β)) β (πΊβπ¦) β β) |
43 | 26, 42 | subcld 11571 |
. . 3
β’ (((π β§ πΊ βπ πΏ) β§ π¦ β (π[,)+β)) β ((πΊβπ) β (πΊβπ¦)) β β) |
44 | | pnfxr 11268 |
. . . . . . 7
β’ +β
β β* |
45 | | icossre 13405 |
. . . . . . 7
β’ ((π β β β§ +β
β β*) β (π[,)+β) β
β) |
46 | 5, 44, 45 | sylancl 587 |
. . . . . 6
β’ (π β (π[,)+β) β
β) |
47 | 46 | adantr 482 |
. . . . 5
β’ ((π β§ πΊ βπ πΏ) β (π[,)+β) β
β) |
48 | | rlimf 15445 |
. . . . . . . 8
β’ (πΊ βπ
πΏ β πΊ:dom πΊβΆβ) |
49 | 48 | adantl 483 |
. . . . . . 7
β’ ((π β§ πΊ βπ πΏ) β πΊ:dom πΊβΆβ) |
50 | | ovex 7442 |
. . . . . . . . 9
β’
(Ξ£π β
(π...(ββπ₯))πΆ β π΄) β V |
51 | 50, 21 | dmmpti 6695 |
. . . . . . . 8
β’ dom πΊ = π |
52 | 51 | feq2i 6710 |
. . . . . . 7
β’ (πΊ:dom πΊβΆβ β πΊ:πβΆβ) |
53 | 49, 52 | sylib 217 |
. . . . . 6
β’ ((π β§ πΊ βπ πΏ) β πΊ:πβΆβ) |
54 | 4 | adantr 482 |
. . . . . 6
β’ ((π β§ πΊ βπ πΏ) β π β π) |
55 | 53, 54 | ffvelcdmd 7088 |
. . . . 5
β’ ((π β§ πΊ βπ πΏ) β (πΊβπ) β β) |
56 | | rlimconst 15488 |
. . . . 5
β’ (((π[,)+β) β β
β§ (πΊβπ) β β) β (π¦ β (π[,)+β) β¦ (πΊβπ)) βπ (πΊβπ)) |
57 | 47, 55, 56 | syl2anc 585 |
. . . 4
β’ ((π β§ πΊ βπ πΏ) β (π¦ β (π[,)+β) β¦ (πΊβπ)) βπ (πΊβπ)) |
58 | 53 | feqmptd 6961 |
. . . . . 6
β’ ((π β§ πΊ βπ πΏ) β πΊ = (π¦ β π β¦ (πΊβπ¦))) |
59 | | simpr 486 |
. . . . . 6
β’ ((π β§ πΊ βπ πΏ) β πΊ βπ πΏ) |
60 | 58, 59 | eqbrtrrd 5173 |
. . . . 5
β’ ((π β§ πΊ βπ πΏ) β (π¦ β π β¦ (πΊβπ¦)) βπ πΏ) |
61 | 39, 60 | rlimres2 15505 |
. . . 4
β’ ((π β§ πΊ βπ πΏ) β (π¦ β (π[,)+β) β¦ (πΊβπ¦)) βπ πΏ) |
62 | 26, 42, 57, 61 | rlimsub 15589 |
. . 3
β’ ((π β§ πΊ βπ πΏ) β (π¦ β (π[,)+β) β¦ ((πΊβπ) β (πΊβπ¦))) βπ ((πΊβπ) β πΏ)) |
63 | 43, 62 | rlimabs 15553 |
. 2
β’ ((π β§ πΊ βπ πΏ) β (π¦ β (π[,)+β) β¦ (absβ((πΊβπ) β (πΊβπ¦)))) βπ
(absβ((πΊβπ) β πΏ))) |
64 | 3 | a1i 11 |
. . . . . . . 8
β’ (π β π β β) |
65 | 64, 16, 17, 19 | dvmptrecl 25541 |
. . . . . . 7
β’ ((π β§ π₯ β π) β π΅ β β) |
66 | 65 | ralrimiva 3147 |
. . . . . 6
β’ (π β βπ₯ β π π΅ β β) |
67 | | nfcsb1v 3919 |
. . . . . . . 8
β’
β²π₯β¦π / π₯β¦π΅ |
68 | 67 | nfel1 2920 |
. . . . . . 7
β’
β²π₯β¦π / π₯β¦π΅ β β |
69 | | csbeq1a 3908 |
. . . . . . . 8
β’ (π₯ = π β π΅ = β¦π / π₯β¦π΅) |
70 | 69 | eleq1d 2819 |
. . . . . . 7
β’ (π₯ = π β (π΅ β β β β¦π / π₯β¦π΅ β β)) |
71 | 68, 70 | rspc 3601 |
. . . . . 6
β’ (π β π β (βπ₯ β π π΅ β β β β¦π / π₯β¦π΅ β β)) |
72 | 4, 66, 71 | sylc 65 |
. . . . 5
β’ (π β β¦π / π₯β¦π΅ β β) |
73 | 72 | recnd 11242 |
. . . 4
β’ (π β β¦π / π₯β¦π΅ β β) |
74 | | rlimconst 15488 |
. . . 4
β’ (((π[,)+β) β β
β§ β¦π /
π₯β¦π΅ β β) β (π¦ β (π[,)+β) β¦ β¦π / π₯β¦π΅) βπ
β¦π / π₯β¦π΅) |
75 | 46, 73, 74 | syl2anc 585 |
. . 3
β’ (π β (π¦ β (π[,)+β) β¦ β¦π / π₯β¦π΅) βπ
β¦π / π₯β¦π΅) |
76 | 75 | adantr 482 |
. 2
β’ ((π β§ πΊ βπ πΏ) β (π¦ β (π[,)+β) β¦ β¦π / π₯β¦π΅) βπ
β¦π / π₯β¦π΅) |
77 | 43 | abscld 15383 |
. 2
β’ (((π β§ πΊ βπ πΏ) β§ π¦ β (π[,)+β)) β (absβ((πΊβπ) β (πΊβπ¦))) β β) |
78 | 72 | ad2antrr 725 |
. 2
β’ (((π β§ πΊ βπ πΏ) β§ π¦ β (π[,)+β)) β β¦π / π₯β¦π΅ β β) |
79 | 26, 42 | abssubd 15400 |
. . 3
β’ (((π β§ πΊ βπ πΏ) β§ π¦ β (π[,)+β)) β (absβ((πΊβπ) β (πΊβπ¦))) = (absβ((πΊβπ¦) β (πΊβπ)))) |
80 | 12 | adantr 482 |
. . . . 5
β’ ((π β§ π¦ β (π[,)+β)) β π β β€) |
81 | 13 | adantr 482 |
. . . . 5
β’ ((π β§ π¦ β (π[,)+β)) β π· β β) |
82 | 14 | adantr 482 |
. . . . 5
β’ ((π β§ π¦ β (π[,)+β)) β π β€ (π· + 1)) |
83 | 15 | adantr 482 |
. . . . 5
β’ ((π β§ π¦ β (π[,)+β)) β π β β) |
84 | 16 | adantlr 714 |
. . . . 5
β’ (((π β§ π¦ β (π[,)+β)) β§ π₯ β π) β π΄ β β) |
85 | 17 | adantlr 714 |
. . . . 5
β’ (((π β§ π¦ β (π[,)+β)) β§ π₯ β π) β π΅ β π) |
86 | 18 | adantlr 714 |
. . . . 5
β’ (((π β§ π¦ β (π[,)+β)) β§ π₯ β π) β π΅ β β) |
87 | 19 | adantr 482 |
. . . . 5
β’ ((π β§ π¦ β (π[,)+β)) β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) |
88 | 44 | a1i 11 |
. . . . 5
β’ ((π β§ π¦ β (π[,)+β)) β +β β
β*) |
89 | | 3simpa 1149 |
. . . . . . 7
β’ ((π· β€ π₯ β§ π₯ β€ π β§ π β€ +β) β (π· β€ π₯ β§ π₯ β€ π)) |
90 | | dvfsumrlim.l |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π)) β πΆ β€ π΅) |
91 | 89, 90 | syl3an3 1166 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ +β)) β πΆ β€ π΅) |
92 | 91 | 3adant1r 1178 |
. . . . 5
β’ (((π β§ π¦ β (π[,)+β)) β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ +β)) β πΆ β€ π΅) |
93 | | dvfsumrlim.k |
. . . . . . . 8
β’ (π β (π₯ β π β¦ π΅) βπ
0) |
94 | 1, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 90, 21, 93 | dvfsumrlimge0 25547 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π· β€ π₯)) β 0 β€ π΅) |
95 | 94 | 3adantr3 1172 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π· β€ π₯ β§ π₯ β€ +β)) β 0 β€ π΅) |
96 | 95 | adantlr 714 |
. . . . 5
β’ (((π β§ π¦ β (π[,)+β)) β§ (π₯ β π β§ π· β€ π₯ β§ π₯ β€ +β)) β 0 β€ π΅) |
97 | 4 | adantr 482 |
. . . . 5
β’ ((π β§ π¦ β (π[,)+β)) β π β π) |
98 | 38 | sselda 3983 |
. . . . 5
β’ ((π β§ π¦ β (π[,)+β)) β π¦ β π) |
99 | | dvfsumrlim2.2 |
. . . . . 6
β’ (π β π· β€ π) |
100 | 99 | adantr 482 |
. . . . 5
β’ ((π β§ π¦ β (π[,)+β)) β π· β€ π) |
101 | | elicopnf 13422 |
. . . . . . 7
β’ (π β β β (π¦ β (π[,)+β) β (π¦ β β β§ π β€ π¦))) |
102 | 5, 101 | syl 17 |
. . . . . 6
β’ (π β (π¦ β (π[,)+β) β (π¦ β β β§ π β€ π¦))) |
103 | 102 | simplbda 501 |
. . . . 5
β’ ((π β§ π¦ β (π[,)+β)) β π β€ π¦) |
104 | 102 | simprbda 500 |
. . . . . . 7
β’ ((π β§ π¦ β (π[,)+β)) β π¦ β β) |
105 | 104 | rexrd 11264 |
. . . . . 6
β’ ((π β§ π¦ β (π[,)+β)) β π¦ β β*) |
106 | | pnfge 13110 |
. . . . . 6
β’ (π¦ β β*
β π¦ β€
+β) |
107 | 105, 106 | syl 17 |
. . . . 5
β’ ((π β§ π¦ β (π[,)+β)) β π¦ β€ +β) |
108 | 1, 11, 80, 81, 82, 83, 84, 85, 86, 87, 20, 88, 92, 21, 96, 97, 98, 100, 103, 107 | dvfsumlem4 25546 |
. . . 4
β’ ((π β§ π¦ β (π[,)+β)) β (absβ((πΊβπ¦) β (πΊβπ))) β€ β¦π / π₯β¦π΅) |
109 | 108 | adantlr 714 |
. . 3
β’ (((π β§ πΊ βπ πΏ) β§ π¦ β (π[,)+β)) β (absβ((πΊβπ¦) β (πΊβπ))) β€ β¦π / π₯β¦π΅) |
110 | 79, 109 | eqbrtrd 5171 |
. 2
β’ (((π β§ πΊ βπ πΏ) β§ π¦ β (π[,)+β)) β (absβ((πΊβπ) β (πΊβπ¦))) β€ β¦π / π₯β¦π΅) |
111 | 10, 63, 76, 77, 78, 110 | rlimle 15594 |
1
β’ ((π β§ πΊ βπ πΏ) β (absβ((πΊβπ) β πΏ)) β€ β¦π / π₯β¦π΅) |