Metamath Proof Explorer

Theorem ftc2

Description: The Fundamental Theorem of Calculus, part two. If F is a function continuous on [ A , B ] and continuously differentiable on ( A , B ) , then the integral of the derivative of F is equal to F ( B ) - F ( A ) . This is part of Metamath 100 proof #15. (Contributed by Mario Carneiro, 2-Sep-2014)

Ref Expression
Hypotheses ftc2.a 
|- ( ph -> A e. RR )
ftc2.b 
|- ( ph -> B e. RR )
ftc2.le 
|- ( ph -> A <_ B )
ftc2.c 
|- ( ph -> ( RR _D F ) e. ( ( A (,) B ) -cn-> CC ) )
ftc2.i 
|- ( ph -> ( RR _D F ) e. L^1 )
ftc2.f 
|- ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )
Assertion ftc2 
|- ( ph -> S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t = ( ( F ` B ) - ( F ` A ) ) )

Proof

Step Hyp Ref Expression
1 ftc2.a 
 |-  ( ph -> A e. RR )
2 ftc2.b 
 |-  ( ph -> B e. RR )
3 ftc2.le 
 |-  ( ph -> A <_ B )
4 ftc2.c 
 |-  ( ph -> ( RR _D F ) e. ( ( A (,) B ) -cn-> CC ) )
5 ftc2.i 
 |-  ( ph -> ( RR _D F ) e. L^1 )
6 ftc2.f 
 |-  ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )
7 1 rexrd 
 |-  ( ph -> A e. RR* )
8 2 rexrd 
 |-  ( ph -> B e. RR* )
9 ubicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
10 7 8 3 9 syl3anc 
 |-  ( ph -> B e. ( A [,] B ) )
11 fvex 
 |-  ( ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) e. _V
12 11 fvconst2 
 |-  ( B e. ( A [,] B ) -> ( ( ( A [,] B ) X. { ( ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) } ) ` B ) = ( ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) )
13 10 12 syl 
 |-  ( ph -> ( ( ( A [,] B ) X. { ( ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) } ) ` B ) = ( ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) )
14 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
15 14 subcn 
 |-  - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
16 15 a1i 
 |-  ( ph -> - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
17 eqid 
 |-  ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t ) = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t )
18 ssidd 
 |-  ( ph -> ( A (,) B ) C_ ( A (,) B ) )
19 ioossre 
 |-  ( A (,) B ) C_ RR
20 19 a1i 
 |-  ( ph -> ( A (,) B ) C_ RR )
21 cncff 
 |-  ( ( RR _D F ) e. ( ( A (,) B ) -cn-> CC ) -> ( RR _D F ) : ( A (,) B ) --> CC )
22 4 21 syl 
 |-  ( ph -> ( RR _D F ) : ( A (,) B ) --> CC )
23 17 1 2 3 18 20 5 22 ftc1a 
 |-  ( ph -> ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t ) e. ( ( A [,] B ) -cn-> CC ) )
24 cncff 
 |-  ( F e. ( ( A [,] B ) -cn-> CC ) -> F : ( A [,] B ) --> CC )
25 6 24 syl 
 |-  ( ph -> F : ( A [,] B ) --> CC )
26 25 feqmptd 
 |-  ( ph -> F = ( x e. ( A [,] B ) |-> ( F ` x ) ) )
27 26 6 eqeltrrd 
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( F ` x ) ) e. ( ( A [,] B ) -cn-> CC ) )
28 14 16 23 27 cncfmpt2f 
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
29 ax-resscn 
 |-  RR C_ CC
30 29 a1i 
 |-  ( ph -> RR C_ CC )
31 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
32 1 2 31 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
33 fvex 
 |-  ( ( RR _D F ) ` t ) e. _V
34 33 a1i 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ t e. ( A (,) x ) ) -> ( ( RR _D F ) ` t ) e. _V )
35 2 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> B e. RR )
36 35 rexrd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> B e. RR* )
37 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
38 1 2 37 syl2anc 
 |-  ( ph -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
39 38 biimpa 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( x e. RR /\ A <_ x /\ x <_ B ) )
40 39 simp3d 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x <_ B )
41 iooss2 
 |-  ( ( B e. RR* /\ x <_ B ) -> ( A (,) x ) C_ ( A (,) B ) )
