Metamath Proof Explorer

Theorem neglimc

Description: Limit of the negative function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses neglimc.f 
|- F = ( x e. A |-> B )
neglimc.g 
|- G = ( x e. A |-> -u B )
neglimc.b 
|- ( ( ph /\ x e. A ) -> B e. CC )
neglimc.c 
|- ( ph -> C e. ( F limCC D ) )
Assertion neglimc 
|- ( ph -> -u C e. ( G limCC D ) )

Proof

Step Hyp Ref Expression
1 neglimc.f 
 |-  F = ( x e. A |-> B )
2 neglimc.g 
 |-  G = ( x e. A |-> -u B )
3 neglimc.b 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
4 neglimc.c 
 |-  ( ph -> C e. ( F limCC D ) )
5 limccl 
 |-  ( F limCC D ) C_ CC
6 5 4 sselid 
 |-  ( ph -> C e. CC )
7 6 negcld 
 |-  ( ph -> -u C e. CC )
8 3 1 fmptd 
 |-  ( ph -> F : A --> CC )
9 1 3 4 limcmptdm 
 |-  ( ph -> A C_ CC )
10 limcrcl 
 |-  ( C e. ( F limCC D ) -> ( F : dom F --> CC /\ dom F C_ CC /\ D e. CC ) )
11 4 10 syl 
 |-  ( ph -> ( F : dom F --> CC /\ dom F C_ CC /\ D e. CC ) )
12 11 simp3d 
 |-  ( ph -> D e. CC )
13 8 9 12 ellimc3 
 |-  ( ph -> ( C e. ( F limCC D ) <-> ( C e. CC /\ A. y e. RR+ E. w e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( F ` v ) - C ) ) < y ) ) ) )
14 4 13 mpbid 
 |-  ( ph -> ( C e. CC /\ A. y e. RR+ E. w e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( F ` v ) - C ) ) < y ) ) )
15 14 simprd 
 |-  ( ph -> A. y e. RR+ E. w e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( F ` v ) - C ) ) < y ) )
16 15 r19.21bi 
 |-  ( ( ph /\ y e. RR+ ) -> E. w e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( F ` v ) - C ) ) < y ) )
17 simplll 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ w e. RR+ ) /\ v e. A ) -> ph )
18 17 3ad2ant1 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ w e. RR+ ) /\ v e. A ) /\ ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( F ` v ) - C ) ) < y ) /\ ( v =/= D /\ ( abs ` ( v - D ) ) < w ) ) -> ph )
19 simp1r 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ w e. RR+ ) /\ v e. A ) /\ ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( F ` v ) - C ) ) < y ) /\ ( v =/= D /\ ( abs ` ( v - D ) ) < w ) ) -> v e. A )
20 simp3 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ w e. RR+ ) /\ v e. A ) /\ ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( F ` v ) - C ) ) < y ) /\ ( v =/= D /\ ( abs ` ( v - D ) ) < w ) ) -> ( v =/= D /\ ( abs ` ( v - D ) ) < w ) )
21 simp2 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ w e. RR+ ) /\ v e. A ) /\ ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( F ` v ) - C ) ) < y ) /\ ( v =/= D /\ ( abs ` ( v - D ) ) < w ) ) -> ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( F ` v ) - C ) ) < y ) )
22 20 21 mpd 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ w e. RR+ ) /\ v e. A ) /\ ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( F ` v ) - C ) ) < y ) /\ ( v =/= D /\ ( abs ` ( v - D ) ) < w ) ) -> ( abs ` ( ( F ` v ) - C ) ) < y )
23 nfv 
 |-  F/ x ( ph /\ v e. A )
24 nfmpt1 
 |-  F/_ x ( x e. A |-> -u B )
25 2 24 nfcxfr 
 |-  F/_ x G
26 nfcv 
 |-  F/_ x v
27 25 26 nffv 
 |-  F/_ x ( G ` v )
28 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
29 1 28 nfcxfr 
 |-  F/_ x F
30 29 26 nffv 
 |-  F/_ x ( F ` v )
31 30 nfneg 
 |-  F/_ x -u ( F ` v )
32 27 31 nfeq 
 |-  F/ x ( G ` v ) = -u ( F ` v )
33 23 32 nfim 
 |-  F/ x ( ( ph /\ v e. A ) -> ( G ` v ) = -u ( F ` v ) )
34 eleq1w 
 |-  ( x = v -> ( x e. A <-> v e. A ) )
35 34 anbi2d 
 |-  ( x = v -> ( ( ph /\ x e. A ) <-> ( ph /\ v e. A ) ) )
36 fveq2 
 |-  ( x = v -> ( G ` x ) = ( G ` v ) )
37 fveq2 
 |-  ( x = v -> ( F ` x ) = ( F ` v ) )
38 37 negeqd 
 |-  ( x = v -> -u ( F ` x ) = -u ( F ` v ) )
39 36 38 eqeq12d 
 |-  ( x = v -> ( ( G ` x ) = -u ( F ` x ) <-> ( G ` v ) = -u ( F ` v ) ) )
40 35 39 imbi12d 
 |-  ( x = v -> ( ( ( ph /\ x e. A ) -> ( G ` x ) = -u ( F ` x ) ) <-> ( ( ph /\ v e. A ) -> ( G ` v ) = -u ( F ` v ) ) ) )
41 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
42 3 negcld 
 |-  ( ( ph /\ x e. A ) -> -u B e. CC )
43 2 fvmpt2 
 |-  ( ( x e. A /\ -u B e. CC ) -> ( G ` x ) = -u B )
