Metamath Proof Explorer

Theorem ftc2re

Description: The Fundamental Theorem of Calculus, part two, for functions continuous on D . (Contributed by Thierry Arnoux, 1-Dec-2021)

Ref Expression
Hypotheses ftc2re.e 
|- E = ( C (,) D )
ftc2re.a 
|- ( ph -> A e. E )
ftc2re.b 
|- ( ph -> B e. E )
ftc2re.le 
|- ( ph -> A <_ B )
ftc2re.f 
|- ( ph -> F : E --> CC )
ftc2re.1 
|- ( ph -> ( RR _D F ) e. ( E -cn-> CC ) )
Assertion ftc2re 
|- ( ph -> S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t = ( ( F ` B ) - ( F ` A ) ) )

Proof

Step Hyp Ref Expression
1 ftc2re.e 
 |-  E = ( C (,) D )
2 ftc2re.a 
 |-  ( ph -> A e. E )
3 ftc2re.b 
 |-  ( ph -> B e. E )
4 ftc2re.le 
 |-  ( ph -> A <_ B )
5 ftc2re.f 
 |-  ( ph -> F : E --> CC )
6 ftc2re.1 
 |-  ( ph -> ( RR _D F ) e. ( E -cn-> CC ) )
7 ioossre 
 |-  ( C (,) D ) C_ RR
8 1 7 eqsstri 
 |-  E C_ RR
9 8 a1i 
 |-  ( ph -> E C_ RR )
10 9 2 sseldd 
 |-  ( ph -> A e. RR )
11 9 3 sseldd 
 |-  ( ph -> B e. RR )
12 ax-resscn 
 |-  RR C_ CC
13 12 a1i 
 |-  ( ph -> RR C_ CC )
14 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
15 10 11 14 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
16 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
17 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
18 16 17 dvres 
 |-  ( ( ( RR C_ CC /\ F : E --> CC ) /\ ( E C_ RR /\ ( A [,] B ) C_ RR ) ) -> ( RR _D ( F |` ( A [,] B ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) ) )
19 13 5 9 15 18 syl22anc 
 |-  ( ph -> ( RR _D ( F |` ( A [,] B ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) ) )
20 iccntr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
21 10 11 20 syl2anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
22 21 reseq2d 
 |-  ( ph -> ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) ) = ( ( RR _D F ) |` ( A (,) B ) ) )
23 19 22 eqtrd 
 |-  ( ph -> ( RR _D ( F |` ( A [,] B ) ) ) = ( ( RR _D F ) |` ( A (,) B ) ) )
24 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
25 24 a1i 
 |-  ( ph -> ( A (,) B ) C_ ( A [,] B ) )
26 1 2 3 fct2relem 
 |-  ( ph -> ( A [,] B ) C_ E )
27 25 26 sstrd 
 |-  ( ph -> ( A (,) B ) C_ E )
28 rescncf 
 |-  ( ( A (,) B ) C_ E -> ( ( RR _D F ) e. ( E -cn-> CC ) -> ( ( RR _D F ) |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) ) )
29 27 6 28 sylc 
 |-  ( ph -> ( ( RR _D F ) |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) )
30 23 29 eqeltrd 
 |-  ( ph -> ( RR _D ( F |` ( A [,] B ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
31 ioombl 
 |-  ( A (,) B ) e. dom vol
32 31 a1i 
 |-  ( ph -> ( A (,) B ) e. dom vol )
33 cnmbf 
 |-  ( ( ( A (,) B ) e. dom vol /\ ( ( RR _D F ) |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) ) -> ( ( RR _D F ) |` ( A (,) B ) ) e. MblFn )
34 32 29 33 syl2anc 
 |-  ( ph -> ( ( RR _D F ) |` ( A (,) B ) ) e. MblFn )
35 dmres 
 |-  dom ( ( RR _D F ) |` ( A (,) B ) ) = ( ( A (,) B ) i^i dom ( RR _D F ) )
36 35 fveq2i 
 |-  ( vol ` dom ( ( RR _D F ) |` ( A (,) B ) ) ) = ( vol ` ( ( A (,) B ) i^i dom ( RR _D F ) ) )
37 cncff 
 |-  ( ( RR _D F ) e. ( E -cn-> CC ) -> ( RR _D F ) : E --> CC )
38 6 37 syl 
 |-  ( ph -> ( RR _D F ) : E --> CC )
39 38 fdmd 
 |-  ( ph -> dom ( RR _D F ) = E )
40 39 ineq2d 
 |-  ( ph -> ( ( A (,) B ) i^i dom ( RR _D F ) ) = ( ( A (,) B ) i^i E ) )
41 dfss2 
 |-  ( ( A (,) B ) C_ E <-> ( ( A (,) B ) i^i E ) = ( A (,) B ) )
42 27 41 sylib 
 |-  ( ph -> ( ( A (,) B ) i^i E ) = ( A (,) B ) )
43 40 42 eqtrd 
 |-  ( ph -> ( ( A (,) B ) i^i dom ( RR _D F ) ) = ( A (,) B ) )
44 43 fveq2d 
 |-  ( ph -> ( vol ` ( ( A (,) B ) i^i dom ( RR _D F ) ) ) = ( vol ` ( A (,) B ) ) )
45 volioo 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol ` ( A (,) B ) ) = ( B - A ) )
46 10 11 4 45 syl3anc 
 |-  ( ph -> ( vol ` ( A (,) B ) ) = ( B - A ) )
47 11 10 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
48 46 47 eqeltrd 
 |-  ( ph -> ( vol ` ( A (,) B ) ) e. RR )
49 44 48 eqeltrd 
 |-  ( ph -> ( vol ` ( ( A (,) B ) i^i dom ( RR _D F ) ) ) e. RR )
50 36 49 eqeltrid 
 |-  ( ph -> ( vol ` dom ( ( RR _D F ) |` ( A (,) B ) ) ) e. RR )
