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 ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 = if ( 𝐴 ≤ 𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ⊢ 𝐴
1 cB ⊢ 𝐵
2 cC ⊢ 𝐶
3 vx ⊢ 𝑥
4 3 0 1 2 cdit ⊢ ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥
5 cle ⊢ ≤
6 0 1 5 wbr ⊢ 𝐴 ≤ 𝐵
7 cioo ⊢ (,)
8 0 1 7 co ⊢ ( 𝐴 (,) 𝐵 )
9 3 8 2 citg ⊢ ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥
10 1 0 7 co ⊢ ( 𝐵 (,) 𝐴 )
11 3 10 2 citg ⊢ ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥
12 11 cneg ⊢ - ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥
13 6 9 12 cif ⊢ if ( 𝐴 ≤ 𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 )
14 4 13 wceq ⊢ ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 = if ( 𝐴 ≤ 𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 )