Metamath Proof Explorer

Theorem limcperiod

Description: If F is a periodic function with period T , the limit doesn't change if we shift the limiting point by T . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses limcperiod.f 
|- ( ph -> F : dom F --> CC )
limcperiod.assc 
|- ( ph -> A C_ CC )
limcperiod.3 
|- ( ph -> A C_ dom F )
limcperiod.t 
|- ( ph -> T e. CC )
limcperiod.b 
|- B = { x e. CC | E. y e. A x = ( y + T ) }
limcperiod.bss 
|- ( ph -> B C_ dom F )
limcperiod.fper 
|- ( ( ph /\ y e. A ) -> ( F ` ( y + T ) ) = ( F ` y ) )
limcperiod.clim 
|- ( ph -> C e. ( ( F |` A ) limCC D ) )
Assertion limcperiod 
|- ( ph -> C e. ( ( F |` B ) limCC ( D + T ) ) )

Proof

Step Hyp Ref Expression
1 limcperiod.f 
 |-  ( ph -> F : dom F --> CC )
2 limcperiod.assc 
 |-  ( ph -> A C_ CC )
3 limcperiod.3 
 |-  ( ph -> A C_ dom F )
4 limcperiod.t 
 |-  ( ph -> T e. CC )
5 limcperiod.b 
 |-  B = { x e. CC | E. y e. A x = ( y + T ) }
6 limcperiod.bss 
 |-  ( ph -> B C_ dom F )
7 limcperiod.fper 
 |-  ( ( ph /\ y e. A ) -> ( F ` ( y + T ) ) = ( F ` y ) )
8 limcperiod.clim 
 |-  ( ph -> C e. ( ( F |` A ) limCC D ) )
9 limccl 
 |-  ( ( F |` A ) limCC D ) C_ CC
10 9 8 sselid 
 |-  ( ph -> C e. CC )
11 1 3 fssresd 
 |-  ( ph -> ( F |` A ) : A --> CC )
12 limcrcl 
 |-  ( C e. ( ( F |` A ) limCC D ) -> ( ( F |` A ) : dom ( F |` A ) --> CC /\ dom ( F |` A ) C_ CC /\ D e. CC ) )
13 8 12 syl 
 |-  ( ph -> ( ( F |` A ) : dom ( F |` A ) --> CC /\ dom ( F |` A ) C_ CC /\ D e. CC ) )
14 13 simp3d 
 |-  ( ph -> D e. CC )
