Metamath Proof Explorer


Theorem ftc2nc

Description: Choice-free proof of ftc2 . (Contributed by Brendan Leahy, 19-Jun-2018)

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

Proof

Step Hyp Ref Expression
1 ftc2nc.a
 |-  ( ph -> A e. RR )
2 ftc2nc.b
 |-  ( ph -> B e. RR )
3 ftc2nc.le
 |-  ( ph -> A <_ B )
4 ftc2nc.c
 |-  ( ph -> ( RR _D F ) e. ( ( A (,) B ) -cn-> CC ) )
5 ftc2nc.i
 |-  ( ph -> ( RR _D F ) e. L^1 )
6 ftc2nc.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 ioof
 |-  (,) : ( RR* X. RR* ) --> ~P RR
24 ffun
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> Fun (,) )
25 23 24 ax-mp
 |-  Fun (,)
26 fvelima
 |-  ( ( Fun (,) /\ s e. ( (,) " ( ( A [,] B ) X. ( A [,] B ) ) ) ) -> E. x e. ( ( A [,] B ) X. ( A [,] B ) ) ( (,) ` x ) = s )
27 25 26 mpan
 |-  ( s e. ( (,) " ( ( A [,] B ) X. ( A [,] B ) ) ) -> E. x e. ( ( A [,] B ) X. ( A [,] B ) ) ( (,) ` x ) = s )
28 1st2nd2
 |-  ( x e. ( ( A [,] B ) X. ( A [,] B ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
29 28 fveq2d
 |-  ( x e. ( ( A [,] B ) X. ( A [,] B ) ) -> ( (,) ` x ) = ( (,) ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
30 df-ov
 |-  ( ( 1st ` x ) (,) ( 2nd ` x ) ) = ( (,) ` <. ( 1st ` x ) , ( 2nd ` x ) >. )
31 29 30 eqtr4di
 |-  ( x e. ( ( A [,] B ) X. ( A [,] B ) ) -> ( (,) ` x ) = ( ( 1st ` x ) (,) ( 2nd ` x ) ) )
32 31 eqeq1d
 |-  ( x e. ( ( A [,] B ) X. ( A [,] B ) ) -> ( ( (,) ` x ) = s <-> ( ( 1st ` x ) (,) ( 2nd ` x ) ) = s ) )
33 32 adantl
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( ( (,) ` x ) = s <-> ( ( 1st ` x ) (,) ( 2nd ` x ) ) = s ) )
34 7 8 jca
 |-  ( ph -> ( A e. RR* /\ B e. RR* ) )
35 34 adantr
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( A e. RR* /\ B e. RR* ) )
36 xp1st
 |-  ( x e. ( ( A [,] B ) X. ( A [,] B ) ) -> ( 1st ` x ) e. ( A [,] B ) )
37 elicc1
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( 1st ` x ) e. ( A [,] B ) <-> ( ( 1st ` x ) e. RR* /\ A <_ ( 1st ` x ) /\ ( 1st ` x ) <_ B ) ) )
38 7 8 37 syl2anc
 |-  ( ph -> ( ( 1st ` x ) e. ( A [,] B ) <-> ( ( 1st ` x ) e. RR* /\ A <_ ( 1st ` x ) /\ ( 1st ` x ) <_ B ) ) )
39 38 biimpa
 |-  ( ( ph /\ ( 1st ` x ) e. ( A [,] B ) ) -> ( ( 1st ` x ) e. RR* /\ A <_ ( 1st ` x ) /\ ( 1st ` x ) <_ B ) )
40 39 simp2d
 |-  ( ( ph /\ ( 1st ` x ) e. ( A [,] B ) ) -> A <_ ( 1st ` x ) )
41 36 40 sylan2
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> A <_ ( 1st ` x ) )
42 xp2nd
 |-  ( x e. ( ( A [,] B ) X. ( A [,] B ) ) -> ( 2nd ` x ) e. ( A [,] B ) )
43 iccleub
 |-  ( ( A e. RR* /\ B e. RR* /\ ( 2nd ` x ) e. ( A [,] B ) ) -> ( 2nd ` x ) <_ B )
44 43 3expa
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( 2nd ` x ) e. ( A [,] B ) ) -> ( 2nd ` x ) <_ B )
45 34 42 44 syl2an
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( 2nd ` x ) <_ B )
46 ioossioo
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( A <_ ( 1st ` x ) /\ ( 2nd ` x ) <_ B ) ) -> ( ( 1st ` x ) (,) ( 2nd ` x ) ) C_ ( A (,) B ) )
47 35 41 45 46 syl12anc
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( ( 1st ` x ) (,) ( 2nd ` x ) ) C_ ( A (,) B ) )
48 47 sselda
 |-  ( ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) /\ t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) -> t e. ( A (,) B ) )
49 22 ffvelrnda
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> ( ( RR _D F ) ` t ) e. CC )
50 49 adantlr
 |-  ( ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) /\ t e. ( A (,) B ) ) -> ( ( RR _D F ) ` t ) e. CC )
51 48 50 syldan
 |-  ( ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) /\ t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) -> ( ( RR _D F ) ` t ) e. CC )
52 ioombl
 |-  ( ( 1st ` x ) (,) ( 2nd ` x ) ) e. dom vol
53 52 a1i
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( ( 1st ` x ) (,) ( 2nd ` x ) ) e. dom vol )
54 fvexd
 |-  ( ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) /\ t e. ( A (,) B ) ) -> ( ( RR _D F ) ` t ) e. _V )
55 22 feqmptd
 |-  ( ph -> ( RR _D F ) = ( t e. ( A (,) B ) |-> ( ( RR _D F ) ` t ) ) )
