Metamath Proof Explorer

Theorem unbdqndv2

Description: Variant of unbdqndv1 with the hypothesis that ( ( ( Fy ) - ( Fx ) ) / ( y - x ) ) is unbounded where x <_ A and A <_ y . (Contributed by Asger C. Ipsen, 12-May-2021)

Ref Expression
Hypotheses unbdqndv2.x 
|- ( ph -> X C_ RR )
unbdqndv2.f 
|- ( ph -> F : X --> CC )
unbdqndv2.1 
|- ( ph -> A. b e. RR+ A. d e. RR+ E. x e. X E. y e. X ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ b <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) )
Assertion unbdqndv2 
|- ( ph -> -. A e. dom ( RR _D F ) )

Proof

Step Hyp Ref Expression
1 unbdqndv2.x 
 |-  ( ph -> X C_ RR )
2 unbdqndv2.f 
 |-  ( ph -> F : X --> CC )
3 unbdqndv2.1 
 |-  ( ph -> A. b e. RR+ A. d e. RR+ E. x e. X E. y e. X ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ b <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) )
4 eqid 
 |-  ( z e. ( X \ { A } ) |-> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) ) = ( z e. ( X \ { A } ) |-> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) )
5 ax-resscn 
 |-  RR C_ CC
6 5 a1i 
 |-  ( ( ph /\ A e. dom ( RR _D F ) ) -> RR C_ CC )
7 1 adantr 
 |-  ( ( ph /\ A e. dom ( RR _D F ) ) -> X C_ RR )
8 2 adantr 
 |-  ( ( ph /\ A e. dom ( RR _D F ) ) -> F : X --> CC )
9 breq1 
 |-  ( b = ( 2 x. c ) -> ( b <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) <-> ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) )
10 9 3anbi3d 
 |-  ( b = ( 2 x. c ) -> ( ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ b <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) <-> ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) ) )
11 10 rexbidv 
 |-  ( b = ( 2 x. c ) -> ( E. y e. X ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ b <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) <-> E. y e. X ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) ) )
12 11 rexbidv 
 |-  ( b = ( 2 x. c ) -> ( E. x e. X E. y e. X ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ b <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) <-> E. x e. X E. y e. X ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) ) )
13 12 ralbidv 
 |-  ( b = ( 2 x. c ) -> ( A. d e. RR+ E. x e. X E. y e. X ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ b <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) <-> A. d e. RR+ E. x e. X E. y e. X ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) ) )
14 3 ad2antrr 
 |-  ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> A. b e. RR+ A. d e. RR+ E. x e. X E. y e. X ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ b <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) )
15 2rp 
 |-  2 e. RR+
16 15 a1i 
 |-  ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> 2 e. RR+ )
17 simprl 
 |-  ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> c e. RR+ )
18 16 17 rpmulcld 
 |-  ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> ( 2 x. c ) e. RR+ )
19 13 14 18 rspcdva 
 |-  ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> A. d e. RR+ E. x e. X E. y e. X ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) )
20 simprr 
 |-  ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> d e. RR+ )
21 rsp 
 |-  ( A. d e. RR+ E. x e. X E. y e. X ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) -> ( d e. RR+ -> E. x e. X E. y e. X ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) ) )
22 19 20 21 sylc 
 |-  ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> E. x e. X E. y e. X ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) )
23 eqid 
 |-  if ( ( c x. ( y - x ) ) <_ ( abs ` ( ( F ` x ) - ( F ` A ) ) ) , x , y ) = if ( ( c x. ( y - x ) ) <_ ( abs ` ( ( F ` x ) - ( F ` A ) ) ) , x , y )
24 7 ad3antrrr 
 |-  ( ( ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. X /\ y e. X ) ) /\ ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) ) -> X C_ RR )
25 8 ad3antrrr 
 |-  ( ( ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. X /\ y e. X ) ) /\ ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) ) -> F : X --> CC )
26 6 8 7 dvbss 
 |-  ( ( ph /\ A e. dom ( RR _D F ) ) -> dom ( RR _D F ) C_ X )
27 simpr 
 |-  ( ( ph /\ A e. dom ( RR _D F ) ) -> A e. dom ( RR _D F ) )
28 26 27 sseldd 
 |-  ( ( ph /\ A e. dom ( RR _D F ) ) -> A e. X )
29 28 adantr 
 |-  ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> A e. X )
