# 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 ${⊢}{\int }_{{A}}{B}d{x}={\int }_{\left({A}\cap ℝ\right)}{B}d{x}$

### Proof

Step Hyp Ref Expression
1 simpr ${⊢}\left({k}\in \left(0\dots 3\right)\wedge {x}\in ℝ\right)\to {x}\in ℝ$
2 1 biantrud ${⊢}\left({k}\in \left(0\dots 3\right)\wedge {x}\in ℝ\right)\to \left({x}\in {A}↔\left({x}\in {A}\wedge {x}\in ℝ\right)\right)$
3 elin ${⊢}{x}\in \left({A}\cap ℝ\right)↔\left({x}\in {A}\wedge {x}\in ℝ\right)$
4 2 3 syl6bbr ${⊢}\left({k}\in \left(0\dots 3\right)\wedge {x}\in ℝ\right)\to \left({x}\in {A}↔{x}\in \left({A}\cap ℝ\right)\right)$
5 4 anbi1d ${⊢}\left({k}\in \left(0\dots 3\right)\wedge {x}\in ℝ\right)\to \left(\left({x}\in {A}\wedge 0\le \Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)\right)↔\left({x}\in \left({A}\cap ℝ\right)\wedge 0\le \Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)\right)\right)$
6 5 ifbid ${⊢}\left({k}\in \left(0\dots 3\right)\wedge {x}\in ℝ\right)\to if\left(\left({x}\in {A}\wedge 0\le \Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right),0\right)=if\left(\left({x}\in \left({A}\cap ℝ\right)\wedge 0\le \Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right),0\right)$
7 6 mpteq2dva ${⊢}{k}\in \left(0\dots 3\right)\to \left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right),0\right)\right)=\left({x}\in ℝ⟼if\left(\left({x}\in \left({A}\cap ℝ\right)\wedge 0\le \Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right),0\right)\right)$
8 7 fveq2d ${⊢}{k}\in \left(0\dots 3\right)\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right),0\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in \left({A}\cap ℝ\right)\wedge 0\le \Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right),0\right)\right)\right)$
9 8 oveq2d ${⊢}{k}\in \left(0\dots 3\right)\to {\mathrm{i}}^{{k}}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right),0\right)\right)\right)={\mathrm{i}}^{{k}}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in \left({A}\cap ℝ\right)\wedge 0\le \Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right),0\right)\right)\right)$
10 9 sumeq2i ${⊢}\sum _{{k}=0}^{3}{\mathrm{i}}^{{k}}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right),0\right)\right)\right)=\sum _{{k}=0}^{3}{\mathrm{i}}^{{k}}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in \left({A}\cap ℝ\right)\wedge 0\le \Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right),0\right)\right)\right)$
11 eqid ${⊢}\Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)=\Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)$
12 11 dfitg ${⊢}{\int }_{{A}}{B}d{x}=\sum _{{k}=0}^{3}{\mathrm{i}}^{{k}}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right),0\right)\right)\right)$
13 11 dfitg ${⊢}{\int }_{\left({A}\cap ℝ\right)}{B}d{x}=\sum _{{k}=0}^{3}{\mathrm{i}}^{{k}}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in \left({A}\cap ℝ\right)\wedge 0\le \Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right),0\right)\right)\right)$
14 10 12 13 3eqtr4i ${⊢}{\int }_{{A}}{B}d{x}={\int }_{\left({A}\cap ℝ\right)}{B}d{x}$