Metamath Proof Explorer

Theorem ditgneg

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

Ref Expression
Hypotheses ditgpos.1 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
ditgneg.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ditgneg.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
Assertion ditgneg ( 𝜑 → ⨜ [ 𝐵 → 𝐴 ] 𝐶 d 𝑥 = - ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 )

Proof

Step Hyp Ref Expression
1 ditgpos.1 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
2 ditgneg.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 ditgneg.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 1 biantrurd ⊢ ( 𝜑 → ( 𝐵 ≤ 𝐴 ↔ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴 ) ) )
5 2 3 letri3d ⊢ ( 𝜑 → ( 𝐴 = 𝐵 ↔ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴 ) ) )
6 4 5 bitr4d ⊢ ( 𝜑 → ( 𝐵 ≤ 𝐴 ↔ 𝐴 = 𝐵 ) )
7 ditg0 ⊢ ⨜ [ 𝐵 → 𝐵 ] 𝐶 d 𝑥 = 0
8 neg0 ⊢ - 0 = 0
9 7 8 eqtr4i ⊢ ⨜ [ 𝐵 → 𝐵 ] 𝐶 d 𝑥 = - 0
10 ditgeq2 ⊢ ( 𝐴 = 𝐵 → ⨜ [ 𝐵 → 𝐴 ] 𝐶 d 𝑥 = ⨜ [ 𝐵 → 𝐵 ] 𝐶 d 𝑥 )
11 oveq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 (,) 𝐵 ) = ( 𝐵 (,) 𝐵 ) )
12 iooid ⊢ ( 𝐵 (,) 𝐵 ) = ∅
13 11 12 eqtrdi ⊢ ( 𝐴 = 𝐵 → ( 𝐴 (,) 𝐵 ) = ∅ )
14 itgeq1 ⊢ ( ( 𝐴 (,) 𝐵 ) = ∅ → ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 = ∫ ∅ 𝐶 d 𝑥 )
15 13 14 syl ⊢ ( 𝐴 = 𝐵 → ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 = ∫ ∅ 𝐶 d 𝑥 )
16 itg0 ⊢ ∫ ∅ 𝐶 d 𝑥 = 0
17 15 16 eqtrdi ⊢ ( 𝐴 = 𝐵 → ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 = 0 )
18 17 negeqd ⊢ ( 𝐴 = 𝐵 → - ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 = - 0 )
19 9 10 18 3eqtr4a ⊢ ( 𝐴 = 𝐵 → ⨜ [ 𝐵 → 𝐴 ] 𝐶 d 𝑥 = - ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 )
20 6 19 syl6bi ⊢ ( 𝜑 → ( 𝐵 ≤ 𝐴 → ⨜ [ 𝐵 → 𝐴 ] 𝐶 d 𝑥 = - ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 ) )
21 df-ditg ⊢ ⨜ [ 𝐵 → 𝐴 ] 𝐶 d 𝑥 = if ( 𝐵 ≤ 𝐴 , ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 , - ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 )
22 iffalse ⊢ ( ¬ 𝐵 ≤ 𝐴 → if ( 𝐵 ≤ 𝐴 , ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 , - ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 ) = - ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 )
23 21 22 syl5eq ⊢ ( ¬ 𝐵 ≤ 𝐴 → ⨜ [ 𝐵 → 𝐴 ] 𝐶 d 𝑥 = - ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 )
24 20 23 pm2.61d1 ⊢ ( 𝜑 → ⨜ [ 𝐵 → 𝐴 ] 𝐶 d 𝑥 = - ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 )