Metamath Proof Explorer

Theorem 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 fvmptelrn 
 |-  ( ( 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 fvmptelrn 
 |-  ( ( 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 fvmptelrn 
 |-  ( ( 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 fvmptelrn 
 |-  ( ( 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 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
51 50 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
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 51 50 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 51 50 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 51 50 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 50 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 50 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 ) )