# Metamath Proof Explorer

## Theorem itgeq2

Description: Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion itgeq2 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}\to {\int }_{{A}}{B}d{x}={\int }_{{A}}{C}d{x}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}ℝ=ℝ$
2 simpl ${⊢}\left({x}\in {A}\wedge 0\le \Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)\right)\to {x}\in {A}$
3 2 con3i ${⊢}¬{x}\in {A}\to ¬\left({x}\in {A}\wedge 0\le \Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)\right)$
4 3 iffalsed ${⊢}¬{x}\in {A}\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)=0$
5 simpl ${⊢}\left({x}\in {A}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\right)\to {x}\in {A}$
6 5 con3i ${⊢}¬{x}\in {A}\to ¬\left({x}\in {A}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\right)$
7 6 iffalsed ${⊢}¬{x}\in {A}\to if\left(\left({x}\in {A}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right),0\right)=0$
8 4 7 eqtr4d ${⊢}¬{x}\in {A}\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 {A}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right),0\right)$
9 fvoveq1 ${⊢}{B}={C}\to \Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)=\Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)$
10 9 breq2d ${⊢}{B}={C}\to \left(0\le \Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)↔0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\right)$
11 10 anbi2d ${⊢}{B}={C}\to \left(\left({x}\in {A}\wedge 0\le \Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)\right)↔\left({x}\in {A}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\right)\right)$
12 11 9 ifbieq1d ${⊢}{B}={C}\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 {A}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right),0\right)$
13 8 12 ja ${⊢}\left({x}\in {A}\to {B}={C}\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 {A}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right),0\right)$
14 13 a1d ${⊢}\left({x}\in {A}\to {B}={C}\right)\to \left({x}\in ℝ\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 {A}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right),0\right)\right)$
15 14 ralimi2 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}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 {A}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right),0\right)$
16 mpteq12 ${⊢}\left(ℝ=ℝ\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}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 {A}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right),0\right)\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 {A}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right),0\right)\right)$
17 1 15 16 sylancr ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}\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 {A}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right),0\right)\right)$
18 17 fveq2d ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}\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 {A}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right),0\right)\right)\right)$
19 18 oveq2d ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}\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 {A}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right),0\right)\right)\right)$
20 19 sumeq2sdv ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}\to \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 {A}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right),0\right)\right)\right)$
21 eqid ${⊢}\Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)=\Re \left(\frac{{B}}{{\mathrm{i}}^{{k}}}\right)$
22 21 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)$
23 eqid ${⊢}\Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)=\Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)$
24 23 dfitg ${⊢}{\int }_{{A}}{C}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{{C}}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right),0\right)\right)\right)$
25 20 22 24 3eqtr4g ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}\to {\int }_{{A}}{B}d{x}={\int }_{{A}}{C}d{x}$