Metamath Proof Explorer

Theorem ftc1

Description: The Fundamental Theorem of Calculus, part one. The function formed by varying the right endpoint of an integral is differentiable at C with derivative F ( C ) if the original function is continuous at C . This is part of Metamath 100 proof #15. (Contributed by Mario Carneiro, 1-Sep-2014)

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 )
Assertion ftc1 ( 𝜑 → 𝐶 ( ℝ D 𝐺 ) ( 𝐹 ‘ 𝐶 ) )

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 12 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( 𝐿 ↾t ℝ )
14 10 13 eqtr4i ⊢ 𝐽 = ( topGen ‘ ran (,) )
15 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
16 14 15 eqeltri ⊢ 𝐽 ∈ Top
17 16 a1i ⊢ ( 𝜑 → 𝐽 ∈ Top )
18 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
19 2 3 18 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
20 iooretop ⊢ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
21 20 14 eleqtrri ⊢ ( 𝐴 (,) 𝐵 ) ∈ 𝐽
22 21 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ 𝐽 )
23 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
24 23 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
25 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
26 14 unieqi ⊢ ∪ 𝐽 = ∪ ( topGen ‘ ran (,) )
27 25 26 eqtr4i ⊢ ℝ = ∪ 𝐽
28 27 ssntr ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) ∧ ( ( 𝐴 (,) 𝐵 ) ∈ 𝐽 ∧ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 [,] 𝐵 ) ) )
29 17 19 22 24 28 syl22anc ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 [,] 𝐵 ) ) )
30 29 8 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 [,] 𝐵 ) ) )
31 eqid ⊢ ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) )
32 1 2 3 4 5 6 7 8 9 10 11 12 31 ftc1lem6 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
33 ax-resscn ⊢ ℝ ⊆ ℂ
34 33 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
35 1 2 3 4 5 6 7 8 9 10 11 12 ftc1lem3 ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )
36 1 2 3 4 5 6 7 35 ftc1lem2 ⊢ ( 𝜑 → 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
37 10 12 31 34 36 19 eldv ⊢ ( 𝜑 → ( 𝐶 ( ℝ D 𝐺 ) ( 𝐹 ‘ 𝐶 ) ↔ ( 𝐶 ∈ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝐹 ‘ 𝐶 ) ∈ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) ) ) )
38 30 32 37 mpbir2and ⊢ ( 𝜑 → 𝐶 ( ℝ D 𝐺 ) ( 𝐹 ‘ 𝐶 ) )