Metamath Proof Explorer

Theorem unbdqndv1

Description: If the difference quotient ( ( ( Fz ) - ( FA ) ) / ( z - A ) ) is unbounded near A then F is not differentiable at A . (Contributed by Asger C. Ipsen, 12-May-2021)

Ref Expression
Hypotheses unbdqndv1.g 
|- G = ( z e. ( X \ { A } ) |-> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) )
unbdqndv1.1 
|- ( ph -> S C_ CC )
unbdqndv1.2 
|- ( ph -> X C_ S )
unbdqndv1.3 
|- ( ph -> F : X --> CC )
unbdqndv1.4 
|- ( ph -> A. b e. RR+ A. d e. RR+ E. x e. ( X \ { A } ) ( ( abs ` ( x - A ) ) < d /\ b <_ ( abs ` ( G ` x ) ) ) )
Assertion unbdqndv1 
|- ( ph -> -. A e. dom ( S _D F ) )

Proof

Step Hyp Ref Expression
1 unbdqndv1.g 
 |-  G = ( z e. ( X \ { A } ) |-> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) )
2 unbdqndv1.1 
 |-  ( ph -> S C_ CC )
3 unbdqndv1.2 
 |-  ( ph -> X C_ S )
4 unbdqndv1.3 
 |-  ( ph -> F : X --> CC )
5 unbdqndv1.4 
 |-  ( ph -> A. b e. RR+ A. d e. RR+ E. x e. ( X \ { A } ) ( ( abs ` ( x - A ) ) < d /\ b <_ ( abs ` ( G ` x ) ) ) )
6 noel 
 |-  -. y e. (/)
7 6 a1i 
 |-  ( ( ph /\ A e. dom ( S _D F ) ) -> -. y e. (/) )
8 3 2 sstrd 
 |-  ( ph -> X C_ CC )
9 8 adantr 
 |-  ( ( ph /\ A e. dom ( S _D F ) ) -> X C_ CC )
10 9 ssdifssd 
 |-  ( ( ph /\ A e. dom ( S _D F ) ) -> ( X \ { A } ) C_ CC )
11 4 adantr 
 |-  ( ( ph /\ A e. dom ( S _D F ) ) -> F : X --> CC )
12 2 4 3 dvbss 
 |-  ( ph -> dom ( S _D F ) C_ X )
13 12 sselda 
 |-  ( ( ph /\ A e. dom ( S _D F ) ) -> A e. X )
14 11 9 13 dvlem 
 |-  ( ( ( ph /\ A e. dom ( S _D F ) ) /\ z e. ( X \ { A } ) ) -> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) e. CC )
15 14 1 fmptd 
 |-  ( ( ph /\ A e. dom ( S _D F ) ) -> G : ( X \ { A } ) --> CC )
16 9 13 sseldd 
 |-  ( ( ph /\ A e. dom ( S _D F ) ) -> A e. CC )
17 5 adantr 
 |-  ( ( ph /\ A e. dom ( S _D F ) ) -> A. b e. RR+ A. d e. RR+ E. x e. ( X \ { A } ) ( ( abs ` ( x - A ) ) < d /\ b <_ ( abs ` ( G ` x ) ) ) )
18 10 15 16 17 unblimceq0 
 |-  ( ( ph /\ A e. dom ( S _D F ) ) -> ( G limCC A ) = (/) )
19 7 18 neleqtrrd 
 |-  ( ( ph /\ A e. dom ( S _D F ) ) -> -. y e. ( G limCC A ) )
20 19 intnand 
 |-  ( ( ph /\ A e. dom ( S _D F ) ) -> -. ( A e. ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) /\ y e. ( G limCC A ) ) )
21 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t S ) = ( ( TopOpen ` CCfld ) |`t S )
22 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
23 21 22 1 2 4 3 eldv 
 |-  ( ph -> ( A ( S _D F ) y <-> ( A e. ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) /\ y e. ( G limCC A ) ) ) )
24 23 notbid 
 |-  ( ph -> ( -. A ( S _D F ) y <-> -. ( A e. ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) /\ y e. ( G limCC A ) ) ) )
25 24 adantr 
 |-  ( ( ph /\ A e. dom ( S _D F ) ) -> ( -. A ( S _D F ) y <-> -. ( A e. ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) /\ y e. ( G limCC A ) ) ) )
26 20 25 mpbird 
 |-  ( ( ph /\ A e. dom ( S _D F ) ) -> -. A ( S _D F ) y )
27 26 alrimiv 
 |-  ( ( ph /\ A e. dom ( S _D F ) ) -> A. y -. A ( S _D F ) y )
28 simpr 
 |-  ( ( ph /\ A e. dom ( S _D F ) ) -> A e. dom ( S _D F ) )
29 eldmg 
 |-  ( A e. dom ( S _D F ) -> ( A e. dom ( S _D F ) <-> E. y A ( S _D F ) y ) )
30 28 29 syl 
 |-  ( ( ph /\ A e. dom ( S _D F ) ) -> ( A e. dom ( S _D F ) <-> E. y A ( S _D F ) y ) )
31 30 notbid 
 |-  ( ( ph /\ A e. dom ( S _D F ) ) -> ( -. A e. dom ( S _D F ) <-> -. E. y A ( S _D F ) y ) )
32 alnex 
 |-  ( A. y -. A ( S _D F ) y <-> -. E. y A ( S _D F ) y )
33 32 a1i 
 |-  ( ( ph /\ A e. dom ( S _D F ) ) -> ( A. y -. A ( S _D F ) y <-> -. E. y A ( S _D F ) y ) )
34 33 bicomd 
 |-  ( ( ph /\ A e. dom ( S _D F ) ) -> ( -. E. y A ( S _D F ) y <-> A. y -. A ( S _D F ) y ) )
35 31 34 bitrd 
 |-  ( ( ph /\ A e. dom ( S _D F ) ) -> ( -. A e. dom ( S _D F ) <-> A. y -. A ( S _D F ) y ) )
36 27 35 mpbird 
 |-  ( ( ph /\ A e. dom ( S _D F ) ) -> -. A e. dom ( S _D F ) )
37 36 pm2.01da 
 |-  ( ph -> -. A e. dom ( S _D F ) )