Metamath Proof Explorer

Theorem itgsubsticc

Description: Integration by u-substitution. The main difference with respect to itgsubst is that here we consider the range of A ( x ) to be in the closed interval ( K , L ) . If A ( x ) is a continuous, differentiable function from [ X , Y ] to ( Z , W ) , whose derivative is continuous and integrable, and C ( u ) is a continuous function on ( Z , W ) , then the integral of C ( u ) from K = A ( X ) to L = A ( Y ) is equal to the integral of C ( A ( x ) ) _D A ( x ) from X to Y . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses itgsubsticc.1 ${⊢}{\phi }\to {X}\in ℝ$
itgsubsticc.2 ${⊢}{\phi }\to {Y}\in ℝ$
itgsubsticc.3 ${⊢}{\phi }\to {X}\le {Y}$
itgsubsticc.4 ${⊢}{\phi }\to \left({x}\in \left[{X},{Y}\right]⟼{A}\right):\left[{X},{Y}\right]\underset{cn}{⟶}\left[{K},{L}\right]$
itgsubsticc.5 ${⊢}{\phi }\to \left({u}\in \left[{K},{L}\right]⟼{C}\right):\left[{K},{L}\right]\underset{cn}{⟶}ℂ$
itgsubsticc.6
itgsubsticc.7 ${⊢}{\phi }\to \frac{d\left({x}\in \left[{X},{Y}\right]⟼{A}\right)}{{d}_{ℝ}{x}}=\left({x}\in \left({X},{Y}\right)⟼{B}\right)$
itgsubsticc.8 ${⊢}{u}={A}\to {C}={E}$
itgsubsticc.9 ${⊢}{x}={X}\to {A}={K}$
itgsubsticc.10 ${⊢}{x}={Y}\to {A}={L}$
itgsubsticc.11 ${⊢}{\phi }\to {K}\in ℝ$
itgsubsticc.12 ${⊢}{\phi }\to {L}\in ℝ$
Assertion itgsubsticc ${⊢}{\phi }\to {\int }_{{K}}^{{L}}{C}d{u}={\int }_{{X}}^{{Y}}{E}{B}d{x}$

Proof

Step Hyp Ref Expression
1 itgsubsticc.1 ${⊢}{\phi }\to {X}\in ℝ$
2 itgsubsticc.2 ${⊢}{\phi }\to {Y}\in ℝ$
3 itgsubsticc.3 ${⊢}{\phi }\to {X}\le {Y}$
4 itgsubsticc.4 ${⊢}{\phi }\to \left({x}\in \left[{X},{Y}\right]⟼{A}\right):\left[{X},{Y}\right]\underset{cn}{⟶}\left[{K},{L}\right]$
5 itgsubsticc.5 ${⊢}{\phi }\to \left({u}\in \left[{K},{L}\right]⟼{C}\right):\left[{K},{L}\right]\underset{cn}{⟶}ℂ$
6 itgsubsticc.6
7 itgsubsticc.7 ${⊢}{\phi }\to \frac{d\left({x}\in \left[{X},{Y}\right]⟼{A}\right)}{{d}_{ℝ}{x}}=\left({x}\in \left({X},{Y}\right)⟼{B}\right)$
8 itgsubsticc.8 ${⊢}{u}={A}\to {C}={E}$
9 itgsubsticc.9 ${⊢}{x}={X}\to {A}={K}$
10 itgsubsticc.10 ${⊢}{x}={Y}\to {A}={L}$
11 itgsubsticc.11 ${⊢}{\phi }\to {K}\in ℝ$
12 itgsubsticc.12 ${⊢}{\phi }\to {L}\in ℝ$
13 eqid ${⊢}\left({u}\in \left[{K},{L}\right]⟼{C}\right)=\left({u}\in \left[{K},{L}\right]⟼{C}\right)$
14 eqid ${⊢}\left({u}\in ℝ⟼if\left({u}\in \left[{K},{L}\right],\left({u}\in \left[{K},{L}\right]⟼{C}\right)\left({u}\right),if\left({u}<{K},\left({u}\in \left[{K},{L}\right]⟼{C}\right)\left({K}\right),\left({u}\in \left[{K},{L}\right]⟼{C}\right)\left({L}\right)\right)\right)\right)=\left({u}\in ℝ⟼if\left({u}\in \left[{K},{L}\right],\left({u}\in \left[{K},{L}\right]⟼{C}\right)\left({u}\right),if\left({u}<{K},\left({u}\in \left[{K},{L}\right]⟼{C}\right)\left({K}\right),\left({u}\in \left[{K},{L}\right]⟼{C}\right)\left({L}\right)\right)\right)\right)$
15 eqidd ${⊢}{\phi }\to \left({x}\in \left[{X},{Y}\right]⟼{A}\right)=\left({x}\in \left[{X},{Y}\right]⟼{A}\right)$
16 10 adantl ${⊢}\left({\phi }\wedge {x}={Y}\right)\to {A}={L}$
17 1 rexrd ${⊢}{\phi }\to {X}\in {ℝ}^{*}$
18 2 rexrd ${⊢}{\phi }\to {Y}\in {ℝ}^{*}$
19 ubicc2 ${⊢}\left({X}\in {ℝ}^{*}\wedge {Y}\in {ℝ}^{*}\wedge {X}\le {Y}\right)\to {Y}\in \left[{X},{Y}\right]$
20 17 18 3 19 syl3anc ${⊢}{\phi }\to {Y}\in \left[{X},{Y}\right]$
21 15 16 20 12 fvmptd ${⊢}{\phi }\to \left({x}\in \left[{X},{Y}\right]⟼{A}\right)\left({Y}\right)={L}$
22 cncff ${⊢}\left({x}\in \left[{X},{Y}\right]⟼{A}\right):\left[{X},{Y}\right]\underset{cn}{⟶}\left[{K},{L}\right]\to \left({x}\in \left[{X},{Y}\right]⟼{A}\right):\left[{X},{Y}\right]⟶\left[{K},{L}\right]$
23 4 22 syl ${⊢}{\phi }\to \left({x}\in \left[{X},{Y}\right]⟼{A}\right):\left[{X},{Y}\right]⟶\left[{K},{L}\right]$
24 23 20 ffvelrnd ${⊢}{\phi }\to \left({x}\in \left[{X},{Y}\right]⟼{A}\right)\left({Y}\right)\in \left[{K},{L}\right]$
25 21 24 eqeltrrd ${⊢}{\phi }\to {L}\in \left[{K},{L}\right]$
26 elicc2 ${⊢}\left({K}\in ℝ\wedge {L}\in ℝ\right)\to \left({L}\in \left[{K},{L}\right]↔\left({L}\in ℝ\wedge {K}\le {L}\wedge {L}\le {L}\right)\right)$
27 11 12 26 syl2anc ${⊢}{\phi }\to \left({L}\in \left[{K},{L}\right]↔\left({L}\in ℝ\wedge {K}\le {L}\wedge {L}\le {L}\right)\right)$
28 25 27 mpbid ${⊢}{\phi }\to \left({L}\in ℝ\wedge {K}\le {L}\wedge {L}\le {L}\right)$
29 28 simp2d ${⊢}{\phi }\to {K}\le {L}$
30 13 14 1 2 3 4 6 5 11 12 29 7 8 9 10 itgsubsticclem ${⊢}{\phi }\to {\int }_{{K}}^{{L}}{C}d{u}={\int }_{{X}}^{{Y}}{E}{B}d{x}$