This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ∫ A B C dx = if A ≤ B ∫ A B C dx − ∫ B A C dx

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 cB class B
2 cC class C
3 vx setvar x
4 3 0 1 2 cdit class ∫ A B C dx
5 cle class ≤
6 0 1 5 wbr wff A ≤ B
7 cioo class .
8 0 1 7 co class A B
9 3 8 2 citg class ∫ A B C dx
10 1 0 7 co class B A
11 3 10 2 citg class ∫ B A C dx
12 11 cneg class − ∫ B A C dx
13 6 9 12 cif class if A ≤ B ∫ A B C dx − ∫ B A C dx
14 4 13 wceq wff ∫ A B C dx = if A ≤ B ∫ A B C dx − ∫ B A C dx