51 rescncf 
 |-  ( ( A [,] B ) C_ E -> ( ( RR _D F ) e. ( E -cn-> CC ) -> ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) )
52 26 51 syl 
 |-  ( ph -> ( ( RR _D F ) e. ( E -cn-> CC ) -> ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) )
53 6 52 mpd 
 |-  ( ph -> ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
54 cniccbdd 
 |-  ( ( A e. RR /\ B e. RR /\ ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` y ) ) <_ x )
55 10 11 53 54 syl3anc 
 |-  ( ph -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` y ) ) <_ x )
56 35 43 eqtrid 
 |-  ( ph -> dom ( ( RR _D F ) |` ( A (,) B ) ) = ( A (,) B ) )
57 56 25 eqsstrd 
 |-  ( ph -> dom ( ( RR _D F ) |` ( A (,) B ) ) C_ ( A [,] B ) )
58 ssralv 
 |-  ( dom ( ( RR _D F ) |` ( A (,) B ) ) C_ ( A [,] B ) -> ( A. y e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` y ) ) <_ x -> A. y e. dom ( ( RR _D F ) |` ( A (,) B ) ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` y ) ) <_ x ) )
59 57 58 syl 
 |-  ( ph -> ( A. y e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` y ) ) <_ x -> A. y e. dom ( ( RR _D F ) |` ( A (,) B ) ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` y ) ) <_ x ) )
60 59 adantr 
 |-  ( ( ph /\ x e. RR ) -> ( A. y e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` y ) ) <_ x -> A. y e. dom ( ( RR _D F ) |` ( A (,) B ) ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` y ) ) <_ x ) )
