Definition df-ditg

Description: Define the directed integral, which is just a regular integral but with a sign change when the limits are interchanged. The A and B here are the lower and upper limits of the integral, usually written as a subscript and superscript next to the integral sign. We define the region of integration to be an open interval instead of closed so that we can use +oo , -oo for limits and also integrate up to a singularity at an endpoint. (Contributed by Mario Carneiro, 13-Aug-2014)

	Ref	Expression
Assertion	df-ditg	$$⊢{\int }_A^{B}Cdx=if\left(A\le B,{\int }_{\left(A,B\right)}Cdx,-{\int }_{\left(B,A\right)}Cdx\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2		cC	$$classC$$
3		vx	$$setvarx$$
4	3 0 1 2	cdit	$$class{\int }_A^{B}Cdx$$
5		cle	$$class\le$$
6	0 1 5	wbr	$$wffA\le B$$
7		cioo	$$class\left(.\right)$$
8	0 1 7	co	$$class\left(A,B\right)$$
9	3 8 2	citg	$$class{\int }_{\left(A,B\right)}Cdx$$
10	1 0 7	co	$$class\left(B,A\right)$$
11	3 10 2	citg	$$class{\int }_{\left(B,A\right)}Cdx$$
12	11	cneg	$$class\left(-{\int }_{\left(B,A\right)}Cdx\right)$$
13	6 9 12	cif	$$classif\left(A\le B,{\int }_{\left(A,B\right)}Cdx,-{\int }_{\left(B,A\right)}Cdx\right)$$
14	4 13	wceq	$$wff{\int }_A^{B}Cdx=if\left(A\le B,{\int }_{\left(A,B\right)}Cdx,-{\int }_{\left(B,A\right)}Cdx\right)$$