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	⊢ ( 𝜑 → 𝐹 ∈ 𝐿¹ )
	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	⊢ ( 𝜑 → 𝐹 ∈ 𝐿¹ )
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 𝐺 ) ( 𝐹 ‘ 𝐶 ) )

Metamath Proof Explorer

Theorem ftc1

Proof