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 16 tgioo2
 |-  ( 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 df-ss
 |-  ( ( 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 syl5eq
 |-  ( 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 ) ) )