Metamath Proof Explorer

Theorem ftc1cnnc

Description: Choice-free proof of ftc1cn . (Contributed by Brendan Leahy, 20-Nov-2017)

Ref Expression
Hypotheses ftc1cnnc.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
ftc1cnnc.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ftc1cnnc.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ftc1cnnc.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
ftc1cnnc.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
ftc1cnnc.i ⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
Assertion ftc1cnnc ( 𝜑 → ( ℝ D 𝐺 ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 ftc1cnnc.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
2 ftc1cnnc.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 ftc1cnnc.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 ftc1cnnc.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5 ftc1cnnc.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
6 ftc1cnnc.i ⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
7 dvf ⊢ ( ℝ D 𝐺 ) : dom ( ℝ D 𝐺 ) ⟶ ℂ
8 7 a1i ⊢ ( 𝜑 → ( ℝ D 𝐺 ) : dom ( ℝ D 𝐺 ) ⟶ ℂ )
9 8 ffund ⊢ ( 𝜑 → Fun ( ℝ D 𝐺 ) )
10 ax-resscn ⊢ ℝ ⊆ ℂ
11 10 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
12 ssidd ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) )
13 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
14 13 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
15 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
16 5 15 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
17 1 2 3 4 12 14 6 16 ftc1lem2 ⊢ ( 𝜑 → 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
18 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
19 2 3 18 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
20 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
21 20 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
22 11 17 19 21 20 dvbssntr ⊢ ( 𝜑 → dom ( ℝ D 𝐺 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) )
23 iccntr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
24 2 3 23 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
25 22 24 sseqtrd ⊢ ( 𝜑 → dom ( ℝ D 𝐺 ) ⊆ ( 𝐴 (,) 𝐵 ) )
26 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
27 21 26 eqeltrri ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ∈ Top
28 27 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ∈ Top )
29 19 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
30 iooretop ⊢ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
31 30 21 eleqtri ⊢ ( 𝐴 (,) 𝐵 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
32 31 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 (,) 𝐵 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
33 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
34 33 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
35 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
36 21 unieqi ⊢ ∪ ( topGen ‘ ran (,) ) = ∪ ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
37 35 36 eqtri ⊢ ℝ = ∪ ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
38 37 ssntr ⊢ ( ( ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ∈ Top ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) ∧ ( ( 𝐴 (,) 𝐵 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ∧ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ‘ ( 𝐴 [,] 𝐵 ) ) )
39 28 29 32 34 38 syl22anc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ‘ ( 𝐴 [,] 𝐵 ) ) )
40 simpr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑐 ∈ ( 𝐴 (,) 𝐵 ) )
41 39 40 sseldd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑐 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ‘ ( 𝐴 [,] 𝐵 ) ) )
42 16 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑐 ) ∈ ℂ )
43 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
44 13 10 sstri ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℂ
45 xmetres2 ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℂ ) → ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) ∈ ( ∞Met ‘ ( 𝐴 (,) 𝐵 ) ) )
46 43 44 45 mp2an ⊢ ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) ∈ ( ∞Met ‘ ( 𝐴 (,) 𝐵 ) )
47 46 a1i ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑤 ∈ ℝ+ ) → ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) ∈ ( ∞Met ‘ ( 𝐴 (,) 𝐵 ) ) )
48 43 a1i ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑤 ∈ ℝ+ ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
49 ssid ⊢ ℂ ⊆ ℂ
50 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) )
51 20 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
52 51 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
53 20 50 52 cncfcn ⊢ ( ( ( 𝐴 (,) 𝐵 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
54 44 49 53 mp2an ⊢ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) )
55 5 54 eleqtrdi ⊢ ( 𝜑 → 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
56 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 (,) 𝐵 ) ) )
57 51 44 56 mp2an ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 (,) 𝐵 ) )
58 57 toponunii ⊢ ( 𝐴 (,) 𝐵 ) = ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) )
59 58 eleq2i ⊢ ( 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ↔ 𝑐 ∈ ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) )
60 59 biimpi ⊢ ( 𝑐 ∈ ( 𝐴 (,) 𝐵 ) → 𝑐 ∈ ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) )
61 eqid ⊢ ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) = ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) )
62 61 cncnpi ⊢ ( ( 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) ∧ 𝑐 ∈ ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) ) → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑐 ) )
63 55 60 62 syl2an ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑐 ) )
64 eqid ⊢ ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) = ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) )
65 20 cnfldtopn ⊢ ( TopOpen ‘ ℂfld ) = ( MetOpen ‘ ( abs ∘ − ) )
66 eqid ⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) )
67 64 65 66 metrest ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) ) )
68 43 44 67 mp2an ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) )
69 68 oveq1i ⊢ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) = ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) )
70 69 fveq1i ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑐 ) = ( ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑐 )
71 63 70 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐹 ∈ ( ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑐 ) )
72 71 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑤 ∈ ℝ+ ) → 𝐹 ∈ ( ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑐 ) )
73 simpr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑤 ∈ ℝ+ ) → 𝑤 ∈ ℝ+ )
74 66 65 metcnpi2 ⊢ ( ( ( ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) ∈ ( ∞Met ‘ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ) ∧ ( 𝐹 ∈ ( ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑐 ) ∧ 𝑤 ∈ ℝ+ ) ) → ∃ 𝑣 ∈ ℝ+ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑢 ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) 𝑐 ) < 𝑣 → ( ( 𝐹 ‘ 𝑢 ) ( abs ∘ − ) ( 𝐹 ‘ 𝑐 ) ) < 𝑤 ) )
75 47 48 72 73 74 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑣 ∈ ℝ+ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑢 ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) 𝑐 ) < 𝑣 → ( ( 𝐹 ‘ 𝑢 ) ( abs ∘ − ) ( 𝐹 ‘ 𝑐 ) ) < 𝑤 ) )
76 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑢 ∈ ( 𝐴 (,) 𝐵 ) )
77 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑐 ∈ ( 𝐴 (,) 𝐵 ) )
78 76 77 ovresd ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑢 ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) 𝑐 ) = ( 𝑢 ( abs ∘ − ) 𝑐 ) )
79 elioore ⊢ ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) → 𝑢 ∈ ℝ )
80 79 recnd ⊢ ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) → 𝑢 ∈ ℂ )
81 44 sseli ⊢ ( 𝑐 ∈ ( 𝐴 (,) 𝐵 ) → 𝑐 ∈ ℂ )
82 81 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑐 ∈ ℂ )
83 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
84 83 cnmetdval ⊢ ( ( 𝑢 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( 𝑢 ( abs ∘ − ) 𝑐 ) = ( abs ‘ ( 𝑢 − 𝑐 ) ) )
85 80 82 84 syl2an2 ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑢 ( abs ∘ − ) 𝑐 ) = ( abs ‘ ( 𝑢 − 𝑐 ) ) )
86 78 85 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑢 ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) 𝑐 ) = ( abs ‘ ( 𝑢 − 𝑐 ) ) )
87 86 breq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑢 ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) 𝑐 ) < 𝑣 ↔ ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 ) )
88 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
89 88 ffvelrnda ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑢 ) ∈ ℂ )
90 42 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑐 ) ∈ ℂ )
91 83 cnmetdval ⊢ ( ( ( 𝐹 ‘ 𝑢 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℂ ) → ( ( 𝐹 ‘ 𝑢 ) ( abs ∘ − ) ( 𝐹 ‘ 𝑐 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) )
92 89 90 91 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ 𝑢 ) ( abs ∘ − ) ( 𝐹 ‘ 𝑐 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) )
93 92 breq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑢 ) ( abs ∘ − ) ( 𝐹 ‘ 𝑐 ) ) < 𝑤 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) )
94 87 93 imbi12d ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 𝑢 ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) 𝑐 ) < 𝑣 → ( ( 𝐹 ‘ 𝑢 ) ( abs ∘ − ) ( 𝐹 ‘ 𝑐 ) ) < 𝑤 ) ↔ ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) )
95 94 ralbidva ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) → ( ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑢 ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) 𝑐 ) < 𝑣 → ( ( 𝐹 ‘ 𝑢 ) ( abs ∘ − ) ( 𝐹 ‘ 𝑐 ) ) < 𝑤 ) ↔ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) )
96 simprll ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) → 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) )
97 eldifsni ⊢ ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) → 𝑧 ≠ 𝑐 )
98 96 97 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) → 𝑧 ≠ 𝑐 )
99 19 ssdifssd ⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ⊆ ℝ )
100 99 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ) → 𝑧 ∈ ℝ )
101 100 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ) → 𝑧 ∈ ℝ )
102 101 ad2ant2r ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) → 𝑧 ∈ ℝ )
103 elioore ⊢ ( 𝑐 ∈ ( 𝐴 (,) 𝐵 ) → 𝑐 ∈ ℝ )
104 103 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) → 𝑐 ∈ ℝ )
105 102 104 lttri2d ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) → ( 𝑧 ≠ 𝑐 ↔ ( 𝑧 < 𝑐 ∨ 𝑐 < 𝑧 ) ) )
106 105 biimpa ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 ≠ 𝑐 ) → ( 𝑧 < 𝑐 ∨ 𝑐 < 𝑧 ) )
107 fveq2 ⊢ ( 𝑠 = 𝑧 → ( 𝐺 ‘ 𝑠 ) = ( 𝐺 ‘ 𝑧 ) )
108 107 oveq1d ⊢ ( 𝑠 = 𝑧 → ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) = ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑐 ) ) )
109 oveq1 ⊢ ( 𝑠 = 𝑧 → ( 𝑠 − 𝑐 ) = ( 𝑧 − 𝑐 ) )
110 108 109 oveq12d ⊢ ( 𝑠 = 𝑧 → ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) = ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑧 − 𝑐 ) ) )
111 eqid ⊢ ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) = ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) )
112 ovex ⊢ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑧 − 𝑐 ) ) ∈ V
113 110 111 112 fvmpt ⊢ ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) → ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) = ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑧 − 𝑐 ) ) )
114 113 ad2antrr ⊢ ( ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) → ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) = ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑧 − 𝑐 ) ) )
115 114 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) → ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) = ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑧 − 𝑐 ) ) )
116 17 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) → 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
117 eldifi ⊢ ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) → 𝑧 ∈ ( 𝐴 [,] 𝐵 ) )
118 117 ad2antrr ⊢ ( ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) → 𝑧 ∈ ( 𝐴 [,] 𝐵 ) )
119 118 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) → 𝑧 ∈ ( 𝐴 [,] 𝐵 ) )
120 116 119 ffvelrnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
121 33 sseli ⊢ ( 𝑐 ∈ ( 𝐴 (,) 𝐵 ) → 𝑐 ∈ ( 𝐴 [,] 𝐵 ) )
122 17 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐺 ‘ 𝑐 ) ∈ ℂ )
123 121 122 sylan2 ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑐 ) ∈ ℂ )
124 123 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) → ( 𝐺 ‘ 𝑐 ) ∈ ℂ )
125 102 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) → 𝑧 ∈ ℝ )
126 125 recnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) → 𝑧 ∈ ℂ )
127 81 ad4antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) → 𝑐 ∈ ℂ )
128 ltne ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑧 < 𝑐 ) → 𝑐 ≠ 𝑧 )
129 128 necomd ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑧 < 𝑐 ) → 𝑧 ≠ 𝑐 )
130 102 129 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) → 𝑧 ≠ 𝑐 )
131 120 124 126 127 130 div2subd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) → ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑧 − 𝑐 ) ) = ( ( ( 𝐺 ‘ 𝑐 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑐 − 𝑧 ) ) )
132 115 131 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) → ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) = ( ( ( 𝐺 ‘ 𝑐 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑐 − 𝑧 ) ) )
133 132 fvoveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) → ( abs ‘ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) − ( 𝐹 ‘ 𝑐 ) ) ) = ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑐 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑐 − 𝑧 ) ) − ( 𝐹 ‘ 𝑐 ) ) ) )
134 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) → 𝐴 ∈ ℝ )
135 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) → 𝐵 ∈ ℝ )
136 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) → 𝐴 ≤ 𝐵 )
137 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
138 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) → 𝐹 ∈ 𝐿1 )
139 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) → 𝑐 ∈ ( 𝐴 (,) 𝐵 ) )
140 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) → 𝑤 ∈ ℝ+ )
141 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) → 𝑣 ∈ ℝ+ )
142 simprlr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) → ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) )
143 fvoveq1 ⊢ ( 𝑢 = 𝑦 → ( abs ‘ ( 𝑢 − 𝑐 ) ) = ( abs ‘ ( 𝑦 − 𝑐 ) ) )
144 143 breq1d ⊢ ( 𝑢 = 𝑦 → ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 ↔ ( abs ‘ ( 𝑦 − 𝑐 ) ) < 𝑣 ) )
145 144 imbrov2fvoveq ⊢ ( 𝑢 = 𝑦 → ( ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ↔ ( ( abs ‘ ( 𝑦 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) )
146 145 rspccva ⊢ ( ( ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( abs ‘ ( 𝑦 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) )
147 142 146 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( abs ‘ ( 𝑦 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) )
148 96 117 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) → 𝑧 ∈ ( 𝐴 [,] 𝐵 ) )
149 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) → ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 )
150 121 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) → 𝑐 ∈ ( 𝐴 [,] 𝐵 ) )
151 103 recnd ⊢ ( 𝑐 ∈ ( 𝐴 (,) 𝐵 ) → 𝑐 ∈ ℂ )
152 151 subidd ⊢ ( 𝑐 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝑐 − 𝑐 ) = 0 )
153 152 abs00bd ⊢ ( 𝑐 ∈ ( 𝐴 (,) 𝐵 ) → ( abs ‘ ( 𝑐 − 𝑐 ) ) = 0 )
154 153 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) → ( abs ‘ ( 𝑐 − 𝑐 ) ) = 0 )
155 141 rpgt0d ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) → 0 < 𝑣 )
156 154 155 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) → ( abs ‘ ( 𝑐 − 𝑐 ) ) < 𝑣 )
157 1 134 135 136 137 138 139 111 140 141 147 148 149 150 156 ftc1cnnclem ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑐 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑐 − 𝑧 ) ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 )
158 133 157 eqbrtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) → ( abs ‘ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 )
159 113 fvoveq1d ⊢ ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) → ( abs ‘ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) − ( 𝐹 ‘ 𝑐 ) ) ) = ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑧 − 𝑐 ) ) − ( 𝐹 ‘ 𝑐 ) ) ) )
160 159 ad2antrr ⊢ ( ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) − ( 𝐹 ‘ 𝑐 ) ) ) = ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑧 − 𝑐 ) ) − ( 𝐹 ‘ 𝑐 ) ) ) )
161 160 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) ∧ 𝑐 < 𝑧 ) → ( abs ‘ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) − ( 𝐹 ‘ 𝑐 ) ) ) = ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑧 − 𝑐 ) ) − ( 𝐹 ‘ 𝑐 ) ) ) )
162 1 134 135 136 137 138 139 111 140 141 147 150 156 148 149 ftc1cnnclem ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) ∧ 𝑐 < 𝑧 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑧 − 𝑐 ) ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 )
163 161 162 eqbrtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) ∧ 𝑐 < 𝑧 ) → ( abs ‘ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 )
164 158 163 jaodan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) ∧ ( 𝑧 < 𝑐 ∨ 𝑐 < 𝑧 ) ) → ( abs ‘ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 )
165 106 164 syldan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 ≠ 𝑐 ) → ( abs ‘ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 )
166 98 165 mpdan ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) ) → ( abs ‘ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 )
167 166 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ) → ( ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) )
168 167 adantld ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ∧ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ) → ( ( 𝑧 ≠ 𝑐 ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) )
169 168 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ) → ( ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) → ( ( 𝑧 ≠ 𝑐 ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) )
170 169 ralrimdva ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) → ( ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑢 − 𝑐 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) → ∀ 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ( ( 𝑧 ≠ 𝑐 ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) )
171 95 170 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) → ( ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑢 ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) 𝑐 ) < 𝑣 → ( ( 𝐹 ‘ 𝑢 ) ( abs ∘ − ) ( 𝐹 ‘ 𝑐 ) ) < 𝑤 ) → ∀ 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ( ( 𝑧 ≠ 𝑐 ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) )
172 171 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑣 ∈ ℝ+ ) → ( ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑢 ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) 𝑐 ) < 𝑣 → ( ( 𝐹 ‘ 𝑢 ) ( abs ∘ − ) ( 𝐹 ‘ 𝑐 ) ) < 𝑤 ) → ∀ 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ( ( 𝑧 ≠ 𝑐 ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) )
173 172 reximdva ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑤 ∈ ℝ+ ) → ( ∃ 𝑣 ∈ ℝ+ ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑢 ( ( abs ∘ − ) ↾ ( ( 𝐴 (,) 𝐵 ) × ( 𝐴 (,) 𝐵 ) ) ) 𝑐 ) < 𝑣 → ( ( 𝐹 ‘ 𝑢 ) ( abs ∘ − ) ( 𝐹 ‘ 𝑐 ) ) < 𝑤 ) → ∃ 𝑣 ∈ ℝ+ ∀ 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ( ( 𝑧 ≠ 𝑐 ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) )
174 75 173 mpd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑣 ∈ ℝ+ ∀ 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ( ( 𝑧 ≠ 𝑐 ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) )
175 174 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → ∀ 𝑤 ∈ ℝ+ ∃ 𝑣 ∈ ℝ+ ∀ 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ( ( 𝑧 ≠ 𝑐 ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) )
176 17 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
177 19 10 sstrdi ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
178 177 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
179 121 adantl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑐 ∈ ( 𝐴 [,] 𝐵 ) )
180 176 178 179 dvlem ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ) → ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ∈ ℂ )
181 180 fmpttd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) : ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ⟶ ℂ )
182 177 ssdifssd ⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ⊆ ℂ )
183 182 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ⊆ ℂ )
184 81 adantl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑐 ∈ ℂ )
185 181 183 184 ellimc3 ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ 𝑐 ) ∈ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) limℂ 𝑐 ) ↔ ( ( 𝐹 ‘ 𝑐 ) ∈ ℂ ∧ ∀ 𝑤 ∈ ℝ+ ∃ 𝑣 ∈ ℝ+ ∀ 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ( ( 𝑧 ≠ 𝑐 ∧ ( abs ‘ ( 𝑧 − 𝑐 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) ‘ 𝑧 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝑤 ) ) ) )
186 42 175 185 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑐 ) ∈ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) limℂ 𝑐 ) )
187 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
188 187 20 111 11 17 19 eldv ⊢ ( 𝜑 → ( 𝑐 ( ℝ D 𝐺 ) ( 𝐹 ‘ 𝑐 ) ↔ ( 𝑐 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) limℂ 𝑐 ) ) ) )
189 188 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑐 ( ℝ D 𝐺 ) ( 𝐹 ‘ 𝑐 ) ↔ ( 𝑐 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑠 − 𝑐 ) ) ) limℂ 𝑐 ) ) ) )
190 41 186 189 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑐 ( ℝ D 𝐺 ) ( 𝐹 ‘ 𝑐 ) )
191 vex ⊢ 𝑐 ∈ V
192 fvex ⊢ ( 𝐹 ‘ 𝑐 ) ∈ V
193 191 192 breldm ⊢ ( 𝑐 ( ℝ D 𝐺 ) ( 𝐹 ‘ 𝑐 ) → 𝑐 ∈ dom ( ℝ D 𝐺 ) )
194 190 193 syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑐 ∈ dom ( ℝ D 𝐺 ) )
195 25 194 eqelssd ⊢ ( 𝜑 → dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐵 ) )
196 df-fn ⊢ ( ( ℝ D 𝐺 ) Fn ( 𝐴 (,) 𝐵 ) ↔ ( Fun ( ℝ D 𝐺 ) ∧ dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐵 ) ) )
197 9 195 196 sylanbrc ⊢ ( 𝜑 → ( ℝ D 𝐺 ) Fn ( 𝐴 (,) 𝐵 ) )
198 16 ffnd ⊢ ( 𝜑 → 𝐹 Fn ( 𝐴 (,) 𝐵 ) )
199 9 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → Fun ( ℝ D 𝐺 ) )
200 funbrfv ⊢ ( Fun ( ℝ D 𝐺 ) → ( 𝑐 ( ℝ D 𝐺 ) ( 𝐹 ‘ 𝑐 ) → ( ( ℝ D 𝐺 ) ‘ 𝑐 ) = ( 𝐹 ‘ 𝑐 ) ) )
201 199 190 200 sylc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑐 ) = ( 𝐹 ‘ 𝑐 ) )
202 197 198 201 eqfnfvd ⊢ ( 𝜑 → ( ℝ D 𝐺 ) = 𝐹 )