Metamath Proof Explorer

Theorem fperdvper

Description: The derivative of a periodic function is periodic. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fperdvper.f 
|- ( ph -> F : RR --> CC )
fperdvper.t 
|- ( ph -> T e. RR )
fperdvper.fper 
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fperdvper.g 
|- G = ( RR _D F )
Assertion fperdvper 
|- ( ( ph /\ x e. dom G ) -> ( ( x + T ) e. dom G /\ ( G ` ( x + T ) ) = ( G ` x ) ) )

Proof

Step Hyp Ref Expression
1 fperdvper.f 
 |-  ( ph -> F : RR --> CC )
2 fperdvper.t 
 |-  ( ph -> T e. RR )
3 fperdvper.fper 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
4 fperdvper.g 
 |-  G = ( RR _D F )
5 dvbsss 
 |-  dom ( RR _D F ) C_ RR
6 id 
 |-  ( x e. dom G -> x e. dom G )
7 4 dmeqi 
 |-  dom G = dom ( RR _D F )
8 6 7 eleqtrdi 
 |-  ( x e. dom G -> x e. dom ( RR _D F ) )
9 5 8 sseldi 
 |-  ( x e. dom G -> x e. RR )
10 9 adantl 
 |-  ( ( ph /\ x e. dom G ) -> x e. RR )
11 2 adantr 
 |-  ( ( ph /\ x e. dom G ) -> T e. RR )
12 10 11 readdcld 
 |-  ( ( ph /\ x e. dom G ) -> ( x + T ) e. RR )
13 reopn 
 |-  RR e. ( topGen ` ran (,) )
14 retop 
 |-  ( topGen ` ran (,) ) e. Top
15 ssidd 
 |-  ( ( ph /\ x e. dom G ) -> RR C_ RR )
16 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
17 16 isopn3 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ RR C_ RR ) -> ( RR e. ( topGen ` ran (,) ) <-> ( ( int ` ( topGen ` ran (,) ) ) ` RR ) = RR ) )
18 14 15 17 sylancr 
 |-  ( ( ph /\ x e. dom G ) -> ( RR e. ( topGen ` ran (,) ) <-> ( ( int ` ( topGen ` ran (,) ) ) ` RR ) = RR ) )
19 13 18 mpbii 
 |-  ( ( ph /\ x e. dom G ) -> ( ( int ` ( topGen ` ran (,) ) ) ` RR ) = RR )
20 19 eqcomd 
 |-  ( ( ph /\ x e. dom G ) -> RR = ( ( int ` ( topGen ` ran (,) ) ) ` RR ) )
21 12 20 eleqtrd 
 |-  ( ( ph /\ x e. dom G ) -> ( x + T ) e. ( ( int ` ( topGen ` ran (,) ) ) ` RR ) )
22 8 adantl 
 |-  ( ( ph /\ x e. dom G ) -> x e. dom ( RR _D F ) )
23 4 fveq1i 
 |-  ( G ` x ) = ( ( RR _D F ) ` x )
24 23 eqcomi 
 |-  ( ( RR _D F ) ` x ) = ( G ` x )
25 24 a1i 
 |-  ( ( ph /\ x e. dom G ) -> ( ( RR _D F ) ` x ) = ( G ` x ) )
26 dvf 
 |-  ( RR _D F ) : dom ( RR _D F ) --> CC
27 ffun 
 |-  ( ( RR _D F ) : dom ( RR _D F ) --> CC -> Fun ( RR _D F ) )
28 26 27 ax-mp 
 |-  Fun ( RR _D F )
29 28 a1i 
 |-  ( ph -> Fun ( RR _D F ) )
30 funbrfv2b 
 |-  ( Fun ( RR _D F ) -> ( x ( RR _D F ) ( G ` x ) <-> ( x e. dom ( RR _D F ) /\ ( ( RR _D F ) ` x ) = ( G ` x ) ) ) )
31 29 30 syl 
 |-  ( ph -> ( x ( RR _D F ) ( G ` x ) <-> ( x e. dom ( RR _D F ) /\ ( ( RR _D F ) ` x ) = ( G ` x ) ) ) )
32 31 adantr 
 |-  ( ( ph /\ x e. dom G ) -> ( x ( RR _D F ) ( G ` x ) <-> ( x e. dom ( RR _D F ) /\ ( ( RR _D F ) ` x ) = ( G ` x ) ) ) )
33 22 25 32 mpbir2and 
 |-  ( ( ph /\ x e. dom G ) -> x ( RR _D F ) ( G ` x ) )
34 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
35 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
36 eqid 
 |-  ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) = ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) )
37 ax-resscn 
 |-  RR C_ CC
38 37 a1i 
 |-  ( ( ph /\ x e. dom G ) -> RR C_ CC )
39 1 adantr 
 |-  ( ( ph /\ x e. dom G ) -> F : RR --> CC )
40 34 35 36 38 39 15 eldv 
 |-  ( ( ph /\ x e. dom G ) -> ( x ( RR _D F ) ( G ` x ) <-> ( x e. ( ( int ` ( topGen ` ran (,) ) ) ` RR ) /\ ( G ` x ) e. ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) limCC x ) ) ) )
