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

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 ⊢ φ → A ≤ B
Assertion ditgpos ⊢ φ → ∫ A B C dx = ∫ A B C dx

Proof

Step Hyp Ref Expression
1 ditgpos.1 ⊢ φ → A ≤ B
2 df-ditg ⊢ ∫ A B C dx = if A ≤ B ∫ A B C dx − ∫ B A C dx
3 1 iftrued ⊢ φ → if A ≤ B ∫ A B C dx − ∫ B A C dx = ∫ A B C dx
4 2 3 eqtrid ⊢ φ → ∫ A B C dx = ∫ A B C dx