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	$⊢ G = (x \in [A, B] ⟼ \int_{(A, x)} F (t) d t)$
	ftc1.a	$⊢ φ \to A \in ℝ$
	ftc1.b	$⊢ φ \to B \in ℝ$
	ftc1.le	$⊢ φ \to A \leq B$
	ftc1.s	$⊢ φ \to (A, B) \subseteq D$
	ftc1.d	$⊢ φ \to D \subseteq ℝ$
	ftc1.i	$⊢ φ \to F \in 𝐿^{1}$
	ftc1.c	$⊢ φ \to C \in (A, B)$
	ftc1.f	$⊢ φ \to F \in (K CnP L) (C)$
	ftc1.j	$⊢ J = L ↾_{𝑡} ℝ$
	ftc1.k	$⊢ K = L ↾_{𝑡} D$
	ftc1.l	$⊢ L = TopOpen (ℂ_{fld})$
Assertion	ftc1	$⊢ φ \to C G_{ℝ}^{'} F (C)$

Proof

Step	Hyp	Ref	Expression
1		ftc1.g	$⊢ G = (x \in [A, B] ⟼ \int_{(A, x)} F (t) d t)$
2		ftc1.a	$⊢ φ \to A \in ℝ$
3		ftc1.b	$⊢ φ \to B \in ℝ$
4		ftc1.le	$⊢ φ \to A \leq B$
5		ftc1.s	$⊢ φ \to (A, B) \subseteq D$
6		ftc1.d	$⊢ φ \to D \subseteq ℝ$
7		ftc1.i	$⊢ φ \to F \in 𝐿^{1}$
8		ftc1.c	$⊢ φ \to C \in (A, B)$
9		ftc1.f	$⊢ φ \to F \in (K CnP L) (C)$
10		ftc1.j	$⊢ J = L ↾_{𝑡} ℝ$
11		ftc1.k	$⊢ K = L ↾_{𝑡} D$
12		ftc1.l	$⊢ L = TopOpen (ℂ_{fld})$
13	12	tgioo2	$⊢ topGen (ran (.)) = L ↾_{𝑡} ℝ$
14	10 13	eqtr4i	$⊢ J = topGen (ran (.))$
15		retop	$⊢ topGen (ran (.)) \in Top$
16	14 15	eqeltri	$⊢ J \in Top$
17	16	a1i	$⊢ φ \to J \in Top$
18		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
19	2 3 18	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
20		iooretop	$⊢ (A, B) \in topGen (ran (.))$
21	20 14	eleqtrri	$⊢ (A, B) \in J$
22	21	a1i	$⊢ φ \to (A, B) \in J$
23		ioossicc	$⊢ (A, B) \subseteq [A, B]$
24	23	a1i	$⊢ φ \to (A, B) \subseteq [A, B]$
25		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
26	14	unieqi	$⊢ ⋃ J = ⋃ topGen (ran (.))$
27	25 26	eqtr4i	$⊢ ℝ = ⋃ J$
28	27	ssntr	$⊢ ((J \in Top \land [A, B] \subseteq ℝ) \land ((A, B) \in J \land (A, B) \subseteq [A, B])) \to (A, B) \subseteq int (J) ([A, B])$
29	17 19 22 24 28	syl22anc	$⊢ φ \to (A, B) \subseteq int (J) ([A, B])$
30	29 8	sseldd	$⊢ φ \to C \in int (J) ([A, B])$
31		eqid	$⊢ (z \in ([A, B] ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) = (z \in ([A, B] ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C})$
32	1 2 3 4 5 6 7 8 9 10 11 12 31	ftc1lem6	$⊢ φ \to F (C) \in ((z \in ([A, B] ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C)$
33		ax-resscn	$⊢ ℝ \subseteq ℂ$
34	33	a1i	$⊢ φ \to ℝ \subseteq ℂ$
35	1 2 3 4 5 6 7 8 9 10 11 12	ftc1lem3	$⊢ φ \to F : D ⟶ ℂ$
36	1 2 3 4 5 6 7 35	ftc1lem2	$⊢ φ \to G : [A, B] ⟶ ℂ$
37	10 12 31 34 36 19	eldv	$⊢ φ \to (C G_{ℝ}^{'} F (C) \leftrightarrow (C \in int (J) ([A, B]) \land F (C) \in ((z \in ([A, B] ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C)))$
38	30 32 37	mpbir2and	$⊢ φ \to C G_{ℝ}^{'} F (C)$

Metamath Proof Explorer

Theorem ftc1

Proof