56 55 5 eqeltrrd
 |-  ( ph -> ( t e. ( A (,) B ) |-> ( ( RR _D F ) ` t ) ) e. L^1 )
57 56 adantr
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( t e. ( A (,) B ) |-> ( ( RR _D F ) ` t ) ) e. L^1 )
58 47 53 54 57 iblss
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( ( RR _D F ) ` t ) ) e. L^1 )
59 ax-resscn
 |-  RR C_ CC
60 ssid
 |-  CC C_ CC
61 cncfss
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( CC -cn-> RR ) C_ ( CC -cn-> CC ) )
62 59 60 61 mp2an
 |-  ( CC -cn-> RR ) C_ ( CC -cn-> CC )
63 abscncf
 |-  abs e. ( CC -cn-> RR )
64 62 63 sselii
 |-  abs e. ( CC -cn-> CC )
65 64 a1i
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> abs e. ( CC -cn-> CC ) )
66 55 reseq1d
 |-  ( ph -> ( ( RR _D F ) |` ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) = ( ( t e. ( A (,) B ) |-> ( ( RR _D F ) ` t ) ) |` ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) )
67 66 adantr
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( ( RR _D F ) |` ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) = ( ( t e. ( A (,) B ) |-> ( ( RR _D F ) ` t ) ) |` ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) )
68 47 resmptd
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( ( t e. ( A (,) B ) |-> ( ( RR _D F ) ` t ) ) |` ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) = ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( ( RR _D F ) ` t ) ) )
69 67 68 eqtrd
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( ( RR _D F ) |` ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) = ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( ( RR _D F ) ` t ) ) )
70 4 adantr
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( RR _D F ) e. ( ( A (,) B ) -cn-> CC ) )
71 rescncf
 |-  ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) C_ ( A (,) B ) -> ( ( RR _D F ) e. ( ( A (,) B ) -cn-> CC ) -> ( ( RR _D F ) |` ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) e. ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) -cn-> CC ) ) )
72 47 70 71 sylc
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( ( RR _D F ) |` ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) e. ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) -cn-> CC ) )
73 69 72 eqeltrrd
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( ( RR _D F ) ` t ) ) e. ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) -cn-> CC ) )
74 65 73 cncfmpt1f
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( abs ` ( ( RR _D F ) ` t ) ) ) e. ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) -cn-> CC ) )
75 cnmbf
 |-  ( ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) e. dom vol /\ ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( abs ` ( ( RR _D F ) ` t ) ) ) e. ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) -cn-> CC ) ) -> ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( abs ` ( ( RR _D F ) ` t ) ) ) e. MblFn )
76 52 74 75 sylancr
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( abs ` ( ( RR _D F ) ` t ) ) ) e. MblFn )
77 51 58 itgcl
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t e. CC )
78 77 cjcld
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( * ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) e. CC )
79 ioossre
 |-  ( ( 1st ` x ) (,) ( 2nd ` x ) ) C_ RR
80 79 59 sstri
 |-  ( ( 1st ` x ) (,) ( 2nd ` x ) ) C_ CC
81 cncfmptc
 |-  ( ( ( * ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) e. CC /\ ( ( 1st ` x ) (,) ( 2nd ` x ) ) C_ CC /\ CC C_ CC ) -> ( s e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( * ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) ) e. ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) -cn-> CC ) )
82 80 60 81 mp3an23
 |-  ( ( * ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) e. CC -> ( s e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( * ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) ) e. ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) -cn-> CC ) )
83 78 82 syl
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( s e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( * ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) ) e. ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) -cn-> CC ) )
84 nfcv
 |-  F/_ s ( ( RR _D F ) ` t )
85 nfcsb1v
 |-  F/_ t [_ s / t ]_ ( ( RR _D F ) ` t )
86 csbeq1a
 |-  ( t = s -> ( ( RR _D F ) ` t ) = [_ s / t ]_ ( ( RR _D F ) ` t ) )
87 84 85 86 cbvmpt
 |-  ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( ( RR _D F ) ` t ) ) = ( s e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> [_ s / t ]_ ( ( RR _D F ) ` t ) )
88 87 73 eqeltrrid
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( s e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> [_ s / t ]_ ( ( RR _D F ) ` t ) ) e. ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) -cn-> CC ) )
89 83 88 mulcncf
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( s e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( ( * ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) x. [_ s / t ]_ ( ( RR _D F ) ` t ) ) ) e. ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) -cn-> CC ) )
90 cnmbf
 |-  ( ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) e. dom vol /\ ( s e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( ( * ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) x. [_ s / t ]_ ( ( RR _D F ) ` t ) ) ) e. ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) -cn-> CC ) ) -> ( s e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( ( * ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) x. [_ s / t ]_ ( ( RR _D F ) ` t ) ) ) e. MblFn )
91 52 89 90 sylancr
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( s e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( ( * ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) x. [_ s / t ]_ ( ( RR _D F ) ` t ) ) ) e. MblFn )
92 51 58 76 91 itgabsnc
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( abs ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) <_ S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( abs ` ( ( RR _D F ) ` t ) ) _d t )
93 51 abscld
 |-  ( ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) /\ t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) -> ( abs ` ( ( RR _D F ) ` t ) ) e. RR )