41 33 40 mpbid 
 |-  ( ( ph /\ x e. dom G ) -> ( x e. ( ( int ` ( topGen ` ran (,) ) ) ` RR ) /\ ( G ` x ) e. ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) limCC x ) ) )
42 41 simprd 
 |-  ( ( ph /\ x e. dom G ) -> ( G ` x ) e. ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) limCC x ) )
43 eqidd 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) = ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) )
44 fveq2 
 |-  ( y = d -> ( F ` y ) = ( F ` d ) )
45 44 oveq1d 
 |-  ( y = d -> ( ( F ` y ) - ( F ` ( x + T ) ) ) = ( ( F ` d ) - ( F ` ( x + T ) ) ) )
46 oveq1 
 |-  ( y = d -> ( y - ( x + T ) ) = ( d - ( x + T ) ) )
47 45 46 oveq12d 
 |-  ( y = d -> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) = ( ( ( F ` d ) - ( F ` ( x + T ) ) ) / ( d - ( x + T ) ) ) )
48 eldifi 
 |-  ( d e. ( RR \ { ( x + T ) } ) -> d e. RR )
49 48 recnd 
 |-  ( d e. ( RR \ { ( x + T ) } ) -> d e. CC )
50 49 adantl 
 |-  ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> d e. CC )
51 2 recnd 
 |-  ( ph -> T e. CC )
52 51 adantr 
 |-  ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> T e. CC )
53 50 52 npcand 
 |-  ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ( d - T ) + T ) = d )
54 53 eqcomd 
 |-  ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> d = ( ( d - T ) + T ) )
55 54 fveq2d 
 |-  ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> ( F ` d ) = ( F ` ( ( d - T ) + T ) ) )
56 ovex 
 |-  ( d - T ) e. _V
57 48 adantl 
 |-  ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> d e. RR )
58 2 adantr 
 |-  ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> T e. RR )
59 57 58 resubcld 
 |-  ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> ( d - T ) e. RR )
60 59 ex 
 |-  ( ph -> ( d e. ( RR \ { ( x + T ) } ) -> ( d - T ) e. RR ) )
61 60 imdistani 
 |-  ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ph /\ ( d - T ) e. RR ) )
62 eleq1 
 |-  ( x = ( d - T ) -> ( x e. RR <-> ( d - T ) e. RR ) )
63 62 anbi2d 
 |-  ( x = ( d - T ) -> ( ( ph /\ x e. RR ) <-> ( ph /\ ( d - T ) e. RR ) ) )
64 fvoveq1 
 |-  ( x = ( d - T ) -> ( F ` ( x + T ) ) = ( F ` ( ( d - T ) + T ) ) )
65 fveq2 
 |-  ( x = ( d - T ) -> ( F ` x ) = ( F ` ( d - T ) ) )
66 64 65 eqeq12d 
 |-  ( x = ( d - T ) -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( ( d - T ) + T ) ) = ( F ` ( d - T ) ) ) )
67 63 66 imbi12d 
 |-  ( x = ( d - T ) -> ( ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) ) <-> ( ( ph /\ ( d - T ) e. RR ) -> ( F ` ( ( d - T ) + T ) ) = ( F ` ( d - T ) ) ) ) )
68 67 3 vtoclg 
 |-  ( ( d - T ) e. _V -> ( ( ph /\ ( d - T ) e. RR ) -> ( F ` ( ( d - T ) + T ) ) = ( F ` ( d - T ) ) ) )
69 56 61 68 mpsyl 
 |-  ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> ( F ` ( ( d - T ) + T ) ) = ( F ` ( d - T ) ) )
70 55 69 eqtrd 
 |-  ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> ( F ` d ) = ( F ` ( d - T ) ) )
71 70 adantlr 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( F ` d ) = ( F ` ( d - T ) ) )
72 simpll 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ph )
73 9 ad2antlr 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> x e. RR )
74 72 73 3 syl2anc 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )
75 71 74 oveq12d 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ( F ` d ) - ( F ` ( x + T ) ) ) = ( ( F ` ( d - T ) ) - ( F ` x ) ) )
76 49 adantl 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> d e. CC )
77 72 51 syl 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> T e. CC )
78 10 recnd 
 |-  ( ( ph /\ x e. dom G ) -> x e. CC )
79 78 adantr 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> x e. CC )
80 76 77 79 subsub4d 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ( d - T ) - x ) = ( d - ( T + x ) ) )
81 77 79 addcomd 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( T + x ) = ( x + T ) )
82 81 oveq2d 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( d - ( T + x ) ) = ( d - ( x + T ) ) )
83 80 82 eqtr2d 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( d - ( x + T ) ) = ( ( d - T ) - x ) )
84 75 83 oveq12d 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ( ( F ` d ) - ( F ` ( x + T ) ) ) / ( d - ( x + T ) ) ) = ( ( ( F ` ( d - T ) ) - ( F ` x ) ) / ( ( d - T ) - x ) ) )
85 47 84 sylan9eqr 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ y = d ) -> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) = ( ( ( F ` ( d - T ) ) - ( F ` x ) ) / ( ( d - T ) - x ) ) )
86 simpr 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> d e. ( RR \ { ( x + T ) } ) )
87 1 adantr 
 |-  ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> F : RR --> CC )
