Theorem ditgneg

Description: Value of the directed integral in the backward direction. (Contributed by Mario Carneiro, 13-Aug-2014)

	Ref	Expression
Hypotheses	ditgpos.1	$$⊢\phi \to A\le B$$
	ditgneg.2	$$⊢\phi \to A\in ℝ$$
	ditgneg.3	$$⊢\phi \to B\in ℝ$$
Assertion	ditgneg	$$⊢\phi \to {\int }_B^{A}Cdx=-{\int }_{\left(A,B\right)}Cdx$$

Proof

Step	Hyp	Ref	Expression
1		ditgpos.1	$$⊢\phi \to A\le B$$
2		ditgneg.2	$$⊢\phi \to A\in ℝ$$
3		ditgneg.3	$$⊢\phi \to B\in ℝ$$
4	1	biantrurd	$$⊢\phi \to \left(B\le A\leftrightarrow \left(A\le B\wedge B\le A\right)\right)$$
5	2 3	letri3d	$$⊢\phi \to \left(A=B\leftrightarrow \left(A\le B\wedge B\le A\right)\right)$$
6	4 5	bitr4d	$$⊢\phi \to \left(B\le A\leftrightarrow A=B\right)$$
7		ditg0	$$⊢{\int }_B^{B}Cdx=0$$
8		neg0	$$⊢-0=0$$
9	7 8	eqtr4i	$$⊢{\int }_B^{B}Cdx=-0$$
10		ditgeq2	$$⊢A=B\to {\int }_B^{A}Cdx={\int }_B^{B}Cdx$$
11		oveq1	$$⊢A=B\to \left(A,B\right)=\left(B,B\right)$$
12		iooid	$$⊢\left(B,B\right)=\varnothing$$
13	11 12	eqtrdi	$$⊢A=B\to \left(A,B\right)=\varnothing$$
14		itgeq1	$$⊢\left(A,B\right)=\varnothing \to {\int }_{\left(A,B\right)}Cdx={\int }_{\varnothing }Cdx$$
15	13 14	syl	$$⊢A=B\to {\int }_{\left(A,B\right)}Cdx={\int }_{\varnothing }Cdx$$
16		itg0	$$⊢{\int }_{\varnothing }Cdx=0$$
17	15 16	eqtrdi	$$⊢A=B\to {\int }_{\left(A,B\right)}Cdx=0$$
18	17	negeqd	$$⊢A=B\to -{\int }_{\left(A,B\right)}Cdx=-0$$
19	9 10 18	3eqtr4a	$$⊢A=B\to {\int }_B^{A}Cdx=-{\int }_{\left(A,B\right)}Cdx$$
20	6 19	syl6bi	$$⊢\phi \to \left(B\le A\to {\int }_B^{A}Cdx=-{\int }_{\left(A,B\right)}Cdx\right)$$
21		df-ditg	$$⊢{\int }_B^{A}Cdx=if\left(B\le A,{\int }_{\left(B,A\right)}Cdx,-{\int }_{\left(A,B\right)}Cdx\right)$$
22		iffalse	$$⊢\neg B\le A\to if\left(B\le A,{\int }_{\left(B,A\right)}Cdx,-{\int }_{\left(A,B\right)}Cdx\right)=-{\int }_{\left(A,B\right)}Cdx$$
23	21 22	syl5eq	$$⊢\neg B\le A\to {\int }_B^{A}Cdx=-{\int }_{\left(A,B\right)}Cdx$$
24	20 23	pm2.61d1	$$⊢\phi \to {\int }_B^{A}Cdx=-{\int }_{\left(A,B\right)}Cdx$$