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

Proof

Step Hyp Ref Expression
1 ioodvbdlimc1.a 
 |-  ( ph -> A e. RR )
2 ioodvbdlimc1.b 
 |-  ( ph -> B e. RR )
3 ioodvbdlimc1.f 
 |-  ( ph -> F : ( A (,) B ) --> RR )
4 ioodvbdlimc1.dmdv 
 |-  ( ph -> dom ( RR _D F ) = ( A (,) B ) )
5 ioodvbdlimc1.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 
 |-  ( 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 e. ( ZZ>= ` ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) |-> ( F ` ( A + ( 1 / j ) ) ) ) = ( k e. ( ZZ>= ` ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) |-> ( F ` ( A + ( 1 / k ) ) ) )
21 18 cbvmptv 
 |-  ( j e. ( ZZ>= ` ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) |-> ( A + ( 1 / j ) ) ) = ( k e. ( ZZ>= ` ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) |-> ( A + ( 1 / k ) ) )
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+ ) /\ k 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 ` ( ( ( j e. ( ZZ>= ` ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) |-> ( F ` ( A + ( 1 / j ) ) ) ) ` k ) - ( limsup ` ( j e. ( ZZ>= ` ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) |-> ( F ` ( A + ( 1 / j ) ) ) ) ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - A ) ) < ( 1 / k ) ) <-> ( ( ( ( ( ( ph /\ A < B ) /\ x e. RR+ ) /\ k 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 ` ( ( ( j e. ( ZZ>= ` ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) |-> ( F ` ( A + ( 1 / j ) ) ) ) ` k ) - ( limsup ` ( j e. ( ZZ>= ` ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) |-> ( F ` ( A + ( 1 / j ) ) ) ) ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - A ) ) < ( 1 / k ) ) )
24 6 7 8 9 10 11 15 16 20 21 22 23 ioodvbdlimc1lem2 
 |-  ( ( ph /\ A < B ) -> ( limsup ` ( j e. ( ZZ>= ` ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) |-> ( F ` ( A + ( 1 / j ) ) ) ) ) e. ( F limCC A ) )
25 24 ne0d 
 |-  ( ( ph /\ A < B ) -> ( F limCC A ) =/= (/) )
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 1 recnd 
 |-  ( ph -> A e. CC )
41 40 adantr 
 |-  ( ( ph /\ B <_ A ) -> A e. CC )
42 39 41 limcdm0 
 |-  ( ( ph /\ B <_ A ) -> ( F limCC A ) = 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 A ) =/= (/) )
47 25 46 1 2 ltlecasei 
 |-  ( ph -> ( F limCC A ) =/= (/) )