Metamath Proof Explorer


Theorem ditgpos

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

Ref Expression
Hypothesis ditgpos.1 ( 𝜑𝐴𝐵 )
Assertion ditgpos ( 𝜑 → ⨜ [ 𝐴𝐵 ] 𝐶 d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 )

Proof

Step Hyp Ref Expression
1 ditgpos.1 ( 𝜑𝐴𝐵 )
2 df-ditg ⨜ [ 𝐴𝐵 ] 𝐶 d 𝑥 = if ( 𝐴𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 )
3 1 iftrued ( 𝜑 → if ( 𝐴𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 ) = ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 )
4 2 3 syl5eq ( 𝜑 → ⨜ [ 𝐴𝐵 ] 𝐶 d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 )