94 fvexd
 |-  ( ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) /\ t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) -> ( ( RR _D F ) ` t ) e. _V )
95 94 58 76 iblabsnc
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( abs ` ( ( RR _D F ) ` t ) ) ) e. L^1 )
96 51 absge0d
 |-  ( ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) /\ t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) -> 0 <_ ( abs ` ( ( RR _D F ) ` t ) ) )
97 93 95 96 itgposval
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( abs ` ( ( RR _D F ) ` t ) ) _d t = ( S.2 ` ( t e. RR |-> if ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) ) )
98 92 97 breqtrd
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( abs ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) ) )
99 itgeq1
 |-  ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) = s -> S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t = S. s ( ( RR _D F ) ` t ) _d t )
100 99 fveq2d
 |-  ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) = s -> ( abs ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) = ( abs ` S. s ( ( RR _D F ) ` t ) _d t ) )
101 eleq2
 |-  ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) = s -> ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) <-> t e. s ) )
102 101 ifbid
 |-  ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) = s -> if ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) = if ( t e. s , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) )
103 102 mpteq2dv
 |-  ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) = s -> ( t e. RR |-> if ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) = ( t e. RR |-> if ( t e. s , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) )
104 103 fveq2d
 |-  ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) = s -> ( S.2 ` ( t e. RR |-> if ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) ) = ( S.2 ` ( t e. RR |-> if ( t e. s , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) ) )
105 100 104 breq12d
 |-  ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) = s -> ( ( abs ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) ) <-> ( abs ` S. s ( ( RR _D F ) ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. s , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) ) ) )
