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	$⊢ φ \to X \in ℝ$
	itgsubsticc.2	$⊢ φ \to Y \in ℝ$
	itgsubsticc.3	$⊢ φ \to X \leq Y$
	itgsubsticc.4	$⊢ φ \to (x \in [X, Y] ⟼ A) : [X, Y] \underset{cn}{⟶} [K, L]$
	itgsubsticc.5	$⊢ φ \to (u \in [K, L] ⟼ C) : [K, L] \underset{cn}{⟶} ℂ$
	itgsubsticc.6	$⊢ φ \to (x \in (X, Y) ⟼ B) \in (((X, Y) \underset{cn}{⟶} ℂ) \cap 𝐿^{1})$
	itgsubsticc.7	$⊢ φ \to \frac{d (x \in [X, Y]⟼ A)}{d_{ℝ} x} = (x \in (X, Y) ⟼ B)$
	itgsubsticc.8	$⊢ u = A \to C = E$
	itgsubsticc.9	$⊢ x = X \to A = K$
	itgsubsticc.10	$⊢ x = Y \to A = L$
	itgsubsticc.11	$⊢ φ \to K \in ℝ$
	itgsubsticc.12	$⊢ φ \to L \in ℝ$
Assertion	itgsubsticc	$⊢ φ \to \int_{K}^{L} C d u = \int_{X}^{Y} E B d x$

Proof

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

Metamath Proof Explorer

Theorem itgsubsticc

Proof