itgsubst

Description: Integration by u -substitution. 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 . In this part of the proof we discharge the assumptions in itgsubstlem , which use the fact that ( Z , W ) is open to shrink the interval a little to ( M , N ) where Z < M < N < W - this is possible because A ( x ) is a continuous function on a closed interval, so its range is in fact a closed interval, and we have some wiggle room on the edges. (Contributed by Mario Carneiro, 7-Sep-2014)

	Ref	Expression
Hypotheses	itgsubst.x	$⊢ φ \to X \in ℝ$
	itgsubst.y	$⊢ φ \to Y \in ℝ$
	itgsubst.le	$⊢ φ \to X \leq Y$
	itgsubst.z	$⊢ φ \to Z \in ℝ^{*}$
	itgsubst.w	$⊢ φ \to W \in ℝ^{*}$
	itgsubst.a	$⊢ φ \to (x \in [X, Y] ⟼ A) : [X, Y] \underset{cn}{⟶} (Z, W)$
	itgsubst.b	$⊢ φ \to (x \in (X, Y) ⟼ B) \in (((X, Y) \underset{cn}{⟶} ℂ) \cap 𝐿^{1})$
	itgsubst.c	$⊢ φ \to (u \in (Z, W) ⟼ C) : (Z, W) \underset{cn}{⟶} ℂ$
	itgsubst.da	$⊢ φ \to \frac{d (x \in [X, Y]⟼ A)}{d_{ℝ} x} = (x \in (X, Y) ⟼ B)$
	itgsubst.e	$⊢ u = A \to C = E$
	itgsubst.k	$⊢ x = X \to A = K$
	itgsubst.l	$⊢ x = Y \to A = L$
Assertion	itgsubst	$⊢ φ \to \int_{K}^{L} C d u = \int_{X}^{Y} E B d x$

Proof