106 98 105 syl5ibcom
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) = s -> ( abs ` S. s ( ( RR _D F ) ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. s , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) ) ) )
107 33 106 sylbid
 |-  ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( ( (,) ` x ) = s -> ( abs ` S. s ( ( RR _D F ) ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. s , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) ) ) )
108 107 rexlimdva
 |-  ( ph -> ( E. x e. ( ( A [,] B ) X. ( A [,] B ) ) ( (,) ` x ) = s -> ( abs ` S. s ( ( RR _D F ) ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. s , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) ) ) )
109 27 108 syl5
 |-  ( ph -> ( s e. ( (,) " ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( abs ` S. s ( ( RR _D F ) ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. s , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) ) ) )
110 109 ralrimiv
 |-  ( ph -> A. s e. ( (,) " ( ( A [,] B ) X. ( A [,] B ) ) ) ( abs ` S. s ( ( RR _D F ) ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. s , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) ) )
111 17 1 2 3 18 20 5 22 110 ftc1anc
 |-  ( ph -> ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t ) e. ( ( A [,] B ) -cn-> CC ) )
112 cncff
 |-  ( F e. ( ( A [,] B ) -cn-> CC ) -> F : ( A [,] B ) --> CC )
113 6 112 syl
 |-  ( ph -> F : ( A [,] B ) --> CC )
114 113 feqmptd
 |-  ( ph -> F = ( x e. ( A [,] B ) |-> ( F ` x ) ) )
115 114 6 eqeltrrd
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( F ` x ) ) e. ( ( A [,] B ) -cn-> CC ) )
116 14 16 111 115 cncfmpt2f
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
117 59 a1i
 |-  ( ph -> RR C_ CC )
118 iccssre
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
119 1 2 118 syl2anc
 |-  ( ph -> ( A [,] B ) C_ RR )
120 fvexd
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ t e. ( A (,) x ) ) -> ( ( RR _D F ) ` t ) e. _V )
121 2 adantr
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> B e. RR )
122 121 rexrd
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> B e. RR* )
123 elicc2
 |-  ( ( A e. RR /\ B e. RR ) -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
124 1 2 123 syl2anc
 |-  ( ph -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
125 124 biimpa
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( x e. RR /\ A <_ x /\ x <_ B ) )
126 125 simp3d
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x <_ B )
127 iooss2
 |-  ( ( B e. RR* /\ x <_ B ) -> ( A (,) x ) C_ ( A (,) B ) )
128 122 126 127 syl2anc
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( A (,) x ) C_ ( A (,) B ) )
129 ioombl
 |-  ( A (,) x ) e. dom vol
130 129 a1i
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( A (,) x ) e. dom vol )
131 fvexd
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ t e. ( A (,) B ) ) -> ( ( RR _D F ) ` t ) e. _V )
132 56 adantr
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( t e. ( A (,) B ) |-> ( ( RR _D F ) ` t ) ) e. L^1 )
133 128 130 131 132 iblss
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( t e. ( A (,) x ) |-> ( ( RR _D F ) ` t ) ) e. L^1 )
134 120 133 itgcl
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t e. CC )
135 113 ffvelrnda
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. CC )
136 134 135 subcld
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) e. CC )
137 14 tgioo2
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
138 iccntr
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
139 1 2 138 syl2anc
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
140 117 119 136 137 14 139 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 ) ) ) ) )
141 reelprrecn
 |-  RR e. { RR , CC }
142 141 a1i
 |-  ( ph -> RR e. { RR , CC } )
143 ioossicc
 |-  ( A (,) B ) C_ ( A [,] B )
144 143 sseli
 |-  ( x e. ( A (,) B ) -> x e. ( A [,] B ) )
145 144 134 sylan2
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t e. CC )
146 22 ffvelrnda
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. CC )
147 17 1 2 3 4 5 ftc1cnnc
 |-  ( ph -> ( RR _D ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t ) ) = ( RR _D F ) )
