Metamath Proof Explorer

Theorem ftc1lem6

Description: Lemma for ftc1 . (Contributed by Mario Carneiro, 14-Aug-2014) (Proof shortened by Mario Carneiro, 28-Dec-2016)

Ref Expression
Hypotheses ftc1.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
ftc1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ftc1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ftc1.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
ftc1.s ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
ftc1.d ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
ftc1.i ⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
ftc1.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 (,) 𝐵 ) )
ftc1.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ 𝐶 ) )
ftc1.j ⊢ 𝐽 = ( 𝐿 ↾t ℝ )
ftc1.k ⊢ 𝐾 = ( 𝐿 ↾t 𝐷 )
ftc1.l ⊢ 𝐿 = ( TopOpen ‘ ℂfld )
ftc1.h ⊢ 𝐻 = ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) )
Assertion ftc1lem6 ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ( 𝐻 limℂ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ftc1.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
2 ftc1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 ftc1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 ftc1.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5 ftc1.s ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
6 ftc1.d ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
7 ftc1.i ⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
8 ftc1.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 (,) 𝐵 ) )
9 ftc1.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ 𝐶 ) )
10 ftc1.j ⊢ 𝐽 = ( 𝐿 ↾t ℝ )
11 ftc1.k ⊢ 𝐾 = ( 𝐿 ↾t 𝐷 )
12 ftc1.l ⊢ 𝐿 = ( TopOpen ‘ ℂfld )
13 ftc1.h ⊢ 𝐻 = ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) )
14 1 2 3 4 5 6 7 8 9 10 11 12 ftc1lem3 ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )
15 5 8 sseldd ⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )
16 14 15 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
17 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
18 ax-resscn ⊢ ℝ ⊆ ℂ
19 6 18 sstrdi ⊢ ( 𝜑 → 𝐷 ⊆ ℂ )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → 𝐷 ⊆ ℂ )
21 xmetres2 ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐷 ⊆ ℂ ) → ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) ∈ ( ∞Met ‘ 𝐷 ) )
22 17 20 21 sylancr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) ∈ ( ∞Met ‘ 𝐷 ) )
23 17 a1i ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
24 eqid ⊢ ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) = ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) )
25 12 cnfldtopn ⊢ 𝐿 = ( MetOpen ‘ ( abs ∘ − ) )
26 eqid ⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) )
27 24 25 26 metrest ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐷 ⊆ ℂ ) → ( 𝐿 ↾t 𝐷 ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) ) )
28 17 19 27 sylancr ⊢ ( 𝜑 → ( 𝐿 ↾t 𝐷 ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) ) )
29 11 28 eqtrid ⊢ ( 𝜑 → 𝐾 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) ) )
30 29 oveq1d ⊢ ( 𝜑 → ( 𝐾 CnP 𝐿 ) = ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) ) CnP 𝐿 ) )
31 30 fveq1d ⊢ ( 𝜑 → ( ( 𝐾 CnP 𝐿 ) ‘ 𝐶 ) = ( ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) ) CnP 𝐿 ) ‘ 𝐶 ) )
32 9 31 eleqtrd ⊢ ( 𝜑 → 𝐹 ∈ ( ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) ) CnP 𝐿 ) ‘ 𝐶 ) )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → 𝐹 ∈ ( ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) ) CnP 𝐿 ) ‘ 𝐶 ) )
34 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → 𝑤 ∈ ℝ+ )
35 26 25 metcnpi2 ⊢ ( ( ( ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) ∈ ( ∞Met ‘ 𝐷 ) ∧ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ) ∧ ( 𝐹 ∈ ( ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) ) CnP 𝐿 ) ‘ 𝐶 ) ∧ 𝑤 ∈ ℝ+ ) ) → ∃ 𝑣 ∈ ℝ+ ∀ 𝑦 ∈ 𝐷 ( ( 𝑦 ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) 𝐶 ) < 𝑣 → ( ( 𝐹 ‘ 𝑦 ) ( abs ∘ − ) ( 𝐹 ‘ 𝐶 ) ) < 𝑤 ) )
36 22 23 33 34 35 syl22anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑣 ∈ ℝ+ ∀ 𝑦 ∈ 𝐷 ( ( 𝑦 ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) 𝐶 ) < 𝑣 → ( ( 𝐹 ‘ 𝑦 ) ( abs ∘ − ) ( 𝐹 ‘ 𝐶 ) ) < 𝑤 ) )
37 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝐷 ) → 𝑦 ∈ 𝐷 )
38 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝐷 ) → 𝐶 ∈ 𝐷 )
39 37 38 ovresd ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝐷 ) → ( 𝑦 ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) 𝐶 ) = ( 𝑦 ( abs ∘ − ) 𝐶 ) )
40 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) → 𝐷 ⊆ ℂ )
41 40 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝐷 ) → 𝑦 ∈ ℂ )
42 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
43 2 3 42 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
44 43 18 sstrdi ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
45 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
46 45 8 sselid ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 [,] 𝐵 ) )
47 44 46 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
48 47 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝐷 ) → 𝐶 ∈ ℂ )
49 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
50 49 cnmetdval ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝑦 ( abs ∘ − ) 𝐶 ) = ( abs ‘ ( 𝑦 − 𝐶 ) ) )
51 41 48 50 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝐷 ) → ( 𝑦 ( abs ∘ − ) 𝐶 ) = ( abs ‘ ( 𝑦 − 𝐶 ) ) )
52 39 51 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝐷 ) → ( 𝑦 ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) 𝐶 ) = ( abs ‘ ( 𝑦 − 𝐶 ) ) )
53 52 breq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑦 ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) 𝐶 ) < 𝑣 ↔ ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 ) )
54 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) → 𝐹 : 𝐷 ⟶ ℂ )
55 54 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
56 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝐷 ) → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
57 49 cnmetdval ⊢ ( ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝐶 ) ∈ ℂ ) → ( ( 𝐹 ‘ 𝑦 ) ( abs ∘ − ) ( 𝐹 ‘ 𝐶 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) )
58 55 56 57 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑦 ) ( abs ∘ − ) ( 𝐹 ‘ 𝐶 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) )
59 58 breq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝐷 ) → ( ( ( 𝐹 ‘ 𝑦 ) ( abs ∘ − ) ( 𝐹 ‘ 𝐶 ) ) < 𝑤 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) )
60 53 59 imbi12d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑦 ∈ 𝐷 ) → ( ( ( 𝑦 ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) 𝐶 ) < 𝑣 → ( ( 𝐹 ‘ 𝑦 ) ( abs ∘ − ) ( 𝐹 ‘ 𝐶 ) ) < 𝑤 ) ↔ ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) )
61 60 ralbidva ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) → ( ∀ 𝑦 ∈ 𝐷 ( ( 𝑦 ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) 𝐶 ) < 𝑣 → ( ( 𝐹 ‘ 𝑦 ) ( abs ∘ − ) ( 𝐹 ‘ 𝐶 ) ) < 𝑤 ) ↔ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) )
62 simprll ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ∧ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) ) → 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) )
63 eldifsni ⊢ ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) → 𝑠 ≠ 𝐶 )
64 62 63 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ∧ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) ) → 𝑠 ≠ 𝐶 )
65 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ∧ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) ) → 𝐴 ∈ ℝ )
66 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ∧ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) ) → 𝐵 ∈ ℝ )
67 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ∧ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) ) → 𝐴 ≤ 𝐵 )
68 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ∧ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) ) → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
69 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ∧ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) ) → 𝐷 ⊆ ℝ )
70 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ∧ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) ) → 𝐹 ∈ 𝐿1 )
71 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ∧ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) ) → 𝐶 ∈ ( 𝐴 (,) 𝐵 ) )
72 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ∧ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) ) → 𝐹 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ 𝐶 ) )
73 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ∧ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) ) → 𝑤 ∈ ℝ+ )
74 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ∧ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) ) → 𝑣 ∈ ℝ+ )
75 simprlr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ∧ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) ) → ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) )
76 fvoveq1 ⊢ ( 𝑦 = 𝑢 → ( abs ‘ ( 𝑦 − 𝐶 ) ) = ( abs ‘ ( 𝑢 − 𝐶 ) ) )
77 76 breq1d ⊢ ( 𝑦 = 𝑢 → ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 ↔ ( abs ‘ ( 𝑢 − 𝐶 ) ) < 𝑣 ) )
78 77 imbrov2fvoveq ⊢ ( 𝑦 = 𝑢 → ( ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ↔ ( ( abs ‘ ( 𝑢 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) )
79 78 rspccva ⊢ ( ( ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ∧ 𝑢 ∈ 𝐷 ) → ( ( abs ‘ ( 𝑢 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) )
80 75 79 sylan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ∧ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) ) ∧ 𝑢 ∈ 𝐷 ) → ( ( abs ‘ ( 𝑢 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) )
81 62 eldifad ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ∧ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) )
82 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ∧ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) ) → ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 )
83 1 65 66 67 68 69 70 71 72 10 11 12 13 73 74 80 81 82 ftc1lem5 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ∧ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) ) ∧ 𝑠 ≠ 𝐶 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑠 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 )
84 64 83 mpdan ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ∧ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑠 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 )
85 84 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ∧ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) ) → ( ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐻 ‘ 𝑠 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) )
86 85 adantld ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ∧ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) ) → ( ( 𝑠 ≠ 𝐶 ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑠 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) )
87 86 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ) → ( ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) → ( ( 𝑠 ≠ 𝐶 ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑠 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) )
88 87 ralrimdva ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) → ( ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑣 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) → ∀ 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ( ( 𝑠 ≠ 𝐶 ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑠 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) )
89 61 88 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) → ( ∀ 𝑦 ∈ 𝐷 ( ( 𝑦 ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) 𝐶 ) < 𝑣 → ( ( 𝐹 ‘ 𝑦 ) ( abs ∘ − ) ( 𝐹 ‘ 𝐶 ) ) < 𝑤 ) → ∀ 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ( ( 𝑠 ≠ 𝐶 ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑠 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) )
90 89 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑣 ∈ ℝ+ ) → ( ∀ 𝑦 ∈ 𝐷 ( ( 𝑦 ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) 𝐶 ) < 𝑣 → ( ( 𝐹 ‘ 𝑦 ) ( abs ∘ − ) ( 𝐹 ‘ 𝐶 ) ) < 𝑤 ) → ∀ 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ( ( 𝑠 ≠ 𝐶 ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑠 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) )
91 90 reximdva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ( ∃ 𝑣 ∈ ℝ+ ∀ 𝑦 ∈ 𝐷 ( ( 𝑦 ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) 𝐶 ) < 𝑣 → ( ( 𝐹 ‘ 𝑦 ) ( abs ∘ − ) ( 𝐹 ‘ 𝐶 ) ) < 𝑤 ) → ∃ 𝑣 ∈ ℝ+ ∀ 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ( ( 𝑠 ≠ 𝐶 ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑠 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) )
92 36 91 mpd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑣 ∈ ℝ+ ∀ 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ( ( 𝑠 ≠ 𝐶 ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑠 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) )
93 92 ralrimiva ⊢ ( 𝜑 → ∀ 𝑤 ∈ ℝ+ ∃ 𝑣 ∈ ℝ+ ∀ 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ( ( 𝑠 ≠ 𝐶 ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑠 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) )
94 1 2 3 4 5 6 7 14 ftc1lem2 ⊢ ( 𝜑 → 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
95 94 44 46 dvlem ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ) → ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ∈ ℂ )
96 95 13 fmptd ⊢ ( 𝜑 → 𝐻 : ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ⟶ ℂ )
97 44 ssdifssd ⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ⊆ ℂ )
98 96 97 47 ellimc3 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) ∈ ( 𝐻 limℂ 𝐶 ) ↔ ( ( 𝐹 ‘ 𝐶 ) ∈ ℂ ∧ ∀ 𝑤 ∈ ℝ+ ∃ 𝑣 ∈ ℝ+ ∀ 𝑠 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ( ( 𝑠 ≠ 𝐶 ∧ ( abs ‘ ( 𝑠 − 𝐶 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑠 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑤 ) ) ) )
99 16 93 98 mpbir2and ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ( 𝐻 limℂ 𝐶 ) )