15 11 2 14 ellimc3 
 |-  ( ph -> ( C e. ( ( F |` A ) limCC D ) <-> ( C e. CC /\ A. w e. RR+ E. z e. RR+ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) ) )
16 8 15 mpbid 
 |-  ( ph -> ( C e. CC /\ A. w e. RR+ E. z e. RR+ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) )
17 16 simprd 
 |-  ( ph -> A. w e. RR+ E. z e. RR+ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) )
18 17 r19.21bi 
 |-  ( ( ph /\ w e. RR+ ) -> E. z e. RR+ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) )
19 simpl1l 
 |-  ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) -> ph )
20 19 adantr 
 |-  ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) -> ph )
21 simplr 
 |-  ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) -> b e. B )
22 id 
 |-  ( b e. B -> b e. B )
23 oveq1 
 |-  ( y = z -> ( y + T ) = ( z + T ) )
24 23 eqeq2d 
 |-  ( y = z -> ( x = ( y + T ) <-> x = ( z + T ) ) )
25 24 cbvrexvw 
 |-  ( E. y e. A x = ( y + T ) <-> E. z e. A x = ( z + T ) )
26 eqeq1 
 |-  ( x = w -> ( x = ( z + T ) <-> w = ( z + T ) ) )
27 26 rexbidv 
 |-  ( x = w -> ( E. z e. A x = ( z + T ) <-> E. z e. A w = ( z + T ) ) )
28 25 27 bitrid 
 |-  ( x = w -> ( E. y e. A x = ( y + T ) <-> E. z e. A w = ( z + T ) ) )
29 28 cbvrabv 
 |-  { x e. CC | E. y e. A x = ( y + T ) } = { w e. CC | E. z e. A w = ( z + T ) }
30 5 29 eqtri 
 |-  B = { w e. CC | E. z e. A w = ( z + T ) }
31 22 30 eleqtrdi 
 |-  ( b e. B -> b e. { w e. CC | E. z e. A w = ( z + T ) } )
32 eqeq1 
 |-  ( w = b -> ( w = ( z + T ) <-> b = ( z + T ) ) )
33 32 rexbidv 
 |-  ( w = b -> ( E. z e. A w = ( z + T ) <-> E. z e. A b = ( z + T ) ) )
34 33 elrab 
 |-  ( b e. { w e. CC | E. z e. A w = ( z + T ) } <-> ( b e. CC /\ E. z e. A b = ( z + T ) ) )
35 31 34 sylib 
 |-  ( b e. B -> ( b e. CC /\ E. z e. A b = ( z + T ) ) )
36 35 simprd 
 |-  ( b e. B -> E. z e. A b = ( z + T ) )
37 36 adantl 
 |-  ( ( ph /\ b e. B ) -> E. z e. A b = ( z + T ) )
38 oveq1 
 |-  ( b = ( z + T ) -> ( b - T ) = ( ( z + T ) - T ) )
39 38 3ad2ant3 
 |-  ( ( ph /\ z e. A /\ b = ( z + T ) ) -> ( b - T ) = ( ( z + T ) - T ) )
40 2 sselda 
 |-  ( ( ph /\ z e. A ) -> z e. CC )
41 4 adantr 
 |-  ( ( ph /\ z e. A ) -> T e. CC )
42 40 41 pncand 
 |-  ( ( ph /\ z e. A ) -> ( ( z + T ) - T ) = z )
43 42 3adant3 
 |-  ( ( ph /\ z e. A /\ b = ( z + T ) ) -> ( ( z + T ) - T ) = z )
44 39 43 eqtrd 
 |-  ( ( ph /\ z e. A /\ b = ( z + T ) ) -> ( b - T ) = z )
45 simp2 
 |-  ( ( ph /\ z e. A /\ b = ( z + T ) ) -> z e. A )
46 44 45 eqeltrd 
 |-  ( ( ph /\ z e. A /\ b = ( z + T ) ) -> ( b - T ) e. A )
47 46 3exp 
 |-  ( ph -> ( z e. A -> ( b = ( z + T ) -> ( b - T ) e. A ) ) )
48 47 adantr 
 |-  ( ( ph /\ b e. B ) -> ( z e. A -> ( b = ( z + T ) -> ( b - T ) e. A ) ) )
49 48 rexlimdv 
 |-  ( ( ph /\ b e. B ) -> ( E. z e. A b = ( z + T ) -> ( b - T ) e. A ) )
50 37 49 mpd 
 |-  ( ( ph /\ b e. B ) -> ( b - T ) e. A )
51 5 ssrab3 
 |-  B C_ CC
52 51 a1i 
 |-  ( ph -> B C_ CC )
53 52 sselda 
 |-  ( ( ph /\ b e. B ) -> b e. CC )
54 4 adantr 
 |-  ( ( ph /\ b e. B ) -> T e. CC )
55 53 54 npcand 
 |-  ( ( ph /\ b e. B ) -> ( ( b - T ) + T ) = b )
56 55 eqcomd 
 |-  ( ( ph /\ b e. B ) -> b = ( ( b - T ) + T ) )
57 oveq1 
 |-  ( x = ( b - T ) -> ( x + T ) = ( ( b - T ) + T ) )
58 57 rspceeqv 
 |-  ( ( ( b - T ) e. A /\ b = ( ( b - T ) + T ) ) -> E. x e. A b = ( x + T ) )
59 50 56 58 syl2anc 
 |-  ( ( ph /\ b e. B ) -> E. x e. A b = ( x + T ) )
60 20 21 59 syl2anc 
 |-  ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) -> E. x e. A b = ( x + T ) )
61 nfv 
 |-  F/ x ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) )
62 nfrab1 
 |-  F/_ x { x e. CC | E. y e. A x = ( y + T ) }
63 5 62 nfcxfr 
 |-  F/_ x B
64 63 nfcri 
 |-  F/ x b e. B
65 61 64 nfan 
 |-  F/ x ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B )
66 nfv 
 |-  F/ x ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z )
67 65 66 nfan 
 |-  F/ x ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) )
68 nfcv 
 |-  F/_ x abs
69 nfcv 
 |-  F/_ x F
70 69 63 nfres 
 |-  F/_ x ( F |` B )
71 nfcv 
 |-  F/_ x b
72 70 71 nffv 
 |-  F/_ x ( ( F |` B ) ` b )
73 nfcv 
 |-  F/_ x -
74 nfcv 
 |-  F/_ x C
75 72 73 74 nfov 
 |-  F/_ x ( ( ( F |` B ) ` b ) - C )
76 68 75 nffv 
 |-  F/_ x ( abs ` ( ( ( F |` B ) ` b ) - C ) )
77 nfcv 
 |-  F/_ x <
78 nfcv 
 |-  F/_ x w
79 76 77 78 nfbr 
 |-  F/ x ( abs ` ( ( ( F |` B ) ` b ) - C ) ) < w
80 simp3 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> b = ( x + T ) )
81 80 fveq2d 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> ( ( F |` B ) ` b ) = ( ( F |` B ) ` ( x + T ) ) )
82 21 3ad2ant1 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> b e. B )
83 80 82 eqeltrrd 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> ( x + T ) e. B )
84 83 fvresd 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> ( ( F |` B ) ` ( x + T ) ) = ( F ` ( x + T ) ) )
85 20 3ad2ant1 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> ph )
86 simp2 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> x e. A )
87 eleq1w 
 |-  ( y = x -> ( y e. A <-> x e. A ) )
88 87 anbi2d 
 |-  ( y = x -> ( ( ph /\ y e. A ) <-> ( ph /\ x e. A ) ) )
89 fvoveq1 
 |-  ( y = x -> ( F ` ( y + T ) ) = ( F ` ( x + T ) ) )
90 fveq2 
 |-  ( y = x -> ( F ` y ) = ( F ` x ) )
91 89 90 eqeq12d 
 |-  ( y = x -> ( ( F ` ( y + T ) ) = ( F ` y ) <-> ( F ` ( x + T ) ) = ( F ` x ) ) )
92 88 91 imbi12d 
 |-  ( y = x -> ( ( ( ph /\ y e. A ) -> ( F ` ( y + T ) ) = ( F ` y ) ) <-> ( ( ph /\ x e. A ) -> ( F ` ( x + T ) ) = ( F ` x ) ) ) )
93 92 7 chvarvv 
 |-  ( ( ph /\ x e. A ) -> ( F ` ( x + T ) ) = ( F ` x ) )
94 85 86 93 syl2anc 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )
95 86 fvresd 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> ( ( F |` A ) ` x ) = ( F ` x ) )
96 94 95 eqtr4d 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> ( F ` ( x + T ) ) = ( ( F |` A ) ` x ) )
97 81 84 96 3eqtrd 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> ( ( F |` B ) ` b ) = ( ( F |` A ) ` x ) )
98 97 fvoveq1d 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> ( abs ` ( ( ( F |` B ) ` b ) - C ) ) = ( abs ` ( ( ( F |` A ) ` x ) - C ) ) )
99 simpll3 
 |-  ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) -> A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) )
100 99 3ad2ant1 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) )
101 100 86 jca 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> ( A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) /\ x e. A ) )
102 simp1rl 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> b =/= ( D + T ) )
103 102 neneqd 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> -. b = ( D + T ) )
104 oveq1 
 |-  ( x = D -> ( x + T ) = ( D + T ) )
105 80 104 sylan9eq 
 |-  ( ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) /\ x = D ) -> b = ( D + T ) )
106 103 105 mtand 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> -. x = D )
107 106 neqned 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> x =/= D )
108 80 oveq1d 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> ( b - ( D + T ) ) = ( ( x + T ) - ( D + T ) ) )
109 2 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. CC )
110 85 86 109 syl2anc 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> x e. CC )
111 85 14 syl 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> D e. CC )
112 85 4 syl 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> T e. CC )
113 110 111 112 pnpcan2d 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> ( ( x + T ) - ( D + T ) ) = ( x - D ) )
114 108 113 eqtr2d 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> ( x - D ) = ( b - ( D + T ) ) )
115 114 fveq2d 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> ( abs ` ( x - D ) ) = ( abs ` ( b - ( D + T ) ) ) )
116 simp1rr 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> ( abs ` ( b - ( D + T ) ) ) < z )
117 115 116 eqbrtrd 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> ( abs ` ( x - D ) ) < z )
118 107 117 jca 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> ( x =/= D /\ ( abs ` ( x - D ) ) < z ) )
119 neeq1 
 |-  ( y = x -> ( y =/= D <-> x =/= D ) )