88 87 59 ffvelrnd 
 |-  ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> ( F ` ( d - T ) ) e. CC )
89 88 adantlr 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( F ` ( d - T ) ) e. CC )
90 39 10 ffvelrnd 
 |-  ( ( ph /\ x e. dom G ) -> ( F ` x ) e. CC )
91 90 adantr 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( F ` x ) e. CC )
92 89 91 subcld 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ( F ` ( d - T ) ) - ( F ` x ) ) e. CC )
93 76 77 subcld 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( d - T ) e. CC )
94 93 79 subcld 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ( d - T ) - x ) e. CC )
95 simpr 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( d - T ) = x ) -> ( d - T ) = x )
96 49 ad2antlr 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( d - T ) = x ) -> d e. CC )
97 77 adantr 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( d - T ) = x ) -> T e. CC )
98 79 adantr 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( d - T ) = x ) -> x e. CC )
99 96 97 98 subadd2d 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( d - T ) = x ) -> ( ( d - T ) = x <-> ( x + T ) = d ) )
100 95 99 mpbid 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( d - T ) = x ) -> ( x + T ) = d )
101 100 eqcomd 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( d - T ) = x ) -> d = ( x + T ) )
102 eldifsni 
 |-  ( d e. ( RR \ { ( x + T ) } ) -> d =/= ( x + T ) )
103 102 ad2antlr 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( d - T ) = x ) -> d =/= ( x + T ) )
104 103 neneqd 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( d - T ) = x ) -> -. d = ( x + T ) )
105 101 104 pm2.65da 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> -. ( d - T ) = x )
106 105 neqned 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( d - T ) =/= x )
107 93 79 106 subne0d 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ( d - T ) - x ) =/= 0 )
108 92 94 107 divcld 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ( ( F ` ( d - T ) ) - ( F ` x ) ) / ( ( d - T ) - x ) ) e. CC )
109 43 85 86 108 fvmptd 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) = ( ( ( F ` ( d - T ) ) - ( F ` x ) ) / ( ( d - T ) - x ) ) )
110 109 fvoveq1d 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) = ( abs ` ( ( ( ( F ` ( d - T ) ) - ( F ` x ) ) / ( ( d - T ) - x ) ) - w ) ) )
111 110 ad4ant13 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. c e. ( RR \ { x } ) ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) = ( abs ` ( ( ( ( F ` ( d - T ) ) - ( F ` x ) ) / ( ( d - T ) - x ) ) - w ) ) )
112 neeq1 
 |-  ( c = ( d - T ) -> ( c =/= x <-> ( d - T ) =/= x ) )
113 fvoveq1 
 |-  ( c = ( d - T ) -> ( abs ` ( c - x ) ) = ( abs ` ( ( d - T ) - x ) ) )
114 113 breq1d 
 |-  ( c = ( d - T ) -> ( ( abs ` ( c - x ) ) < b <-> ( abs ` ( ( d - T ) - x ) ) < b ) )
115 112 114 anbi12d 
 |-  ( c = ( d - T ) -> ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) <-> ( ( d - T ) =/= x /\ ( abs ` ( ( d - T ) - x ) ) < b ) ) )
116 115 imbrov2fvoveq 
 |-  ( c = ( d - T ) -> ( ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) <-> ( ( ( d - T ) =/= x /\ ( abs ` ( ( d - T ) - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` ( d - T ) ) - w ) ) < a ) ) )
117 simpllr 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. c e. ( RR \ { x } ) ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> A. c e. ( RR \ { x } ) ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) )
118 48 ad2antlr 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. c e. ( RR \ { x } ) ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> d e. RR )
119 2 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. c e. ( RR \ { x } ) ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> T e. RR )
120 118 119 resubcld 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. c e. ( RR \ { x } ) ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( d - T ) e. RR )
121 elsni 
 |-  ( ( d - T ) e. { x } -> ( d - T ) = x )
122 105 121 nsyl 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> -. ( d - T ) e. { x } )
123 122 ad4ant13 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. c e. ( RR \ { x } ) ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> -. ( d - T ) e. { x } )
124 120 123 eldifd 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. c e. ( RR \ { x } ) ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( d - T ) e. ( RR \ { x } ) )
125 116 117 124 rspcdva 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. c e. ( RR \ { x } ) ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( ( ( d - T ) =/= x /\ ( abs ` ( ( d - T ) - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` ( d - T ) ) - w ) ) < a ) )
126 eqidd 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) = ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) )
127 simpr 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ y = ( d - T ) ) -> y = ( d - T ) )
128 127 fveq2d 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ y = ( d - T ) ) -> ( F ` y ) = ( F ` ( d - T ) ) )
129 128 oveq1d 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ y = ( d - T ) ) -> ( ( F ` y ) - ( F ` x ) ) = ( ( F ` ( d - T ) ) - ( F ` x ) ) )
130 127 oveq1d 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ y = ( d - T ) ) -> ( y - x ) = ( ( d - T ) - x ) )
131 129 130 oveq12d 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ y = ( d - T ) ) -> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) = ( ( ( F ` ( d - T ) ) - ( F ` x ) ) / ( ( d - T ) - x ) ) )
132 48 adantl 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> d e. RR )
133 72 2 syl 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> T e. RR )
134 132 133 resubcld 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( d - T ) e. RR )
135 134 122 eldifd 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( d - T ) e. ( RR \ { x } ) )
136 126 131 135 108 fvmptd 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` ( d - T ) ) = ( ( ( F ` ( d - T ) ) - ( F ` x ) ) / ( ( d - T ) - x ) ) )
137 136 eqcomd 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ( ( F ` ( d - T ) ) - ( F ` x ) ) / ( ( d - T ) - x ) ) = ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` ( d - T ) ) )
138 137 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) /\ ( ( ( d - T ) =/= x /\ ( abs ` ( ( d - T ) - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` ( d - T ) ) - w ) ) < a ) ) -> ( ( ( F ` ( d - T ) ) - ( F ` x ) ) / ( ( d - T ) - x ) ) = ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` ( d - T ) ) )
139 138 fvoveq1d 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) /\ ( ( ( d - T ) =/= x /\ ( abs ` ( ( d - T ) - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` ( d - T ) ) - w ) ) < a ) ) -> ( abs ` ( ( ( ( F ` ( d - T ) ) - ( F ` x ) ) / ( ( d - T ) - x ) ) - w ) ) = ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` ( d - T ) ) - w ) ) )
140 106 adantr 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( d - T ) =/= x )
141 83 eqcomd 
 |-  ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ( d - T ) - x ) = ( d - ( x + T ) ) )
