ftc2ditglem

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

Proof

Step	Hyp	Ref	Expression
1		ftc2ditg.x	$⊢ φ \to X \in ℝ$
2		ftc2ditg.y	$⊢ φ \to Y \in ℝ$
3		ftc2ditg.a	$⊢ φ \to A \in [X, Y]$
4		ftc2ditg.b	$⊢ φ \to B \in [X, Y]$
5		ftc2ditg.c	$⊢ φ \to F_{ℝ}^{'} : (X, Y) \underset{cn}{⟶} ℂ$
6		ftc2ditg.i	$⊢ φ \to ℝ D F \in 𝐿^{1}$
7		ftc2ditg.f	$⊢ φ \to F : [X, Y] \underset{cn}{⟶} ℂ$
8		simpr	$⊢ (φ \land A \leq B) \to A \leq B$
9	8	ditgpos	$⊢ (φ \land A \leq B) \to \int_{A}^{B} F_{ℝ}^{'} (t) d t = \int_{(A, B)} F_{ℝ}^{'} (t) d t$
10		iccssre	$⊢ (X \in ℝ \land Y \in ℝ) \to [X, Y] \subseteq ℝ$
11	1 2 10	syl2anc	$⊢ φ \to [X, Y] \subseteq ℝ$
12	11 3	sseldd	$⊢ φ \to A \in ℝ$
13	12	adantr	$⊢ (φ \land A \leq B) \to A \in ℝ$
14	11 4	sseldd	$⊢ φ \to B \in ℝ$
15	14	adantr	$⊢ (φ \land A \leq B) \to B \in ℝ$
16		ax-resscn	$⊢ ℝ \subseteq ℂ$
17	16	a1i	$⊢ (φ \land A \leq B) \to ℝ \subseteq ℂ$
18		cncff	$⊢ F : [X, Y] \underset{cn}{⟶} ℂ \to F : [X, Y] ⟶ ℂ$
19	7 18	syl	$⊢ φ \to F : [X, Y] ⟶ ℂ$
20	19	adantr	$⊢ (φ \land A \leq B) \to F : [X, Y] ⟶ ℂ$
21	11	adantr	$⊢ (φ \land A \leq B) \to [X, Y] \subseteq ℝ$
22		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
23	12 14 22	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
24	23	adantr	$⊢ (φ \land A \leq B) \to [A, B] \subseteq ℝ$
25		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
26		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
27	25 26	dvres	$⊢ ((ℝ \subseteq ℂ \land F : [X, Y] ⟶ ℂ) \land ([X, Y] \subseteq ℝ \land [A, B] \subseteq ℝ)) \to ℝ D ({F ↾}_{[A, B]}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ([A, B])}$
28	17 20 21 24 27	syl22anc	$⊢ (φ \land A \leq B) \to ℝ D ({F ↾}_{[A, B]}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ([A, B])}$
29		iccntr	$⊢ (A \in ℝ \land B \in ℝ) \to int (topGen (ran (.))) ([A, B]) = (A, B)$
30	12 14 29	syl2anc	$⊢ φ \to int (topGen (ran (.))) ([A, B]) = (A, B)$
31	30	adantr	$⊢ (φ \land A \leq B) \to int (topGen (ran (.))) ([A, B]) = (A, B)$
32	31	reseq2d	$⊢ (φ \land A \leq B) \to {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ([A, B])} = {F_{ℝ}^{'} ↾}_{(A, B)}$
33	28 32	eqtrd	$⊢ (φ \land A \leq B) \to ℝ D ({F ↾}_{[A, B]}) = {F_{ℝ}^{'} ↾}_{(A, B)}$
34	1	rexrd	$⊢ φ \to X \in ℝ^{*}$
35		elicc2	$⊢ (X \in ℝ \land Y \in ℝ) \to (A \in [X, Y] \leftrightarrow (A \in ℝ \land X \leq A \land A \leq Y))$
36	1 2 35	syl2anc	$⊢ φ \to (A \in [X, Y] \leftrightarrow (A \in ℝ \land X \leq A \land A \leq Y))$
37	3 36	mpbid	$⊢ φ \to (A \in ℝ \land X \leq A \land A \leq Y)$
38	37	simp2d	$⊢ φ \to X \leq A$
39		iooss1	$⊢ (X \in ℝ^{*} \land X \leq A) \to (A, B) \subseteq (X, B)$
40	34 38 39	syl2anc	$⊢ φ \to (A, B) \subseteq (X, B)$
41	2	rexrd	$⊢ φ \to Y \in ℝ^{*}$
42		elicc2	$⊢ (X \in ℝ \land Y \in ℝ) \to (B \in [X, Y] \leftrightarrow (B \in ℝ \land X \leq B \land B \leq Y))$
43	1 2 42	syl2anc	$⊢ φ \to (B \in [X, Y] \leftrightarrow (B \in ℝ \land X \leq B \land B \leq Y))$
44	4 43	mpbid	$⊢ φ \to (B \in ℝ \land X \leq B \land B \leq Y)$
45	44	simp3d	$⊢ φ \to B \leq Y$
46		iooss2	$⊢ (Y \in ℝ^{*} \land B \leq Y) \to (X, B) \subseteq (X, Y)$
47	41 45 46	syl2anc	$⊢ φ \to (X, B) \subseteq (X, Y)$
48	40 47	sstrd	$⊢ φ \to (A, B) \subseteq (X, Y)$
49	48	adantr	$⊢ (φ \land A \leq B) \to (A, B) \subseteq (X, Y)$
50	5	adantr	$⊢ (φ \land A \leq B) \to F_{ℝ}^{'} : (X, Y) \underset{cn}{⟶} ℂ$
51		rescncf	$⊢ (A, B) \subseteq (X, Y) \to (F_{ℝ}^{'} : (X, Y) \underset{cn}{⟶} ℂ \to ({F_{ℝ}^{'} ↾}_{(A, B)}) : (A, B) \underset{cn}{⟶} ℂ)$
52	49 50 51	sylc	$⊢ (φ \land A \leq B) \to ({F_{ℝ}^{'} ↾}_{(A, B)}) : (A, B) \underset{cn}{⟶} ℂ$
53	33 52	eqeltrd	$⊢ (φ \land A \leq B) \to {({F ↾}_{[A, B]})}_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ$
54		cncff	$⊢ F_{ℝ}^{'} : (X, Y) \underset{cn}{⟶} ℂ \to F_{ℝ}^{'} : (X, Y) ⟶ ℂ$
55	5 54	syl	$⊢ φ \to F_{ℝ}^{'} : (X, Y) ⟶ ℂ$
56	55	feqmptd	$⊢ φ \to ℝ D F = (t \in (X, Y) ⟼ F_{ℝ}^{'} (t))$
57	56	adantr	$⊢ (φ \land A \leq B) \to ℝ D F = (t \in (X, Y) ⟼ F_{ℝ}^{'} (t))$
58	57	reseq1d	$⊢ (φ \land A \leq B) \to {F_{ℝ}^{'} ↾}_{(A, B)} = {(t \in (X, Y) ⟼ F_{ℝ}^{'} (t)) ↾}_{(A, B)}$
59	49	resmptd	$⊢ (φ \land A \leq B) \to {(t \in (X, Y) ⟼ F_{ℝ}^{'} (t)) ↾}_{(A, B)} = (t \in (A, B) ⟼ F_{ℝ}^{'} (t))$
60	58 59	eqtrd	$⊢ (φ \land A \leq B) \to {F_{ℝ}^{'} ↾}_{(A, B)} = (t \in (A, B) ⟼ F_{ℝ}^{'} (t))$
61	33 60	eqtrd	$⊢ (φ \land A \leq B) \to ℝ D ({F ↾}_{[A, B]}) = (t \in (A, B) ⟼ F_{ℝ}^{'} (t))$
62		ioombl	$⊢ (A, B) \in dom vol$
63	62	a1i	$⊢ (φ \land A \leq B) \to (A, B) \in dom vol$
64		fvexd	$⊢ ((φ \land A \leq B) \land t \in (X, Y)) \to F_{ℝ}^{'} (t) \in V$
65	6	adantr	$⊢ (φ \land A \leq B) \to ℝ D F \in 𝐿^{1}$
66	57 65	eqeltrrd	$⊢ (φ \land A \leq B) \to (t \in (X, Y) ⟼ F_{ℝ}^{'} (t)) \in 𝐿^{1}$
67	49 63 64 66	iblss	$⊢ (φ \land A \leq B) \to (t \in (A, B) ⟼ F_{ℝ}^{'} (t)) \in 𝐿^{1}$
68	61 67	eqeltrd	$⊢ (φ \land A \leq B) \to ℝ D ({F ↾}_{[A, B]}) \in 𝐿^{1}$
69		iccss2	$⊢ (A \in [X, Y] \land B \in [X, Y]) \to [A, B] \subseteq [X, Y]$
70	3 4 69	syl2anc	$⊢ φ \to [A, B] \subseteq [X, Y]$
71		rescncf	$⊢ [A, B] \subseteq [X, Y] \to (F : [X, Y] \underset{cn}{⟶} ℂ \to ({F ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℂ)$
72	70 7 71	sylc	$⊢ φ \to ({F ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℂ$
73	72	adantr	$⊢ (φ \land A \leq B) \to ({F ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℂ$
74	13 15 8 53 68 73	ftc2	$⊢ (φ \land A \leq B) \to \int_{(A, B)} {({F ↾}_{[A, B]})}_{ℝ}^{'} (t) d t = ({F ↾}_{[A, B]}) (B) - ({F ↾}_{[A, B]}) (A)$
75	33	fveq1d	$⊢ (φ \land A \leq B) \to {({F ↾}_{[A, B]})}_{ℝ}^{'} (t) = ({F_{ℝ}^{'} ↾}_{(A, B)}) (t)$
76		fvres	$⊢ t \in (A, B) \to ({F_{ℝ}^{'} ↾}_{(A, B)}) (t) = F_{ℝ}^{'} (t)$
77	75 76	sylan9eq	$⊢ ((φ \land A \leq B) \land t \in (A, B)) \to {({F ↾}_{[A, B]})}_{ℝ}^{'} (t) = F_{ℝ}^{'} (t)$
78	77	itgeq2dv	$⊢ (φ \land A \leq B) \to \int_{(A, B)} {({F ↾}_{[A, B]})}_{ℝ}^{'} (t) d t = \int_{(A, B)} F_{ℝ}^{'} (t) d t$
79	13	rexrd	$⊢ (φ \land A \leq B) \to A \in ℝ^{*}$
80	15	rexrd	$⊢ (φ \land A \leq B) \to B \in ℝ^{*}$
81		ubicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to B \in [A, B]$
82		lbicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \in [A, B]$
83		fvres	$⊢ B \in [A, B] \to ({F ↾}_{[A, B]}) (B) = F (B)$
84		fvres	$⊢ A \in [A, B] \to ({F ↾}_{[A, B]}) (A) = F (A)$
85	83 84	oveqan12d	$⊢ (B \in [A, B] \land A \in [A, B]) \to ({F ↾}_{[A, B]}) (B) - ({F ↾}_{[A, B]}) (A) = F (B) - F (A)$
86	81 82 85	syl2anc	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to ({F ↾}_{[A, B]}) (B) - ({F ↾}_{[A, B]}) (A) = F (B) - F (A)$
87	79 80 8 86	syl3anc	$⊢ (φ \land A \leq B) \to ({F ↾}_{[A, B]}) (B) - ({F ↾}_{[A, B]}) (A) = F (B) - F (A)$
88	74 78 87	3eqtr3d	$⊢ (φ \land A \leq B) \to \int_{(A, B)} F_{ℝ}^{'} (t) d t = F (B) - F (A)$
89	9 88	eqtrd	$⊢ (φ \land A \leq B) \to \int_{A}^{B} F_{ℝ}^{'} (t) d t = F (B) - F (A)$

Metamath Proof Explorer

Theorem ftc2ditglem

Proof