Step	Hyp	Ref	Expression
1		itgsubst.x	$⊢ φ \to X \in ℝ$
2		itgsubst.y	$⊢ φ \to Y \in ℝ$
3		itgsubst.le	$⊢ φ \to X \leq Y$
4		itgsubst.z	$⊢ φ \to Z \in ℝ^{*}$
5		itgsubst.w	$⊢ φ \to W \in ℝ^{*}$
6		itgsubst.a	$⊢ φ \to (x \in [X, Y] ⟼ A) : [X, Y] \underset{cn}{⟶} (Z, W)$
7		itgsubst.b	$⊢ φ \to (x \in (X, Y) ⟼ B) \in (((X, Y) \underset{cn}{⟶} ℂ) \cap 𝐿^{1})$
8		itgsubst.c	$⊢ φ \to (u \in (Z, W) ⟼ C) : (Z, W) \underset{cn}{⟶} ℂ$
9		itgsubst.da	$⊢ φ \to \frac{d (x \in [X, Y]⟼ A)}{d_{ℝ} x} = (x \in (X, Y) ⟼ B)$
10		itgsubst.e	$⊢ u = A \to C = E$
11		itgsubst.k	$⊢ x = X \to A = K$
12		itgsubst.l	$⊢ x = Y \to A = L$
13		ioossre	$⊢ (Z, W) \subseteq ℝ$
14		ax-resscn	$⊢ ℝ \subseteq ℂ$
15		cncfss	$⊢ ((Z, W) \subseteq ℝ \land ℝ \subseteq ℂ) \to [X, Y] \underset{cn}{⟶} (Z, W) \subseteq [X, Y] \underset{cn}{⟶} ℝ$
16	13 14 15	mp2an	$⊢ [X, Y] \underset{cn}{⟶} (Z, W) \subseteq [X, Y] \underset{cn}{⟶} ℝ$
17	16 6	sseldi	$⊢ φ \to (x \in [X, Y] ⟼ A) : [X, Y] \underset{cn}{⟶} ℝ$
18	1 2 3 17	evthicc	$⊢ φ \to (\exists y \in [X, Y] \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y) \land \exists y \in [X, Y] \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))$
19		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
20	13 19	sstri	$⊢ (Z, W) \subseteq ℝ^{*}$
21		cncff	$⊢ (x \in [X, Y] ⟼ A) : [X, Y] \underset{cn}{⟶} (Z, W) \to (x \in [X, Y] ⟼ A) : [X, Y] ⟶ (Z, W)$
22	6 21	syl	$⊢ φ \to (x \in [X, Y] ⟼ A) : [X, Y] ⟶ (Z, W)$
23	22	adantr	$⊢ (φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y))) \to (x \in [X, Y] ⟼ A) : [X, Y] ⟶ (Z, W)$
24		simprl	$⊢ (φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y))) \to y \in [X, Y]$
25	23 24	ffvelrnd	$⊢ (φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y))) \to (x \in [X, Y] ⟼ A) (y) \in (Z, W)$
26	20 25	sseldi	$⊢ (φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y))) \to (x \in [X, Y] ⟼ A) (y) \in ℝ^{*}$
27	5	adantr	$⊢ (φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y))) \to W \in ℝ^{*}$
28		eliooord	$⊢ (x \in [X, Y] ⟼ A) (y) \in (Z, W) \to (Z < (x \in [X, Y] ⟼ A) (y) \land (x \in [X, Y] ⟼ A) (y) < W)$
29	25 28	syl	$⊢ (φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y))) \to (Z < (x \in [X, Y] ⟼ A) (y) \land (x \in [X, Y] ⟼ A) (y) < W)$
30	29	simprd	$⊢ (φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y))) \to (x \in [X, Y] ⟼ A) (y) < W$
31		qbtwnxr	$⊢ ((x \in [X, Y] ⟼ A) (y) \in ℝ^{} \land W \in ℝ^{} \land (x \in [X, Y] ⟼ A) (y) < W) \to \exists n \in ℚ ((x \in [X, Y] ⟼ A) (y) < n \land n < W)$
32	26 27 30 31	syl3anc	$⊢ (φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y))) \to \exists n \in ℚ ((x \in [X, Y] ⟼ A) (y) < n \land n < W)$
33		qre	$⊢ n \in ℚ \to n \in ℝ$
34	33	ad2antrl	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y))) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \to n \in ℝ$
35	4	ad2antrr	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y))) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \to Z \in ℝ^{*}$
36	26	adantr	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y))) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \to (x \in [X, Y] ⟼ A) (y) \in ℝ^{*}$
37	34	rexrd	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y))) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \to n \in ℝ^{*}$
38	29	simpld	$⊢ (φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y))) \to Z < (x \in [X, Y] ⟼ A) (y)$
39	38	adantr	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y))) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \to Z < (x \in [X, Y] ⟼ A) (y)$
40		simprrl	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y))) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \to (x \in [X, Y] ⟼ A) (y) < n$
41	35 36 37 39 40	xrlttrd	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y))) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \to Z < n$
42		simprrr	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y))) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \to n < W$
43	5	ad2antrr	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y))) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \to W \in ℝ^{*}$
44		elioo2	$⊢ (Z \in ℝ^{} \land W \in ℝ^{}) \to (n \in (Z, W) \leftrightarrow (n \in ℝ \land Z < n \land n < W))$
45	35 43 44	syl2anc	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y))) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \to (n \in (Z, W) \leftrightarrow (n \in ℝ \land Z < n \land n < W))$
46	34 41 42 45	mpbir3and	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y))) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \to n \in (Z, W)$
47		anass	$⊢ ((φ \land y \in [X, Y]) \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y)) \leftrightarrow (φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y)))$
48		simprrl	$⊢ ((φ \land y \in [X, Y]) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \to (x \in [X, Y] ⟼ A) (y) < n$
49	48	adantr	$⊢ (((φ \land y \in [X, Y]) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \land z \in [X, Y]) \to (x \in [X, Y] ⟼ A) (y) < n$
50	22	ad2antrr	$⊢ ((φ \land y \in [X, Y]) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \to (x \in [X, Y] ⟼ A) : [X, Y] ⟶ (Z, W)$
51	50	ffvelrnda	$⊢ (((φ \land y \in [X, Y]) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \land z \in [X, Y]) \to (x \in [X, Y] ⟼ A) (z) \in (Z, W)$
52	20 51	sseldi	$⊢ (((φ \land y \in [X, Y]) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \land z \in [X, Y]) \to (x \in [X, Y] ⟼ A) (z) \in ℝ^{*}$
53		simplr	$⊢ ((φ \land y \in [X, Y]) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \to y \in [X, Y]$
54	50 53	ffvelrnd	$⊢ ((φ \land y \in [X, Y]) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \to (x \in [X, Y] ⟼ A) (y) \in (Z, W)$
55	20 54	sseldi	$⊢ ((φ \land y \in [X, Y]) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \to (x \in [X, Y] ⟼ A) (y) \in ℝ^{*}$
56	55	adantr	$⊢ (((φ \land y \in [X, Y]) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \land z \in [X, Y]) \to (x \in [X, Y] ⟼ A) (y) \in ℝ^{*}$
57	33	ad2antrl	$⊢ ((φ \land y \in [X, Y]) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \to n \in ℝ$
58	57	adantr	$⊢ (((φ \land y \in [X, Y]) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \land z \in [X, Y]) \to n \in ℝ$
59	58	rexrd	$⊢ (((φ \land y \in [X, Y]) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \land z \in [X, Y]) \to n \in ℝ^{*}$
60		xrlelttr	$⊢ ((x \in [X, Y] ⟼ A) (z) \in ℝ^{} \land (x \in [X, Y] ⟼ A) (y) \in ℝ^{} \land n \in ℝ^{*}) \to (((x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y) \land (x \in [X, Y] ⟼ A) (y) < n) \to (x \in [X, Y] ⟼ A) (z) < n)$
61	52 56 59 60	syl3anc	$⊢ (((φ \land y \in [X, Y]) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \land z \in [X, Y]) \to (((x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y) \land (x \in [X, Y] ⟼ A) (y) < n) \to (x \in [X, Y] ⟼ A) (z) < n)$
62	49 61	mpan2d	$⊢ (((φ \land y \in [X, Y]) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \land z \in [X, Y]) \to ((x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y) \to (x \in [X, Y] ⟼ A) (z) < n)$
63	62	ralimdva	$⊢ ((φ \land y \in [X, Y]) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \to (\forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y) \to \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) < n)$
64	63	imp	$⊢ (((φ \land y \in [X, Y]) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y)) \to \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) < n$
65	64	an32s	$⊢ (((φ \land y \in [X, Y]) \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y)) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \to \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) < n$
66	47 65	sylanbr	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y))) \land (n \in ℚ \land ((x \in [X, Y] ⟼ A) (y) < n \land n < W))) \to \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) < n$
67	32 46 66	reximssdv	$⊢ (φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y))) \to \exists n \in (Z, W) \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) < n$
68	67	rexlimdvaa	$⊢ φ \to (\exists y \in [X, Y] \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y) \to \exists n \in (Z, W) \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) < n)$
69	4	adantr	$⊢ (φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))) \to Z \in ℝ^{*}$
70	22	adantr	$⊢ (φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))) \to (x \in [X, Y] ⟼ A) : [X, Y] ⟶ (Z, W)$
71		simprl	$⊢ (φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))) \to y \in [X, Y]$
72	70 71	ffvelrnd	$⊢ (φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))) \to (x \in [X, Y] ⟼ A) (y) \in (Z, W)$
73	20 72	sseldi	$⊢ (φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))) \to (x \in [X, Y] ⟼ A) (y) \in ℝ^{*}$
74	72 28	syl	$⊢ (φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))) \to (Z < (x \in [X, Y] ⟼ A) (y) \land (x \in [X, Y] ⟼ A) (y) < W)$
75	74	simpld	$⊢ (φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))) \to Z < (x \in [X, Y] ⟼ A) (y)$
76		qbtwnxr	$⊢ (Z \in ℝ^{} \land (x \in [X, Y] ⟼ A) (y) \in ℝ^{} \land Z < (x \in [X, Y] ⟼ A) (y)) \to \exists m \in ℚ (Z < m \land m < (x \in [X, Y] ⟼ A) (y))$
77	69 73 75 76	syl3anc	$⊢ (φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))) \to \exists m \in ℚ (Z < m \land m < (x \in [X, Y] ⟼ A) (y))$
78		qre	$⊢ m \in ℚ \to m \in ℝ$
79	78	ad2antrl	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \to m \in ℝ$
80		simprrl	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \to Z < m$
81	79	rexrd	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \to m \in ℝ^{*}$
82	73	adantr	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \to (x \in [X, Y] ⟼ A) (y) \in ℝ^{*}$
83	5	ad2antrr	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \to W \in ℝ^{*}$
84		simprrr	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \to m < (x \in [X, Y] ⟼ A) (y)$
85	74	simprd	$⊢ (φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))) \to (x \in [X, Y] ⟼ A) (y) < W$
86	85	adantr	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \to (x \in [X, Y] ⟼ A) (y) < W$
87	81 82 83 84 86	xrlttrd	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \to m < W$
88	4	ad2antrr	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \to Z \in ℝ^{*}$
89		elioo2	$⊢ (Z \in ℝ^{} \land W \in ℝ^{}) \to (m \in (Z, W) \leftrightarrow (m \in ℝ \land Z < m \land m < W))$
90	88 83 89	syl2anc	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \to (m \in (Z, W) \leftrightarrow (m \in ℝ \land Z < m \land m < W))$
91	79 80 87 90	mpbir3and	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \to m \in (Z, W)$
92		anass	$⊢ ((φ \land y \in [X, Y]) \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z)) \leftrightarrow (φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z)))$
93		simprrr	$⊢ ((φ \land y \in [X, Y]) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \to m < (x \in [X, Y] ⟼ A) (y)$
94	93	adantr	$⊢ (((φ \land y \in [X, Y]) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \land z \in [X, Y]) \to m < (x \in [X, Y] ⟼ A) (y)$
95	78	ad2antrl	$⊢ ((φ \land y \in [X, Y]) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \to m \in ℝ$
96	95	adantr	$⊢ (((φ \land y \in [X, Y]) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \land z \in [X, Y]) \to m \in ℝ$
97	96	rexrd	$⊢ (((φ \land y \in [X, Y]) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \land z \in [X, Y]) \to m \in ℝ^{*}$
98	22	ad2antrr	$⊢ ((φ \land y \in [X, Y]) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \to (x \in [X, Y] ⟼ A) : [X, Y] ⟶ (Z, W)$
99		simplr	$⊢ ((φ \land y \in [X, Y]) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \to y \in [X, Y]$
100	98 99	ffvelrnd	$⊢ ((φ \land y \in [X, Y]) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \to (x \in [X, Y] ⟼ A) (y) \in (Z, W)$
101	20 100	sseldi	$⊢ ((φ \land y \in [X, Y]) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \to (x \in [X, Y] ⟼ A) (y) \in ℝ^{*}$
102	101	adantr	$⊢ (((φ \land y \in [X, Y]) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \land z \in [X, Y]) \to (x \in [X, Y] ⟼ A) (y) \in ℝ^{*}$
103	98	ffvelrnda	$⊢ (((φ \land y \in [X, Y]) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \land z \in [X, Y]) \to (x \in [X, Y] ⟼ A) (z) \in (Z, W)$
104	20 103	sseldi	$⊢ (((φ \land y \in [X, Y]) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \land z \in [X, Y]) \to (x \in [X, Y] ⟼ A) (z) \in ℝ^{*}$
105		xrltletr	$⊢ (m \in ℝ^{} \land (x \in [X, Y] ⟼ A) (y) \in ℝ^{} \land (x \in [X, Y] ⟼ A) (z) \in ℝ^{*}) \to ((m < (x \in [X, Y] ⟼ A) (y) \land (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z)) \to m < (x \in [X, Y] ⟼ A) (z))$
106	97 102 104 105	syl3anc	$⊢ (((φ \land y \in [X, Y]) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \land z \in [X, Y]) \to ((m < (x \in [X, Y] ⟼ A) (y) \land (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z)) \to m < (x \in [X, Y] ⟼ A) (z))$
107	94 106	mpand	$⊢ (((φ \land y \in [X, Y]) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \land z \in [X, Y]) \to ((x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z) \to m < (x \in [X, Y] ⟼ A) (z))$
108	107	ralimdva	$⊢ ((φ \land y \in [X, Y]) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \to (\forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z) \to \forall z \in [X, Y] m < (x \in [X, Y] ⟼ A) (z))$
109	108	imp	$⊢ (((φ \land y \in [X, Y]) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z)) \to \forall z \in [X, Y] m < (x \in [X, Y] ⟼ A) (z)$
110	109	an32s	$⊢ (((φ \land y \in [X, Y]) \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z)) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \to \forall z \in [X, Y] m < (x \in [X, Y] ⟼ A) (z)$
111	92 110	sylanbr	$⊢ ((φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))) \land (m \in ℚ \land (Z < m \land m < (x \in [X, Y] ⟼ A) (y)))) \to \forall z \in [X, Y] m < (x \in [X, Y] ⟼ A) (z)$
112	77 91 111	reximssdv	$⊢ (φ \land (y \in [X, Y] \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z))) \to \exists m \in (Z, W) \forall z \in [X, Y] m < (x \in [X, Y] ⟼ A) (z)$
113	112	rexlimdvaa	$⊢ φ \to (\exists y \in [X, Y] \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z) \to \exists m \in (Z, W) \forall z \in [X, Y] m < (x \in [X, Y] ⟼ A) (z))$
114		ancom	$⊢ (\exists n \in (Z, W) \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) < n \land \exists m \in (Z, W) \forall z \in [X, Y] m < (x \in [X, Y] ⟼ A) (z)) \leftrightarrow (\exists m \in (Z, W) \forall z \in [X, Y] m < (x \in [X, Y] ⟼ A) (z) \land \exists n \in (Z, W) \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) < n)$
115		reeanv	$⊢ \exists m \in (Z, W) \exists n \in (Z, W) (\forall z \in [X, Y] m < (x \in [X, Y] ⟼ A) (z) \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) < n) \leftrightarrow (\exists m \in (Z, W) \forall z \in [X, Y] m < (x \in [X, Y] ⟼ A) (z) \land \exists n \in (Z, W) \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) < n)$
116	114 115	bitr4i	$⊢ (\exists n \in (Z, W) \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) < n \land \exists m \in (Z, W) \forall z \in [X, Y] m < (x \in [X, Y] ⟼ A) (z)) \leftrightarrow \exists m \in (Z, W) \exists n \in (Z, W) (\forall z \in [X, Y] m < (x \in [X, Y] ⟼ A) (z) \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) < n)$
117		r19.26	$⊢ \forall z \in [X, Y] (m < (x \in [X, Y] ⟼ A) (z) \land (x \in [X, Y] ⟼ A) (z) < n) \leftrightarrow (\forall z \in [X, Y] m < (x \in [X, Y] ⟼ A) (z) \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) < n)$
118	22	adantr	$⊢ (φ \land (m \in (Z, W) \land n \in (Z, W))) \to (x \in [X, Y] ⟼ A) : [X, Y] ⟶ (Z, W)$
119	118	ffvelrnda	$⊢ ((φ \land (m \in (Z, W) \land n \in (Z, W))) \land z \in [X, Y]) \to (x \in [X, Y] ⟼ A) (z) \in (Z, W)$
120	13 119	sseldi	$⊢ ((φ \land (m \in (Z, W) \land n \in (Z, W))) \land z \in [X, Y]) \to (x \in [X, Y] ⟼ A) (z) \in ℝ$
121	120	3biant1d	$⊢ ((φ \land (m \in (Z, W) \land n \in (Z, W))) \land z \in [X, Y]) \to ((m < (x \in [X, Y] ⟼ A) (z) \land (x \in [X, Y] ⟼ A) (z) < n) \leftrightarrow ((x \in [X, Y] ⟼ A) (z) \in ℝ \land m < (x \in [X, Y] ⟼ A) (z) \land (x \in [X, Y] ⟼ A) (z) < n))$
122		simplrl	$⊢ ((φ \land (m \in (Z, W) \land n \in (Z, W))) \land z \in [X, Y]) \to m \in (Z, W)$
123	20 122	sseldi	$⊢ ((φ \land (m \in (Z, W) \land n \in (Z, W))) \land z \in [X, Y]) \to m \in ℝ^{*}$
124		simplrr	$⊢ ((φ \land (m \in (Z, W) \land n \in (Z, W))) \land z \in [X, Y]) \to n \in (Z, W)$
125	20 124	sseldi	$⊢ ((φ \land (m \in (Z, W) \land n \in (Z, W))) \land z \in [X, Y]) \to n \in ℝ^{*}$
126		elioo2	$⊢ (m \in ℝ^{} \land n \in ℝ^{}) \to ((x \in [X, Y] ⟼ A) (z) \in (m, n) \leftrightarrow ((x \in [X, Y] ⟼ A) (z) \in ℝ \land m < (x \in [X, Y] ⟼ A) (z) \land (x \in [X, Y] ⟼ A) (z) < n))$
127	123 125 126	syl2anc	$⊢ ((φ \land (m \in (Z, W) \land n \in (Z, W))) \land z \in [X, Y]) \to ((x \in [X, Y] ⟼ A) (z) \in (m, n) \leftrightarrow ((x \in [X, Y] ⟼ A) (z) \in ℝ \land m < (x \in [X, Y] ⟼ A) (z) \land (x \in [X, Y] ⟼ A) (z) < n))$
128	121 127	bitr4d	$⊢ ((φ \land (m \in (Z, W) \land n \in (Z, W))) \land z \in [X, Y]) \to ((m < (x \in [X, Y] ⟼ A) (z) \land (x \in [X, Y] ⟼ A) (z) < n) \leftrightarrow (x \in [X, Y] ⟼ A) (z) \in (m, n))$
129	128	ralbidva	$⊢ (φ \land (m \in (Z, W) \land n \in (Z, W))) \to (\forall z \in [X, Y] (m < (x \in [X, Y] ⟼ A) (z) \land (x \in [X, Y] ⟼ A) (z) < n) \leftrightarrow \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \in (m, n))$
130		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in [X, Y] ⟼ A) (z)$
131	130	nfel1	$⊢ Ⅎ x (x \in [X, Y] ⟼ A) (z) \in (m, n)$
132		nfv	$⊢ Ⅎ z (x \in [X, Y] ⟼ A) (x) \in (m, n)$
133		fveq2	$⊢ z = x \to (x \in [X, Y] ⟼ A) (z) = (x \in [X, Y] ⟼ A) (x)$
134	133	eleq1d	$⊢ z = x \to ((x \in [X, Y] ⟼ A) (z) \in (m, n) \leftrightarrow (x \in [X, Y] ⟼ A) (x) \in (m, n))$
135	131 132 134	cbvralw	$⊢ \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \in (m, n) \leftrightarrow \forall x \in [X, Y] (x \in [X, Y] ⟼ A) (x) \in (m, n)$
136		simpr	$⊢ (φ \land x \in [X, Y]) \to x \in [X, Y]$
137	22	fvmptelrn	$⊢ (φ \land x \in [X, Y]) \to A \in (Z, W)$
138		eqid	$⊢ (x \in [X, Y] ⟼ A) = (x \in [X, Y] ⟼ A)$
139	138	fvmpt2	$⊢ (x \in [X, Y] \land A \in (Z, W)) \to (x \in [X, Y] ⟼ A) (x) = A$
140	136 137 139	syl2anc	$⊢ (φ \land x \in [X, Y]) \to (x \in [X, Y] ⟼ A) (x) = A$
141	140	eleq1d	$⊢ (φ \land x \in [X, Y]) \to ((x \in [X, Y] ⟼ A) (x) \in (m, n) \leftrightarrow A \in (m, n))$
142	141	ralbidva	$⊢ φ \to (\forall x \in [X, Y] (x \in [X, Y] ⟼ A) (x) \in (m, n) \leftrightarrow \forall x \in [X, Y] A \in (m, n))$
143	135 142	syl5bb	$⊢ φ \to (\forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \in (m, n) \leftrightarrow \forall x \in [X, Y] A \in (m, n))$
144	143	adantr	$⊢ (φ \land (m \in (Z, W) \land n \in (Z, W))) \to (\forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \in (m, n) \leftrightarrow \forall x \in [X, Y] A \in (m, n))$
145	1	adantr	$⊢ (φ \land ((m \in (Z, W) \land n \in (Z, W)) \land \forall x \in [X, Y] A \in (m, n))) \to X \in ℝ$
146	2	adantr	$⊢ (φ \land ((m \in (Z, W) \land n \in (Z, W)) \land \forall x \in [X, Y] A \in (m, n))) \to Y \in ℝ$
147	3	adantr	$⊢ (φ \land ((m \in (Z, W) \land n \in (Z, W)) \land \forall x \in [X, Y] A \in (m, n))) \to X \leq Y$
148	4	adantr	$⊢ (φ \land ((m \in (Z, W) \land n \in (Z, W)) \land \forall x \in [X, Y] A \in (m, n))) \to Z \in ℝ^{*}$
149	5	adantr	$⊢ (φ \land ((m \in (Z, W) \land n \in (Z, W)) \land \forall x \in [X, Y] A \in (m, n))) \to W \in ℝ^{*}$
150		nfcv	$⊢ \underline{Ⅎ} y A$
151		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ A$
152		csbeq1a	$⊢ x = y \to A = ⦋ y / x ⦌ A$
153	150 151 152	cbvmpt	$⊢ (x \in [X, Y] ⟼ A) = (y \in [X, Y] ⟼ ⦋ y / x ⦌ A)$
154	153 6	eqeltrrid	$⊢ φ \to (y \in [X, Y] ⟼ ⦋ y / x ⦌ A) : [X, Y] \underset{cn}{⟶} (Z, W)$
155	154	adantr	$⊢ (φ \land ((m \in (Z, W) \land n \in (Z, W)) \land \forall x \in [X, Y] A \in (m, n))) \to (y \in [X, Y] ⟼ ⦋ y / x ⦌ A) : [X, Y] \underset{cn}{⟶} (Z, W)$
156		nfcv	$⊢ \underline{Ⅎ} y B$
157		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ B$
158		csbeq1a	$⊢ x = y \to B = ⦋ y / x ⦌ B$
159	156 157 158	cbvmpt	$⊢ (x \in (X, Y) ⟼ B) = (y \in (X, Y) ⟼ ⦋ y / x ⦌ B)$
160	159 7	eqeltrrid	$⊢ φ \to (y \in (X, Y) ⟼ ⦋ y / x ⦌ B) \in (((X, Y) \underset{cn}{⟶} ℂ) \cap 𝐿^{1})$
161	160	adantr	$⊢ (φ \land ((m \in (Z, W) \land n \in (Z, W)) \land \forall x \in [X, Y] A \in (m, n))) \to (y \in (X, Y) ⟼ ⦋ y / x ⦌ B) \in (((X, Y) \underset{cn}{⟶} ℂ) \cap 𝐿^{1})$
162		nfcv	$⊢ \underline{Ⅎ} v C$
163		nfcsb1v	$⊢ \underline{Ⅎ} u ⦋ v / u ⦌ C$
164		csbeq1a	$⊢ u = v \to C = ⦋ v / u ⦌ C$
165	162 163 164	cbvmpt	$⊢ (u \in (Z, W) ⟼ C) = (v \in (Z, W) ⟼ ⦋ v / u ⦌ C)$
166	165 8	eqeltrrid	$⊢ φ \to (v \in (Z, W) ⟼ ⦋ v / u ⦌ C) : (Z, W) \underset{cn}{⟶} ℂ$
167	166	adantr	$⊢ (φ \land ((m \in (Z, W) \land n \in (Z, W)) \land \forall x \in [X, Y] A \in (m, n))) \to (v \in (Z, W) ⟼ ⦋ v / u ⦌ C) : (Z, W) \underset{cn}{⟶} ℂ$
168	153	oveq2i	$⊢ \frac{d (x \in [X, Y]⟼ A)}{d_{ℝ} x} = \frac{d (y \in [X, Y]⟼ ⦋ y / x ⦌ A)}{d_{ℝ} y}$
169	9 168 159	3eqtr3g	$⊢ φ \to \frac{d (y \in [X, Y]⟼ ⦋ y / x ⦌ A)}{d_{ℝ} y} = (y \in (X, Y) ⟼ ⦋ y / x ⦌ B)$
170	169	adantr	$⊢ (φ \land ((m \in (Z, W) \land n \in (Z, W)) \land \forall x \in [X, Y] A \in (m, n))) \to \frac{d (y \in [X, Y]⟼ ⦋ y / x ⦌ A)}{d_{ℝ} y} = (y \in (X, Y) ⟼ ⦋ y / x ⦌ B)$
171		csbeq1	$⊢ v = ⦋ y / x ⦌ A \to ⦋ v / u ⦌ C = ⦋ ⦋ y / x ⦌ A / u ⦌ C$
172		csbeq1	$⊢ y = X \to ⦋ y / x ⦌ A = ⦋ X / x ⦌ A$
173		csbeq1	$⊢ y = Y \to ⦋ y / x ⦌ A = ⦋ Y / x ⦌ A$
174		simprll	$⊢ (φ \land ((m \in (Z, W) \land n \in (Z, W)) \land \forall x \in [X, Y] A \in (m, n))) \to m \in (Z, W)$
175		simprlr	$⊢ (φ \land ((m \in (Z, W) \land n \in (Z, W)) \land \forall x \in [X, Y] A \in (m, n))) \to n \in (Z, W)$
176		simprr	$⊢ (φ \land ((m \in (Z, W) \land n \in (Z, W)) \land \forall x \in [X, Y] A \in (m, n))) \to \forall x \in [X, Y] A \in (m, n)$
177	151	nfel1	$⊢ Ⅎ x ⦋ y / x ⦌ A \in (m, n)$
178	152	eleq1d	$⊢ x = y \to (A \in (m, n) \leftrightarrow ⦋ y / x ⦌ A \in (m, n))$
179	177 178	rspc	$⊢ y \in [X, Y] \to (\forall x \in [X, Y] A \in (m, n) \to ⦋ y / x ⦌ A \in (m, n))$
180	176 179	mpan9	$⊢ ((φ \land ((m \in (Z, W) \land n \in (Z, W)) \land \forall x \in [X, Y] A \in (m, n))) \land y \in [X, Y]) \to ⦋ y / x ⦌ A \in (m, n)$
181	145 146 147 148 149 155 161 167 170 171 172 173 174 175 180	itgsubstlem	$⊢ (φ \land ((m \in (Z, W) \land n \in (Z, W)) \land \forall x \in [X, Y] A \in (m, n))) \to \int_{⦋ X / x ⦌ A}^{⦋ Y / x ⦌ A} ⦋ v / u ⦌ C d v = \int_{X}^{Y} ⦋ ⦋ y / x ⦌ A / u ⦌ C ⦋ y / x ⦌ B d y$
182	164 162 163	cbvditg	$⊢ \int_{⦋ X / x ⦌ A}^{⦋ Y / x ⦌ A} C d u = \int_{⦋ X / x ⦌ A}^{⦋ Y / x ⦌ A} ⦋ v / u ⦌ C d v$
183		nfcvd	$⊢ X \in ℝ \to \underline{Ⅎ} x K$
184	183 11	csbiegf	$⊢ X \in ℝ \to ⦋ X / x ⦌ A = K$
185		ditgeq1	$⊢ ⦋ X / x ⦌ A = K \to \int_{⦋ X / x ⦌ A}^{⦋ Y / x ⦌ A} C d u = \int_{K}^{⦋ Y / x ⦌ A} C d u$
186	1 184 185	3syl	$⊢ φ \to \int_{⦋ X / x ⦌ A}^{⦋ Y / x ⦌ A} C d u = \int_{K}^{⦋ Y / x ⦌ A} C d u$
187		nfcvd	$⊢ Y \in ℝ \to \underline{Ⅎ} x L$
188	187 12	csbiegf	$⊢ Y \in ℝ \to ⦋ Y / x ⦌ A = L$
189		ditgeq2	$⊢ ⦋ Y / x ⦌ A = L \to \int_{K}^{⦋ Y / x ⦌ A} C d u = \int_{K}^{L} C d u$
190	2 188 189	3syl	$⊢ φ \to \int_{K}^{⦋ Y / x ⦌ A} C d u = \int_{K}^{L} C d u$
191	186 190	eqtrd	$⊢ φ \to \int_{⦋ X / x ⦌ A}^{⦋ Y / x ⦌ A} C d u = \int_{K}^{L} C d u$
192	182 191	eqtr3id	$⊢ φ \to \int_{⦋ X / x ⦌ A}^{⦋ Y / x ⦌ A} ⦋ v / u ⦌ C d v = \int_{K}^{L} C d u$
193	192	adantr	$⊢ (φ \land ((m \in (Z, W) \land n \in (Z, W)) \land \forall x \in [X, Y] A \in (m, n))) \to \int_{⦋ X / x ⦌ A}^{⦋ Y / x ⦌ A} ⦋ v / u ⦌ C d v = \int_{K}^{L} C d u$
194	152	csbeq1d	$⊢ x = y \to ⦋ A / u ⦌ C = ⦋ ⦋ y / x ⦌ A / u ⦌ C$
195	194 158	oveq12d	$⊢ x = y \to ⦋ A / u ⦌ C B = ⦋ ⦋ y / x ⦌ A / u ⦌ C ⦋ y / x ⦌ B$
196		nfcv	$⊢ \underline{Ⅎ} y ⦋ A / u ⦌ C B$
197		nfcv	$⊢ \underline{Ⅎ} x C$
198	151 197	nfcsbw	$⊢ \underline{Ⅎ} x ⦋ ⦋ y / x ⦌ A / u ⦌ C$
199		nfcv	$⊢ \underline{Ⅎ} x \times$
200	198 199 157	nfov	$⊢ \underline{Ⅎ} x ⦋ ⦋ y / x ⦌ A / u ⦌ C ⦋ y / x ⦌ B$
201	195 196 200	cbvditg	$⊢ \int_{X}^{Y} ⦋ A / u ⦌ C B d x = \int_{X}^{Y} ⦋ ⦋ y / x ⦌ A / u ⦌ C ⦋ y / x ⦌ B d y$
202		ioossicc	$⊢ (X, Y) \subseteq [X, Y]$
203	202	sseli	$⊢ x \in (X, Y) \to x \in [X, Y]$
204	203 137	sylan2	$⊢ (φ \land x \in (X, Y)) \to A \in (Z, W)$
205		nfcvd	$⊢ A \in (Z, W) \to \underline{Ⅎ} u E$
206	205 10	csbiegf	$⊢ A \in (Z, W) \to ⦋ A / u ⦌ C = E$
207	204 206	syl	$⊢ (φ \land x \in (X, Y)) \to ⦋ A / u ⦌ C = E$
208	207	oveq1d	$⊢ (φ \land x \in (X, Y)) \to ⦋ A / u ⦌ C B = E B$
209	208	itgeq2dv	$⊢ φ \to \int_{(X, Y)} ⦋ A / u ⦌ C B d x = \int_{(X, Y)} E B d x$
210	3	ditgpos	$⊢ φ \to \int_{X}^{Y} ⦋ A / u ⦌ C B d x = \int_{(X, Y)} ⦋ A / u ⦌ C B d x$
211	3	ditgpos	$⊢ φ \to \int_{X}^{Y} E B d x = \int_{(X, Y)} E B d x$
212	209 210 211	3eqtr4d	$⊢ φ \to \int_{X}^{Y} ⦋ A / u ⦌ C B d x = \int_{X}^{Y} E B d x$
213	201 212	eqtr3id	$⊢ φ \to \int_{X}^{Y} ⦋ ⦋ y / x ⦌ A / u ⦌ C ⦋ y / x ⦌ B d y = \int_{X}^{Y} E B d x$
214	213	adantr	$⊢ (φ \land ((m \in (Z, W) \land n \in (Z, W)) \land \forall x \in [X, Y] A \in (m, n))) \to \int_{X}^{Y} ⦋ ⦋ y / x ⦌ A / u ⦌ C ⦋ y / x ⦌ B d y = \int_{X}^{Y} E B d x$
215	181 193 214	3eqtr3d	$⊢ (φ \land ((m \in (Z, W) \land n \in (Z, W)) \land \forall x \in [X, Y] A \in (m, n))) \to \int_{K}^{L} C d u = \int_{X}^{Y} E B d x$
216	215	expr	$⊢ (φ \land (m \in (Z, W) \land n \in (Z, W))) \to (\forall x \in [X, Y] A \in (m, n) \to \int_{K}^{L} C d u = \int_{X}^{Y} E B d x)$
217	144 216	sylbid	$⊢ (φ \land (m \in (Z, W) \land n \in (Z, W))) \to (\forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \in (m, n) \to \int_{K}^{L} C d u = \int_{X}^{Y} E B d x)$
218	129 217	sylbid	$⊢ (φ \land (m \in (Z, W) \land n \in (Z, W))) \to (\forall z \in [X, Y] (m < (x \in [X, Y] ⟼ A) (z) \land (x \in [X, Y] ⟼ A) (z) < n) \to \int_{K}^{L} C d u = \int_{X}^{Y} E B d x)$
219	117 218	syl5bir	$⊢ (φ \land (m \in (Z, W) \land n \in (Z, W))) \to ((\forall z \in [X, Y] m < (x \in [X, Y] ⟼ A) (z) \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) < n) \to \int_{K}^{L} C d u = \int_{X}^{Y} E B d x)$
220	219	rexlimdvva	$⊢ φ \to (\exists m \in (Z, W) \exists n \in (Z, W) (\forall z \in [X, Y] m < (x \in [X, Y] ⟼ A) (z) \land \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) < n) \to \int_{K}^{L} C d u = \int_{X}^{Y} E B d x)$
221	116 220	syl5bi	$⊢ φ \to ((\exists n \in (Z, W) \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) < n \land \exists m \in (Z, W) \forall z \in [X, Y] m < (x \in [X, Y] ⟼ A) (z)) \to \int_{K}^{L} C d u = \int_{X}^{Y} E B d x)$
222	68 113 221	syl2and	$⊢ φ \to ((\exists y \in [X, Y] \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (z) \leq (x \in [X, Y] ⟼ A) (y) \land \exists y \in [X, Y] \forall z \in [X, Y] (x \in [X, Y] ⟼ A) (y) \leq (x \in [X, Y] ⟼ A) (z)) \to \int_{K}^{L} C d u = \int_{X}^{Y} E B d x)$
223	18 222	mpd	$⊢ φ \to \int_{K}^{L} C d u = \int_{X}^{Y} E B d x$

Metamath Proof Explorer

Theorem itgsubst

Proof