142 141 adantr 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( ( d - T ) - x ) = ( d - ( x + T ) ) )
143 142 fveq2d 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( d - T ) - x ) ) = ( abs ` ( d - ( x + T ) ) ) )
144 simpr 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( d - ( x + T ) ) ) < b )
145 143 144 eqbrtrd 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( d - T ) - x ) ) < b )
146 140 145 jca 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( ( d - T ) =/= x /\ ( abs ` ( ( d - T ) - x ) ) < b ) )
147 146 adantr 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) /\ ( ( ( d - T ) =/= x /\ ( abs ` ( ( d - T ) - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` ( d - T ) ) - w ) ) < a ) ) -> ( ( d - T ) =/= x /\ ( abs ` ( ( d - T ) - x ) ) < b ) )
148 simpr 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) /\ ( ( ( d - T ) =/= x /\ ( abs ` ( ( d - T ) - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` ( d - T ) ) - w ) ) < a ) ) -> ( ( ( d - T ) =/= x /\ ( abs ` ( ( d - T ) - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` ( d - T ) ) - w ) ) < a ) )
149 147 148 mpd 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) /\ ( ( ( d - T ) =/= x /\ ( abs ` ( ( d - T ) - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` ( d - T ) ) - w ) ) < a ) ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` ( d - T ) ) - w ) ) < a )
150 139 149 eqbrtrd 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) /\ ( ( ( d - T ) =/= x /\ ( abs ` ( ( d - T ) - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` ( d - T ) ) - w ) ) < a ) ) -> ( abs ` ( ( ( ( F ` ( d - T ) ) - ( F ` x ) ) / ( ( d - T ) - x ) ) - w ) ) < a )
151 150 ex 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( ( ( ( d - T ) =/= x /\ ( abs ` ( ( d - T ) - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` ( d - T ) ) - w ) ) < a ) -> ( abs ` ( ( ( ( F ` ( d - T ) ) - ( F ` x ) ) / ( ( d - T ) - x ) ) - w ) ) < a ) )
152 151 adantllr 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. c e. ( RR \ { x } ) ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( ( ( ( d - T ) =/= x /\ ( abs ` ( ( d - T ) - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` ( d - T ) ) - w ) ) < a ) -> ( abs ` ( ( ( ( F ` ( d - T ) ) - ( F ` x ) ) / ( ( d - T ) - x ) ) - w ) ) < a ) )
153 125 152 mpd 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. c e. ( RR \ { x } ) ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( ( F ` ( d - T ) ) - ( F ` x ) ) / ( ( d - T ) - x ) ) - w ) ) < a )
154 153 adantrl 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. c e. ( RR \ { x } ) ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) ) -> ( abs ` ( ( ( ( F ` ( d - T ) ) - ( F ` x ) ) / ( ( d - T ) - x ) ) - w ) ) < a )
155 111 154 eqbrtrd 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. c e. ( RR \ { x } ) ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a )
156 155 ex 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ A. c e. ( RR \ { x } ) ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) )
157 156 ralrimiva 
 |-  ( ( ( ph /\ x e. dom G ) /\ A. c e. ( RR \ { x } ) ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) ) -> A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) )
158 eqidd 
 |-  ( c e. ( RR \ { x } ) -> ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) = ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) )
159 fveq2 
 |-  ( y = c -> ( F ` y ) = ( F ` c ) )
160 159 oveq1d 
 |-  ( y = c -> ( ( F ` y ) - ( F ` x ) ) = ( ( F ` c ) - ( F ` x ) ) )
161 oveq1 
 |-  ( y = c -> ( y - x ) = ( c - x ) )
