ftc1cn

Description: Strengthen the assumptions of ftc1 to when the function F is continuous on the entire interval ( A , B ) ; in this case we can calculate _D G exactly. (Contributed by Mario Carneiro, 1-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		ftc1cn.g	$⊢ G = (x \in [A, B] ⟼ \int_{(A, x)} F (t) d t)$
2		ftc1cn.a	$⊢ φ \to A \in ℝ$
3		ftc1cn.b	$⊢ φ \to B \in ℝ$
4		ftc1cn.le	$⊢ φ \to A \leq B$
5		ftc1cn.f	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℂ$
6		ftc1cn.i	$⊢ φ \to F \in 𝐿^{1}$
7		dvf	$⊢ G_{ℝ}^{'} : dom G_{ℝ}^{'} ⟶ ℂ$
8	7	a1i	$⊢ φ \to G_{ℝ}^{'} : dom G_{ℝ}^{'} ⟶ ℂ$
9	8	ffund	$⊢ φ \to Fun G_{ℝ}^{'}$
10		ax-resscn	$⊢ ℝ \subseteq ℂ$
11	10	a1i	$⊢ φ \to ℝ \subseteq ℂ$
12		ssidd	$⊢ φ \to (A, B) \subseteq (A, B)$
13		ioossre	$⊢ (A, B) \subseteq ℝ$
14	13	a1i	$⊢ φ \to (A, B) \subseteq ℝ$
15		cncff	$⊢ F : (A, B) \underset{cn}{⟶} ℂ \to F : (A, B) ⟶ ℂ$
16	5 15	syl	$⊢ φ \to F : (A, B) ⟶ ℂ$
17	1 2 3 4 12 14 6 16	ftc1lem2	$⊢ φ \to G : [A, B] ⟶ ℂ$
18		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
19	2 3 18	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
20		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
21	20	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
22	11 17 19 21 20	dvbssntr	$⊢ φ \to dom G_{ℝ}^{'} \subseteq int (topGen (ran (.))) ([A, B])$
23		iccntr	$⊢ (A \in ℝ \land B \in ℝ) \to int (topGen (ran (.))) ([A, B]) = (A, B)$
24	2 3 23	syl2anc	$⊢ φ \to int (topGen (ran (.))) ([A, B]) = (A, B)$
25	22 24	sseqtrd	$⊢ φ \to dom G_{ℝ}^{'} \subseteq (A, B)$
26	2	adantr	$⊢ (φ \land y \in (A, B)) \to A \in ℝ$
27	3	adantr	$⊢ (φ \land y \in (A, B)) \to B \in ℝ$
28	4	adantr	$⊢ (φ \land y \in (A, B)) \to A \leq B$
29		ssidd	$⊢ (φ \land y \in (A, B)) \to (A, B) \subseteq (A, B)$
30	13	a1i	$⊢ (φ \land y \in (A, B)) \to (A, B) \subseteq ℝ$
31	6	adantr	$⊢ (φ \land y \in (A, B)) \to F \in 𝐿^{1}$
32		simpr	$⊢ (φ \land y \in (A, B)) \to y \in (A, B)$
33	13 10	sstri	$⊢ (A, B) \subseteq ℂ$
34		ssid	$⊢ ℂ \subseteq ℂ$
35		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B) = TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)$
36	20	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
37	36	toponrestid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
38	20 35 37	cncfcn	$⊢ ((A, B) \subseteq ℂ \land ℂ \subseteq ℂ) \to (A, B) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) Cn TopOpen (ℂ_{fld})$
39	33 34 38	mp2an	$⊢ (A, B) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) Cn TopOpen (ℂ_{fld})$
40	5 39	eleqtrdi	$⊢ φ \to F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) Cn TopOpen (ℂ_{fld}))$
41	40	adantr	$⊢ (φ \land y \in (A, B)) \to F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) Cn TopOpen (ℂ_{fld}))$
42	33	a1i	$⊢ φ \to (A, B) \subseteq ℂ$
43		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land (A, B) \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B) \in TopOn ((A, B))$
44	36 42 43	sylancr	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B) \in TopOn ((A, B))$
45		toponuni	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B) \in TopOn ((A, B)) \to (A, B) = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B))$
46	44 45	syl	$⊢ φ \to (A, B) = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B))$
47	46	eleq2d	$⊢ φ \to (y \in (A, B) \leftrightarrow y \in ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)))$
48	47	biimpa	$⊢ (φ \land y \in (A, B)) \to y \in ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B))$
49		eqid	$⊢ ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B))$
50	49	cncnpi	$⊢ (F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) Cn TopOpen (ℂ_{fld})) \land y \in ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B))) \to F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (y)$
51	41 48 50	syl2anc	$⊢ (φ \land y \in (A, B)) \to F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (y)$
52	1 26 27 28 29 30 31 32 51 21 35 20	ftc1	$⊢ (φ \land y \in (A, B)) \to y G_{ℝ}^{'} F (y)$
53		vex	$⊢ y \in V$
54		fvex	$⊢ F (y) \in V$
55	53 54	breldm	$⊢ y G_{ℝ}^{'} F (y) \to y \in dom G_{ℝ}^{'}$
56	52 55	syl	$⊢ (φ \land y \in (A, B)) \to y \in dom G_{ℝ}^{'}$
57	25 56	eqelssd	$⊢ φ \to dom G_{ℝ}^{'} = (A, B)$
58		df-fn	$⊢ G_{ℝ}^{'} Fn (A, B) \leftrightarrow (Fun G_{ℝ}^{'} \land dom G_{ℝ}^{'} = (A, B))$
59	9 57 58	sylanbrc	$⊢ φ \to G_{ℝ}^{'} Fn (A, B)$
60	16	ffnd	$⊢ φ \to F Fn (A, B)$
61	9	adantr	$⊢ (φ \land y \in (A, B)) \to Fun G_{ℝ}^{'}$
62		funbrfv	$⊢ Fun G_{ℝ}^{'} \to (y G_{ℝ}^{'} F (y) \to G_{ℝ}^{'} (y) = F (y))$
63	61 52 62	sylc	$⊢ (φ \land y \in (A, B)) \to G_{ℝ}^{'} (y) = F (y)$
64	59 60 63	eqfnfvd	$⊢ φ \to ℝ D G = F$

Metamath Proof Explorer

Theorem ftc1cn

Proof