148 117 119 134 137 14 139 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 ) ) )
149 22 feqmptd
 |-  ( ph -> ( RR _D F ) = ( x e. ( A (,) B ) |-> ( ( RR _D F ) ` x ) ) )
150 147 148 149 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 ) ) )
151 144 135 sylan2
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( F ` x ) e. CC )
152 114 oveq2d
 |-  ( ph -> ( RR _D F ) = ( RR _D ( x e. ( A [,] B ) |-> ( F ` x ) ) ) )
153 117 119 135 137 14 139 dvmptntr
 |-  ( ph -> ( RR _D ( x e. ( A [,] B ) |-> ( F ` x ) ) ) = ( RR _D ( x e. ( A (,) B ) |-> ( F ` x ) ) ) )
154 152 149 153 3eqtr3rd
 |-  ( ph -> ( RR _D ( x e. ( A (,) B ) |-> ( F ` x ) ) ) = ( x e. ( A (,) B ) |-> ( ( RR _D F ) ` x ) ) )
155 142 145 146 150 151 146 154 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 ) ) ) )
156 146 subidd
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( RR _D F ) ` x ) - ( ( RR _D F ) ` x ) ) = 0 )
157 156 mpteq2dva
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( ( ( RR _D F ) ` x ) - ( ( RR _D F ) ` x ) ) ) = ( x e. ( A (,) B ) |-> 0 ) )
158 140 155 157 3eqtrd
 |-  ( ph -> ( RR _D ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ) = ( x e. ( A (,) B ) |-> 0 ) )
159 fconstmpt
 |-  ( ( A (,) B ) X. { 0 } ) = ( x e. ( A (,) B ) |-> 0 )
160 158 159 eqtr4di
 |-  ( ph -> ( RR _D ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ) = ( ( A (,) B ) X. { 0 } ) )
161 1 2 116 160 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 ) } ) )
162 161 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 ) )
163 oveq2
 |-  ( x = B -> ( A (,) x ) = ( A (,) B ) )
164 itgeq1
 |-  ( ( A (,) x ) = ( A (,) B ) -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t = S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t )
165 163 164 syl
 |-  ( x = B -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t = S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t )
166 fveq2
 |-  ( x = B -> ( F ` x ) = ( F ` B ) )
167 165 166 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 ) ) )
168 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 ) ) )
169 ovex
 |-  ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) e. _V
170 167 168 169 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 ) ) )
171 10 170 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 ) ) )
172 162 171 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 ) ) )
173 lbicc2
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
174 7 8 3 173 syl3anc
 |-  ( ph -> A e. ( A [,] B ) )
175 oveq2
 |-  ( x = A -> ( A (,) x ) = ( A (,) A ) )
176 iooid
 |-  ( A (,) A ) = (/)
177 175 176 eqtrdi
 |-  ( x = A -> ( A (,) x ) = (/) )
178 itgeq1
 |-  ( ( A (,) x ) = (/) -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t = S. (/) ( ( RR _D F ) ` t ) _d t )
179 177 178 syl
 |-  ( x = A -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t = S. (/) ( ( RR _D F ) ` t ) _d t )
180 itg0
 |-  S. (/) ( ( RR _D F ) ` t ) _d t = 0
181 179 180 eqtrdi
 |-  ( x = A -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t = 0 )
182 fveq2
 |-  ( x = A -> ( F ` x ) = ( F ` A ) )
183 181 182 oveq12d
 |-  ( x = A -> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) = ( 0 - ( F ` A ) ) )
184 df-neg
 |-  -u ( F ` A ) = ( 0 - ( F ` A ) )
185 183 184 eqtr4di
 |-  ( x = A -> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) = -u ( F ` A ) )
186 negex
 |-  -u ( F ` A ) e. _V
187 185 168 186 fvmpt
 |-  ( A e. ( A [,] B ) -> ( ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) = -u ( F ` A ) )
188 174 187 syl
 |-  ( ph -> ( ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) = -u ( F ` A ) )
189 13 172 188 3eqtr3d
 |-  ( ph -> ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) = -u ( F ` A ) )
190 189 oveq2d
 |-  ( ph -> ( ( F ` B ) + ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) ) = ( ( F ` B ) + -u ( F ` A ) ) )
191 113 10 ffvelrnd
 |-  ( ph -> ( F ` B ) e. CC )
192 fvexd
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> ( ( RR _D F ) ` t ) e. _V )
193 192 56 itgcl
 |-  ( ph -> S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t e. CC )
194 191 193 pncan3d
 |-  ( ph -> ( ( F ` B ) + ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) ) = S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t )
195 113 174 ffvelrnd
 |-  ( ph -> ( F ` A ) e. CC )
196 191 195 negsubd
 |-  ( ph -> ( ( F ` B ) + -u ( F ` A ) ) = ( ( F ` B ) - ( F ` A ) ) )
197 190 194 196 3eqtr3d
 |-  ( ph -> S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t = ( ( F ` B ) - ( F ` A ) ) )