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

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 ⊢ φ → A ≤ B
ditgneg.2 ⊢ φ → A ∈ ℝ
ditgneg.3 ⊢ φ → B ∈ ℝ
Assertion ditgneg ⊢ φ → ∫ B A C dx = − ∫ A B C dx

Proof

Step Hyp Ref Expression
1 ditgpos.1 ⊢ φ → A ≤ B
2 ditgneg.2 ⊢ φ → A ∈ ℝ
3 ditgneg.3 ⊢ φ → B ∈ ℝ
4 1 biantrurd ⊢ φ → B ≤ A ↔ A ≤ B ∧ B ≤ A
5 2 3 letri3d ⊢ φ → A = B ↔ A ≤ B ∧ B ≤ A
6 4 5 bitr4d ⊢ φ → B ≤ A ↔ A = B
7 ditg0 ⊢ ∫ B B C dx = 0
8 neg0 ⊢ − 0 = 0
9 7 8 eqtr4i ⊢ ∫ B B C dx = − 0
10 ditgeq2 ⊢ A = B → ∫ B A C dx = ∫ B B C dx
11 oveq1 ⊢ A = B → A B = B B
12 iooid ⊢ B B = ∅
13 11 12 eqtrdi ⊢ A = B → A B = ∅
14 itgeq1 ⊢ A B = ∅ → ∫ A B C dx = ∫ ∅ C dx
15 13 14 syl ⊢ A = B → ∫ A B C dx = ∫ ∅ C dx
16 itg0 ⊢ ∫ ∅ C dx = 0
17 15 16 eqtrdi ⊢ A = B → ∫ A B C dx = 0
18 17 negeqd ⊢ A = B → − ∫ A B C dx = − 0
19 9 10 18 3eqtr4a ⊢ A = B → ∫ B A C dx = − ∫ A B C dx
20 6 19 biimtrdi ⊢ φ → B ≤ A → ∫ B A C dx = − ∫ A B C dx
21 df-ditg ⊢ ∫ B A C dx = if B ≤ A ∫ B A C dx − ∫ A B C dx
22 iffalse ⊢ ¬ B ≤ A → if B ≤ A ∫ B A C dx − ∫ A B C dx = − ∫ A B C dx
23 21 22 eqtrid ⊢ ¬ B ≤ A → ∫ B A C dx = − ∫ A B C dx
24 20 23 pm2.61d1 ⊢ φ → ∫ B A C dx = − ∫ A B C dx