Metamath Proof Explorer

Theorem ftc1lem5

Description: Lemma for ftc1 . (Contributed by Mario Carneiro, 14-Aug-2014) (Revised 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 ⊢ 𝐻 = ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) )
ftc1.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
ftc1.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
ftc1.fc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 ) )
ftc1.x1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 [,] 𝐵 ) )
ftc1.x2 ⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐶 ) ) < 𝑅 )
Assertion ftc1lem5 ( ( 𝜑 ∧ 𝑋 ≠ 𝐶 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑋 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 )

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 ftc1.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
15 ftc1.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
16 ftc1.fc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 ) )
17 ftc1.x1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 [,] 𝐵 ) )
18 ftc1.x2 ⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐶 ) ) < 𝑅 )
19 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
20 2 3 19 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
21 20 17 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
22 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
23 22 8 sseldi ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 [,] 𝐵 ) )
24 20 23 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
25 21 24 lttri2d ⊢ ( 𝜑 → ( 𝑋 ≠ 𝐶 ↔ ( 𝑋 < 𝐶 ∨ 𝐶 < 𝑋 ) ) )
26 25 biimpa ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝐶 ) → ( 𝑋 < 𝐶 ∨ 𝐶 < 𝑋 ) )
27 17 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐶 ) → 𝑋 ∈ ( 𝐴 [,] 𝐵 ) )
28 21 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐶 ) → 𝑋 ∈ ℝ )
29 simpr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐶 ) → 𝑋 < 𝐶 )
30 28 29 ltned ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐶 ) → 𝑋 ≠ 𝐶 )
31 eldifsn ⊢ ( 𝑋 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ↔ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑋 ≠ 𝐶 ) )
32 27 30 31 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐶 ) → 𝑋 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) )
33 fveq2 ⊢ ( 𝑧 = 𝑋 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑋 ) )
34 33 oveq1d ⊢ ( 𝑧 = 𝑋 → ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) = ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝐶 ) ) )
35 oveq1 ⊢ ( 𝑧 = 𝑋 → ( 𝑧 − 𝐶 ) = ( 𝑋 − 𝐶 ) )
36 34 35 oveq12d ⊢ ( 𝑧 = 𝑋 → ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) = ( ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑋 − 𝐶 ) ) )
37 ovex ⊢ ( ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑋 − 𝐶 ) ) ∈ V
38 36 13 37 fvmpt ⊢ ( 𝑋 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) → ( 𝐻 ‘ 𝑋 ) = ( ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑋 − 𝐶 ) ) )
39 32 38 syl ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐶 ) → ( 𝐻 ‘ 𝑋 ) = ( ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑋 − 𝐶 ) ) )
40 1 2 3 4 5 6 7 8 9 10 11 12 ftc1lem3 ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )
41 1 2 3 4 5 6 7 40 ftc1lem2 ⊢ ( 𝜑 → 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
42 41 17 ffvelrnd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ ℂ )
43 41 23 ffvelrnd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) ∈ ℂ )
44 42 43 subcld ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝐶 ) ) ∈ ℂ )
45 44 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐶 ) → ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝐶 ) ) ∈ ℂ )
46 21 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
47 24 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
48 46 47 subcld ⊢ ( 𝜑 → ( 𝑋 − 𝐶 ) ∈ ℂ )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐶 ) → ( 𝑋 − 𝐶 ) ∈ ℂ )
50 46 47 subeq0ad ⊢ ( 𝜑 → ( ( 𝑋 − 𝐶 ) = 0 ↔ 𝑋 = 𝐶 ) )
51 50 necon3bid ⊢ ( 𝜑 → ( ( 𝑋 − 𝐶 ) ≠ 0 ↔ 𝑋 ≠ 𝐶 ) )
52 51 biimpar ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝐶 ) → ( 𝑋 − 𝐶 ) ≠ 0 )
53 30 52 syldan ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐶 ) → ( 𝑋 − 𝐶 ) ≠ 0 )
54 45 49 53 div2negd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐶 ) → ( - ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝐶 ) ) / - ( 𝑋 − 𝐶 ) ) = ( ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑋 − 𝐶 ) ) )
55 42 43 negsubdi2d ⊢ ( 𝜑 → - ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝐶 ) ) = ( ( 𝐺 ‘ 𝐶 ) − ( 𝐺 ‘ 𝑋 ) ) )
56 46 47 negsubdi2d ⊢ ( 𝜑 → - ( 𝑋 − 𝐶 ) = ( 𝐶 − 𝑋 ) )
57 55 56 oveq12d ⊢ ( 𝜑 → ( - ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝐶 ) ) / - ( 𝑋 − 𝐶 ) ) = ( ( ( 𝐺 ‘ 𝐶 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝐶 − 𝑋 ) ) )
58 57 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐶 ) → ( - ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝐶 ) ) / - ( 𝑋 − 𝐶 ) ) = ( ( ( 𝐺 ‘ 𝐶 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝐶 − 𝑋 ) ) )
59 39 54 58 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐶 ) → ( 𝐻 ‘ 𝑋 ) = ( ( ( 𝐺 ‘ 𝐶 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝐶 − 𝑋 ) ) )
60 59 fvoveq1d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐶 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑋 ) − ( 𝐹 ‘ 𝐶 ) ) ) = ( abs ‘ ( ( ( ( 𝐺 ‘ 𝐶 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝐶 − 𝑋 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) )
61 47 subidd ⊢ ( 𝜑 → ( 𝐶 − 𝐶 ) = 0 )
62 61 abs00bd ⊢ ( 𝜑 → ( abs ‘ ( 𝐶 − 𝐶 ) ) = 0 )
63 15 rpgt0d ⊢ ( 𝜑 → 0 < 𝑅 )
64 62 63 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ ( 𝐶 − 𝐶 ) ) < 𝑅 )
65 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 23 64 ftc1lem4 ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐶 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝐶 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝐶 − 𝑋 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 )
66 60 65 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐶 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑋 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 )
67 17 adantr ⊢ ( ( 𝜑 ∧ 𝐶 < 𝑋 ) → 𝑋 ∈ ( 𝐴 [,] 𝐵 ) )
68 24 adantr ⊢ ( ( 𝜑 ∧ 𝐶 < 𝑋 ) → 𝐶 ∈ ℝ )
69 simpr ⊢ ( ( 𝜑 ∧ 𝐶 < 𝑋 ) → 𝐶 < 𝑋 )
70 68 69 gtned ⊢ ( ( 𝜑 ∧ 𝐶 < 𝑋 ) → 𝑋 ≠ 𝐶 )
71 67 70 31 sylanbrc ⊢ ( ( 𝜑 ∧ 𝐶 < 𝑋 ) → 𝑋 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) )
72 71 38 syl ⊢ ( ( 𝜑 ∧ 𝐶 < 𝑋 ) → ( 𝐻 ‘ 𝑋 ) = ( ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑋 − 𝐶 ) ) )
73 72 fvoveq1d ⊢ ( ( 𝜑 ∧ 𝐶 < 𝑋 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑋 ) − ( 𝐹 ‘ 𝐶 ) ) ) = ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑋 − 𝐶 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) )
74 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 23 64 17 18 ftc1lem4 ⊢ ( ( 𝜑 ∧ 𝐶 < 𝑋 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑋 − 𝐶 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 )
75 73 74 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝐶 < 𝑋 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑋 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 )
76 66 75 jaodan ⊢ ( ( 𝜑 ∧ ( 𝑋 < 𝐶 ∨ 𝐶 < 𝑋 ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑋 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 )
77 26 76 syldan ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝐶 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑋 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 )