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	\|- ( ph -> X e. RR )
	itgparts.y	\|- ( ph -> Y e. RR )
	itgparts.le	\|- ( ph -> X <_ Y )
	itgparts.a	\|- ( ph -> ( x e. ( X [,] Y ) \|-> A ) e. ( ( X [,] Y ) -cn-> CC ) )
	itgparts.c	\|- ( ph -> ( x e. ( X [,] Y ) \|-> C ) e. ( ( X [,] Y ) -cn-> CC ) )
	itgparts.b	\|- ( ph -> ( x e. ( X (,) Y ) \|-> B ) e. ( ( X (,) Y ) -cn-> CC ) )
	itgparts.d	\|- ( ph -> ( x e. ( X (,) Y ) \|-> D ) e. ( ( X (,) Y ) -cn-> CC ) )
	itgparts.ad	\|- ( ph -> ( x e. ( X (,) Y ) \|-> ( A x. D ) ) e. L^1 )
	itgparts.bc	\|- ( ph -> ( x e. ( X (,) Y ) \|-> ( B x. C ) ) e. L^1 )
	itgparts.da	\|- ( ph -> ( RR _D ( x e. ( X [,] Y ) \|-> A ) ) = ( x e. ( X (,) Y ) \|-> B ) )
	itgparts.dc	\|- ( ph -> ( RR _D ( x e. ( X [,] Y ) \|-> C ) ) = ( x e. ( X (,) Y ) \|-> D ) )
	itgparts.e	\|- ( ( ph /\ x = X ) -> ( A x. C ) = E )
	itgparts.f	\|- ( ( ph /\ x = Y ) -> ( A x. C ) = F )
Assertion	itgparts	\|- ( ph -> S. ( X (,) Y ) ( A x. D ) _d x = ( ( F - E ) - S. ( X (,) Y ) ( B x. C ) _d x ) )

Proof

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

Metamath Proof Explorer

Theorem itgparts

Proof