MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ditg Structured version   Visualization version   GIF version

Definition df-ditg 24773
Description: Define the directed integral, which is just a regular integral but with a sign change when the limits are interchanged. The 𝐴 and 𝐵 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 +∞, -∞ for limits and also integrate up to a singularity at an endpoint. (Contributed by Mario Carneiro, 13-Aug-2014.)
Assertion
Ref Expression
df-ditg ⨜[𝐴𝐵]𝐶 d𝑥 = if(𝐴𝐵, ∫(𝐴(,)𝐵)𝐶 d𝑥, -∫(𝐵(,)𝐴)𝐶 d𝑥)

Detailed syntax breakdown of Definition df-ditg
StepHypRef Expression
1 vx . . 3 setvar 𝑥
2 cA . . 3 class 𝐴
3 cB . . 3 class 𝐵
4 cC . . 3 class 𝐶
51, 2, 3, 4cdit 24772 . 2 class ⨜[𝐴𝐵]𝐶 d𝑥
6 cle 10895 . . . 4 class
72, 3, 6wbr 5069 . . 3 wff 𝐴𝐵
8 cioo 12962 . . . . 5 class (,)
92, 3, 8co 7234 . . . 4 class (𝐴(,)𝐵)
101, 9, 4citg 24544 . . 3 class ∫(𝐴(,)𝐵)𝐶 d𝑥
113, 2, 8co 7234 . . . . 5 class (𝐵(,)𝐴)
121, 11, 4citg 24544 . . . 4 class ∫(𝐵(,)𝐴)𝐶 d𝑥
1312cneg 11090 . . 3 class -∫(𝐵(,)𝐴)𝐶 d𝑥
147, 10, 13cif 4455 . 2 class if(𝐴𝐵, ∫(𝐴(,)𝐵)𝐶 d𝑥, -∫(𝐵(,)𝐴)𝐶 d𝑥)
155, 14wceq 1543 1 wff ⨜[𝐴𝐵]𝐶 d𝑥 = if(𝐴𝐵, ∫(𝐴(,)𝐵)𝐶 d𝑥, -∫(𝐵(,)𝐴)𝐶 d𝑥)
Colors of variables: wff setvar class
This definition is referenced by:  ditgeq1  24774  ditgeq2  24775  ditgeq3  24776  ditgex  24778  ditg0  24779  cbvditg  24780  ditgpos  24782  ditgneg  24783  ditgeq3d  43213
  Copyright terms: Public domain W3C validator