61 57 adantr 
 |-  ( ( ph /\ x e. RR ) -> dom ( ( RR _D F ) |` ( A (,) B ) ) C_ ( A [,] B ) )
62 61 sselda 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. dom ( ( RR _D F ) |` ( A (,) B ) ) ) -> y e. ( A [,] B ) )
63 fvres 
 |-  ( y e. ( A [,] B ) -> ( ( ( RR _D F ) |` ( A [,] B ) ) ` y ) = ( ( RR _D F ) ` y ) )
64 62 63 syl 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. dom ( ( RR _D F ) |` ( A (,) B ) ) ) -> ( ( ( RR _D F ) |` ( A [,] B ) ) ` y ) = ( ( RR _D F ) ` y ) )
65 simpr 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. dom ( ( RR _D F ) |` ( A (,) B ) ) ) -> y e. dom ( ( RR _D F ) |` ( A (,) B ) ) )
66 56 ad2antrr 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. dom ( ( RR _D F ) |` ( A (,) B ) ) ) -> dom ( ( RR _D F ) |` ( A (,) B ) ) = ( A (,) B ) )
67 65 66 eleqtrd 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. dom ( ( RR _D F ) |` ( A (,) B ) ) ) -> y e. ( A (,) B ) )
68 fvres 
 |-  ( y e. ( A (,) B ) -> ( ( ( RR _D F ) |` ( A (,) B ) ) ` y ) = ( ( RR _D F ) ` y ) )
69 67 68 syl 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. dom ( ( RR _D F ) |` ( A (,) B ) ) ) -> ( ( ( RR _D F ) |` ( A (,) B ) ) ` y ) = ( ( RR _D F ) ` y ) )
70 64 69 eqtr4d 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. dom ( ( RR _D F ) |` ( A (,) B ) ) ) -> ( ( ( RR _D F ) |` ( A [,] B ) ) ` y ) = ( ( ( RR _D F ) |` ( A (,) B ) ) ` y ) )
71 70 fveq2d 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. dom ( ( RR _D F ) |` ( A (,) B ) ) ) -> ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` y ) ) = ( abs ` ( ( ( RR _D F ) |` ( A (,) B ) ) ` y ) ) )
72 71 breq1d 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. dom ( ( RR _D F ) |` ( A (,) B ) ) ) -> ( ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` y ) ) <_ x <-> ( abs ` ( ( ( RR _D F ) |` ( A (,) B ) ) ` y ) ) <_ x ) )
73 72 biimpd 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. dom ( ( RR _D F ) |` ( A (,) B ) ) ) -> ( ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` y ) ) <_ x -> ( abs ` ( ( ( RR _D F ) |` ( A (,) B ) ) ` y ) ) <_ x ) )
74 73 ralimdva 
 |-  ( ( ph /\ x e. RR ) -> ( A. y e. dom ( ( RR _D F ) |` ( A (,) B ) ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` y ) ) <_ x -> A. y e. dom ( ( RR _D F ) |` ( A (,) B ) ) ( abs ` ( ( ( RR _D F ) |` ( A (,) B ) ) ` y ) ) <_ x ) )
75 60 74 syld 
 |-  ( ( ph /\ x e. RR ) -> ( A. y e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` y ) ) <_ x -> A. y e. dom ( ( RR _D F ) |` ( A (,) B ) ) ( abs ` ( ( ( RR _D F ) |` ( A (,) B ) ) ` y ) ) <_ x ) )
76 75 reximdva 
 |-  ( ph -> ( E. x e. RR A. y e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` y ) ) <_ x -> E. x e. RR A. y e. dom ( ( RR _D F ) |` ( A (,) B ) ) ( abs ` ( ( ( RR _D F ) |` ( A (,) B ) ) ` y ) ) <_ x ) )
77 55 76 mpd 
 |-  ( ph -> E. x e. RR A. y e. dom ( ( RR _D F ) |` ( A (,) B ) ) ( abs ` ( ( ( RR _D F ) |` ( A (,) B ) ) ` y ) ) <_ x )
78 bddibl 
 |-  ( ( ( ( RR _D F ) |` ( A (,) B ) ) e. MblFn /\ ( vol ` dom ( ( RR _D F ) |` ( A (,) B ) ) ) e. RR /\ E. x e. RR A. y e. dom ( ( RR _D F ) |` ( A (,) B ) ) ( abs ` ( ( ( RR _D F ) |` ( A (,) B ) ) ` y ) ) <_ x ) -> ( ( RR _D F ) |` ( A (,) B ) ) e. L^1 )
79 34 50 77 78 syl3anc 
 |-  ( ph -> ( ( RR _D F ) |` ( A (,) B ) ) e. L^1 )
