Theorem ftc2ditg

Description: Directed integral analogue of ftc2 . (Contributed by Mario Carneiro, 3-Sep-2014)

	Ref	Expression
Hypotheses	ftc2ditg.x	$$⊢\phi \to X\in ℝ$$
	ftc2ditg.y	$$⊢\phi \to Y\in ℝ$$
	ftc2ditg.a	$$⊢\phi \to A\in \left[X,Y\right]$$
	ftc2ditg.b	$$⊢\phi \to B\in \left[X,Y\right]$$
	ftc2ditg.c	$$⊢\phi \to F_{ℝ}^{\prime }:\left(X,Y\right)\underset{cn}{⟶}ℂ$$
	ftc2ditg.i	$$⊢\phi \to ℝ\mathrm{D}F\in {𝐿}^1$$
	ftc2ditg.f	$$⊢\phi \to F:\left[X,Y\right]\underset{cn}{⟶}ℂ$$
Assertion	ftc2ditg	$$⊢\phi \to {\int }_A^B{F}_{ℝ}^{\prime }\left(t\right)dt=F\left(B\right)-F\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ftc2ditg.x	$$⊢\phi \to X\in ℝ$$
2		ftc2ditg.y	$$⊢\phi \to Y\in ℝ$$
3		ftc2ditg.a	$$⊢\phi \to A\in \left[X,Y\right]$$
4		ftc2ditg.b	$$⊢\phi \to B\in \left[X,Y\right]$$
5		ftc2ditg.c	$$⊢\phi \to F_{ℝ}^{\prime }:\left(X,Y\right)\underset{cn}{⟶}ℂ$$
6		ftc2ditg.i	$$⊢\phi \to ℝ\mathrm{D}F\in {𝐿}^1$$
7		ftc2ditg.f	$$⊢\phi \to F:\left[X,Y\right]\underset{cn}{⟶}ℂ$$
8		iccssre	$$⊢\left(X\in ℝ\wedge Y\in ℝ\right)\to \left[X,Y\right]\subseteq ℝ$$
9	1 2 8	syl2anc	$$⊢\phi \to \left[X,Y\right]\subseteq ℝ$$
10	9 3	sseldd	$$⊢\phi \to A\in ℝ$$
11	9 4	sseldd	$$⊢\phi \to B\in ℝ$$
12	1 2 3 4 5 6 7	ftc2ditglem	$$⊢\left(\phi \wedge A\le B\right)\to {\int }_A^B{F}_{ℝ}^{\prime }\left(t\right)dt=F\left(B\right)-F\left(A\right)$$
13		fvexd	$$⊢\left(\phi \wedge t\in \left(X,Y\right)\right)\to F_{ℝ}^{\prime }\left(t\right)\in \mathrm{V}$$
14		cncff	$$⊢F_{ℝ}^{\prime }:\left(X,Y\right)\underset{cn}{⟶}ℂ\to F_{ℝ}^{\prime }:\left(X,Y\right)⟶ℂ$$
15	5 14	syl	$$⊢\phi \to F_{ℝ}^{\prime }:\left(X,Y\right)⟶ℂ$$
16	15	feqmptd	$$⊢\phi \to ℝ\mathrm{D}F=\left(t\in \left(X,Y\right)⟼F_{ℝ}^{\prime }\left(t\right)\right)$$
17	16 6	eqeltrrd	$$⊢\phi \to \left(t\in \left(X,Y\right)⟼F_{ℝ}^{\prime }\left(t\right)\right)\in {𝐿}^1$$
18	1 2 4 3 13 17	ditgswap	$$⊢\phi \to {\int }_A^B{F}_{ℝ}^{\prime }\left(t\right)dt=-{\int }_B^A{F}_{ℝ}^{\prime }\left(t\right)dt$$
19	18	adantr	$$⊢\left(\phi \wedge B\le A\right)\to {\int }_A^B{F}_{ℝ}^{\prime }\left(t\right)dt=-{\int }_B^A{F}_{ℝ}^{\prime }\left(t\right)dt$$
20	1 2 4 3 5 6 7	ftc2ditglem	$$⊢\left(\phi \wedge B\le A\right)\to {\int }_B^A{F}_{ℝ}^{\prime }\left(t\right)dt=F\left(A\right)-F\left(B\right)$$
21	20	negeqd	$$⊢\left(\phi \wedge B\le A\right)\to -{\int }_B^A{F}_{ℝ}^{\prime }\left(t\right)dt=-\left(F\left(A\right)-F\left(B\right)\right)$$
22		cncff	$$⊢F:\left[X,Y\right]\underset{cn}{⟶}ℂ\to F:\left[X,Y\right]⟶ℂ$$
23	7 22	syl	$$⊢\phi \to F:\left[X,Y\right]⟶ℂ$$
24	23 3	ffvelrnd	$$⊢\phi \to F\left(A\right)\in ℂ$$
25	23 4	ffvelrnd	$$⊢\phi \to F\left(B\right)\in ℂ$$
26	24 25	negsubdi2d	$$⊢\phi \to -\left(F\left(A\right)-F\left(B\right)\right)=F\left(B\right)-F\left(A\right)$$
27	26	adantr	$$⊢\left(\phi \wedge B\le A\right)\to -\left(F\left(A\right)-F\left(B\right)\right)=F\left(B\right)-F\left(A\right)$$
28	19 21 27	3eqtrd	$$⊢\left(\phi \wedge B\le A\right)\to {\int }_A^B{F}_{ℝ}^{\prime }\left(t\right)dt=F\left(B\right)-F\left(A\right)$$
29	10 11 12 28	lecasei	$$⊢\phi \to {\int }_A^B{F}_{ℝ}^{\prime }\left(t\right)dt=F\left(B\right)-F\left(A\right)$$