ftc2

Description: The Fundamental Theorem of Calculus, part two. If F is a function continuous on [ A , B ] and continuously differentiable on ( A , B ) , then the integral of the derivative of F is equal to F ( B ) - F ( A ) . This is part of Metamath 100 proof #15. (Contributed by Mario Carneiro, 2-Sep-2014)

	Ref	Expression
Hypotheses	ftc2.a	$⊢ φ \to A \in ℝ$
	ftc2.b	$⊢ φ \to B \in ℝ$
	ftc2.le	$⊢ φ \to A \leq B$
	ftc2.c	$⊢ φ \to F_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ$
	ftc2.i	$⊢ φ \to ℝ D F \in 𝐿^{1}$
	ftc2.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℂ$
Assertion	ftc2	$⊢ φ \to \int_{(A, B)} F_{ℝ}^{'} (t) d t = F (B) - F (A)$

Proof

Step	Hyp	Ref	Expression
1		ftc2.a	$⊢ φ \to A \in ℝ$
2		ftc2.b	$⊢ φ \to B \in ℝ$
3		ftc2.le	$⊢ φ \to A \leq B$
4		ftc2.c	$⊢ φ \to F_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ$
5		ftc2.i	$⊢ φ \to ℝ D F \in 𝐿^{1}$
6		ftc2.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℂ$
7	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
8	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
9		ubicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to B \in [A, B]$
10	7 8 3 9	syl3anc	$⊢ φ \to B \in [A, B]$
11		fvex	$⊢ (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (A) \in V$
12	11	fvconst2	$⊢ B \in [A, B] \to ([A, B] \times \{(x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (A)\}) (B) = (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (A)$
13	10 12	syl	$⊢ φ \to ([A, B] \times \{(x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (A)\}) (B) = (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (A)$
14		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
15	14	subcn	$⊢ - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
16	15	a1i	$⊢ φ \to - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
17		eqid	$⊢ (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t) = (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t)$
18		ssidd	$⊢ φ \to (A, B) \subseteq (A, B)$
19		ioossre	$⊢ (A, B) \subseteq ℝ$
20	19	a1i	$⊢ φ \to (A, B) \subseteq ℝ$
21		cncff	$⊢ F_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ \to F_{ℝ}^{'} : (A, B) ⟶ ℂ$
22	4 21	syl	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ ℂ$
23	17 1 2 3 18 20 5 22	ftc1a	$⊢ φ \to (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t) : [A, B] \underset{cn}{⟶} ℂ$
24		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℂ \to F : [A, B] ⟶ ℂ$
25	6 24	syl	$⊢ φ \to F : [A, B] ⟶ ℂ$
26	25	feqmptd	$⊢ φ \to F = (x \in [A, B] ⟼ F (x))$
27	26 6	eqeltrrd	$⊢ φ \to (x \in [A, B] ⟼ F (x)) : [A, B] \underset{cn}{⟶} ℂ$
28	14 16 23 27	cncfmpt2f	$⊢ φ \to (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) : [A, B] \underset{cn}{⟶} ℂ$
29		ax-resscn	$⊢ ℝ \subseteq ℂ$
30	29	a1i	$⊢ φ \to ℝ \subseteq ℂ$
31		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
32	1 2 31	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
33		fvex	$⊢ F_{ℝ}^{'} (t) \in V$
34	33	a1i	$⊢ ((φ \land x \in [A, B]) \land t \in (A, x)) \to F_{ℝ}^{'} (t) \in V$
35	2	adantr	$⊢ (φ \land x \in [A, B]) \to B \in ℝ$
36	35	rexrd	$⊢ (φ \land x \in [A, B]) \to B \in ℝ^{*}$
37		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (x \in [A, B] \leftrightarrow (x \in ℝ \land A \leq x \land x \leq B))$
38	1 2 37	syl2anc	$⊢ φ \to (x \in [A, B] \leftrightarrow (x \in ℝ \land A \leq x \land x \leq B))$
39	38	biimpa	$⊢ (φ \land x \in [A, B]) \to (x \in ℝ \land A \leq x \land x \leq B)$
40	39	simp3d	$⊢ (φ \land x \in [A, B]) \to x \leq B$
41		iooss2	$⊢ (B \in ℝ^{*} \land x \leq B) \to (A, x) \subseteq (A, B)$
42	36 40 41	syl2anc	$⊢ (φ \land x \in [A, B]) \to (A, x) \subseteq (A, B)$
43		ioombl	$⊢ (A, x) \in dom vol$
44	43	a1i	$⊢ (φ \land x \in [A, B]) \to (A, x) \in dom vol$
45	33	a1i	$⊢ ((φ \land x \in [A, B]) \land t \in (A, B)) \to F_{ℝ}^{'} (t) \in V$
46	22	feqmptd	$⊢ φ \to ℝ D F = (t \in (A, B) ⟼ F_{ℝ}^{'} (t))$
47	46 5	eqeltrrd	$⊢ φ \to (t \in (A, B) ⟼ F_{ℝ}^{'} (t)) \in 𝐿^{1}$
48	47	adantr	$⊢ (φ \land x \in [A, B]) \to (t \in (A, B) ⟼ F_{ℝ}^{'} (t)) \in 𝐿^{1}$
49	42 44 45 48	iblss	$⊢ (φ \land x \in [A, B]) \to (t \in (A, x) ⟼ F_{ℝ}^{'} (t)) \in 𝐿^{1}$
50	34 49	itgcl	$⊢ (φ \land x \in [A, B]) \to \int_{(A, x)} F_{ℝ}^{'} (t) d t \in ℂ$
51	25	ffvelrnda	$⊢ (φ \land x \in [A, B]) \to F (x) \in ℂ$
52	50 51	subcld	$⊢ (φ \land x \in [A, B]) \to \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x) \in ℂ$
53	14	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
54		iccntr	$⊢ (A \in ℝ \land B \in ℝ) \to int (topGen (ran (.))) ([A, B]) = (A, B)$
55	1 2 54	syl2anc	$⊢ φ \to int (topGen (ran (.))) ([A, B]) = (A, B)$
56	30 32 52 53 14 55	dvmptntr	$⊢ φ \to \frac{d (x \in [A, B]⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x))}{d_{ℝ} x} = \frac{d (x \in (A, B)⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x))}{d_{ℝ} x}$
57		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
58	57	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
59		ioossicc	$⊢ (A, B) \subseteq [A, B]$
60	59	sseli	$⊢ x \in (A, B) \to x \in [A, B]$
61	60 50	sylan2	$⊢ (φ \land x \in (A, B)) \to \int_{(A, x)} F_{ℝ}^{'} (t) d t \in ℂ$
62	22	ffvelrnda	$⊢ (φ \land x \in (A, B)) \to F_{ℝ}^{'} (x) \in ℂ$
63	17 1 2 3 4 5	ftc1cn	$⊢ φ \to \frac{d (x \in [A, B]⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t)}{d_{ℝ} x} = ℝ D F$
64	30 32 50 53 14 55	dvmptntr	$⊢ φ \to \frac{d (x \in [A, B]⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t)}{d_{ℝ} x} = \frac{d (x \in (A, B)⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t)}{d_{ℝ} x}$
65	22	feqmptd	$⊢ φ \to ℝ D F = (x \in (A, B) ⟼ F_{ℝ}^{'} (x))$
66	63 64 65	3eqtr3d	$⊢ φ \to \frac{d (x \in (A, B)⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t)}{d_{ℝ} x} = (x \in (A, B) ⟼ F_{ℝ}^{'} (x))$
67	60 51	sylan2	$⊢ (φ \land x \in (A, B)) \to F (x) \in ℂ$
68	30 32 51 53 14 55	dvmptntr	$⊢ φ \to \frac{d (x \in [A, B]⟼ F (x))}{d_{ℝ} x} = \frac{d (x \in (A, B)⟼ F (x))}{d_{ℝ} x}$
69	26	oveq2d	$⊢ φ \to ℝ D F = \frac{d (x \in [A, B]⟼ F (x))}{d_{ℝ} x}$
70	69 65	eqtr3d	$⊢ φ \to \frac{d (x \in [A, B]⟼ F (x))}{d_{ℝ} x} = (x \in (A, B) ⟼ F_{ℝ}^{'} (x))$
71	68 70	eqtr3d	$⊢ φ \to \frac{d (x \in (A, B)⟼ F (x))}{d_{ℝ} x} = (x \in (A, B) ⟼ F_{ℝ}^{'} (x))$
72	58 61 62 66 67 62 71	dvmptsub	$⊢ φ \to \frac{d (x \in (A, B)⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x))}{d_{ℝ} x} = (x \in (A, B) ⟼ F_{ℝ}^{'} (x) - F_{ℝ}^{'} (x))$
73	62	subidd	$⊢ (φ \land x \in (A, B)) \to F_{ℝ}^{'} (x) - F_{ℝ}^{'} (x) = 0$
74	73	mpteq2dva	$⊢ φ \to (x \in (A, B) ⟼ F_{ℝ}^{'} (x) - F_{ℝ}^{'} (x)) = (x \in (A, B) ⟼ 0)$
75	56 72 74	3eqtrd	$⊢ φ \to \frac{d (x \in [A, B]⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x))}{d_{ℝ} x} = (x \in (A, B) ⟼ 0)$
76		fconstmpt	$⊢ (A, B) \times \{0\} = (x \in (A, B) ⟼ 0)$
77	75 76	eqtr4di	$⊢ φ \to \frac{d (x \in [A, B]⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x))}{d_{ℝ} x} = (A, B) \times \{0\}$
78	1 2 28 77	dveq0	$⊢ φ \to (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) = [A, B] \times \{(x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (A)\}$
79	78	fveq1d	$⊢ φ \to (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (B) = ([A, B] \times \{(x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (A)\}) (B)$
80		oveq2	$⊢ x = B \to (A, x) = (A, B)$
81		itgeq1	$⊢ (A, x) = (A, B) \to \int_{(A, x)} F_{ℝ}^{'} (t) d t = \int_{(A, B)} F_{ℝ}^{'} (t) d t$
82	80 81	syl	$⊢ x = B \to \int_{(A, x)} F_{ℝ}^{'} (t) d t = \int_{(A, B)} F_{ℝ}^{'} (t) d t$
83		fveq2	$⊢ x = B \to F (x) = F (B)$
84	82 83	oveq12d	$⊢ x = B \to \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x) = \int_{(A, B)} F_{ℝ}^{'} (t) d t - F (B)$
85		eqid	$⊢ (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) = (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x))$
86		ovex	$⊢ \int_{(A, B)} F_{ℝ}^{'} (t) d t - F (B) \in V$
87	84 85 86	fvmpt	$⊢ B \in [A, B] \to (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (B) = \int_{(A, B)} F_{ℝ}^{'} (t) d t - F (B)$
88	10 87	syl	$⊢ φ \to (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (B) = \int_{(A, B)} F_{ℝ}^{'} (t) d t - F (B)$
89	79 88	eqtr3d	$⊢ φ \to ([A, B] \times \{(x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (A)\}) (B) = \int_{(A, B)} F_{ℝ}^{'} (t) d t - F (B)$
90		lbicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \in [A, B]$
91	7 8 3 90	syl3anc	$⊢ φ \to A \in [A, B]$
92		oveq2	$⊢ x = A \to (A, x) = (A, A)$
93		iooid	$⊢ (A, A) = \emptyset$
94	92 93	eqtrdi	$⊢ x = A \to (A, x) = \emptyset$
95		itgeq1	$⊢ (A, x) = \emptyset \to \int_{(A, x)} F_{ℝ}^{'} (t) d t = \int_{\emptyset} F_{ℝ}^{'} (t) d t$
96	94 95	syl	$⊢ x = A \to \int_{(A, x)} F_{ℝ}^{'} (t) d t = \int_{\emptyset} F_{ℝ}^{'} (t) d t$
97		itg0	$⊢ \int_{\emptyset} F_{ℝ}^{'} (t) d t = 0$
98	96 97	eqtrdi	$⊢ x = A \to \int_{(A, x)} F_{ℝ}^{'} (t) d t = 0$
99		fveq2	$⊢ x = A \to F (x) = F (A)$
100	98 99	oveq12d	$⊢ x = A \to \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x) = 0 - F (A)$
101		df-neg	$⊢ - F (A) = 0 - F (A)$
102	100 101	eqtr4di	$⊢ x = A \to \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x) = - F (A)$
103		negex	$⊢ - F (A) \in V$
104	102 85 103	fvmpt	$⊢ A \in [A, B] \to (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (A) = - F (A)$
105	91 104	syl	$⊢ φ \to (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (A) = - F (A)$
106	13 89 105	3eqtr3d	$⊢ φ \to \int_{(A, B)} F_{ℝ}^{'} (t) d t - F (B) = - F (A)$
107	106	oveq2d	$⊢ φ \to F (B) + \int_{(A, B)} F_{ℝ}^{'} (t) d t - F (B) = F (B) + (- F (A))$
108	25 10	ffvelrnd	$⊢ φ \to F (B) \in ℂ$
109	33	a1i	$⊢ (φ \land t \in (A, B)) \to F_{ℝ}^{'} (t) \in V$
110	109 47	itgcl	$⊢ φ \to \int_{(A, B)} F_{ℝ}^{'} (t) d t \in ℂ$
111	108 110	pncan3d	$⊢ φ \to F (B) + \int_{(A, B)} F_{ℝ}^{'} (t) d t - F (B) = \int_{(A, B)} F_{ℝ}^{'} (t) d t$
112	25 91	ffvelrnd	$⊢ φ \to F (A) \in ℂ$
113	108 112	negsubd	$⊢ φ \to F (B) + (- F (A)) = F (B) - F (A)$
114	107 111 113	3eqtr3d	$⊢ φ \to \int_{(A, B)} F_{ℝ}^{'} (t) d t = F (B) - F (A)$

Metamath Proof Explorer

Theorem ftc2

Proof