Metamath Proof Explorer


Theorem ioodvbdlimc1

Description: A real function with bounded derivative, has a limit at the upper bound of an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Proof shortened by AV, 3-Oct-2020)

Ref Expression
Hypotheses ioodvbdlimc1.a φ A
ioodvbdlimc1.b φ B
ioodvbdlimc1.f φ F : A B
ioodvbdlimc1.dmdv φ dom F = A B
ioodvbdlimc1.dvbd φ y x A B F x y
Assertion ioodvbdlimc1 φ F lim A

Proof

Step Hyp Ref Expression
1 ioodvbdlimc1.a φ A
2 ioodvbdlimc1.b φ B
3 ioodvbdlimc1.f φ F : A B
4 ioodvbdlimc1.dmdv φ dom F = A B
5 ioodvbdlimc1.dvbd φ y x A B F x y
6 1 adantr φ A < B A
7 2 adantr φ A < B B
8 simpr φ A < B A < B
9 3 adantr φ A < B F : A B
10 4 adantr φ A < B dom F = A B
11 5 adantr φ A < B y x A B F x y
12 2fveq3 y = x F y = F x
13 12 cbvmptv y A B F y = x A B F x
14 13 rneqi ran y A B F y = ran x A B F x
15 14 supeq1i sup ran y A B F y < = sup ran x A B F x <
16 eqid 1 B A + 1 = 1 B A + 1
17 oveq2 j = k 1 j = 1 k
18 17 oveq2d j = k A + 1 j = A + 1 k
19 18 fveq2d j = k F A + 1 j = F A + 1 k
20 19 cbvmptv j 1 B A + 1 F A + 1 j = k 1 B A + 1 F A + 1 k
21 18 cbvmptv j 1 B A + 1 A + 1 j = k 1 B A + 1 A + 1 k
22 eqid if 1 B A + 1 sup ran y A B F y < x 2 + 1 sup ran y A B F y < x 2 + 1 1 B A + 1 = if 1 B A + 1 sup ran y A B F y < x 2 + 1 sup ran y A B F y < x 2 + 1 1 B A + 1
23 biid φ A < B x + k if 1 B A + 1 sup ran y A B F y < x 2 + 1 sup ran y A B F y < x 2 + 1 1 B A + 1 j 1 B A + 1 F A + 1 j k lim sup j 1 B A + 1 F A + 1 j < x 2 z A B z A < 1 k φ A < B x + k if 1 B A + 1 sup ran y A B F y < x 2 + 1 sup ran y A B F y < x 2 + 1 1 B A + 1 j 1 B A + 1 F A + 1 j k lim sup j 1 B A + 1 F A + 1 j < x 2 z A B z A < 1 k
24 6 7 8 9 10 11 15 16 20 21 22 23 ioodvbdlimc1lem2 φ A < B lim sup j 1 B A + 1 F A + 1 j F lim A
25 24 ne0d φ A < B F lim A
26 ax-resscn
27 26 a1i φ
28 3 27 fssd φ F : A B
29 28 adantr φ B A F : A B
30 simpr φ B A B A
31 1 rexrd φ A *
32 31 adantr φ B A A *
33 2 rexrd φ B *
34 33 adantr φ B A B *
35 ioo0 A * B * A B = B A
36 32 34 35 syl2anc φ B A A B = B A
37 30 36 mpbird φ B A A B =
38 37 feq2d φ B A F : A B F :
39 29 38 mpbid φ B A F :
40 1 recnd φ A
41 40 adantr φ B A A
42 39 41 limcdm0 φ B A F lim A =
43 0cn 0
44 43 ne0ii
45 44 a1i φ B A
46 42 45 eqnetrd φ B A F lim A
47 25 46 1 2 ltlecasei φ F lim A