44 41 42 43 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) = -u B )
45 1 fvmpt2 
 |-  ( ( x e. A /\ B e. CC ) -> ( F ` x ) = B )
46 41 3 45 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) = B )
47 46 negeqd 
 |-  ( ( ph /\ x e. A ) -> -u ( F ` x ) = -u B )
48 44 47 eqtr4d 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) = -u ( F ` x ) )
49 33 40 48 chvarfv 
 |-  ( ( ph /\ v e. A ) -> ( G ` v ) = -u ( F ` v ) )
50 49 oveq1d 
 |-  ( ( ph /\ v e. A ) -> ( ( G ` v ) - -u C ) = ( -u ( F ` v ) - -u C ) )
51 8 ffvelrnda 
 |-  ( ( ph /\ v e. A ) -> ( F ` v ) e. CC )
52 6 adantr 
 |-  ( ( ph /\ v e. A ) -> C e. CC )
53 51 52 negsubdi3d 
 |-  ( ( ph /\ v e. A ) -> -u ( ( F ` v ) - C ) = ( -u ( F ` v ) - -u C ) )
54 50 53 eqtr4d 
 |-  ( ( ph /\ v e. A ) -> ( ( G ` v ) - -u C ) = -u ( ( F ` v ) - C ) )
55 54 fveq2d 
 |-  ( ( ph /\ v e. A ) -> ( abs ` ( ( G ` v ) - -u C ) ) = ( abs ` -u ( ( F ` v ) - C ) ) )
56 51 52 subcld 
 |-  ( ( ph /\ v e. A ) -> ( ( F ` v ) - C ) e. CC )
57 56 absnegd 
 |-  ( ( ph /\ v e. A ) -> ( abs ` -u ( ( F ` v ) - C ) ) = ( abs ` ( ( F ` v ) - C ) ) )
58 55 57 eqtrd 
 |-  ( ( ph /\ v e. A ) -> ( abs ` ( ( G ` v ) - -u C ) ) = ( abs ` ( ( F ` v ) - C ) ) )
59 58 adantr 
 |-  ( ( ( ph /\ v e. A ) /\ ( abs ` ( ( F ` v ) - C ) ) < y ) -> ( abs ` ( ( G ` v ) - -u C ) ) = ( abs ` ( ( F ` v ) - C ) ) )
60 simpr 
 |-  ( ( ( ph /\ v e. A ) /\ ( abs ` ( ( F ` v ) - C ) ) < y ) -> ( abs ` ( ( F ` v ) - C ) ) < y )
61 59 60 eqbrtrd 
 |-  ( ( ( ph /\ v e. A ) /\ ( abs ` ( ( F ` v ) - C ) ) < y ) -> ( abs ` ( ( G ` v ) - -u C ) ) < y )
62 18 19 22 61 syl21anc 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ w e. RR+ ) /\ v e. A ) /\ ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( F ` v ) - C ) ) < y ) /\ ( v =/= D /\ ( abs ` ( v - D ) ) < w ) ) -> ( abs ` ( ( G ` v ) - -u C ) ) < y )
63 62 3exp 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ w e. RR+ ) /\ v e. A ) -> ( ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( F ` v ) - C ) ) < y ) -> ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( G ` v ) - -u C ) ) < y ) ) )
64 63 ralimdva 
 |-  ( ( ( ph /\ y e. RR+ ) /\ w e. RR+ ) -> ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( F ` v ) - C ) ) < y ) -> A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( G ` v ) - -u C ) ) < y ) ) )
65 64 reximdva 
 |-  ( ( ph /\ y e. RR+ ) -> ( E. w e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( F ` v ) - C ) ) < y ) -> E. w e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( G ` v ) - -u C ) ) < y ) ) )
66 16 65 mpd 
 |-  ( ( ph /\ y e. RR+ ) -> E. w e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( G ` v ) - -u C ) ) < y ) )
67 66 ralrimiva 
 |-  ( ph -> A. y e. RR+ E. w e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( G ` v ) - -u C ) ) < y ) )
68 42 2 fmptd 
 |-  ( ph -> G : A --> CC )
69 68 9 12 ellimc3 
 |-  ( ph -> ( -u C e. ( G limCC D ) <-> ( -u C e. CC /\ A. y e. RR+ E. w e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( G ` v ) - -u C ) ) < y ) ) ) )
70 7 67 69 mpbir2and 
 |-  ( ph -> -u C e. ( G limCC D ) )