30 29 adantr 
 |-  ( ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. X /\ y e. X ) ) -> A e. X )
31 30 adantr 
 |-  ( ( ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. X /\ y e. X ) ) /\ ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) ) -> A e. X )
32 17 ad2antrr 
 |-  ( ( ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. X /\ y e. X ) ) /\ ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) ) -> c e. RR+ )
33 20 ad2antrr 
 |-  ( ( ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. X /\ y e. X ) ) /\ ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) ) -> d e. RR+ )
34 simplrl 
 |-  ( ( ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. X /\ y e. X ) ) /\ ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) ) -> x e. X )
35 simplrr 
 |-  ( ( ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. X /\ y e. X ) ) /\ ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) ) -> y e. X )
36 simpr2r 
 |-  ( ( ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. X /\ y e. X ) ) /\ ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) ) -> x =/= y )
37 simpr1l 
 |-  ( ( ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. X /\ y e. X ) ) /\ ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) ) -> x <_ A )
38 simpr1r 
 |-  ( ( ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. X /\ y e. X ) ) /\ ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) ) -> A <_ y )
39 simpr2l 
 |-  ( ( ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. X /\ y e. X ) ) /\ ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) ) -> ( y - x ) < d )
40 simpr3 
 |-  ( ( ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. X /\ y e. X ) ) /\ ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) ) -> ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) )
41 4 23 24 25 31 32 33 34 35 36 37 38 39 40 unbdqndv2lem2 
 |-  ( ( ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. X /\ y e. X ) ) /\ ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) ) -> ( if ( ( c x. ( y - x ) ) <_ ( abs ` ( ( F ` x ) - ( F ` A ) ) ) , x , y ) e. ( X \ { A } ) /\ ( ( abs ` ( if ( ( c x. ( y - x ) ) <_ ( abs ` ( ( F ` x ) - ( F ` A ) ) ) , x , y ) - A ) ) < d /\ c <_ ( abs ` ( ( z e. ( X \ { A } ) |-> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) ) ` if ( ( c x. ( y - x ) ) <_ ( abs ` ( ( F ` x ) - ( F ` A ) ) ) , x , y ) ) ) ) ) )
