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 ) ) ) |