162 160 161 oveq12d 
 |-  ( y = c -> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) = ( ( ( F ` c ) - ( F ` x ) ) / ( c - x ) ) )
163 162 adantl 
 |-  ( ( c e. ( RR \ { x } ) /\ y = c ) -> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) = ( ( ( F ` c ) - ( F ` x ) ) / ( c - x ) ) )
164 id 
 |-  ( c e. ( RR \ { x } ) -> c e. ( RR \ { x } ) )
165 ovexd 
 |-  ( c e. ( RR \ { x } ) -> ( ( ( F ` c ) - ( F ` x ) ) / ( c - x ) ) e. _V )
166 158 163 164 165 fvmptd 
 |-  ( c e. ( RR \ { x } ) -> ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) = ( ( ( F ` c ) - ( F ` x ) ) / ( c - x ) ) )
167 166 fvoveq1d 
 |-  ( c e. ( RR \ { x } ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) = ( abs ` ( ( ( ( F ` c ) - ( F ` x ) ) / ( c - x ) ) - w ) ) )
168 167 ad2antlr 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) ) /\ c e. ( RR \ { x } ) ) /\ ( c =/= x /\ ( abs ` ( c - x ) ) < b ) ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) = ( abs ` ( ( ( ( F ` c ) - ( F ` x ) ) / ( c - x ) ) - w ) ) )
169 simpll 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ph )
170 eldifi 
 |-  ( c e. ( RR \ { x } ) -> c e. RR )
171 170 adantl 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> c e. RR )
172 eleq1 
 |-  ( x = c -> ( x e. RR <-> c e. RR ) )
173 172 anbi2d 
 |-  ( x = c -> ( ( ph /\ x e. RR ) <-> ( ph /\ c e. RR ) ) )
174 fvoveq1 
 |-  ( x = c -> ( F ` ( x + T ) ) = ( F ` ( c + T ) ) )
175 fveq2 
 |-  ( x = c -> ( F ` x ) = ( F ` c ) )
176 174 175 eqeq12d 
 |-  ( x = c -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( c + T ) ) = ( F ` c ) ) )
177 173 176 imbi12d 
 |-  ( x = c -> ( ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) ) <-> ( ( ph /\ c e. RR ) -> ( F ` ( c + T ) ) = ( F ` c ) ) ) )
178 177 3 chvarvv 
 |-  ( ( ph /\ c e. RR ) -> ( F ` ( c + T ) ) = ( F ` c ) )
179 178 eqcomd 
 |-  ( ( ph /\ c e. RR ) -> ( F ` c ) = ( F ` ( c + T ) ) )
180 169 171 179 syl2anc 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( F ` c ) = ( F ` ( c + T ) ) )
181 9 ad2antlr 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> x e. RR )
182 169 181 3 syl2anc 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )
183 182 eqcomd 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( F ` x ) = ( F ` ( x + T ) ) )
184 180 183 oveq12d 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( ( F ` c ) - ( F ` x ) ) = ( ( F ` ( c + T ) ) - ( F ` ( x + T ) ) ) )
185 171 recnd 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> c e. CC )
186 78 adantr 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> x e. CC )
187 169 51 syl 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> T e. CC )
188 185 186 187 pnpcan2d 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( ( c + T ) - ( x + T ) ) = ( c - x ) )
189 188 eqcomd 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( c - x ) = ( ( c + T ) - ( x + T ) ) )
190 184 189 oveq12d 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( ( ( F ` c ) - ( F ` x ) ) / ( c - x ) ) = ( ( ( F ` ( c + T ) ) - ( F ` ( x + T ) ) ) / ( ( c + T ) - ( x + T ) ) ) )
191 190 fvoveq1d 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( abs ` ( ( ( ( F ` c ) - ( F ` x ) ) / ( c - x ) ) - w ) ) = ( abs ` ( ( ( ( F ` ( c + T ) ) - ( F ` ( x + T ) ) ) / ( ( c + T ) - ( x + T ) ) ) - w ) ) )
192 191 ad4ant13 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( ( F ` c ) - ( F ` x ) ) / ( c - x ) ) - w ) ) = ( abs ` ( ( ( ( F ` ( c + T ) ) - ( F ` ( x + T ) ) ) / ( ( c + T ) - ( x + T ) ) ) - w ) ) )
193 neeq1 
 |-  ( d = ( c + T ) -> ( d =/= ( x + T ) <-> ( c + T ) =/= ( x + T ) ) )
194 fvoveq1 
 |-  ( d = ( c + T ) -> ( abs ` ( d - ( x + T ) ) ) = ( abs ` ( ( c + T ) - ( x + T ) ) ) )
195 194 breq1d 
 |-  ( d = ( c + T ) -> ( ( abs ` ( d - ( x + T ) ) ) < b <-> ( abs ` ( ( c + T ) - ( x + T ) ) ) < b ) )
196 193 195 anbi12d 
 |-  ( d = ( c + T ) -> ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) <-> ( ( c + T ) =/= ( x + T ) /\ ( abs ` ( ( c + T ) - ( x + T ) ) ) < b ) ) )
