itgparts

Description: Integration by parts. If B ( x ) is the derivative of A ( x ) and D ( x ) is the derivative of C ( x ) , and E = ( A x. B ) ( X ) and F = ( A x. B ) ( Y ) , then under suitable integrability and differentiability assumptions, the integral of A x. D from X to Y is equal to F - E minus the integral of B x. C . (Contributed by Mario Carneiro, 3-Sep-2014)

	Ref	Expression
Hypotheses	itgparts.x	$⊢ φ \to X \in ℝ$
	itgparts.y	$⊢ φ \to Y \in ℝ$
	itgparts.le	$⊢ φ \to X \leq Y$
	itgparts.a	$⊢ φ \to (x \in [X, Y] ⟼ A) : [X, Y] \underset{cn}{⟶} ℂ$
	itgparts.c	$⊢ φ \to (x \in [X, Y] ⟼ C) : [X, Y] \underset{cn}{⟶} ℂ$
	itgparts.b	$⊢ φ \to (x \in (X, Y) ⟼ B) : (X, Y) \underset{cn}{⟶} ℂ$
	itgparts.d	$⊢ φ \to (x \in (X, Y) ⟼ D) : (X, Y) \underset{cn}{⟶} ℂ$
	itgparts.ad	$⊢ φ \to (x \in (X, Y) ⟼ A D) \in 𝐿^{1}$
	itgparts.bc	$⊢ φ \to (x \in (X, Y) ⟼ B C) \in 𝐿^{1}$
	itgparts.da	$⊢ φ \to \frac{d (x \in [X, Y]⟼ A)}{d_{ℝ} x} = (x \in (X, Y) ⟼ B)$
	itgparts.dc	$⊢ φ \to \frac{d (x \in [X, Y]⟼ C)}{d_{ℝ} x} = (x \in (X, Y) ⟼ D)$
	itgparts.e	$⊢ (φ \land x = X) \to A C = E$
	itgparts.f	$⊢ (φ \land x = Y) \to A C = F$
Assertion	itgparts	$⊢ φ \to \int_{(X, Y)} A D d x = F - E - \int_{(X, Y)} B C d x$

Proof

