Step | Hyp | Ref
| Expression |
1 | | ioodvbdlimc1.a |
. . . . 5
β’ (π β π΄ β β) |
2 | 1 | adantr 482 |
. . . 4
β’ ((π β§ π΄ < π΅) β π΄ β β) |
3 | | ioodvbdlimc1.b |
. . . . 5
β’ (π β π΅ β β) |
4 | 3 | adantr 482 |
. . . 4
β’ ((π β§ π΄ < π΅) β π΅ β β) |
5 | | simpr 486 |
. . . 4
β’ ((π β§ π΄ < π΅) β π΄ < π΅) |
6 | | ioodvbdlimc1.f |
. . . . 5
β’ (π β πΉ:(π΄(,)π΅)βΆβ) |
7 | 6 | adantr 482 |
. . . 4
β’ ((π β§ π΄ < π΅) β πΉ:(π΄(,)π΅)βΆβ) |
8 | | ioodvbdlimc1.dmdv |
. . . . 5
β’ (π β dom (β D πΉ) = (π΄(,)π΅)) |
9 | 8 | adantr 482 |
. . . 4
β’ ((π β§ π΄ < π΅) β dom (β D πΉ) = (π΄(,)π΅)) |
10 | | ioodvbdlimc1.dvbd |
. . . . 5
β’ (π β βπ¦ β β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π¦) |
11 | 10 | adantr 482 |
. . . 4
β’ ((π β§ π΄ < π΅) β βπ¦ β β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π¦) |
12 | | 2fveq3 6851 |
. . . . . . 7
β’ (π¦ = π₯ β (absβ((β D πΉ)βπ¦)) = (absβ((β D πΉ)βπ₯))) |
13 | 12 | cbvmptv 5222 |
. . . . . 6
β’ (π¦ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ¦))) = (π₯ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ₯))) |
14 | 13 | rneqi 5896 |
. . . . 5
β’ ran
(π¦ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ¦))) = ran (π₯ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ₯))) |
15 | 14 | supeq1i 9391 |
. . . 4
β’ sup(ran
(π¦ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ¦))), β, < ) = sup(ran (π₯ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ₯))), β, < ) |
16 | | eqid 2733 |
. . . 4
β’
((ββ(1 / (π΅ β π΄))) + 1) = ((ββ(1 / (π΅ β π΄))) + 1) |
17 | | oveq2 7369 |
. . . . . . 7
β’ (π = π β (1 / π) = (1 / π)) |
18 | 17 | oveq2d 7377 |
. . . . . 6
β’ (π = π β (π΄ + (1 / π)) = (π΄ + (1 / π))) |
19 | 18 | fveq2d 6850 |
. . . . 5
β’ (π = π β (πΉβ(π΄ + (1 / π))) = (πΉβ(π΄ + (1 / π)))) |
20 | 19 | cbvmptv 5222 |
. . . 4
β’ (π β
(β€β₯β((ββ(1 / (π΅ β π΄))) + 1)) β¦ (πΉβ(π΄ + (1 / π)))) = (π β
(β€β₯β((ββ(1 / (π΅ β π΄))) + 1)) β¦ (πΉβ(π΄ + (1 / π)))) |
21 | 18 | cbvmptv 5222 |
. . . 4
β’ (π β
(β€β₯β((ββ(1 / (π΅ β π΄))) + 1)) β¦ (π΄ + (1 / π))) = (π β
(β€β₯β((ββ(1 / (π΅ β π΄))) + 1)) β¦ (π΄ + (1 / π))) |
22 | | eqid 2733 |
. . . 4
β’
if(((ββ(1 / (π΅ β π΄))) + 1) β€ ((ββ(sup(ran
(π¦ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ¦))), β, < ) / (π₯ / 2))) + 1), ((ββ(sup(ran (π¦ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ¦))), β, < ) / (π₯ / 2))) + 1), ((ββ(1 / (π΅ β π΄))) + 1)) = if(((ββ(1 / (π΅ β π΄))) + 1) β€ ((ββ(sup(ran
(π¦ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ¦))), β, < ) / (π₯ / 2))) + 1), ((ββ(sup(ran (π¦ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ¦))), β, < ) / (π₯ / 2))) + 1), ((ββ(1 / (π΅ β π΄))) + 1)) |
23 | | biid 261 |
. . . 4
β’
(((((((π β§ π΄ < π΅) β§ π₯ β β+) β§ π β
(β€β₯βif(((ββ(1 / (π΅ β π΄))) + 1) β€ ((ββ(sup(ran
(π¦ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ¦))), β, < ) / (π₯ / 2))) + 1), ((ββ(sup(ran (π¦ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ¦))), β, < ) / (π₯ / 2))) + 1), ((ββ(1 / (π΅ β π΄))) + 1)))) β§ (absβ(((π β
(β€β₯β((ββ(1 / (π΅ β π΄))) + 1)) β¦ (πΉβ(π΄ + (1 / π))))βπ) β (lim supβ(π β
(β€β₯β((ββ(1 / (π΅ β π΄))) + 1)) β¦ (πΉβ(π΄ + (1 / π))))))) < (π₯ / 2)) β§ π§ β (π΄(,)π΅)) β§ (absβ(π§ β π΄)) < (1 / π)) β ((((((π β§ π΄ < π΅) β§ π₯ β β+) β§ π β
(β€β₯βif(((ββ(1 / (π΅ β π΄))) + 1) β€ ((ββ(sup(ran
(π¦ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ¦))), β, < ) / (π₯ / 2))) + 1), ((ββ(sup(ran (π¦ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ¦))), β, < ) / (π₯ / 2))) + 1), ((ββ(1 / (π΅ β π΄))) + 1)))) β§ (absβ(((π β
(β€β₯β((ββ(1 / (π΅ β π΄))) + 1)) β¦ (πΉβ(π΄ + (1 / π))))βπ) β (lim supβ(π β
(β€β₯β((ββ(1 / (π΅ β π΄))) + 1)) β¦ (πΉβ(π΄ + (1 / π))))))) < (π₯ / 2)) β§ π§ β (π΄(,)π΅)) β§ (absβ(π§ β π΄)) < (1 / π))) |
24 | 2, 4, 5, 7, 9, 11,
15, 16, 20, 21, 22, 23 | ioodvbdlimc1lem2 44263 |
. . 3
β’ ((π β§ π΄ < π΅) β (lim supβ(π β
(β€β₯β((ββ(1 / (π΅ β π΄))) + 1)) β¦ (πΉβ(π΄ + (1 / π))))) β (πΉ limβ π΄)) |
25 | 24 | ne0d 4299 |
. 2
β’ ((π β§ π΄ < π΅) β (πΉ limβ π΄) β β
) |
26 | | ax-resscn 11116 |
. . . . . . . 8
β’ β
β β |
27 | 26 | a1i 11 |
. . . . . . 7
β’ (π β β β
β) |
28 | 6, 27 | fssd 6690 |
. . . . . 6
β’ (π β πΉ:(π΄(,)π΅)βΆβ) |
29 | 28 | adantr 482 |
. . . . 5
β’ ((π β§ π΅ β€ π΄) β πΉ:(π΄(,)π΅)βΆβ) |
30 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π΅ β€ π΄) β π΅ β€ π΄) |
31 | 1 | rexrd 11213 |
. . . . . . . . 9
β’ (π β π΄ β
β*) |
32 | 31 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π΅ β€ π΄) β π΄ β
β*) |
33 | 3 | rexrd 11213 |
. . . . . . . . 9
β’ (π β π΅ β
β*) |
34 | 33 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π΅ β€ π΄) β π΅ β
β*) |
35 | | ioo0 13298 |
. . . . . . . 8
β’ ((π΄ β β*
β§ π΅ β
β*) β ((π΄(,)π΅) = β
β π΅ β€ π΄)) |
36 | 32, 34, 35 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π΅ β€ π΄) β ((π΄(,)π΅) = β
β π΅ β€ π΄)) |
37 | 30, 36 | mpbird 257 |
. . . . . 6
β’ ((π β§ π΅ β€ π΄) β (π΄(,)π΅) = β
) |
38 | 37 | feq2d 6658 |
. . . . 5
β’ ((π β§ π΅ β€ π΄) β (πΉ:(π΄(,)π΅)βΆβ β πΉ:β
βΆβ)) |
39 | 29, 38 | mpbid 231 |
. . . 4
β’ ((π β§ π΅ β€ π΄) β πΉ:β
βΆβ) |
40 | 1 | recnd 11191 |
. . . . 5
β’ (π β π΄ β β) |
41 | 40 | adantr 482 |
. . . 4
β’ ((π β§ π΅ β€ π΄) β π΄ β β) |
42 | 39, 41 | limcdm0 43949 |
. . 3
β’ ((π β§ π΅ β€ π΄) β (πΉ limβ π΄) = β) |
43 | | 0cn 11155 |
. . . . 5
β’ 0 β
β |
44 | 43 | ne0ii 4301 |
. . . 4
β’ β
β β
|
45 | 44 | a1i 11 |
. . 3
β’ ((π β§ π΅ β€ π΄) β β β
β
) |
46 | 42, 45 | eqnetrd 3008 |
. 2
β’ ((π β§ π΅ β€ π΄) β (πΉ limβ π΄) β β
) |
47 | 25, 46, 1, 3 | ltlecasei 11271 |
1
β’ (π β (πΉ limβ π΄) β β
) |