120 fvoveq1 
 |-  ( y = x -> ( abs ` ( y - D ) ) = ( abs ` ( x - D ) ) )
121 120 breq1d 
 |-  ( y = x -> ( ( abs ` ( y - D ) ) < z <-> ( abs ` ( x - D ) ) < z ) )
122 119 121 anbi12d 
 |-  ( y = x -> ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) <-> ( x =/= D /\ ( abs ` ( x - D ) ) < z ) ) )
123 122 imbrov2fvoveq 
 |-  ( y = x -> ( ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) <-> ( ( x =/= D /\ ( abs ` ( x - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` x ) - C ) ) < w ) ) )
124 123 rspccva 
 |-  ( ( A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) /\ x e. A ) -> ( ( x =/= D /\ ( abs ` ( x - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` x ) - C ) ) < w ) )
125 101 118 124 sylc 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> ( abs ` ( ( ( F |` A ) ` x ) - C ) ) < w )
126 98 125 eqbrtrd 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) /\ x e. A /\ b = ( x + T ) ) -> ( abs ` ( ( ( F |` B ) ` b ) - C ) ) < w )
127 126 3exp 
 |-  ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) -> ( x e. A -> ( b = ( x + T ) -> ( abs ` ( ( ( F |` B ) ` b ) - C ) ) < w ) ) )
