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 𝑥 ) |
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 𝑥 ) |