Theorem ditgpos

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

	Ref	Expression
Hypothesis	ditgpos.1	$$⊢\phi \to A\le B$$
Assertion	ditgpos	$$⊢\phi \to {\int }_A^{B}Cdx={\int }_{\left(A,B\right)}Cdx$$

Proof

Step	Hyp	Ref	Expression
1		ditgpos.1	$$⊢\phi \to A\le B$$
2		df-ditg	$$⊢{\int }_A^{B}Cdx=if\left(A\le B,{\int }_{\left(A,B\right)}Cdx,-{\int }_{\left(B,A\right)}Cdx\right)$$
3	1	iftrued	$$⊢\phi \to if\left(A\le B,{\int }_{\left(A,B\right)}Cdx,-{\int }_{\left(B,A\right)}Cdx\right)={\int }_{\left(A,B\right)}Cdx$$
4	2 3	syl5eq	$$⊢\phi \to {\int }_A^{B}Cdx={\int }_{\left(A,B\right)}Cdx$$