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

Metamath Proof Explorer

Theorem ditg0

Description: Value of the directed integral from a point to itself. (Contributed by Mario Carneiro, 13-Aug-2014)

Ref Expression
Assertion ditg0 ⊢ ∫ A A B dx = 0

Proof

Step Hyp Ref Expression
1 df-ditg ⊢ ∫ A A B dx = if A ≤ A ∫ A A B dx − ∫ A A B dx
2 iooid ⊢ A A = ∅
3 itgeq1 ⊢ A A = ∅ → ∫ A A B dx = ∫ ∅ B dx
4 2 3 ax-mp ⊢ ∫ A A B dx = ∫ ∅ B dx
5 itg0 ⊢ ∫ ∅ B dx = 0
6 4 5 eqtri ⊢ ∫ A A B dx = 0
7 6 negeqi ⊢ − ∫ A A B dx = − 0
8 neg0 ⊢ − 0 = 0
9 7 8 eqtri ⊢ − ∫ A A B dx = 0
10 ifeq12 ⊢ ∫ A A B dx = 0 ∧ − ∫ A A B dx = 0 → if A ≤ A ∫ A A B dx − ∫ A A B dx = if A ≤ A 0 0
11 6 9 10 mp2an ⊢ if A ≤ A ∫ A A B dx − ∫ A A B dx = if A ≤ A 0 0
12 ifid ⊢ if A ≤ A 0 0 = 0
13 11 12 eqtri ⊢ if A ≤ A ∫ A A B dx − ∫ A A B dx = 0
14 1 13 eqtri ⊢ ∫ A A B dx = 0