42 36 40 41 syl2anc 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( A (,) x ) C_ ( A (,) B ) )
43 ioombl 
 |-  ( A (,) x ) e. dom vol
44 43 a1i 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( A (,) x ) e. dom vol )
45 33 a1i 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ t e. ( A (,) B ) ) -> ( ( RR _D F ) ` t ) e. _V )
46 22 feqmptd 
 |-  ( ph -> ( RR _D F ) = ( t e. ( A (,) B ) |-> ( ( RR _D F ) ` t ) ) )
47 46 5 eqeltrrd 
 |-  ( ph -> ( t e. ( A (,) B ) |-> ( ( RR _D F ) ` t ) ) e. L^1 )
48 47 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( t e. ( A (,) B ) |-> ( ( RR _D F ) ` t ) ) e. L^1 )
49 42 44 45 48 iblss 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( t e. ( A (,) x ) |-> ( ( RR _D F ) ` t ) ) e. L^1 )
50 34 49 itgcl 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t e. CC )
51 25 ffvelrnda 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. CC )
52 50 51 subcld 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) e. CC )
53 14 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
54 iccntr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
55 1 2 54 syl2anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
56 30 32 52 53 14 55 dvmptntr 
 |-  ( ph -> ( RR _D ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ) = ( RR _D ( x e. ( A (,) B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ) )
57 reelprrecn 
 |-  RR e. { RR , CC }
58 57 a1i 
 |-  ( ph -> RR e. { RR , CC } )
59 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
60 59 sseli 
 |-  ( x e. ( A (,) B ) -> x e. ( A [,] B ) )
61 60 50 sylan2 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t e. CC )
62 22 ffvelrnda 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. CC )
63 17 1 2 3 4 5 ftc1cn 
 |-  ( ph -> ( RR _D ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t ) ) = ( RR _D F ) )
64 30 32 50 53 14 55 dvmptntr 
 |-  ( ph -> ( RR _D ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t ) ) = ( RR _D ( x e. ( A (,) B ) |-> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t ) ) )
65 22 feqmptd 
 |-  ( ph -> ( RR _D F ) = ( x e. ( A (,) B ) |-> ( ( RR _D F ) ` x ) ) )
66 63 64 65 3eqtr3d 
 |-  ( ph -> ( RR _D ( x e. ( A (,) B ) |-> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t ) ) = ( x e. ( A (,) B ) |-> ( ( RR _D F ) ` x ) ) )
67 60 51 sylan2 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( F ` x ) e. CC )
68 30 32 51 53 14 55 dvmptntr 
 |-  ( ph -> ( RR _D ( x e. ( A [,] B ) |-> ( F ` x ) ) ) = ( RR _D ( x e. ( A (,) B ) |-> ( F ` x ) ) ) )
69 26 oveq2d 
 |-  ( ph -> ( RR _D F ) = ( RR _D ( x e. ( A [,] B ) |-> ( F ` x ) ) ) )
70 69 65 eqtr3d 
 |-  ( ph -> ( RR _D ( x e. ( A [,] B ) |-> ( F ` x ) ) ) = ( x e. ( A (,) B ) |-> ( ( RR _D F ) ` x ) ) )
71 68 70 eqtr3d 
 |-  ( ph -> ( RR _D ( x e. ( A (,) B ) |-> ( F ` x ) ) ) = ( x e. ( A (,) B ) |-> ( ( RR _D F ) ` x ) ) )
72 58 61 62 66 67 62 71 dvmptsub 
 |-  ( ph -> ( RR _D ( x e. ( A (,) B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ) = ( x e. ( A (,) B ) |-> ( ( ( RR _D F ) ` x ) - ( ( RR _D F ) ` x ) ) ) )
73 62 subidd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( RR _D F ) ` x ) - ( ( RR _D F ) ` x ) ) = 0 )
74 73 mpteq2dva 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( ( ( RR _D F ) ` x ) - ( ( RR _D F ) ` x ) ) ) = ( x e. ( A (,) B ) |-> 0 ) )
75 56 72 74 3eqtrd 
 |-  ( ph -> ( RR _D ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ) = ( x e. ( A (,) B ) |-> 0 ) )
76 fconstmpt 
 |-  ( ( A (,) B ) X. { 0 } ) = ( x e. ( A (,) B ) |-> 0 )
77 75 76 eqtr4di 
 |-  ( ph -> ( RR _D ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ) = ( ( A (,) B ) X. { 0 } ) )
78 1 2 28 77 dveq0 
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) = ( ( A [,] B ) X. { ( ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) } ) )
79 78 fveq1d 
 |-  ( ph -> ( ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` B ) = ( ( ( A [,] B ) X. { ( ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) } ) ` B ) )
80 oveq2 
 |-  ( x = B -> ( A (,) x ) = ( A (,) B ) )
81 itgeq1 
 |-  ( ( A (,) x ) = ( A (,) B ) -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t = S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t )
82 80 81 syl 
 |-  ( x = B -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t = S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t )
83 fveq2 
 |-  ( x = B -> ( F ` x ) = ( F ` B ) )
84 82 83 oveq12d 
 |-  ( x = B -> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) = ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) )
85 eqid 
 |-  ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) = ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) )
86 ovex 
 |-  ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) e. _V
87 84 85 86 fvmpt 
 |-  ( B e. ( A [,] B ) -> ( ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` B ) = ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) )
