Metamath Proof Explorer


Theorem fperdvper

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

Ref Expression
Hypotheses fperdvper.f ( 𝜑𝐹 : ℝ ⟶ ℂ )
fperdvper.t ( 𝜑𝑇 ∈ ℝ )
fperdvper.fper ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹𝑥 ) )
fperdvper.g 𝐺 = ( ℝ D 𝐹 )
Assertion fperdvper ( ( 𝜑𝑥 ∈ dom 𝐺 ) → ( ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐺𝑥 ) ) )

Proof

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