197 196 imbrov2fvoveq 
 |-  ( d = ( c + T ) -> ( ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) <-> ( ( ( c + T ) =/= ( x + T ) /\ ( abs ` ( ( c + T ) - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` ( c + T ) ) - w ) ) < a ) ) )
198 simpllr 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) )
199 170 ad2antlr 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> c e. RR )
200 2 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> T e. RR )
201 199 200 readdcld 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> ( c + T ) e. RR )
202 eldifsni 
 |-  ( c e. ( RR \ { x } ) -> c =/= x )
203 202 adantl 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> c =/= x )
204 185 186 187 203 addneintr2d 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( c + T ) =/= ( x + T ) )
205 204 ad4ant13 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> ( c + T ) =/= ( x + T ) )
206 nelsn 
 |-  ( ( c + T ) =/= ( x + T ) -> -. ( c + T ) e. { ( x + T ) } )
207 205 206 syl 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> -. ( c + T ) e. { ( x + T ) } )
208 201 207 eldifd 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> ( c + T ) e. ( RR \ { ( x + T ) } ) )
209 197 198 208 rspcdva 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> ( ( ( c + T ) =/= ( x + T ) /\ ( abs ` ( ( c + T ) - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` ( c + T ) ) - w ) ) < a ) )
210 eqidd 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) = ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) )
211 fveq2 
 |-  ( y = ( c + T ) -> ( F ` y ) = ( F ` ( c + T ) ) )
212 211 oveq1d 
 |-  ( y = ( c + T ) -> ( ( F ` y ) - ( F ` ( x + T ) ) ) = ( ( F ` ( c + T ) ) - ( F ` ( x + T ) ) ) )
213 oveq1 
 |-  ( y = ( c + T ) -> ( y - ( x + T ) ) = ( ( c + T ) - ( x + T ) ) )
214 212 213 oveq12d 
 |-  ( y = ( c + T ) -> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) = ( ( ( F ` ( c + T ) ) - ( F ` ( x + T ) ) ) / ( ( c + T ) - ( x + T ) ) ) )
215 214 adantl 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) /\ y = ( c + T ) ) -> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) = ( ( ( F ` ( c + T ) ) - ( F ` ( x + T ) ) ) / ( ( c + T ) - ( x + T ) ) ) )
216 169 2 syl 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> T e. RR )
217 171 216 readdcld 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( c + T ) e. RR )
218 204 206 syl 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> -. ( c + T ) e. { ( x + T ) } )
219 217 218 eldifd 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( c + T ) e. ( RR \ { ( x + T ) } ) )
220 ovexd 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( ( ( F ` ( c + T ) ) - ( F ` ( x + T ) ) ) / ( ( c + T ) - ( x + T ) ) ) e. _V )
221 210 215 219 220 fvmptd 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` ( c + T ) ) = ( ( ( F ` ( c + T ) ) - ( F ` ( x + T ) ) ) / ( ( c + T ) - ( x + T ) ) ) )
222 221 eqcomd 
 |-  ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( ( ( F ` ( c + T ) ) - ( F ` ( x + T ) ) ) / ( ( c + T ) - ( x + T ) ) ) = ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` ( c + T ) ) )
