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 sselid ⊢ ( 𝑥 ∈ 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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( ℝ ∖ { ( 𝑥 + 𝑇 ) } ) ) → ( 𝐹 ‘ ( 𝑑 − 𝑇 ) ) ∈ ℂ )
89 88 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) ∧ 𝑑 ∈ ( ℝ ∖ { ( 𝑥 + 𝑇 ) } ) ) → ( 𝐹 ‘ ( 𝑑 − 𝑇 ) ) ∈ ℂ )
90 39 10 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 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 𝐺 ∧ ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐺 ‘ 𝑥 ) ) )