fperdvper

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

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

Proof

Step	Hyp	Ref	Expression
1		fperdvper.f	\|- ( ph -> F : RR --> CC )
2		fperdvper.t	\|- ( ph -> T e. RR )
3		fperdvper.fper	\|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
4		fperdvper.g	\|- G = ( RR _D F )
5		dvbsss	\|- dom ( RR _D F ) C_ RR
6		id	\|- ( x e. dom G -> x e. dom G )
7	4	dmeqi	\|- dom G = dom ( RR _D F )
8	6 7	eleqtrdi	\|- ( x e. dom G -> x e. dom ( RR _D F ) )
9	5 8	sselid	\|- ( 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	ffvelcdmd	\|- ( ( 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	ffvelcdmd	\|- ( ( 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 ) ) )

Metamath Proof Explorer

Theorem fperdvper

Proof