223 222 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) /\ ( ( ( c + T ) =/= ( x + T ) /\ ( abs ` ( ( c + T ) - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` ( c + T ) ) - w ) ) < a ) ) -> ( ( ( F ` ( c + T ) ) - ( F ` ( x + T ) ) ) / ( ( c + T ) - ( x + T ) ) ) = ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` ( c + T ) ) )
224 223 fvoveq1d 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) /\ ( ( ( c + T ) =/= ( x + T ) /\ ( abs ` ( ( c + T ) - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` ( c + T ) ) - w ) ) < a ) ) -> ( abs ` ( ( ( ( F ` ( c + T ) ) - ( F ` ( x + T ) ) ) / ( ( c + T ) - ( x + T ) ) ) - w ) ) = ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` ( c + T ) ) - w ) ) )
225 204 adantr 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> ( c + T ) =/= ( x + T ) )
226 170 recnd 
 |-  ( c e. ( RR \ { x } ) -> c e. CC )
227 226 ad2antlr 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> c e. CC )
228 186 adantr 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> x e. CC )
229 187 adantr 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> T e. CC )
230 227 228 229 pnpcan2d 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> ( ( c + T ) - ( x + T ) ) = ( c - x ) )
231 230 fveq2d 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( c + T ) - ( x + T ) ) ) = ( abs ` ( c - x ) ) )
232 simpr 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( c - x ) ) < b )
233 231 232 eqbrtrd 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( c + T ) - ( x + T ) ) ) < b )
234 225 233 jca 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> ( ( c + T ) =/= ( x + T ) /\ ( abs ` ( ( c + T ) - ( x + T ) ) ) < b ) )
235 234 adantr 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) /\ ( ( ( c + T ) =/= ( x + T ) /\ ( abs ` ( ( c + T ) - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` ( c + T ) ) - w ) ) < a ) ) -> ( ( c + T ) =/= ( x + T ) /\ ( abs ` ( ( c + T ) - ( x + T ) ) ) < b ) )
236 simpr 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) /\ ( ( ( c + T ) =/= ( x + T ) /\ ( abs ` ( ( c + T ) - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` ( c + T ) ) - w ) ) < a ) ) -> ( ( ( c + T ) =/= ( x + T ) /\ ( abs ` ( ( c + T ) - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` ( c + T ) ) - w ) ) < a ) )
237 235 236 mpd 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) /\ ( ( ( c + T ) =/= ( x + T ) /\ ( abs ` ( ( c + T ) - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` ( c + T ) ) - w ) ) < a ) ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` ( c + T ) ) - w ) ) < a )
238 224 237 eqbrtrd 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) /\ ( ( ( c + T ) =/= ( x + T ) /\ ( abs ` ( ( c + T ) - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` ( c + T ) ) - w ) ) < a ) ) -> ( abs ` ( ( ( ( F ` ( c + T ) ) - ( F ` ( x + T ) ) ) / ( ( c + T ) - ( x + T ) ) ) - w ) ) < a )
239 238 ex 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> ( ( ( ( c + T ) =/= ( x + T ) /\ ( abs ` ( ( c + T ) - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` ( c + T ) ) - w ) ) < a ) -> ( abs ` ( ( ( ( F ` ( c + T ) ) - ( F ` ( x + T ) ) ) / ( ( c + T ) - ( x + T ) ) ) - w ) ) < a ) )
240 239 adantllr 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> ( ( ( ( c + T ) =/= ( x + T ) /\ ( abs ` ( ( c + T ) - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` ( c + T ) ) - w ) ) < a ) -> ( abs ` ( ( ( ( F ` ( c + T ) ) - ( F ` ( x + T ) ) ) / ( ( c + T ) - ( x + T ) ) ) - w ) ) < a ) )
241 209 240 mpd 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( ( F ` ( c + T ) ) - ( F ` ( x + T ) ) ) / ( ( c + T ) - ( x + T ) ) ) - w ) ) < a )
242 192 241 eqbrtrd 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( ( F ` c ) - ( F ` x ) ) / ( c - x ) ) - w ) ) < a )
243 242 adantrl 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) ) /\ c e. ( RR \ { x } ) ) /\ ( c =/= x /\ ( abs ` ( c - x ) ) < b ) ) -> ( abs ` ( ( ( ( F ` c ) - ( F ` x ) ) / ( c - x ) ) - w ) ) < a )
244 168 243 eqbrtrd 
 |-  ( ( ( ( ( ph /\ x e. dom G ) /\ A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) ) /\ c e. ( RR \ { x } ) ) /\ ( c =/= x /\ ( abs ` ( c - x ) ) < b ) ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a )
245 244 ex 
 |-  ( ( ( ( ph /\ x e. dom G ) /\ A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) ) /\ c e. ( RR \ { x } ) ) -> ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) )
246 245 ralrimiva 
 |-  ( ( ( ph /\ x e. dom G ) /\ A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) ) -> A. c e. ( RR \ { x } ) ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) )
247 157 246 impbida 
 |-  ( ( ph /\ x e. dom G ) -> ( A. c e. ( RR \ { x } ) ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) <-> A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) ) )
248 247 rexbidv 
 |-  ( ( ph /\ x e. dom G ) -> ( E. b e. RR+ A. c e. ( RR \ { x } ) ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) <-> E. b e. RR+ A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) ) )
249 248 ralbidv 
 |-  ( ( ph /\ x e. dom G ) -> ( A. a e. RR+ E. b e. RR+ A. c e. ( RR \ { x } ) ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) <-> A. a e. RR+ E. b e. RR+ A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) ) )
250 249 anbi2d 
 |-  ( ( ph /\ x e. dom G ) -> ( ( w e. CC /\ A. a e. RR+ E. b e. RR+ A. c e. ( RR \ { x } ) ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) ) <-> ( w e. CC /\ A. a e. RR+ E. b e. RR+ A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) ) ) )
251 39 38 10 dvlem 
 |-  ( ( ( ph /\ x e. dom G ) /\ y e. ( RR \ { x } ) ) -> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) e. CC )
252 251 fmpttd 
 |-  ( ( ph /\ x e. dom G ) -> ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) : ( RR \ { x } ) --> CC )
253 38 ssdifssd 
 |-  ( ( ph /\ x e. dom G ) -> ( RR \ { x } ) C_ CC )
254 252 253 78 ellimc3 
 |-  ( ( ph /\ x e. dom G ) -> ( w e. ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) limCC x ) <-> ( w e. CC /\ A. a e. RR+ E. b e. RR+ A. c e. ( RR \ { x } ) ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a ) ) ) )
255 39 38 12 dvlem 
 |-  ( ( ( ph /\ x e. dom G ) /\ y e. ( RR \ { ( x + T ) } ) ) -> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) e. CC )
256 255 fmpttd 
 |-  ( ( ph /\ x e. dom G ) -> ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) : ( RR \ { ( x + T ) } ) --> CC )
257 38 ssdifssd 
 |-  ( ( ph /\ x e. dom G ) -> ( RR \ { ( x + T ) } ) C_ CC )
258 12 recnd 
 |-  ( ( ph /\ x e. dom G ) -> ( x + T ) e. CC )
259 256 257 258 ellimc3 
 |-  ( ( ph /\ x e. dom G ) -> ( w e. ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) limCC ( x + T ) ) <-> ( w e. CC /\ A. a e. RR+ E. b e. RR+ A. d e. ( RR \ { ( x + T ) } ) ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a ) ) ) )
260 250 254 259 3bitr4d 
 |-  ( ( ph /\ x e. dom G ) -> ( w e. ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) limCC x ) <-> w e. ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) limCC ( x + T ) ) ) )
261 260 eqrdv 
 |-  ( ( ph /\ x e. dom G ) -> ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) limCC x ) = ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) limCC ( x + T ) ) )
262 fveq2 
 |-  ( y = z -> ( F ` y ) = ( F ` z ) )
263 262 oveq1d 
 |-  ( y = z -> ( ( F ` y ) - ( F ` ( x + T ) ) ) = ( ( F ` z ) - ( F ` ( x + T ) ) ) )
264 oveq1 
 |-  ( y = z -> ( y - ( x + T ) ) = ( z - ( x + T ) ) )
265 263 264 oveq12d 
 |-  ( y = z -> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) = ( ( ( F ` z ) - ( F ` ( x + T ) ) ) / ( z - ( x + T ) ) ) )
266 265 cbvmptv 
 |-  ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) = ( z e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` z ) - ( F ` ( x + T ) ) ) / ( z - ( x + T ) ) ) )
267 266 oveq1i 
 |-  ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) limCC ( x + T ) ) = ( ( z e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` z ) - ( F ` ( x + T ) ) ) / ( z - ( x + T ) ) ) ) limCC ( x + T ) )
268 261 267 eqtrdi 
 |-  ( ( ph /\ x e. dom G ) -> ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) limCC x ) = ( ( z e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` z ) - ( F ` ( x + T ) ) ) / ( z - ( x + T ) ) ) ) limCC ( x + T ) ) )
269 42 268 eleqtrd 
 |-  ( ( ph /\ x e. dom G ) -> ( G ` x ) e. ( ( z e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` z ) - ( F ` ( x + T ) ) ) / ( z - ( x + T ) ) ) ) limCC ( x + T ) ) )