Step	Hyp	Ref	Expression
1		itgparts.x	$⊢ φ \to X \in ℝ$
2		itgparts.y	$⊢ φ \to Y \in ℝ$
3		itgparts.le	$⊢ φ \to X \leq Y$
4		itgparts.a	$⊢ φ \to (x \in [X, Y] ⟼ A) : [X, Y] \underset{cn}{⟶} ℂ$
5		itgparts.c	$⊢ φ \to (x \in [X, Y] ⟼ C) : [X, Y] \underset{cn}{⟶} ℂ$
6		itgparts.b	$⊢ φ \to (x \in (X, Y) ⟼ B) : (X, Y) \underset{cn}{⟶} ℂ$
7		itgparts.d	$⊢ φ \to (x \in (X, Y) ⟼ D) : (X, Y) \underset{cn}{⟶} ℂ$
8		itgparts.ad	$⊢ φ \to (x \in (X, Y) ⟼ A D) \in 𝐿^{1}$
9		itgparts.bc	$⊢ φ \to (x \in (X, Y) ⟼ B C) \in 𝐿^{1}$
10		itgparts.da	$⊢ φ \to \frac{d (x \in [X, Y]⟼ A)}{d_{ℝ} x} = (x \in (X, Y) ⟼ B)$
11		itgparts.dc	$⊢ φ \to \frac{d (x \in [X, Y]⟼ C)}{d_{ℝ} x} = (x \in (X, Y) ⟼ D)$
12		itgparts.e	$⊢ (φ \land x = X) \to A C = E$
13		itgparts.f	$⊢ (φ \land x = Y) \to A C = F$
14		cncff	$⊢ (x \in (X, Y) ⟼ B) : (X, Y) \underset{cn}{⟶} ℂ \to (x \in (X, Y) ⟼ B) : (X, Y) ⟶ ℂ$
15	6 14	syl	$⊢ φ \to (x \in (X, Y) ⟼ B) : (X, Y) ⟶ ℂ$
16	15	fvmptelrn	$⊢ (φ \land x \in (X, Y)) \to B \in ℂ$
17		ioossicc	$⊢ (X, Y) \subseteq [X, Y]$
18	17	sseli	$⊢ x \in (X, Y) \to x \in [X, Y]$
19		cncff	$⊢ (x \in [X, Y] ⟼ C) : [X, Y] \underset{cn}{⟶} ℂ \to (x \in [X, Y] ⟼ C) : [X, Y] ⟶ ℂ$
20	5 19	syl	$⊢ φ \to (x \in [X, Y] ⟼ C) : [X, Y] ⟶ ℂ$
21	20	fvmptelrn	$⊢ (φ \land x \in [X, Y]) \to C \in ℂ$
22	18 21	sylan2	$⊢ (φ \land x \in (X, Y)) \to C \in ℂ$
23	16 22	mulcld	$⊢ (φ \land x \in (X, Y)) \to B C \in ℂ$
24	23 9	itgcl	$⊢ φ \to \int_{(X, Y)} B C d x \in ℂ$
25		cncff	$⊢ (x \in [X, Y] ⟼ A) : [X, Y] \underset{cn}{⟶} ℂ \to (x \in [X, Y] ⟼ A) : [X, Y] ⟶ ℂ$
26	4 25	syl	$⊢ φ \to (x \in [X, Y] ⟼ A) : [X, Y] ⟶ ℂ$
27	26	fvmptelrn	$⊢ (φ \land x \in [X, Y]) \to A \in ℂ$
28	18 27	sylan2	$⊢ (φ \land x \in (X, Y)) \to A \in ℂ$
29		cncff	$⊢ (x \in (X, Y) ⟼ D) : (X, Y) \underset{cn}{⟶} ℂ \to (x \in (X, Y) ⟼ D) : (X, Y) ⟶ ℂ$
30	7 29	syl	$⊢ φ \to (x \in (X, Y) ⟼ D) : (X, Y) ⟶ ℂ$
31	30	fvmptelrn	$⊢ (φ \land x \in (X, Y)) \to D \in ℂ$
32	28 31	mulcld	$⊢ (φ \land x \in (X, Y)) \to A D \in ℂ$
33	32 8	itgcl	$⊢ φ \to \int_{(X, Y)} A D d x \in ℂ$
34	24 33	pncan2d	$⊢ φ \to \int_{(X, Y)} B C d x + \int_{(X, Y)} A D d x - \int_{(X, Y)} B C d x = \int_{(X, Y)} A D d x$
35	23 9 32 8	itgadd	$⊢ φ \to \int_{(X, Y)} (B C + A D) d x = \int_{(X, Y)} B C d x + \int_{(X, Y)} A D d x$
36		fveq2	$⊢ x = t \to \frac{d (x \in [X, Y]⟼ A C)}{d_{ℝ} x} (x) = \frac{d (x \in [X, Y]⟼ A C)}{d_{ℝ} x} (t)$
37		nfcv	$⊢ \underline{Ⅎ} t \frac{d (x \in [X, Y]⟼ A C)}{d_{ℝ} x} (x)$
38		nfcv	$⊢ \underline{Ⅎ} x ℝ$
39		nfcv	$⊢ \underline{Ⅎ} x D$
40		nfmpt1	$⊢ \underline{Ⅎ} x (x \in [X, Y] ⟼ A C)$
41	38 39 40	nfov	$⊢ \underline{Ⅎ} x \frac{d (x \in [X, Y]⟼ A C)}{d_{ℝ} x}$
42		nfcv	$⊢ \underline{Ⅎ} x t$
43	41 42	nffv	$⊢ \underline{Ⅎ} x \frac{d (x \in [X, Y]⟼ A C)}{d_{ℝ} x} (t)$
44	36 37 43	cbvitg	$⊢ \int_{(X, Y)} \frac{d (x \in [X, Y]⟼ A C)}{d_{ℝ} x} (x) d x = \int_{(X, Y)} \frac{d (x \in [X, Y]⟼ A C)}{d_{ℝ} x} (t) d t$
45		ax-resscn	$⊢ ℝ \subseteq ℂ$
46	45	a1i	$⊢ φ \to ℝ \subseteq ℂ$
47		iccssre	$⊢ (X \in ℝ \land Y \in ℝ) \to [X, Y] \subseteq ℝ$
48	1 2 47	syl2anc	$⊢ φ \to [X, Y] \subseteq ℝ$
49	27 21	mulcld	$⊢ (φ \land x \in [X, Y]) \to A C \in ℂ$
50		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
51	50	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
52		iccntr	$⊢ (X \in ℝ \land Y \in ℝ) \to int (topGen (ran (.))) ([X, Y]) = (X, Y)$
53	1 2 52	syl2anc	$⊢ φ \to int (topGen (ran (.))) ([X, Y]) = (X, Y)$
54	46 48 49 51 50 53	dvmptntr	$⊢ φ \to \frac{d (x \in [X, Y]⟼ A C)}{d_{ℝ} x} = \frac{d (x \in (X, Y)⟼ A C)}{d_{ℝ} x}$
55		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
56	55	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
57	46 48 27 51 50 53	dvmptntr	$⊢ φ \to \frac{d (x \in [X, Y]⟼ A)}{d_{ℝ} x} = \frac{d (x \in (X, Y)⟼ A)}{d_{ℝ} x}$
58	57 10	eqtr3d	$⊢ φ \to \frac{d (x \in (X, Y)⟼ A)}{d_{ℝ} x} = (x \in (X, Y) ⟼ B)$
59	46 48 21 51 50 53	dvmptntr	$⊢ φ \to \frac{d (x \in [X, Y]⟼ C)}{d_{ℝ} x} = \frac{d (x \in (X, Y)⟼ C)}{d_{ℝ} x}$
60	59 11	eqtr3d	$⊢ φ \to \frac{d (x \in (X, Y)⟼ C)}{d_{ℝ} x} = (x \in (X, Y) ⟼ D)$
61	56 28 16 58 22 31 60	dvmptmul	$⊢ φ \to \frac{d (x \in (X, Y)⟼ A C)}{d_{ℝ} x} = (x \in (X, Y) ⟼ B C + D A)$
62	31 28	mulcomd	$⊢ (φ \land x \in (X, Y)) \to D A = A D$
63	62	oveq2d	$⊢ (φ \land x \in (X, Y)) \to B C + D A = B C + A D$
64	63	mpteq2dva	$⊢ φ \to (x \in (X, Y) ⟼ B C + D A) = (x \in (X, Y) ⟼ B C + A D)$
65	54 61 64	3eqtrd	$⊢ φ \to \frac{d (x \in [X, Y]⟼ A C)}{d_{ℝ} x} = (x \in (X, Y) ⟼ B C + A D)$
66	50	addcn	$⊢ + \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
67	66	a1i	$⊢ φ \to + \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
68		resmpt	$⊢ (X, Y) \subseteq [X, Y] \to {(x \in [X, Y] ⟼ C) ↾}_{(X, Y)} = (x \in (X, Y) ⟼ C)$
69	17 68	ax-mp	$⊢ {(x \in [X, Y] ⟼ C) ↾}_{(X, Y)} = (x \in (X, Y) ⟼ C)$
70		rescncf	$⊢ (X, Y) \subseteq [X, Y] \to ((x \in [X, Y] ⟼ C) : [X, Y] \underset{cn}{⟶} ℂ \to ({(x \in [X, Y] ⟼ C) ↾}_{(X, Y)}) : (X, Y) \underset{cn}{⟶} ℂ)$
71	17 5 70	mpsyl	$⊢ φ \to ({(x \in [X, Y] ⟼ C) ↾}_{(X, Y)}) : (X, Y) \underset{cn}{⟶} ℂ$
72	69 71	eqeltrrid	$⊢ φ \to (x \in (X, Y) ⟼ C) : (X, Y) \underset{cn}{⟶} ℂ$
73	6 72	mulcncf	$⊢ φ \to (x \in (X, Y) ⟼ B C) : (X, Y) \underset{cn}{⟶} ℂ$
74		resmpt	$⊢ (X, Y) \subseteq [X, Y] \to {(x \in [X, Y] ⟼ A) ↾}_{(X, Y)} = (x \in (X, Y) ⟼ A)$
75	17 74	ax-mp	$⊢ {(x \in [X, Y] ⟼ A) ↾}_{(X, Y)} = (x \in (X, Y) ⟼ A)$
76		rescncf	$⊢ (X, Y) \subseteq [X, Y] \to ((x \in [X, Y] ⟼ A) : [X, Y] \underset{cn}{⟶} ℂ \to ({(x \in [X, Y] ⟼ A) ↾}_{(X, Y)}) : (X, Y) \underset{cn}{⟶} ℂ)$
77	17 4 76	mpsyl	$⊢ φ \to ({(x \in [X, Y] ⟼ A) ↾}_{(X, Y)}) : (X, Y) \underset{cn}{⟶} ℂ$
78	75 77	eqeltrrid	$⊢ φ \to (x \in (X, Y) ⟼ A) : (X, Y) \underset{cn}{⟶} ℂ$
79	78 7	mulcncf	$⊢ φ \to (x \in (X, Y) ⟼ A D) : (X, Y) \underset{cn}{⟶} ℂ$
80	50 67 73 79	cncfmpt2f	$⊢ φ \to (x \in (X, Y) ⟼ B C + A D) : (X, Y) \underset{cn}{⟶} ℂ$
81	65 80	eqeltrd	$⊢ φ \to \frac{d (x \in [X, Y]⟼ A C)}{d_{ℝ} x} : (X, Y) \underset{cn}{⟶} ℂ$
82	23 9 32 8	ibladd	$⊢ φ \to (x \in (X, Y) ⟼ B C + A D) \in 𝐿^{1}$
83	65 82	eqeltrd	$⊢ φ \to \frac{d (x \in [X, Y]⟼ A C)}{d_{ℝ} x} \in 𝐿^{1}$
84	4 5	mulcncf	$⊢ φ \to (x \in [X, Y] ⟼ A C) : [X, Y] \underset{cn}{⟶} ℂ$
85	1 2 3 81 83 84	ftc2	$⊢ φ \to \int_{(X, Y)} \frac{d (x \in [X, Y]⟼ A C)}{d_{ℝ} x} (t) d t = (x \in [X, Y] ⟼ A C) (Y) - (x \in [X, Y] ⟼ A C) (X)$
86	44 85	syl5eq	$⊢ φ \to \int_{(X, Y)} \frac{d (x \in [X, Y]⟼ A C)}{d_{ℝ} x} (x) d x = (x \in [X, Y] ⟼ A C) (Y) - (x \in [X, Y] ⟼ A C) (X)$
87	65	fveq1d	$⊢ φ \to \frac{d (x \in [X, Y]⟼ A C)}{d_{ℝ} x} (x) = (x \in (X, Y) ⟼ B C + A D) (x)$
88	87	adantr	$⊢ (φ \land x \in (X, Y)) \to \frac{d (x \in [X, Y]⟼ A C)}{d_{ℝ} x} (x) = (x \in (X, Y) ⟼ B C + A D) (x)$
89		simpr	$⊢ (φ \land x \in (X, Y)) \to x \in (X, Y)$
90		ovex	$⊢ B C + A D \in V$
91		eqid	$⊢ (x \in (X, Y) ⟼ B C + A D) = (x \in (X, Y) ⟼ B C + A D)$
92	91	fvmpt2	$⊢ (x \in (X, Y) \land B C + A D \in V) \to (x \in (X, Y) ⟼ B C + A D) (x) = B C + A D$
93	89 90 92	sylancl	$⊢ (φ \land x \in (X, Y)) \to (x \in (X, Y) ⟼ B C + A D) (x) = B C + A D$
94	88 93	eqtrd	$⊢ (φ \land x \in (X, Y)) \to \frac{d (x \in [X, Y]⟼ A C)}{d_{ℝ} x} (x) = B C + A D$
95	94	itgeq2dv	$⊢ φ \to \int_{(X, Y)} \frac{d (x \in [X, Y]⟼ A C)}{d_{ℝ} x} (x) d x = \int_{(X, Y)} (B C + A D) d x$
96	1	rexrd	$⊢ φ \to X \in ℝ^{*}$
97	2	rexrd	$⊢ φ \to Y \in ℝ^{*}$
98		ubicc2	$⊢ (X \in ℝ^{} \land Y \in ℝ^{} \land X \leq Y) \to Y \in [X, Y]$
99	96 97 3 98	syl3anc	$⊢ φ \to Y \in [X, Y]$
100		ovex	$⊢ A C \in V$
101	100	csbex	$⊢ ⦋ Y / x ⦌ A C \in V$
102		eqid	$⊢ (x \in [X, Y] ⟼ A C) = (x \in [X, Y] ⟼ A C)$
103	102	fvmpts	$⊢ (Y \in [X, Y] \land ⦋ Y / x ⦌ A C \in V) \to (x \in [X, Y] ⟼ A C) (Y) = ⦋ Y / x ⦌ A C$
104	99 101 103	sylancl	$⊢ φ \to (x \in [X, Y] ⟼ A C) (Y) = ⦋ Y / x ⦌ A C$
105	2 13	csbied	$⊢ φ \to ⦋ Y / x ⦌ A C = F$
106	104 105	eqtrd	$⊢ φ \to (x \in [X, Y] ⟼ A C) (Y) = F$
107		lbicc2	$⊢ (X \in ℝ^{} \land Y \in ℝ^{} \land X \leq Y) \to X \in [X, Y]$
108	96 97 3 107	syl3anc	$⊢ φ \to X \in [X, Y]$
109	100	csbex	$⊢ ⦋ X / x ⦌ A C \in V$
110	102	fvmpts	$⊢ (X \in [X, Y] \land ⦋ X / x ⦌ A C \in V) \to (x \in [X, Y] ⟼ A C) (X) = ⦋ X / x ⦌ A C$
111	108 109 110	sylancl	$⊢ φ \to (x \in [X, Y] ⟼ A C) (X) = ⦋ X / x ⦌ A C$
112	1 12	csbied	$⊢ φ \to ⦋ X / x ⦌ A C = E$
113	111 112	eqtrd	$⊢ φ \to (x \in [X, Y] ⟼ A C) (X) = E$
114	106 113	oveq12d	$⊢ φ \to (x \in [X, Y] ⟼ A C) (Y) - (x \in [X, Y] ⟼ A C) (X) = F - E$
115	86 95 114	3eqtr3d	$⊢ φ \to \int_{(X, Y)} (B C + A D) d x = F - E$
116	35 115	eqtr3d	$⊢ φ \to \int_{(X, Y)} B C d x + \int_{(X, Y)} A D d x = F - E$
117	116	oveq1d	$⊢ φ \to \int_{(X, Y)} B C d x + \int_{(X, Y)} A D d x - \int_{(X, Y)} B C d x = F - E - \int_{(X, Y)} B C d x$
118	34 117	eqtr3d	$⊢ φ \to \int_{(X, Y)} A D d x = F - E - \int_{(X, Y)} B C d x$

Metamath Proof Explorer

Theorem itgparts

Proof