ftc2re

Description: The Fundamental Theorem of Calculus, part two, for functions continuous on D . (Contributed by Thierry Arnoux, 1-Dec-2021)

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

Proof

Step	Hyp	Ref	Expression
1		ftc2re.e	$⊢ E = (C, D)$
2		ftc2re.a	$⊢ φ \to A \in E$
3		ftc2re.b	$⊢ φ \to B \in E$
4		ftc2re.le	$⊢ φ \to A \leq B$
5		ftc2re.f	$⊢ φ \to F : E ⟶ ℂ$
6		ftc2re.1	$⊢ φ \to F_{ℝ}^{'} : E \underset{cn}{⟶} ℂ$
7		ioossre	$⊢ (C, D) \subseteq ℝ$
8	1 7	eqsstri	$⊢ E \subseteq ℝ$
9	8	a1i	$⊢ φ \to E \subseteq ℝ$
10	9 2	sseldd	$⊢ φ \to A \in ℝ$
11	9 3	sseldd	$⊢ φ \to B \in ℝ$
12		ax-resscn	$⊢ ℝ \subseteq ℂ$
13	12	a1i	$⊢ φ \to ℝ \subseteq ℂ$
14		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
15	10 11 14	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
16		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
17		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
18	16 17	dvres	$⊢ ((ℝ \subseteq ℂ \land F : E ⟶ ℂ) \land (E \subseteq ℝ \land [A, B] \subseteq ℝ)) \to ℝ D ({F ↾}_{[A, B]}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ([A, B])}$
19	13 5 9 15 18	syl22anc	$⊢ φ \to ℝ D ({F ↾}_{[A, B]}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ([A, B])}$
20		iccntr	$⊢ (A \in ℝ \land B \in ℝ) \to int (topGen (ran (.))) ([A, B]) = (A, B)$
21	10 11 20	syl2anc	$⊢ φ \to int (topGen (ran (.))) ([A, B]) = (A, B)$
22	21	reseq2d	$⊢ φ \to {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ([A, B])} = {F_{ℝ}^{'} ↾}_{(A, B)}$
23	19 22	eqtrd	$⊢ φ \to ℝ D ({F ↾}_{[A, B]}) = {F_{ℝ}^{'} ↾}_{(A, B)}$
24		ioossicc	$⊢ (A, B) \subseteq [A, B]$
25	24	a1i	$⊢ φ \to (A, B) \subseteq [A, B]$
26	1 2 3	fct2relem	$⊢ φ \to [A, B] \subseteq E$
27	25 26	sstrd	$⊢ φ \to (A, B) \subseteq E$
28		rescncf	$⊢ (A, B) \subseteq E \to (F_{ℝ}^{'} : E \underset{cn}{⟶} ℂ \to ({F_{ℝ}^{'} ↾}_{(A, B)}) : (A, B) \underset{cn}{⟶} ℂ)$
29	27 6 28	sylc	$⊢ φ \to ({F_{ℝ}^{'} ↾}_{(A, B)}) : (A, B) \underset{cn}{⟶} ℂ$
30	23 29	eqeltrd	$⊢ φ \to {({F ↾}_{[A, B]})}_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ$
31		ioombl	$⊢ (A, B) \in dom vol$
32	31	a1i	$⊢ φ \to (A, B) \in dom vol$
33		cnmbf	$⊢ ((A, B) \in dom vol \land ({F_{ℝ}^{'} ↾}_{(A, B)}) : (A, B) \underset{cn}{⟶} ℂ) \to {F_{ℝ}^{'} ↾}_{(A, B)} \in MblFn$
34	32 29 33	syl2anc	$⊢ φ \to {F_{ℝ}^{'} ↾}_{(A, B)} \in MblFn$
35		dmres	$⊢ dom ({F_{ℝ}^{'} ↾}_{(A, B)}) = (A, B) \cap dom F_{ℝ}^{'}$
36	35	fveq2i	$⊢ vol (dom ({F_{ℝ}^{'} ↾}_{(A, B)})) = vol ((A, B) \cap dom F_{ℝ}^{'})$
37		cncff	$⊢ F_{ℝ}^{'} : E \underset{cn}{⟶} ℂ \to F_{ℝ}^{'} : E ⟶ ℂ$
38	6 37	syl	$⊢ φ \to F_{ℝ}^{'} : E ⟶ ℂ$
39	38	fdmd	$⊢ φ \to dom F_{ℝ}^{'} = E$
40	39	ineq2d	$⊢ φ \to (A, B) \cap dom F_{ℝ}^{'} = (A, B) \cap E$
41		dfss2	$⊢ (A, B) \subseteq E \leftrightarrow (A, B) \cap E = (A, B)$
42	27 41	sylib	$⊢ φ \to (A, B) \cap E = (A, B)$
43	40 42	eqtrd	$⊢ φ \to (A, B) \cap dom F_{ℝ}^{'} = (A, B)$
44	43	fveq2d	$⊢ φ \to vol ((A, B) \cap dom F_{ℝ}^{'}) = vol ((A, B))$
45		volioo	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol ((A, B)) = B - A$
46	10 11 4 45	syl3anc	$⊢ φ \to vol ((A, B)) = B - A$
47	11 10	resubcld	$⊢ φ \to B - A \in ℝ$
48	46 47	eqeltrd	$⊢ φ \to vol ((A, B)) \in ℝ$
49	44 48	eqeltrd	$⊢ φ \to vol ((A, B) \cap dom F_{ℝ}^{'}) \in ℝ$
50	36 49	eqeltrid	$⊢ φ \to vol (dom ({F_{ℝ}^{'} ↾}_{(A, B)})) \in ℝ$
51		rescncf	$⊢ [A, B] \subseteq E \to (F_{ℝ}^{'} : E \underset{cn}{⟶} ℂ \to ({F_{ℝ}^{'} ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℂ)$
52	26 51	syl	$⊢ φ \to (F_{ℝ}^{'} : E \underset{cn}{⟶} ℂ \to ({F_{ℝ}^{'} ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℂ)$
53	6 52	mpd	$⊢ φ \to ({F_{ℝ}^{'} ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℂ$
54		cniccbdd	$⊢ (A \in ℝ \land B \in ℝ \land ({F_{ℝ}^{'} ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℂ) \to \exists x \in ℝ \forall y \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (y)\| \leq x$
55	10 11 53 54	syl3anc	$⊢ φ \to \exists x \in ℝ \forall y \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (y)\| \leq x$
56	35 43	eqtrid	$⊢ φ \to dom ({F_{ℝ}^{'} ↾}_{(A, B)}) = (A, B)$
57	56 25	eqsstrd	$⊢ φ \to dom ({F_{ℝ}^{'} ↾}_{(A, B)}) \subseteq [A, B]$
58		ssralv	$⊢ dom ({F_{ℝ}^{'} ↾}_{(A, B)}) \subseteq [A, B] \to (\forall y \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (y)\| \leq x \to \forall y \in dom ({F_{ℝ}^{'} ↾}_{(A, B)}) \|({F_{ℝ}^{'} ↾}_{[A, B]}) (y)\| \leq x)$
59	57 58	syl	$⊢ φ \to (\forall y \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (y)\| \leq x \to \forall y \in dom ({F_{ℝ}^{'} ↾}_{(A, B)}) \|({F_{ℝ}^{'} ↾}_{[A, B]}) (y)\| \leq x)$
60	59	adantr	$⊢ (φ \land x \in ℝ) \to (\forall y \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (y)\| \leq x \to \forall y \in dom ({F_{ℝ}^{'} ↾}_{(A, B)}) \|({F_{ℝ}^{'} ↾}_{[A, B]}) (y)\| \leq x)$
61	57	adantr	$⊢ (φ \land x \in ℝ) \to dom ({F_{ℝ}^{'} ↾}_{(A, B)}) \subseteq [A, B]$
62	61	sselda	$⊢ ((φ \land x \in ℝ) \land y \in dom ({F_{ℝ}^{'} ↾}_{(A, B)})) \to y \in [A, B]$
63		fvres	$⊢ y \in [A, B] \to ({F_{ℝ}^{'} ↾}_{[A, B]}) (y) = F_{ℝ}^{'} (y)$
64	62 63	syl	$⊢ ((φ \land x \in ℝ) \land y \in dom ({F_{ℝ}^{'} ↾}_{(A, B)})) \to ({F_{ℝ}^{'} ↾}_{[A, B]}) (y) = F_{ℝ}^{'} (y)$
65		simpr	$⊢ ((φ \land x \in ℝ) \land y \in dom ({F_{ℝ}^{'} ↾}_{(A, B)})) \to y \in dom ({F_{ℝ}^{'} ↾}_{(A, B)})$
66	56	ad2antrr	$⊢ ((φ \land x \in ℝ) \land y \in dom ({F_{ℝ}^{'} ↾}_{(A, B)})) \to dom ({F_{ℝ}^{'} ↾}_{(A, B)}) = (A, B)$
67	65 66	eleqtrd	$⊢ ((φ \land x \in ℝ) \land y \in dom ({F_{ℝ}^{'} ↾}_{(A, B)})) \to y \in (A, B)$
68		fvres	$⊢ y \in (A, B) \to ({F_{ℝ}^{'} ↾}_{(A, B)}) (y) = F_{ℝ}^{'} (y)$
69	67 68	syl	$⊢ ((φ \land x \in ℝ) \land y \in dom ({F_{ℝ}^{'} ↾}_{(A, B)})) \to ({F_{ℝ}^{'} ↾}_{(A, B)}) (y) = F_{ℝ}^{'} (y)$
70	64 69	eqtr4d	$⊢ ((φ \land x \in ℝ) \land y \in dom ({F_{ℝ}^{'} ↾}_{(A, B)})) \to ({F_{ℝ}^{'} ↾}_{[A, B]}) (y) = ({F_{ℝ}^{'} ↾}_{(A, B)}) (y)$
71	70	fveq2d	$⊢ ((φ \land x \in ℝ) \land y \in dom ({F_{ℝ}^{'} ↾}_{(A, B)})) \to \|({F_{ℝ}^{'} ↾}_{[A, B]}) (y)\| = \|({F_{ℝ}^{'} ↾}_{(A, B)}) (y)\|$
72	71	breq1d	$⊢ ((φ \land x \in ℝ) \land y \in dom ({F_{ℝ}^{'} ↾}_{(A, B)})) \to (\|({F_{ℝ}^{'} ↾}_{[A, B]}) (y)\| \leq x \leftrightarrow \|({F_{ℝ}^{'} ↾}_{(A, B)}) (y)\| \leq x)$
73	72	biimpd	$⊢ ((φ \land x \in ℝ) \land y \in dom ({F_{ℝ}^{'} ↾}_{(A, B)})) \to (\|({F_{ℝ}^{'} ↾}_{[A, B]}) (y)\| \leq x \to \|({F_{ℝ}^{'} ↾}_{(A, B)}) (y)\| \leq x)$
74	73	ralimdva	$⊢ (φ \land x \in ℝ) \to (\forall y \in dom ({F_{ℝ}^{'} ↾}_{(A, B)}) \|({F_{ℝ}^{'} ↾}_{[A, B]}) (y)\| \leq x \to \forall y \in dom ({F_{ℝ}^{'} ↾}_{(A, B)}) \|({F_{ℝ}^{'} ↾}_{(A, B)}) (y)\| \leq x)$
75	60 74	syld	$⊢ (φ \land x \in ℝ) \to (\forall y \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (y)\| \leq x \to \forall y \in dom ({F_{ℝ}^{'} ↾}_{(A, B)}) \|({F_{ℝ}^{'} ↾}_{(A, B)}) (y)\| \leq x)$
76	75	reximdva	$⊢ φ \to (\exists x \in ℝ \forall y \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (y)\| \leq x \to \exists x \in ℝ \forall y \in dom ({F_{ℝ}^{'} ↾}_{(A, B)}) \|({F_{ℝ}^{'} ↾}_{(A, B)}) (y)\| \leq x)$
77	55 76	mpd	$⊢ φ \to \exists x \in ℝ \forall y \in dom ({F_{ℝ}^{'} ↾}_{(A, B)}) \|({F_{ℝ}^{'} ↾}_{(A, B)}) (y)\| \leq x$
78		bddibl	$⊢ ({F_{ℝ}^{'} ↾}_{(A, B)} \in MblFn \land vol (dom ({F_{ℝ}^{'} ↾}_{(A, B)})) \in ℝ \land \exists x \in ℝ \forall y \in dom ({F_{ℝ}^{'} ↾}_{(A, B)}) \|({F_{ℝ}^{'} ↾}_{(A, B)}) (y)\| \leq x) \to {F_{ℝ}^{'} ↾}_{(A, B)} \in 𝐿^{1}$
79	34 50 77 78	syl3anc	$⊢ φ \to {F_{ℝ}^{'} ↾}_{(A, B)} \in 𝐿^{1}$
80	23 79	eqeltrd	$⊢ φ \to ℝ D ({F ↾}_{[A, B]}) \in 𝐿^{1}$
81		dvcn	$⊢ ((ℝ \subseteq ℂ \land F : E ⟶ ℂ \land E \subseteq ℝ) \land dom F_{ℝ}^{'} = E) \to F : E \underset{cn}{⟶} ℂ$
82	13 5 9 39 81	syl31anc	$⊢ φ \to F : E \underset{cn}{⟶} ℂ$
83		rescncf	$⊢ [A, B] \subseteq E \to (F : E \underset{cn}{⟶} ℂ \to ({F ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℂ)$
84	26 83	syl	$⊢ φ \to (F : E \underset{cn}{⟶} ℂ \to ({F ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℂ)$
85	82 84	mpd	$⊢ φ \to ({F ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℂ$
86	10 11 4 30 80 85	ftc2	$⊢ φ \to \int_{(A, B)} {({F ↾}_{[A, B]})}_{ℝ}^{'} (t) d t = ({F ↾}_{[A, B]}) (B) - ({F ↾}_{[A, B]}) (A)$
87	23	fveq1d	$⊢ φ \to {({F ↾}_{[A, B]})}_{ℝ}^{'} (t) = ({F_{ℝ}^{'} ↾}_{(A, B)}) (t)$
88		fvres	$⊢ t \in (A, B) \to ({F_{ℝ}^{'} ↾}_{(A, B)}) (t) = F_{ℝ}^{'} (t)$
89	87 88	sylan9eq	$⊢ (φ \land t \in (A, B)) \to {({F ↾}_{[A, B]})}_{ℝ}^{'} (t) = F_{ℝ}^{'} (t)$
90	89	ralrimiva	$⊢ φ \to \forall t \in (A, B) {({F ↾}_{[A, B]})}_{ℝ}^{'} (t) = F_{ℝ}^{'} (t)$
91		itgeq2	$⊢ \forall t \in (A, B) {({F ↾}_{[A, B]})}_{ℝ}^{'} (t) = F_{ℝ}^{'} (t) \to \int_{(A, B)} {({F ↾}_{[A, B]})}_{ℝ}^{'} (t) d t = \int_{(A, B)} F_{ℝ}^{'} (t) d t$
92	90 91	syl	$⊢ φ \to \int_{(A, B)} {({F ↾}_{[A, B]})}_{ℝ}^{'} (t) d t = \int_{(A, B)} F_{ℝ}^{'} (t) d t$
93	10	rexrd	$⊢ φ \to A \in ℝ^{*}$
94	11	rexrd	$⊢ φ \to B \in ℝ^{*}$
95		ubicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to B \in [A, B]$
96	93 94 4 95	syl3anc	$⊢ φ \to B \in [A, B]$
97	96	fvresd	$⊢ φ \to ({F ↾}_{[A, B]}) (B) = F (B)$
98		lbicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \in [A, B]$
99	93 94 4 98	syl3anc	$⊢ φ \to A \in [A, B]$
100	99	fvresd	$⊢ φ \to ({F ↾}_{[A, B]}) (A) = F (A)$
101	97 100	oveq12d	$⊢ φ \to ({F ↾}_{[A, B]}) (B) - ({F ↾}_{[A, B]}) (A) = F (B) - F (A)$
102	86 92 101	3eqtr3d	$⊢ φ \to \int_{(A, B)} F_{ℝ}^{'} (t) d t = F (B) - F (A)$

Metamath Proof Explorer

Theorem ftc2re

Proof