270 eqid 
 |-  ( z e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` z ) - ( F ` ( x + T ) ) ) / ( z - ( x + T ) ) ) ) = ( z e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` z ) - ( F ` ( x + T ) ) ) / ( z - ( x + T ) ) ) )
271 37 a1i 
 |-  ( ph -> RR C_ CC )
272 ssidd 
 |-  ( ph -> RR C_ RR )
273 34 35 270 271 1 272 eldv 
 |-  ( ph -> ( ( x + T ) ( RR _D F ) ( G ` x ) <-> ( ( x + T ) e. ( ( int ` ( topGen ` ran (,) ) ) ` RR ) /\ ( G ` x ) e. ( ( z e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` z ) - ( F ` ( x + T ) ) ) / ( z - ( x + T ) ) ) ) limCC ( x + T ) ) ) ) )
274 273 adantr 
 |-  ( ( ph /\ x e. dom G ) -> ( ( x + T ) ( RR _D F ) ( G ` x ) <-> ( ( x + T ) e. ( ( int ` ( topGen ` ran (,) ) ) ` RR ) /\ ( G ` x ) e. ( ( z e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` z ) - ( F ` ( x + T ) ) ) / ( z - ( x + T ) ) ) ) limCC ( x + T ) ) ) ) )
275 21 269 274 mpbir2and 
 |-  ( ( ph /\ x e. dom G ) -> ( x + T ) ( RR _D F ) ( G ` x ) )
276 4 a1i 
 |-  ( ( ph /\ x e. dom G ) -> G = ( RR _D F ) )
277 276 breqd 
 |-  ( ( ph /\ x e. dom G ) -> ( ( x + T ) G ( G ` x ) <-> ( x + T ) ( RR _D F ) ( G ` x ) ) )
278 275 277 mpbird 
 |-  ( ( ph /\ x e. dom G ) -> ( x + T ) G ( G ` x ) )
279 4 a1i 
 |-  ( ph -> G = ( RR _D F ) )
280 279 funeqd 
 |-  ( ph -> ( Fun G <-> Fun ( RR _D F ) ) )
281 29 280 mpbird 
 |-  ( ph -> Fun G )
282 281 adantr 
 |-  ( ( ph /\ x e. dom G ) -> Fun G )
283 funbrfv2b 
 |-  ( Fun G -> ( ( x + T ) G ( G ` x ) <-> ( ( x + T ) e. dom G /\ ( G ` ( x + T ) ) = ( G ` x ) ) ) )
284 282 283 syl 
 |-  ( ( ph /\ x e. dom G ) -> ( ( x + T ) G ( G ` x ) <-> ( ( x + T ) e. dom G /\ ( G ` ( x + T ) ) = ( G ` x ) ) ) )
285 278 284 mpbid 
 |-  ( ( ph /\ x e. dom G ) -> ( ( x + T ) e. dom G /\ ( G ` ( x + T ) ) = ( G ` x ) ) )