Theorem fperdvper 37616

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

Hypotheses

Ref	Expression
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

Ref	Expression
fperdvper	|- ( ( ph /\ x e. dom G ) -> ( ( x + T ) e. dom G /\ ( G ` ( x + T ) ) = ( G ` x ) ) )

Distinct variable groups:   x, F   x, T   ph, x

Allowed substitution hint:   G( x)

Proof of Theorem fperdvper

Dummy variables a b c d w y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dvbsss 22849	. . . . . . . 8 |- dom ( RR _D F ) C_ RR
2		id 23	. . . . . . . . 9 |- ( x e. dom G -> x e. dom G )
3		fperdvper.g	. . . . . . . . . 10 |- G = ( RR _D F )
4	3	dmeqi 5053	. . . . . . . . 9 |- dom G = dom ( RR _D F )
5	2, 4	syl6eleq 2521	. . . . . . . 8 |- ( x e. dom G -> x e. dom ( RR _D F ) )
6	1, 5	sseldi 3463	. . . . . . 7 |- ( x e. dom G -> x e. RR )
7	6	adantl 468	. . . . . 6 |- ( ( ph /\ x e. dom G ) -> x e. RR )
8		fperdvper.t	. . . . . . 7 |- ( ph -> T e. RR )
9	8	adantr 467	. . . . . 6 |- ( ( ph /\ x e. dom G ) -> T e. RR )
10	7, 9	readdcld 9672	. . . . 5 |- ( ( ph /\ x e. dom G ) -> ( x + T ) e. RR )
11		reopn 37350	. . . . . . 7 |- RR e. ( topGen ` ran (,) )
12		retop 21774	. . . . . . . 8 |- ( topGen ` ran (,) ) e. Top
13		ssid 3484	. . . . . . . . 9 |- RR C_ RR
14	13	a1i 11	. . . . . . . 8 |- ( ( ph /\ x e. dom G ) -> RR C_ RR )
15		uniretop 21775	. . . . . . . . 9 |- RR = U. ( topGen ` ran (,) )
16	15	isopn3 20074	. . . . . . . 8 |- ( ( ( topGen ` ran (,) ) e. Top /\ RR C_ RR ) -> ( RR e. ( topGen ` ran (,) ) <-> ( ( int ` ( topGen ` ran (,) ) ) ` RR ) = RR ) )
17	12, 14, 16	sylancr 668	. . . . . . 7 |- ( ( ph /\ x e. dom G ) -> ( RR e. ( topGen ` ran (,) ) <-> ( ( int ` ( topGen ` ran (,) ) ) ` RR ) = RR ) )
18	11, 17	mpbii 215	. . . . . 6 |- ( ( ph /\ x e. dom G ) -> ( ( int ` ( topGen ` ran (,) ) ) ` RR ) = RR )
19	18	eqcomd 2431	. . . . 5 |- ( ( ph /\ x e. dom G ) -> RR = ( ( int ` ( topGen ` ran (,) ) ) ` RR ) )
20	10, 19	eleqtrd 2513	. . . 4 |- ( ( ph /\ x e. dom G ) -> ( x + T ) e. ( ( int ` ( topGen ` ran (,) ) ) ` RR ) )
21	5	adantl 468	. . . . . . . 8 |- ( ( ph /\ x e. dom G ) -> x e. dom ( RR _D F ) )
22	3	fveq1i 5880	. . . . . . . . . 10 |- ( G ` x ) = ( ( RR _D F ) ` x )
23	22	eqcomi 2436	. . . . . . . . 9 |- ( ( RR _D F ) ` x ) = ( G ` x )
24	23	a1i 11	. . . . . . . 8 |- ( ( ph /\ x e. dom G ) -> ( ( RR _D F ) ` x ) = ( G ` x ) )
25		dvf 22854	. . . . . . . . . . . 12 |- ( RR _D F ) : dom ( RR _D F ) --> CC
26		ffun 5746	. . . . . . . . . . . 12 |- ( ( RR _D F ) : dom ( RR _D F ) --> CC -> Fun ( RR _D F ) )
27	25, 26	ax-mp 5	. . . . . . . . . . 11 |- Fun ( RR _D F )
28	27	a1i 11	. . . . . . . . . 10 |- ( ph -> Fun ( RR _D F ) )
29		funbrfv2b 5923	. . . . . . . . . 10 |- ( Fun ( RR _D F ) -> ( x ( RR _D F ) ( G ` x ) <-> ( x e. dom ( RR _D F ) /\ ( ( RR _D F ) ` x ) = ( G ` x ) ) ) )
30	28, 29	syl 17	. . . . . . . . 9 |- ( ph -> ( x ( RR _D F ) ( G ` x ) <-> ( x e. dom ( RR _D F ) /\ ( ( RR _D F ) ` x ) = ( G ` x ) ) ) )
31	30	adantr 467	. . . . . . . 8 |- ( ( ph /\ x e. dom G ) -> ( x ( RR _D F ) ( G ` x ) <-> ( x e. dom ( RR _D F ) /\ ( ( RR _D F ) ` x ) = ( G ` x ) ) ) )
32	21, 24, 31	mpbir2and 931	. . . . . . 7 |- ( ( ph /\ x e. dom G ) -> x ( RR _D F ) ( G ` x ) )
33		eqid 2423	. . . . . . . . 9 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
34	33	tgioo2 21813	. . . . . . . 8 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
35		eqid 2423	. . . . . . . 8 |- ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) = ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) )
36		ax-resscn 9598	. . . . . . . . 9 |- RR C_ CC
37	36	a1i 11	. . . . . . . 8 |- ( ( ph /\ x e. dom G ) -> RR C_ CC )
38		fperdvper.f	. . . . . . . . 9 |- ( ph -> F : RR --> CC )
39	38	adantr 467	. . . . . . . 8 |- ( ( ph /\ x e. dom G ) -> F : RR --> CC )
40	34, 33, 35, 37, 39, 14	eldv 22845	. . . . . . 7 |- ( ( 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 ) ) ) lim CC x ) ) ) )
41	32, 40	mpbid 214	. . . . . 6 |- ( ( ph /\ x e. dom G ) -> ( x e. ( ( int ` ( topGen ` ran (,) ) ) ` RR ) /\ ( G ` x ) e. ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) lim CC x ) ) )
42	41	simprd 465	. . . . 5 |- ( ( ph /\ x e. dom G ) -> ( G ` x ) e. ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) lim CC x ) )
43		eqidd 2424	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 5879	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y = d -> ( F ` y ) = ( F ` d ) )
45	44	oveq1d 6318	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y = d -> ( ( F ` y ) - ( F ` ( x + T ) ) ) = ( ( F ` d ) - ( F ` ( x + T ) ) ) )
46		oveq1 6310	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y = d -> ( y - ( x + T ) ) = ( d - ( x + T ) ) )
47	45, 46	oveq12d 6321	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = d -> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) = ( ( ( F ` d ) - ( F ` ( x + T ) ) ) / ( d - ( x + T ) ) ) )
48		eldifi 3588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( d e. ( RR \ { ( x + T ) } ) -> d e. RR )
49	48	recnd 9671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( d e. ( RR \ { ( x + T ) } ) -> d e. CC )
50	49	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> d e. CC )
51	8	recnd 9671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ph -> T e. CC )
52	51	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> T e. CC )
53	50, 52	npcand 9992	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ( d - T ) + T ) = d )
54	53	eqcomd 2431	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> d = ( ( d - T ) + T ) )
55	54	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> ( F ` d ) = ( F ` ( ( d - T ) + T ) ) )
56		ovex 6331	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( d - T ) e. _V
57	48	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> d e. RR )
58	8	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> T e. RR )
59	57, 58	resubcld 10049	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> ( d - T ) e. RR )
60	59	ex 436	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> ( d e. ( RR \ { ( x + T ) } ) -> ( d - T ) e. RR ) )
61	60	imdistani 695	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ph /\ ( d - T ) e. RR ) )
62		eleq1 2495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x = ( d - T ) -> ( x e. RR <-> ( d - T ) e. RR ) )
63	62	anbi2d 709	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x = ( d - T ) -> ( ( ph /\ x e. RR ) <-> ( ph /\ ( d - T ) e. RR ) ) )
64		oveq1 6310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( x = ( d - T ) -> ( x + T ) = ( ( d - T ) + T ) )
65	64	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x = ( d - T ) -> ( F ` ( x + T ) ) = ( F ` ( ( d - T ) + T ) ) )
66		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x = ( d - T ) -> ( F ` x ) = ( F ` ( d - T ) ) )
67	65, 66	eqeq12d 2445	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x = ( d - T ) -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( ( d - T ) + T ) ) = ( F ` ( d - T ) ) ) )
68	63, 67	imbi12d 322	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x = ( d - T ) -> ( ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) ) <-> ( ( ph /\ ( d - T ) e. RR ) -> ( F ` ( ( d - T ) + T ) ) = ( F ` ( d - T ) ) ) ) )
69		fperdvper.fper	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
70	68, 69	vtoclg 3140	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( d - T ) e. _V -> ( ( ph /\ ( d - T ) e. RR ) -> ( F ` ( ( d - T ) + T ) ) = ( F ` ( d - T ) ) ) )
71	56, 61, 70	mpsyl 66	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> ( F ` ( ( d - T ) + T ) ) = ( F ` ( d - T ) ) )
72	55, 71	eqtrd 2464	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> ( F ` d ) = ( F ` ( d - T ) ) )
73	72	adantlr 720	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( F ` d ) = ( F ` ( d - T ) ) )
74		simpll 759	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ph )
75	6	ad2antlr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> x e. RR )
76	74, 75, 69	syl2anc 666	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )
77	73, 76	oveq12d 6321	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ( F ` d ) - ( F ` ( x + T ) ) ) = ( ( F ` ( d - T ) ) - ( F ` x ) ) )
78	49	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> d e. CC )
79	74, 51	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> T e. CC )
80	7	recnd 9671	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ x e. dom G ) -> x e. CC )
81	80	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> x e. CC )
82	78, 79, 81	subsub4d 10019	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ( d - T ) - x ) = ( d - ( T + x ) ) )
83	79, 81	addcomd 9837	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( T + x ) = ( x + T ) )
84	83	oveq2d 6319	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( d - ( T + x ) ) = ( d - ( x + T ) ) )
85	82, 84	eqtr2d 2465	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( d - ( x + T ) ) = ( ( d - T ) - x ) )
86	77, 85	oveq12d 6321	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 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 ) ) )
87	47, 86	sylan9eqr 2486	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 ) ) )
88		simpr 463	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> d e. ( RR \ { ( x + T ) } ) )
89	38	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> F : RR --> CC )
90	89, 59	ffvelrnd 6036	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ d e. ( RR \ { ( x + T ) } ) ) -> ( F ` ( d - T ) ) e. CC )
91	90	adantlr 720	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( F ` ( d - T ) ) e. CC )
92	39, 7	ffvelrnd 6036	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ x e. dom G ) -> ( F ` x ) e. CC )
93	92	adantr 467	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( F ` x ) e. CC )
94	91, 93	subcld 9988	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ( F ` ( d - T ) ) - ( F ` x ) ) e. CC )
95	78, 79	subcld 9988	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( d - T ) e. CC )
96	95, 81	subcld 9988	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ( d - T ) - x ) e. CC )
97		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( d - T ) = x ) -> ( d - T ) = x )
98	49	ad2antlr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( d - T ) = x ) -> d e. CC )
99	79	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( d - T ) = x ) -> T e. CC )
100	81	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( d - T ) = x ) -> x e. CC )
101	98, 99, 100	subadd2d 10007	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( d - T ) = x ) -> ( ( d - T ) = x <-> ( x + T ) = d ) )
102	97, 101	mpbid 214	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( d - T ) = x ) -> ( x + T ) = d )
103	102	eqcomd 2431	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( d - T ) = x ) -> d = ( x + T ) )
104		eldifsni 4124	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( d e. ( RR \ { ( x + T ) } ) -> d =/= ( x + T ) )
105	104	ad2antlr 732	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( d - T ) = x ) -> d =/= ( x + T ) )
106	105	neneqd 2626	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( d - T ) = x ) -> -. d = ( x + T ) )
107	103, 106	pm2.65da 579	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> -. ( d - T ) = x )
108	107	neqned 2628	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( d - T ) =/= x )
109	95, 81, 108	subne0d 9997	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ( d - T ) - x ) =/= 0 )
110	94, 96, 109	divcld 10385	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ( ( F ` ( d - T ) ) - ( F ` x ) ) / ( ( d - T ) - x ) ) e. CC )
111	43, 87, 88, 110	fvmptd 5968	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) ) )
112	111	oveq1d 6318	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) = ( ( ( ( F ` ( d - T ) ) - ( F ` x ) ) / ( ( d - T ) - x ) ) - w ) )
113	112	fveq2d 5883	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) ) )
114	113	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. dom G ) /\ 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 ) ) )
115	114	adantllr 724	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( 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 ) ) )
116		simpllr 768	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( 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 ) )
117	48	ad2antlr 732	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( 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 )
118	8	ad4antr 737	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( 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 )
119	117, 118	resubcld 10049	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( 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 )
120		elsni 4022	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( d - T ) e. { x } -> ( d - T ) = x )
121	107, 120	nsyl 125	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> -. ( d - T ) e. { x } )
122	121	adantr 467	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> -. ( d - T ) e. { x } )
123	122	adantllr 724	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( 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	119, 123	eldifd 3448	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( 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		neeq1 2706	. . . . . . . . . . . . . . . . . . . . 21 |- ( c = ( d - T ) -> ( c =/= x <-> ( d - T ) =/= x ) )
126		oveq1 6310	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( c = ( d - T ) -> ( c - x ) = ( ( d - T ) - x ) )
127	126	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . 22 |- ( c = ( d - T ) -> ( abs ` ( c - x ) ) = ( abs ` ( ( d - T ) - x ) ) )
128	127	breq1d 4431	. . . . . . . . . . . . . . . . . . . . 21 |- ( c = ( d - T ) -> ( ( abs ` ( c - x ) ) < b <-> ( abs ` ( ( d - T ) - x ) ) < b ) )
129	125, 128	anbi12d 716	. . . . . . . . . . . . . . . . . . . 20 |- ( c = ( d - T ) -> ( ( c =/= x /\ ( abs ` ( c - x ) ) < b ) <-> ( ( d - T ) =/= x /\ ( abs ` ( ( d - T ) - x ) ) < b ) ) )
130		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( c = ( d - T ) -> ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) = ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` ( d - T ) ) )
131	130	oveq1d 6318	. . . . . . . . . . . . . . . . . . . . . 22 |- ( c = ( d - T ) -> ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) = ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` ( d - T ) ) - w ) )
132	131	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . 21 |- ( c = ( d - T ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) = ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` ( d - T ) ) - w ) ) )
133	132	breq1d 4431	. . . . . . . . . . . . . . . . . . . 20 |- ( c = ( d - T ) -> ( ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) ) < a <-> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` ( d - T ) ) - w ) ) < a ) )
134	129, 133	imbi12d 322	. . . . . . . . . . . . . . . . . . 19 |- ( 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 ) ) )
135	134	rspccva 3182	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 - T ) e. ( RR \ { x } ) ) -> ( ( ( d - T ) =/= x /\ ( abs ` ( ( d - T ) - x ) ) < b ) -> ( abs ` ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` ( d - T ) ) - w ) ) < a ) )
136	116, 124, 135	syl2anc 666	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( 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 ) )
137		eqidd 2424	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 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 ) ) ) )
138		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ y = ( d - T ) ) -> y = ( d - T ) )
139	138	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ y = ( d - T ) ) -> ( F ` y ) = ( F ` ( d - T ) ) )
140	139	oveq1d 6318	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ y = ( d - T ) ) -> ( ( F ` y ) - ( F ` x ) ) = ( ( F ` ( d - T ) ) - ( F ` x ) ) )
141	138	oveq1d 6318	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ y = ( d - T ) ) -> ( y - x ) = ( ( d - T ) - x ) )
142	140, 141	oveq12d 6321	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( 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 ) ) )
143	48	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> d e. RR )
144	74, 8	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> T e. RR )
145	143, 144	resubcld 10049	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( d - T ) e. RR )
146	145, 121	eldifd 3448	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( d - T ) e. ( RR \ { x } ) )
147	137, 142, 146, 110	fvmptd 5968	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( 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 ) ) )
148	147	eqcomd 2431	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( 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 ) ) )
149	148	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( 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 ) ) )
150	149	oveq1d 6318	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( 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 ) ) - w ) = ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` ( d - T ) ) - w ) )
151	150	fveq2d 5883	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( 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 ) ) )
152	108	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( d - T ) =/= x )
153	85	eqcomd 2431	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) -> ( ( d - T ) - x ) = ( d - ( x + T ) ) )
154	153	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( ( d - T ) - x ) = ( d - ( x + T ) ) )
155	154	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( d - T ) - x ) ) = ( abs ` ( d - ( x + T ) ) ) )
156		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( d - ( x + T ) ) ) < b )
157	155, 156	eqbrtrd 4442	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( abs ` ( ( d - T ) - x ) ) < b )
158	152, 157	jca 535	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ x e. dom G ) /\ d e. ( RR \ { ( x + T ) } ) ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) -> ( ( d - T ) =/= x /\ ( abs ` ( ( d - T ) - x ) ) < b ) )
159	158	adantr 467	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( 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 ) )
160		simpr 463	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( 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 ) )
161	159, 160	mpd 15	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( 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 )
162	151, 161	eqbrtrd 4442	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( 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 )
163	162	ex 436	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 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 ) )
164	163	adantllr 724	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( 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 ) )
165	136, 164	mpd 15	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( 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 )
166	165	adantrl 721	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( 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 )
167	115, 166	eqbrtrd 4442	. . . . . . . . . . . . . 14 |- ( ( ( ( ( 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 )
168	167	ex 436	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) )
169	168	ralrimiva 2840	. . . . . . . . . . . 12 |- ( ( ( 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 ) )
170		eqidd 2424	. . . . . . . . . . . . . . . . . . 19 |- ( c e. ( RR \ { x } ) -> ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) = ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) )
171		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y = c -> ( F ` y ) = ( F ` c ) )
172	171	oveq1d 6318	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = c -> ( ( F ` y ) - ( F ` x ) ) = ( ( F ` c ) - ( F ` x ) ) )
173		oveq1 6310	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = c -> ( y - x ) = ( c - x ) )
174	172, 173	oveq12d 6321	. . . . . . . . . . . . . . . . . . . 20 |- ( y = c -> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) = ( ( ( F ` c ) - ( F ` x ) ) / ( c - x ) ) )
175	174	adantl 468	. . . . . . . . . . . . . . . . . . 19 |- ( ( c e. ( RR \ { x } ) /\ y = c ) -> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) = ( ( ( F ` c ) - ( F ` x ) ) / ( c - x ) ) )
176		id 23	. . . . . . . . . . . . . . . . . . 19 |- ( c e. ( RR \ { x } ) -> c e. ( RR \ { x } ) )
177		ovex 6331	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( F ` c ) - ( F ` x ) ) / ( c - x ) ) e. _V
178	177	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( c e. ( RR \ { x } ) -> ( ( ( F ` c ) - ( F ` x ) ) / ( c - x ) ) e. _V )
179	170, 175, 176, 178	fvmptd 5968	. . . . . . . . . . . . . . . . . 18 |- ( c e. ( RR \ { x } ) -> ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) = ( ( ( F ` c ) - ( F ` x ) ) / ( c - x ) ) )
180	179	oveq1d 6318	. . . . . . . . . . . . . . . . 17 |- ( c e. ( RR \ { x } ) -> ( ( ( y e. ( RR \ { x } ) |-> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) ` c ) - w ) = ( ( ( ( F ` c ) - ( F ` x ) ) / ( c - x ) ) - w ) )
181	180	fveq2d 5883	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) )
182	181	ad2antlr 732	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( 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 ) ) )
183		simpll 759	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ph )
184		eldifi 3588	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( c e. ( RR \ { x } ) -> c e. RR )
185	184	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> c e. RR )
186		eleq1 2495	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x = c -> ( x e. RR <-> c e. RR ) )
187	186	anbi2d 709	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x = c -> ( ( ph /\ x e. RR ) <-> ( ph /\ c e. RR ) ) )
188		oveq1 6310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x = c -> ( x + T ) = ( c + T ) )
189	188	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x = c -> ( F ` ( x + T ) ) = ( F ` ( c + T ) ) )
190		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x = c -> ( F ` x ) = ( F ` c ) )
191	189, 190	eqeq12d 2445	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x = c -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( c + T ) ) = ( F ` c ) ) )
192	187, 191	imbi12d 322	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x = c -> ( ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) ) <-> ( ( ph /\ c e. RR ) -> ( F ` ( c + T ) ) = ( F ` c ) ) ) )
193	192, 69	chvarv 2069	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ c e. RR ) -> ( F ` ( c + T ) ) = ( F ` c ) )
194	193	eqcomd 2431	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ c e. RR ) -> ( F ` c ) = ( F ` ( c + T ) ) )
195	183, 185, 194	syl2anc 666	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( F ` c ) = ( F ` ( c + T ) ) )
196	6	ad2antlr 732	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> x e. RR )
197	183, 196, 69	syl2anc 666	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )
198	197	eqcomd 2431	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( F ` x ) = ( F ` ( x + T ) ) )
199	195, 198	oveq12d 6321	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( ( F ` c ) - ( F ` x ) ) = ( ( F ` ( c + T ) ) - ( F ` ( x + T ) ) ) )
200	185	recnd 9671	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> c e. CC )
201	80	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> x e. CC )
202	183, 51	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> T e. CC )
203	200, 201, 202	pnpcan2d 10026	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( ( c + T ) - ( x + T ) ) = ( c - x ) )
204	203	eqcomd 2431	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( c - x ) = ( ( c + T ) - ( x + T ) ) )
205	199, 204	oveq12d 6321	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 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 ) ) ) )
206	205	oveq1d 6318	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( ( ( ( F ` c ) - ( F ` x ) ) / ( c - x ) ) - w ) = ( ( ( ( F ` ( c + T ) ) - ( F ` ( x + T ) ) ) / ( ( c + T ) - ( x + T ) ) ) - w ) )
207	206	fveq2d 5883	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) ) )
208	207	adantr 467	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ x e. dom G ) /\ 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 ) ) )
209	208	adantllr 724	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( 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 ) ) )
210		simpllr 768	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( 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 ) )
211	184	ad2antlr 732	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( 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 )
212	8	ad4antr 737	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( 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 )
213	211, 212	readdcld 9672	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( 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 )
214		eldifsni 4124	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( c e. ( RR \ { x } ) -> c =/= x )
215	214	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> c =/= x )
216	200, 201, 202, 215	addneintr2d 9843	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( c + T ) =/= ( x + T ) )
217	216	adantr 467	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) -> ( c + T ) =/= ( x + T ) )
218	217	adantllr 724	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( 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 ) )
219		elsni 4022	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( c + T ) e. { ( x + T ) } -> ( c + T ) = ( x + T ) )
220	219	necon3ai 2653	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( c + T ) =/= ( x + T ) -> -. ( c + T ) e. { ( x + T ) } )
221	218, 220	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( 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 ) } )
222	213, 221	eldifd 3448	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( 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 ) } ) )
223		neeq1 2706	. . . . . . . . . . . . . . . . . . . . . 22 |- ( d = ( c + T ) -> ( d =/= ( x + T ) <-> ( c + T ) =/= ( x + T ) ) )
224		oveq1 6310	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( d = ( c + T ) -> ( d - ( x + T ) ) = ( ( c + T ) - ( x + T ) ) )
225	224	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( d = ( c + T ) -> ( abs ` ( d - ( x + T ) ) ) = ( abs ` ( ( c + T ) - ( x + T ) ) ) )
226	225	breq1d 4431	. . . . . . . . . . . . . . . . . . . . . 22 |- ( d = ( c + T ) -> ( ( abs ` ( d - ( x + T ) ) ) < b <-> ( abs ` ( ( c + T ) - ( x + T ) ) ) < b ) )
227	223, 226	anbi12d 716	. . . . . . . . . . . . . . . . . . . . 21 |- ( d = ( c + T ) -> ( ( d =/= ( x + T ) /\ ( abs ` ( d - ( x + T ) ) ) < b ) <-> ( ( c + T ) =/= ( x + T ) /\ ( abs ` ( ( c + T ) - ( x + T ) ) ) < b ) ) )
228		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( d = ( c + T ) -> ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) = ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` ( c + T ) ) )
229	228	oveq1d 6318	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( d = ( c + T ) -> ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) = ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` ( c + T ) ) - w ) )
230	229	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . 22 |- ( d = ( c + T ) -> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) = ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` ( c + T ) ) - w ) ) )
231	230	breq1d 4431	. . . . . . . . . . . . . . . . . . . . 21 |- ( d = ( c + T ) -> ( ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` d ) - w ) ) < a <-> ( abs ` ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` ( c + T ) ) - w ) ) < a ) )
232	227, 231	imbi12d 322	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) ) )
233	232	rspccva 3182	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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 + T ) e. ( RR \ { ( x + T ) } ) ) -> ( ( ( 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 ) )
234	210, 222, 233	syl2anc 666	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( 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 ) )
235		eqidd 2424	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( 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 ) ) ) ) )
236		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( y = ( c + T ) -> ( F ` y ) = ( F ` ( c + T ) ) )
237	236	oveq1d 6318	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( y = ( c + T ) -> ( ( F ` y ) - ( F ` ( x + T ) ) ) = ( ( F ` ( c + T ) ) - ( F ` ( x + T ) ) ) )
238		oveq1 6310	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( y = ( c + T ) -> ( y - ( x + T ) ) = ( ( c + T ) - ( x + T ) ) )
239	237, 238	oveq12d 6321	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( y = ( c + T ) -> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) = ( ( ( F ` ( c + T ) ) - ( F ` ( x + T ) ) ) / ( ( c + T ) - ( x + T ) ) ) )
240	239	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( 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 ) ) ) )
241	183, 8	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> T e. RR )
242	185, 241	readdcld 9672	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( c + T ) e. RR )
243	216, 220	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> -. ( c + T ) e. { ( x + T ) } )
244	242, 243	eldifd 3448	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( c + T ) e. ( RR \ { ( x + T ) } ) )
245	205, 177	syl6eqelr 2520	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) -> ( ( ( F ` ( c + T ) ) - ( F ` ( x + T ) ) ) / ( ( c + T ) - ( x + T ) ) ) e. _V )
246	235, 240, 244, 245	fvmptd 5968	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 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 ) ) ) )
247	246	eqcomd 2431	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( 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 ) ) )
248	247	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( 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 ) ) )
249	248	oveq1d 6318	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( 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 ) ) ) - w ) = ( ( ( y e. ( RR \ { ( x + T ) } ) |-> ( ( ( F ` y ) - ( F ` ( x + T ) ) ) / ( y - ( x + T ) ) ) ) ` ( c + T ) ) - w ) )
250	249	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ x e. dom G ) /\ c e. ( RR \ { x } ) ) /\ ( abs ` ( c - x ) ) < b ) /\ ( ( ( c + T ) =/= ( x + T ) /\ ( abs ` ( ( c + T ) - ( x + T ) ) ) <