Metamath Proof Explorer


Theorem itgresr

Description: The domain of an integral only matters in its intersection with RR . (Contributed by Mario Carneiro, 29-Jun-2014)

Ref Expression
Assertion itgresr A B dx = A B dx

Proof

Step Hyp Ref Expression
1 simpr k 0 3 x x
2 1 biantrud k 0 3 x x A x A x
3 elin x A x A x
4 2 3 bitr4di k 0 3 x x A x A
5 4 anbi1d k 0 3 x x A 0 B i k x A 0 B i k
6 5 ifbid k 0 3 x if x A 0 B i k B i k 0 = if x A 0 B i k B i k 0
7 6 mpteq2dva k 0 3 x if x A 0 B i k B i k 0 = x if x A 0 B i k B i k 0
8 7 fveq2d k 0 3 2 x if x A 0 B i k B i k 0 = 2 x if x A 0 B i k B i k 0
9 8 oveq2d k 0 3 i k 2 x if x A 0 B i k B i k 0 = i k 2 x if x A 0 B i k B i k 0
10 9 sumeq2i k = 0 3 i k 2 x if x A 0 B i k B i k 0 = k = 0 3 i k 2 x if x A 0 B i k B i k 0
11 eqid B i k = B i k
12 11 dfitg A B dx = k = 0 3 i k 2 x if x A 0 B i k B i k 0
13 11 dfitg A B dx = k = 0 3 i k 2 x if x A 0 B i k B i k 0
14 10 12 13 3eqtr4i A B dx = A B dx