Metamath Proof Explorer


Theorem ioodvbdlimc2

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 ioodvbdlimc2.a
|- ( ph -> A e. RR )
ioodvbdlimc2.b
|- ( ph -> B e. RR )
ioodvbdlimc2.f
|- ( ph -> F : ( A (,) B ) --> RR )
ioodvbdlimc2.dmdv
|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
ioodvbdlimc2.dvbd
|- ( ph -> E. y e. RR A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ y )
Assertion ioodvbdlimc2
|- ( ph -> ( F limCC B ) =/= (/) )

Proof

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