42 41 simpld 
 |-  ( ( ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. X /\ y e. X ) ) /\ ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) ) -> if ( ( c x. ( y - x ) ) <_ ( abs ` ( ( F ` x ) - ( F ` A ) ) ) , x , y ) e. ( X \ { A } ) )
43 fvoveq1 
 |-  ( w = if ( ( c x. ( y - x ) ) <_ ( abs ` ( ( F ` x ) - ( F ` A ) ) ) , x , y ) -> ( abs ` ( w - A ) ) = ( abs ` ( if ( ( c x. ( y - x ) ) <_ ( abs ` ( ( F ` x ) - ( F ` A ) ) ) , x , y ) - A ) ) )
44 43 breq1d 
 |-  ( w = if ( ( c x. ( y - x ) ) <_ ( abs ` ( ( F ` x ) - ( F ` A ) ) ) , x , y ) -> ( ( abs ` ( w - A ) ) < d <-> ( abs ` ( if ( ( c x. ( y - x ) ) <_ ( abs ` ( ( F ` x ) - ( F ` A ) ) ) , x , y ) - A ) ) < d ) )
45 2fveq3 
 |-  ( w = if ( ( c x. ( y - x ) ) <_ ( abs ` ( ( F ` x ) - ( F ` A ) ) ) , x , y ) -> ( abs ` ( ( z e. ( X \ { A } ) |-> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) ) ` w ) ) = ( abs ` ( ( z e. ( X \ { A } ) |-> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) ) ` if ( ( c x. ( y - x ) ) <_ ( abs ` ( ( F ` x ) - ( F ` A ) ) ) , x , y ) ) ) )
46 45 breq2d 
 |-  ( w = if ( ( c x. ( y - x ) ) <_ ( abs ` ( ( F ` x ) - ( F ` A ) ) ) , x , y ) -> ( c <_ ( abs ` ( ( z e. ( X \ { A } ) |-> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) ) ` w ) ) <-> c <_ ( abs ` ( ( z e. ( X \ { A } ) |-> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) ) ` if ( ( c x. ( y - x ) ) <_ ( abs ` ( ( F ` x ) - ( F ` A ) ) ) , x , y ) ) ) ) )
47 44 46 anbi12d 
 |-  ( w = if ( ( c x. ( y - x ) ) <_ ( abs ` ( ( F ` x ) - ( F ` A ) ) ) , x , y ) -> ( ( ( abs ` ( w - A ) ) < d /\ c <_ ( abs ` ( ( z e. ( X \ { A } ) |-> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) ) ` w ) ) ) <-> ( ( abs ` ( if ( ( c x. ( y - x ) ) <_ ( abs ` ( ( F ` x ) - ( F ` A ) ) ) , x , y ) - A ) ) < d /\ c <_ ( abs ` ( ( z e. ( X \ { A } ) |-> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) ) ` if ( ( c x. ( y - x ) ) <_ ( abs ` ( ( F ` x ) - ( F ` A ) ) ) , x , y ) ) ) ) ) )
48 47 adantl 
 |-  ( ( ( ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. X /\ y e. X ) ) /\ ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) ) /\ w = if ( ( c x. ( y - x ) ) <_ ( abs ` ( ( F ` x ) - ( F ` A ) ) ) , x , y ) ) -> ( ( ( abs ` ( w - A ) ) < d /\ c <_ ( abs ` ( ( z e. ( X \ { A } ) |-> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) ) ` w ) ) ) <-> ( ( abs ` ( if ( ( c x. ( y - x ) ) <_ ( abs ` ( ( F ` x ) - ( F ` A ) ) ) , x , y ) - A ) ) < d /\ c <_ ( abs ` ( ( z e. ( X \ { A } ) |-> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) ) ` if ( ( c x. ( y - x ) ) <_ ( abs ` ( ( F ` x ) - ( F ` A ) ) ) , x , y ) ) ) ) ) )
49 41 simprd 
 |-  ( ( ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. X /\ y e. X ) ) /\ ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) ) -> ( ( abs ` ( if ( ( c x. ( y - x ) ) <_ ( abs ` ( ( F ` x ) - ( F ` A ) ) ) , x , y ) - A ) ) < d /\ c <_ ( abs ` ( ( z e. ( X \ { A } ) |-> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) ) ` if ( ( c x. ( y - x ) ) <_ ( abs ` ( ( F ` x ) - ( F ` A ) ) ) , x , y ) ) ) ) )
50 42 48 49 rspcedvd 
 |-  ( ( ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. X /\ y e. X ) ) /\ ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) ) -> E. w e. ( X \ { A } ) ( ( abs ` ( w - A ) ) < d /\ c <_ ( abs ` ( ( z e. ( X \ { A } ) |-> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) ) ` w ) ) ) )
51 50 ex 
 |-  ( ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. X /\ y e. X ) ) -> ( ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) -> E. w e. ( X \ { A } ) ( ( abs ` ( w - A ) ) < d /\ c <_ ( abs ` ( ( z e. ( X \ { A } ) |-> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) ) ` w ) ) ) ) )
52 51 rexlimdvva 
 |-  ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> ( E. x e. X E. y e. X ( ( x <_ A /\ A <_ y ) /\ ( ( y - x ) < d /\ x =/= y ) /\ ( 2 x. c ) <_ ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( y - x ) ) ) -> E. w e. ( X \ { A } ) ( ( abs ` ( w - A ) ) < d /\ c <_ ( abs ` ( ( z e. ( X \ { A } ) |-> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) ) ` w ) ) ) ) )
53 22 52 mpd 
 |-  ( ( ( ph /\ A e. dom ( RR _D F ) ) /\ ( c e. RR+ /\ d e. RR+ ) ) -> E. w e. ( X \ { A } ) ( ( abs ` ( w - A ) ) < d /\ c <_ ( abs ` ( ( z e. ( X \ { A } ) |-> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) ) ` w ) ) ) )
54 53 ralrimivva 
 |-  ( ( ph /\ A e. dom ( RR _D F ) ) -> A. c e. RR+ A. d e. RR+ E. w e. ( X \ { A } ) ( ( abs ` ( w - A ) ) < d /\ c <_ ( abs ` ( ( z e. ( X \ { A } ) |-> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) ) ` w ) ) ) )
55 4 6 7 8 54 unbdqndv1 
 |-  ( ( ph /\ A e. dom ( RR _D F ) ) -> -. A e. dom ( RR _D F ) )
56 55 pm2.01da 
 |-  ( ph -> -. A e. dom ( RR _D F ) )