128 67 79 127 rexlimd 
 |-  ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) -> ( E. x e. A b = ( x + T ) -> ( abs ` ( ( ( F |` B ) ` b ) - C ) ) < w ) )
129 60 128 mpd 
 |-  ( ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) /\ ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) ) -> ( abs ` ( ( ( F |` B ) ` b ) - C ) ) < w )
130 129 ex 
 |-  ( ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) /\ b e. B ) -> ( ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) -> ( abs ` ( ( ( F |` B ) ` b ) - C ) ) < w ) )
131 130 ralrimiva 
 |-  ( ( ( ph /\ w e. RR+ ) /\ z e. RR+ /\ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) ) -> A. b e. B ( ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) -> ( abs ` ( ( ( F |` B ) ` b ) - C ) ) < w ) )
132 131 3exp 
 |-  ( ( ph /\ w e. RR+ ) -> ( z e. RR+ -> ( A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) -> A. b e. B ( ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) -> ( abs ` ( ( ( F |` B ) ` b ) - C ) ) < w ) ) ) )
133 132 reximdvai 
 |-  ( ( ph /\ w e. RR+ ) -> ( E. z e. RR+ A. y e. A ( ( y =/= D /\ ( abs ` ( y - D ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` y ) - C ) ) < w ) -> E. z e. RR+ A. b e. B ( ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) -> ( abs ` ( ( ( F |` B ) ` b ) - C ) ) < w ) ) )
134 18 133 mpd 
 |-  ( ( ph /\ w e. RR+ ) -> E. z e. RR+ A. b e. B ( ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) -> ( abs ` ( ( ( F |` B ) ` b ) - C ) ) < w ) )
135 134 ralrimiva 
 |-  ( ph -> A. w e. RR+ E. z e. RR+ A. b e. B ( ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) -> ( abs ` ( ( ( F |` B ) ` b ) - C ) ) < w ) )
136 1 6 fssresd 
 |-  ( ph -> ( F |` B ) : B --> CC )
137 14 4 addcld 
 |-  ( ph -> ( D + T ) e. CC )
138 136 52 137 ellimc3 
 |-  ( ph -> ( C e. ( ( F |` B ) limCC ( D + T ) ) <-> ( C e. CC /\ A. w e. RR+ E. z e. RR+ A. b e. B ( ( b =/= ( D + T ) /\ ( abs ` ( b - ( D + T ) ) ) < z ) -> ( abs ` ( ( ( F |` B ) ` b ) - C ) ) < w ) ) ) )
139 10 135 138 mpbir2and 
 |-  ( ph -> C e. ( ( F |` B ) limCC ( D + T ) ) )