88 10 87 syl 
 |-  ( ph -> ( ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` B ) = ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) )
89 79 88 eqtr3d 
 |-  ( ph -> ( ( ( A [,] B ) X. { ( ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) } ) ` B ) = ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) )
90 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
91 7 8 3 90 syl3anc 
 |-  ( ph -> A e. ( A [,] B ) )
92 oveq2 
 |-  ( x = A -> ( A (,) x ) = ( A (,) A ) )
93 iooid 
 |-  ( A (,) A ) = (/)
94 92 93 eqtrdi 
 |-  ( x = A -> ( A (,) x ) = (/) )
95 itgeq1 
 |-  ( ( A (,) x ) = (/) -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t = S. (/) ( ( RR _D F ) ` t ) _d t )
96 94 95 syl 
 |-  ( x = A -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t = S. (/) ( ( RR _D F ) ` t ) _d t )
97 itg0 
 |-  S. (/) ( ( RR _D F ) ` t ) _d t = 0
98 96 97 eqtrdi 
 |-  ( x = A -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t = 0 )
99 fveq2 
 |-  ( x = A -> ( F ` x ) = ( F ` A ) )
100 98 99 oveq12d 
 |-  ( x = A -> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) = ( 0 - ( F ` A ) ) )
101 df-neg 
 |-  -u ( F ` A ) = ( 0 - ( F ` A ) )
102 100 101 eqtr4di 
 |-  ( x = A -> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) = -u ( F ` A ) )
103 negex 
 |-  -u ( F ` A ) e. _V
104 102 85 103 fvmpt 
 |-  ( A e. ( A [,] B ) -> ( ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) = -u ( F ` A ) )
105 91 104 syl 
 |-  ( ph -> ( ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) = -u ( F ` A ) )
106 13 89 105 3eqtr3d 
 |-  ( ph -> ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) = -u ( F ` A ) )
107 106 oveq2d 
 |-  ( ph -> ( ( F ` B ) + ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) ) = ( ( F ` B ) + -u ( F ` A ) ) )
108 25 10 ffvelrnd 
 |-  ( ph -> ( F ` B ) e. CC )
109 33 a1i 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> ( ( RR _D F ) ` t ) e. _V )
110 109 47 itgcl 
 |-  ( ph -> S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t e. CC )
111 108 110 pncan3d 
 |-  ( ph -> ( ( F ` B ) + ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) ) = S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t )
112 25 91 ffvelrnd 
 |-  ( ph -> ( F ` A ) e. CC )
113 108 112 negsubd 
 |-  ( ph -> ( ( F ` B ) + -u ( F ` A ) ) = ( ( F ` B ) - ( F ` A ) ) )
114 107 111 113 3eqtr3d 
 |-  ( ph -> S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t = ( ( F ` B ) - ( F ` A ) ) )