80 23 79 eqeltrd 
 |-  ( ph -> ( RR _D ( F |` ( A [,] B ) ) ) e. L^1 )
81 dvcn 
 |-  ( ( ( RR C_ CC /\ F : E --> CC /\ E C_ RR ) /\ dom ( RR _D F ) = E ) -> F e. ( E -cn-> CC ) )
82 13 5 9 39 81 syl31anc 
 |-  ( ph -> F e. ( E -cn-> CC ) )
83 rescncf 
 |-  ( ( A [,] B ) C_ E -> ( F e. ( E -cn-> CC ) -> ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) )
84 26 83 syl 
 |-  ( ph -> ( F e. ( E -cn-> CC ) -> ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) )
85 82 84 mpd 
 |-  ( ph -> ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
86 10 11 4 30 80 85 ftc2 
 |-  ( ph -> S. ( A (,) B ) ( ( RR _D ( F |` ( A [,] B ) ) ) ` t ) _d t = ( ( ( F |` ( A [,] B ) ) ` B ) - ( ( F |` ( A [,] B ) ) ` A ) ) )
87 23 fveq1d 
 |-  ( ph -> ( ( RR _D ( F |` ( A [,] B ) ) ) ` t ) = ( ( ( RR _D F ) |` ( A (,) B ) ) ` t ) )
88 fvres 
 |-  ( t e. ( A (,) B ) -> ( ( ( RR _D F ) |` ( A (,) B ) ) ` t ) = ( ( RR _D F ) ` t ) )
89 87 88 sylan9eq 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> ( ( RR _D ( F |` ( A [,] B ) ) ) ` t ) = ( ( RR _D F ) ` t ) )
90 89 ralrimiva 
 |-  ( ph -> A. t e. ( A (,) B ) ( ( RR _D ( F |` ( A [,] B ) ) ) ` t ) = ( ( RR _D F ) ` t ) )
91 itgeq2 
 |-  ( A. t e. ( A (,) B ) ( ( RR _D ( F |` ( A [,] B ) ) ) ` t ) = ( ( RR _D F ) ` t ) -> S. ( A (,) B ) ( ( RR _D ( F |` ( A [,] B ) ) ) ` t ) _d t = S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t )
92 90 91 syl 
 |-  ( ph -> S. ( A (,) B ) ( ( RR _D ( F |` ( A [,] B ) ) ) ` t ) _d t = S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t )
93 10 rexrd 
 |-  ( ph -> A e. RR* )
94 11 rexrd 
 |-  ( ph -> B e. RR* )
95 ubicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
96 93 94 4 95 syl3anc 
 |-  ( ph -> B e. ( A [,] B ) )
97 96 fvresd 
 |-  ( ph -> ( ( F |` ( A [,] B ) ) ` B ) = ( F ` B ) )
98 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
99 93 94 4 98 syl3anc 
 |-  ( ph -> A e. ( A [,] B ) )
100 99 fvresd 
 |-  ( ph -> ( ( F |` ( A [,] B ) ) ` A ) = ( F ` A ) )
101 97 100 oveq12d 
 |-  ( ph -> ( ( ( F |` ( A [,] B ) ) ` B ) - ( ( F |` ( A [,] B ) ) ` A ) ) = ( ( F ` B ) - ( F ` A ) ) )
102 86 92 101 3eqtr3d 
 |-  ( ph -> S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t = ( ( F ` B ) - ( F ` A ) ) )