Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ftc2nc Structured version   Unicode version

Theorem ftc2nc 28419
Description: Choice-free proof of ftc2 21485. (Contributed by Brendan Leahy, 19-Jun-2018.)
Hypotheses
Ref Expression
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
Ref Expression
ftc2nc  |-  ( ph  ->  S. ( A (,) B ) ( ( RR  _D  F ) `
 t )  _d t  =  ( ( F `  B )  -  ( F `  A ) ) )
Distinct variable groups:    t, A    t, B    t, F    ph, t

Proof of Theorem ftc2nc
Dummy variables  s  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ftc2nc.a . . . . . . 7  |-  ( ph  ->  A  e.  RR )
21rexrd 9425 . . . . . 6  |-  ( ph  ->  A  e.  RR* )
3 ftc2nc.b . . . . . . 7  |-  ( ph  ->  B  e.  RR )
43rexrd 9425 . . . . . 6  |-  ( ph  ->  B  e.  RR* )
5 ftc2nc.le . . . . . 6  |-  ( ph  ->  A  <_  B )
6 ubicc2 11394 . . . . . 6  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  A  <_  B )  ->  B  e.  ( A [,] B
) )
72, 4, 5, 6syl3anc 1218 . . . . 5  |-  ( ph  ->  B  e.  ( A [,] B ) )
8 fvex 5694 . . . . . 6  |-  ( ( x  e.  ( A [,] B )  |->  ( S. ( A (,) x ) ( ( RR  _D  F ) `
 t )  _d t  -  ( F `
 x ) ) ) `  A )  e.  _V
98fvconst2 5926 . . . . 5  |-  ( 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
) )
107, 9syl 16 . . . 4  |-  ( 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 ) )
11 eqid 2437 . . . . . . . 8  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
1211subcn 20411 . . . . . . . . 9  |-  -  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) )
1312a1i 11 . . . . . . . 8  |-  ( ph  ->  -  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
)  Cn  ( TopOpen ` fld )
) )
14 eqid 2437 . . . . . . . . 9  |-  ( 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 )
15 ssid 3368 . . . . . . . . . 10  |-  ( A (,) B )  C_  ( A (,) B )
1615a1i 11 . . . . . . . . 9  |-  ( ph  ->  ( A (,) B
)  C_  ( A (,) B ) )
17 ioossre 11349 . . . . . . . . . 10  |-  ( A (,) B )  C_  RR
1817a1i 11 . . . . . . . . 9  |-  ( ph  ->  ( A (,) B
)  C_  RR )
19 ftc2nc.i . . . . . . . . 9  |-  ( ph  ->  ( RR  _D  F
)  e.  L^1 )
20 ftc2nc.c . . . . . . . . . 10  |-  ( ph  ->  ( RR  _D  F
)  e.  ( ( A (,) B )
-cn-> CC ) )
21 cncff 20438 . . . . . . . . . 10  |-  ( ( RR  _D  F )  e.  ( ( A (,) B ) -cn-> CC )  ->  ( RR  _D  F ) : ( A (,) B ) --> CC )
2220, 21syl 16 . . . . . . . . 9  |-  ( ph  ->  ( RR  _D  F
) : ( A (,) B ) --> CC )
23 ioof 11379 . . . . . . . . . . . . 13  |-  (,) :
( RR*  X.  RR* ) --> ~P RR
24 ffun 5554 . . . . . . . . . . . . 13  |-  ( (,)
: ( RR*  X.  RR* )
--> ~P RR  ->  Fun  (,) )
2523, 24ax-mp 5 . . . . . . . . . . . 12  |-  Fun  (,)
26 fvelima 5736 . . . . . . . . . . . 12  |-  ( ( Fun  (,)  /\  s  e.  ( (,) " (
( A [,] B
)  X.  ( A [,] B ) ) ) )  ->  E. x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) ( (,) `  x
)  =  s )
2725, 26mpan 670 . . . . . . . . . . 11  |-  ( s  e.  ( (,) " (
( A [,] B
)  X.  ( A [,] B ) ) )  ->  E. x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) ( (,) `  x
)  =  s )
28 1st2nd2 6608 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( ( A [,] B )  X.  ( A [,] B
) )  ->  x  =  <. ( 1st `  x
) ,  ( 2nd `  x ) >. )
2928fveq2d 5688 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( ( A [,] B )  X.  ( A [,] B
) )  ->  ( (,) `  x )  =  ( (,) `  <. ( 1st `  x ) ,  ( 2nd `  x
) >. ) )
30 df-ov 6089 . . . . . . . . . . . . . . . 16  |-  ( ( 1st `  x ) (,) ( 2nd `  x
) )  =  ( (,) `  <. ( 1st `  x ) ,  ( 2nd `  x
) >. )
3129, 30syl6eqr 2487 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( ( A [,] B )  X.  ( A [,] B
) )  ->  ( (,) `  x )  =  ( ( 1st `  x
) (,) ( 2nd `  x ) ) )
3231eqeq1d 2445 . . . . . . . . . . . . . 14  |-  ( x  e.  ( ( A [,] B )  X.  ( A [,] B
) )  ->  (
( (,) `  x
)  =  s  <->  ( ( 1st `  x ) (,) ( 2nd `  x
) )  =  s ) )
3332adantl 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  ->  ( ( (,) `  x )  =  s  <->  ( ( 1st `  x ) (,) ( 2nd `  x ) )  =  s ) )
342, 4jca 532 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( A  e.  RR*  /\  B  e.  RR* )
)
3534adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  ->  ( A  e.  RR*  /\  B  e. 
RR* ) )
36 xp1st 6601 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( ( A [,] B )  X.  ( A [,] B
) )  ->  ( 1st `  x )  e.  ( A [,] B
) )
37 elicc1 11336 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  (
( 1st `  x
)  e.  ( A [,] B )  <->  ( ( 1st `  x )  e. 
RR*  /\  A  <_  ( 1st `  x )  /\  ( 1st `  x
)  <_  B )
) )
382, 4, 37syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( 1st `  x
)  e.  ( A [,] B )  <->  ( ( 1st `  x )  e. 
RR*  /\  A  <_  ( 1st `  x )  /\  ( 1st `  x
)  <_  B )
) )
3938biimpa 484 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( 1st `  x )  e.  ( A [,] B ) )  ->  ( ( 1st `  x )  e. 
RR*  /\  A  <_  ( 1st `  x )  /\  ( 1st `  x
)  <_  B )
)
4039simp2d 1001 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( 1st `  x )  e.  ( A [,] B ) )  ->  A  <_  ( 1st `  x ) )
4136, 40sylan2 474 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  ->  A  <_  ( 1st `  x ) )
42 xp2nd 6602 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( ( A [,] B )  X.  ( A [,] B
) )  ->  ( 2nd `  x )  e.  ( A [,] B
) )
43 iccleub 11343 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( 2nd `  x )  e.  ( A [,] B ) )  ->  ( 2nd `  x )  <_  B
)
44433expa 1187 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( 2nd `  x
)  e.  ( A [,] B ) )  ->  ( 2nd `  x
)  <_  B )
4534, 42, 44syl2an 477 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  ->  ( 2nd `  x )  <_  B
)
46 df-ioo 11296 . . . . . . . . . . . . . . . . . . . 20  |-  (,)  =  ( s  e.  RR* ,  t  e.  RR*  |->  { y  e.  RR*  |  (
s  <  y  /\  y  <  t ) } )
47 xrlelttr 11122 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  RR*  /\  ( 1st `  x )  e. 
RR*  /\  z  e.  RR* )  ->  ( ( A  <_  ( 1st `  x
)  /\  ( 1st `  x )  <  z
)  ->  A  <  z ) )
48 xrltletr 11123 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( z  e.  RR*  /\  ( 2nd `  x )  e. 
RR*  /\  B  e.  RR* )  ->  ( (
z  <  ( 2nd `  x )  /\  ( 2nd `  x )  <_  B )  ->  z  <  B ) )
4946, 46, 47, 48ixxss12 11312 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <_  ( 1st `  x )  /\  ( 2nd `  x )  <_  B ) )  ->  ( ( 1st `  x ) (,) ( 2nd `  x ) ) 
C_  ( A (,) B ) )
5035, 41, 45, 49syl12anc 1216 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  ->  ( ( 1st `  x ) (,) ( 2nd `  x
) )  C_  ( A (,) B ) )
5150sselda 3349 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  /\  t  e.  ( ( 1st `  x
) (,) ( 2nd `  x ) ) )  ->  t  e.  ( A (,) B ) )
5222ffvelrnda 5836 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  ( A (,) B ) )  ->  ( ( RR  _D  F ) `  t )  e.  CC )
5352adantlr 714 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  /\  t  e.  ( A (,) B
) )  ->  (
( RR  _D  F
) `  t )  e.  CC )
5451, 53syldan 470 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  /\  t  e.  ( ( 1st `  x
) (,) ( 2nd `  x ) ) )  ->  ( ( RR 
_D  F ) `  t )  e.  CC )
55 ioombl 21015 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1st `  x ) (,) ( 2nd `  x
) )  e.  dom  vol
5655a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  ->  ( ( 1st `  x ) (,) ( 2nd `  x
) )  e.  dom  vol )
57 fvex 5694 . . . . . . . . . . . . . . . . . 18  |-  ( ( RR  _D  F ) `
 t )  e. 
_V
5857a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  /\  t  e.  ( A (,) B
) )  ->  (
( RR  _D  F
) `  t )  e.  _V )
5922feqmptd 5737 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( RR  _D  F
)  =  ( t  e.  ( A (,) B )  |->  ( ( RR  _D  F ) `
 t ) ) )
6059, 19eqeltrrd 2512 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( t  e.  ( A (,) B ) 
|->  ( ( RR  _D  F ) `  t
) )  e.  L^1 )
6160adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  ->  ( t  e.  ( A (,) B
)  |->  ( ( RR 
_D  F ) `  t ) )  e.  L^1 )
6250, 56, 58, 61iblss 21251 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  ->  ( t  e.  ( ( 1st `  x
) (,) ( 2nd `  x ) )  |->  ( ( RR  _D  F
) `  t )
)  e.  L^1 )
63 ax-resscn 9331 . . . . . . . . . . . . . . . . . . . . 21  |-  RR  C_  CC
64 ssid 3368 . . . . . . . . . . . . . . . . . . . . 21  |-  CC  C_  CC
65 cncfss 20444 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( RR  C_  CC  /\  CC  C_  CC )  ->  ( CC -cn-> RR )  C_  ( CC -cn-> CC ) )
6663, 64, 65mp2an 672 . . . . . . . . . . . . . . . . . . . 20  |-  ( CC
-cn-> RR )  C_  ( CC -cn-> CC )
67 abscncf 20446 . . . . . . . . . . . . . . . . . . . 20  |-  abs  e.  ( CC -cn-> RR )
6866, 67sselii 3346 . . . . . . . . . . . . . . . . . . 19  |-  abs  e.  ( CC -cn-> CC )
6968a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  ->  abs  e.  ( CC -cn-> CC ) )
7059reseq1d 5101 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( RR  _D  F )  |`  (
( 1st `  x
) (,) ( 2nd `  x ) ) )  =  ( ( t  e.  ( A (,) B )  |->  ( ( RR  _D  F ) `
 t ) )  |`  ( ( 1st `  x
) (,) ( 2nd `  x ) ) ) )
7170adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
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 ) ) ) )
72 resmpt 5149 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 1st `  x
) (,) ( 2nd `  x ) )  C_  ( A (,) B )  ->  ( ( t  e.  ( A (,) B )  |->  ( ( RR  _D  F ) `
 t ) )  |`  ( ( 1st `  x
) (,) ( 2nd `  x ) ) )  =  ( t  e.  ( ( 1st `  x
) (,) ( 2nd `  x ) )  |->  ( ( RR  _D  F
) `  t )
) )
7350, 72syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
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
) ) )
7471, 73eqtrd 2469 . . . . . . . . . . . . . . . . . . 19  |-  ( (
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 )
) )
7520adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  ->  ( RR  _D  F )  e.  ( ( A (,) B
) -cn-> CC ) )
76 rescncf 20442 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 ) ) )
7750, 75, 76sylc 60 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  ->  ( ( RR  _D  F )  |`  ( ( 1st `  x
) (,) ( 2nd `  x ) ) )  e.  ( ( ( 1st `  x ) (,) ( 2nd `  x
) ) -cn-> CC ) )
7874, 77eqeltrrd 2512 . . . . . . . . . . . . . . . . . 18  |-  ( (
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 ) )
7969, 78cncfmpt1f 20458 . . . . . . . . . . . . . . . . 17  |-  ( (
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 ) )
80 cnmbf 21106 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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
)
8155, 79, 80sylancr 663 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  ->  ( t  e.  ( ( 1st `  x
) (,) ( 2nd `  x ) )  |->  ( abs `  ( ( RR  _D  F ) `
 t ) ) )  e. MblFn )
8211mulcn 20412 . . . . . . . . . . . . . . . . . . 19  |-  x.  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) )
8382a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  ->  x.  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) ) )
8454, 62itgcl 21230 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  ->  S. (
( 1st `  x
) (,) ( 2nd `  x ) ) ( ( RR  _D  F
) `  t )  _d t  e.  CC )
8584cjcld 12677 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  ->  ( * `  S. ( ( 1st `  x ) (,) ( 2nd `  x ) ) ( ( RR  _D  F ) `  t
)  _d t )  e.  CC )
86 ioossre 11349 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1st `  x ) (,) ( 2nd `  x
) )  C_  RR
8786, 63sstri 3358 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1st `  x ) (,) ( 2nd `  x
) )  C_  CC
88 cncfmptc 20456 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( * `  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 ) )
8987, 64, 88mp3an23 1306 . . . . . . . . . . . . . . . . . . 19  |-  ( ( * `  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 ) )
9085, 89syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( (
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 ) )
91 nfcv 2573 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ s
( ( RR  _D  F ) `  t
)
92 nfcsb1v 3297 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ t [_ s  /  t ]_ ( ( RR  _D  F ) `  t
)
93 csbeq1a 3290 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  s  ->  (
( RR  _D  F
) `  t )  =  [_ s  /  t ]_ ( ( RR  _D  F ) `  t
) )
9491, 92, 93cbvmpt 4375 . . . . . . . . . . . . . . . . . . 19  |-  ( t  e.  ( ( 1st `  x ) (,) ( 2nd `  x ) ) 
|->  ( ( RR  _D  F ) `  t
) )  =  ( s  e.  ( ( 1st `  x ) (,) ( 2nd `  x
) )  |->  [_ s  /  t ]_ (
( RR  _D  F
) `  t )
)
9594, 78syl5eqelr 2522 . . . . . . . . . . . . . . . . . 18  |-  ( (
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 ) )
9611, 83, 90, 95cncfmpt2f 20459 . . . . . . . . . . . . . . . . 17  |-  ( (
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 ) )
97 cnmbf 21106 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 )
9855, 96, 97sylancr 663 . . . . . . . . . . . . . . . 16  |-  ( (
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 )
9954, 62, 81, 98itgabsnc 28404 . . . . . . . . . . . . . . 15  |-  ( (
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 )
10054abscld 12914 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  /\  t  e.  ( ( 1st `  x
) (,) ( 2nd `  x ) ) )  ->  ( abs `  (
( RR  _D  F
) `  t )
)  e.  RR )
10157a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  /\  t  e.  ( ( 1st `  x
) (,) ( 2nd `  x ) ) )  ->  ( ( RR 
_D  F ) `  t )  e.  _V )
102101, 62, 81iblabsnc 28399 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  ->  ( t  e.  ( ( 1st `  x
) (,) ( 2nd `  x ) )  |->  ( abs `  ( ( RR  _D  F ) `
 t ) ) )  e.  L^1 )
10354absge0d 12922 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( ( A [,] B )  X.  ( A [,] B ) ) )  /\  t  e.  ( ( 1st `  x
) (,) ( 2nd `  x ) ) )  ->  0  <_  ( abs `  ( ( RR 
_D  F ) `  t ) ) )
104100, 102, 103itgposval 21242 . . . . . . . . . . . . . . 15  |-  ( (
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 ) ) ) )
10599, 104breqtrd 4309 . . . . . . . . . . . . . 14  |-  ( (
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 ) ) ) )
106 itgeq1 21219 . . . . . . . . . . . . . . . 16  |-  ( ( ( 1st `  x
) (,) ( 2nd `  x ) )  =  s  ->  S. (
( 1st `  x
) (,) ( 2nd `  x ) ) ( ( RR  _D  F
) `  t )  _d t  =  S. s ( ( RR 
_D  F ) `  t )  _d t )
107106fveq2d 5688 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) )
108 eleq2 2498 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 1st `  x
) (,) ( 2nd `  x ) )  =  s  ->  ( t  e.  ( ( 1st `  x
) (,) ( 2nd `  x ) )  <->  t  e.  s ) )
109108ifbid 3804 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) )
110109mpteq2dv 4372 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) )
111110fveq2d 5688 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) ) )
112107, 111breq12d 4298 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) ) ) )
113105, 112syl5ibcom 220 . . . . . . . . . . . . 13  |-  ( (
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 ) ) ) ) )
11433, 113sylbid 215 . . . . . . . . . . . 12  |-  ( (
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 ) ) ) ) )
115114rexlimdva 2835 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) )
11627, 115syl5 32 . . . . . . . . . 10  |-  ( 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 ) ) ) ) )
117116ralrimiv 2792 . . . . . . . . 9  |-  ( 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 ) ) ) )
11814, 1, 3, 5, 16, 18, 19, 22, 117ftc1anc 28418 . . . . . . . 8  |-  ( ph  ->  ( x  e.  ( A [,] B ) 
|->  S. ( A (,) x ) ( ( RR  _D  F ) `
 t )  _d t )  e.  ( ( A [,] B
) -cn-> CC ) )
119 ftc2nc.f . . . . . . . . . . 11  |-  ( ph  ->  F  e.  ( ( A [,] B )
-cn-> CC ) )
120 cncff 20438 . . . . . . . . . . 11  |-  ( F  e.  ( ( A [,] B ) -cn-> CC )  ->  F :
( A [,] B
) --> CC )
121119, 120syl 16 . . . . . . . . . 10  |-  ( ph  ->  F : ( A [,] B ) --> CC )
122121feqmptd 5737 . . . . . . . . 9  |-  ( ph  ->  F  =  ( x  e.  ( A [,] B )  |->  ( F `
 x ) ) )
123122, 119eqeltrrd 2512 . . . . . . . 8  |-  ( ph  ->  ( x  e.  ( A [,] B ) 
|->  ( F `  x
) )  e.  ( ( A [,] B
) -cn-> CC ) )
12411, 13, 118, 123cncfmpt2f 20459 . . . . . . 7  |-  ( ph  ->  ( x  e.  ( A [,] B ) 
|->  ( S. ( A (,) x ) ( ( RR  _D  F
) `  t )  _d t  -  ( F `  x )
) )  e.  ( ( A [,] B
) -cn-> CC ) )
12563a1i 11 . . . . . . . . . 10  |-  ( ph  ->  RR  C_  CC )
126 iccssre 11369 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  C_  RR )
1271, 3, 126syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( A [,] B
)  C_  RR )
12857a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( A [,] B
) )  /\  t  e.  ( A (,) x
) )  ->  (
( RR  _D  F
) `  t )  e.  _V )
1293adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  B  e.  RR )
130129rexrd 9425 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  B  e.  RR* )
131 elicc2 11352 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( x  e.  ( A [,] B )  <-> 
( x  e.  RR  /\  A  <_  x  /\  x  <_  B ) ) )
1321, 3, 131syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( x  e.  ( A [,] B )  <-> 
( x  e.  RR  /\  A  <_  x  /\  x  <_  B ) ) )
133132biimpa 484 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( x  e.  RR  /\  A  <_  x  /\  x  <_  B
) )
134133simp3d 1002 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  x  <_  B )
135 iooss2 11328 . . . . . . . . . . . . . 14  |-  ( ( B  e.  RR*  /\  x  <_  B )  ->  ( A (,) x )  C_  ( A (,) B ) )
136130, 134, 135syl2anc 661 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( A (,) x )  C_  ( A (,) B ) )
137 ioombl 21015 . . . . . . . . . . . . . 14  |-  ( A (,) x )  e. 
dom  vol
138137a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( A (,) x )  e.  dom  vol )
13957a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( A [,] B
) )  /\  t  e.  ( A (,) B
) )  ->  (
( RR  _D  F
) `  t )  e.  _V )
14060adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( t  e.  ( A (,) B
)  |->  ( ( RR 
_D  F ) `  t ) )  e.  L^1 )
141136, 138, 139, 140iblss 21251 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( t  e.  ( A (,) x
)  |->  ( ( RR 
_D  F ) `  t ) )  e.  L^1 )
142128, 141itgcl 21230 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  S. ( A (,) x ) ( ( RR  _D  F
) `  t )  _d t  e.  CC )
143121ffvelrnda 5836 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( F `  x )  e.  CC )
144142, 143subcld 9711 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( S. ( A (,) x ) ( ( RR  _D  F ) `  t
)  _d t  -  ( F `  x ) )  e.  CC )
14511tgioo2 20349 . . . . . . . . . 10  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
146 iccntr 20367 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) )  =  ( A (,) B
) )
1471, 3, 146syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) )  =  ( A (,) B
) )
148125, 127, 144, 145, 11, 147dvmptntr 21414 . . . . . . . . 9  |-  ( 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 ) ) ) ) )
149 reelprrecn 9366 . . . . . . . . . . 11  |-  RR  e.  { RR ,  CC }
150149a1i 11 . . . . . . . . . 10  |-  ( ph  ->  RR  e.  { RR ,  CC } )
151 ioossicc 11373 . . . . . . . . . . . 12  |-  ( A (,) B )  C_  ( A [,] B )
152151sseli 3345 . . . . . . . . . . 11  |-  ( x  e.  ( A (,) B )  ->  x  e.  ( A [,] B
) )
153152, 142sylan2 474 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  S. ( A (,) x ) ( ( RR  _D  F
) `  t )  _d t  e.  CC )
15422ffvelrnda 5836 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( ( RR  _D  F ) `  x )  e.  CC )
15514, 1, 3, 5, 20, 19ftc1cnnc 28409 . . . . . . . . . . 11  |-  ( ph  ->  ( RR  _D  (
x  e.  ( A [,] B )  |->  S. ( A (,) x
) ( ( RR 
_D  F ) `  t )  _d t ) )  =  ( RR  _D  F ) )
156125, 127, 142, 145, 11, 147dvmptntr 21414 . . . . . . . . . . 11  |-  ( 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 ) ) )
15722feqmptd 5737 . . . . . . . . . . 11  |-  ( ph  ->  ( RR  _D  F
)  =  ( x  e.  ( A (,) B )  |->  ( ( RR  _D  F ) `
 x ) ) )
158155, 156, 1573eqtr3d 2477 . . . . . . . . . 10  |-  ( ph  ->  ( RR  _D  (
x  e.  ( A (,) B )  |->  S. ( A (,) x
) ( ( RR 
_D  F ) `  t )  _d t ) )  =  ( x  e.  ( A (,) B )  |->  ( ( RR  _D  F
) `  x )
) )
159152, 143sylan2 474 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( F `  x )  e.  CC )
160122oveq2d 6102 . . . . . . . . . . 11  |-  ( ph  ->  ( RR  _D  F
)  =  ( RR 
_D  ( x  e.  ( A [,] B
)  |->  ( F `  x ) ) ) )
161125, 127, 143, 145, 11, 147dvmptntr 21414 . . . . . . . . . . 11  |-  ( ph  ->  ( RR  _D  (
x  e.  ( A [,] B )  |->  ( F `  x ) ) )  =  ( RR  _D  ( x  e.  ( A (,) B )  |->  ( F `
 x ) ) ) )
162160, 157, 1613eqtr3rd 2478 . . . . . . . . . 10  |-  ( ph  ->  ( RR  _D  (
x  e.  ( A (,) B )  |->  ( F `  x ) ) )  =  ( x  e.  ( A (,) B )  |->  ( ( RR  _D  F
) `  x )
) )
163150, 153, 154, 158, 159, 154, 162dvmptsub 21410 . . . . . . . . 9  |-  ( 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 ) ) ) )
164154subidd 9699 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( (
( RR  _D  F
) `  x )  -  ( ( RR 
_D  F ) `  x ) )  =  0 )
165164mpteq2dva 4371 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  ( A (,) B ) 
|->  ( ( ( RR 
_D  F ) `  x )  -  (
( RR  _D  F
) `  x )
) )  =  ( x  e.  ( A (,) B )  |->  0 ) )
166148, 163, 1653eqtrd 2473 . . . . . . . 8  |-  ( ph  ->  ( RR  _D  (
x  e.  ( A [,] B )  |->  ( S. ( A (,) x ) ( ( RR  _D  F ) `
 t )  _d t  -  ( F `
 x ) ) ) )  =  ( x  e.  ( A (,) B )  |->  0 ) )
167 fconstmpt 4874 . . . . . . . 8  |-  ( ( A (,) B )  X.  { 0 } )  =  ( x  e.  ( A (,) B )  |->  0 )
168166, 167syl6eqr 2487 . . . . . . 7  |-  ( ph  ->  ( RR  _D  (
x  e.  ( A [,] B )  |->  ( S. ( A (,) x ) ( ( RR  _D  F ) `
 t )  _d t  -  ( F `
 x ) ) ) )  =  ( ( A (,) B
)  X.  { 0 } ) )
1691, 3, 124, 168dveq0 21441 . . . . . 6  |-  ( 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
) } ) )
170169fveq1d 5686 . . . . 5  |-  ( 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 ) )
171 oveq2 6094 . . . . . . . . 9  |-  ( x  =  B  ->  ( A (,) x )  =  ( A (,) B
) )
172 itgeq1 21219 . . . . . . . . 9  |-  ( ( A (,) x )  =  ( A (,) B )  ->  S. ( A (,) x ) ( ( RR  _D  F ) `  t
)  _d t  =  S. ( A (,) B ) ( ( RR  _D  F ) `
 t )  _d t )
173171, 172syl 16 . . . . . . . 8  |-  ( x  =  B  ->  S. ( A (,) x ) ( ( RR  _D  F ) `  t
)  _d t  =  S. ( A (,) B ) ( ( RR  _D  F ) `
 t )  _d t )
174 fveq2 5684 . . . . . . . 8  |-  ( x  =  B  ->  ( F `  x )  =  ( F `  B ) )
175173, 174oveq12d 6104 . . . . . . 7  |-  ( x  =  B  ->  ( S. ( A (,) x
) ( ( RR 
_D  F ) `  t )  _d t  -  ( F `  x ) )  =  ( S. ( A (,) B ) ( ( RR  _D  F
) `  t )  _d t  -  ( F `  B )
) )
176 eqid 2437 . . . . . . 7  |-  ( 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 ) ) )
177 ovex 6111 . . . . . . 7  |-  ( S. ( A (,) B
) ( ( RR 
_D  F ) `  t )  _d t  -  ( F `  B ) )  e. 
_V
178175, 176, 177fvmpt 5767 . . . . . 6  |-  ( 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 ) ) )
1797, 178syl 16 . . . . 5  |-  ( 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 ) ) )
180170, 179eqtr3d 2471 . . . 4  |-  ( 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 ) ) )
181 lbicc2 11393 . . . . . 6  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  A  <_  B )  ->  A  e.  ( A [,] B
) )
1822, 4, 5, 181syl3anc 1218 . . . . 5  |-  ( ph  ->  A  e.  ( A [,] B ) )
183 oveq2 6094 . . . . . . . . . . 11  |-  ( x  =  A  ->  ( A (,) x )  =  ( A (,) A
) )
184 iooid 11320 . . . . . . . . . . 11  |-  ( A (,) A )  =  (/)
185183, 184syl6eq 2485 . . . . . . . . . 10  |-  ( x  =  A  ->  ( A (,) x )  =  (/) )
186 itgeq1 21219 . . . . . . . . . 10  |-  ( ( A (,) x )  =  (/)  ->  S. ( A (,) x ) ( ( RR  _D  F ) `  t
)  _d t  =  S. (/) ( ( RR 
_D  F ) `  t )  _d t )
187185, 186syl 16 . . . . . . . . 9  |-  ( x  =  A  ->  S. ( A (,) x ) ( ( RR  _D  F ) `  t
)  _d t  =  S. (/) ( ( RR 
_D  F ) `  t )  _d t )
188 itg0 21226 . . . . . . . . 9  |-  S. (/) ( ( RR  _D  F ) `  t
)  _d t  =  0
189187, 188syl6eq 2485 . . . . . . . 8  |-  ( x  =  A  ->  S. ( A (,) x ) ( ( RR  _D  F ) `  t
)  _d t  =  0 )
190 fveq2 5684 . . . . . . . 8  |-  ( x  =  A  ->  ( F `  x )  =  ( F `  A ) )
191189, 190oveq12d 6104 . . . . . . 7  |-  ( x  =  A  ->  ( S. ( A (,) x
) ( ( RR 
_D  F ) `  t )  _d t  -  ( F `  x ) )  =  ( 0  -  ( F `  A )
) )
192 df-neg 9590 . . . . . . 7  |-  -u ( F `  A )  =  ( 0  -  ( F `  A
) )
193191, 192syl6eqr 2487 . . . . . 6  |-  ( x  =  A  ->  ( S. ( A (,) x
) ( ( RR 
_D  F ) `  t )  _d t  -  ( F `  x ) )  = 
-u ( F `  A ) )
194 negex 9600 . . . . . 6  |-  -u ( F `  A )  e.  _V
195193, 176, 194fvmpt 5767 . . . . 5  |-  ( A  e.  ( A [,] B )  ->  (
( x  e.  ( A [,] B ) 
|->  ( S. ( A (,) x ) ( ( RR  _D  F
) `  t )  _d t  -  ( F `  x )
) ) `  A
)  =  -u ( F `  A )
)
196182, 195syl 16 . . . 4  |-  ( ph  ->  ( ( x  e.  ( A [,] B
)  |->  ( S. ( A (,) x ) ( ( RR  _D  F ) `  t
)  _d t  -  ( F `  x ) ) ) `  A
)  =  -u ( F `  A )
)
19710, 180, 1963eqtr3d 2477 . . 3  |-  ( ph  ->  ( S. ( A (,) B ) ( ( RR  _D  F
) `  t )  _d t  -  ( F `  B )
)  =  -u ( F `  A )
)
198197oveq2d 6102 . 2  |-  ( ph  ->  ( ( F `  B )  +  ( S. ( A (,) B ) ( ( RR  _D  F ) `
 t )  _d t  -  ( F `
 B ) ) )  =  ( ( F `  B )  +  -u ( F `  A ) ) )
199121, 7ffvelrnd 5837 . . 3  |-  ( ph  ->  ( F `  B
)  e.  CC )
20057a1i 11 . . . 4  |-  ( (
ph  /\  t  e.  ( A (,) B ) )  ->  ( ( RR  _D  F ) `  t )  e.  _V )
201200, 60itgcl 21230 . . 3  |-  ( ph  ->  S. ( A (,) B ) ( ( RR  _D  F ) `
 t )  _d t  e.  CC )
202199, 201pncan3d 9714 . 2  |-  ( ph  ->  ( ( F `  B )  +  ( S. ( A (,) B ) ( ( RR  _D  F ) `
 t )  _d t  -  ( F `
 B ) ) )  =  S. ( A (,) B ) ( ( RR  _D  F ) `  t
)  _d t )
203121, 182ffvelrnd 5837 . . 3  |-  ( ph  ->  ( F `  A
)  e.  CC )
204199, 203negsubd 9717 . 2  |-  ( ph  ->  ( ( F `  B )  +  -u ( F `  A ) )  =  ( ( F `  B )  -  ( F `  A ) ) )
205198, 202, 2043eqtr3d 2477 1  |-  ( ph  ->  S. ( A (,) B ) ( ( RR  _D  F ) `
 t )  _d t  =  ( ( F `  B )  -  ( F `  A ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756   E.wrex 2710   _Vcvv 2966   [_csb 3281    C_ wss 3321   (/)c0 3630   ifcif 3784   ~Pcpw 3853   {csn 3870   {cpr 3872   <.cop 3876   class class class wbr 4285    e. cmpt 4343    X. cxp 4830   dom cdm 4832   ran crn 4833    |` cres 4834   "cima 4835   Fun wfun 5405   -->wf 5407   ` cfv 5411  (class class class)co 6086   1stc1st 6570   2ndc2nd 6571   CCcc 9272   RRcr 9273   0cc0 9274    + caddc 9277    x. cmul 9279   RR*cxr 9409    < clt 9410    <_ cle 9411    - cmin 9587   -ucneg 9588   (,)cioo 11292   [,]cicc 11295   *ccj 12577   abscabs 12715   TopOpenctopn 14352   topGenctg 14368  ℂfldccnfld 17787   intcnt 18590    Cn ccn 18797    tX ctx 19102   -cn->ccncf 20421   volcvol 20916  MblFncmbf 21063   S.2citg2 21065   L^1cibl 21066   S.citg 21067    _D cdv 21307
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-rep 4396  ax-sep 4406  ax-nul 4414  ax-pow 4463  ax-pr 4524  ax-un 6367  ax-inf2 7839  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351  ax-pre-sup 9352  ax-addf 9353  ax-mulf 9354
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3282  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3631  df-if 3785  df-pw 3855  df-sn 3871  df-pr 3873  df-tp 3875  df-op 3877  df-uni 4085  df-int 4122  df-iun 4166  df-iin 4167  df-disj 4256  df-br 4286  df-opab 4344  df-mpt 4345  df-tr 4379  df-eprel 4624  df-id 4628  df-po 4633  df-so 4634  df-fr 4671  df-se 4672  df-we 4673  df-ord 4714  df-on 4715  df-lim 4716  df-suc 4717  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5374  df-fun 5413  df-fn 5414  df-f 5415  df-f1 5416  df-fo 5417  df-f1o 5418  df-fv 5419  df-isom 5420  df-riota 6045  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-of 6315  df-ofr 6316  df-om 6472  df-1st 6572  df-2nd 6573  df-supp 6686  df-recs 6824  df-rdg 6858  df-1o 6912  df-2o 6913  df-oadd 6916  df-omul 6917  df-er 7093  df-map 7208  df-pm 7209  df-ixp 7256  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-fsupp 7613  df-fi 7653  df-sup 7683  df-oi 7716  df-card 8101  df-acn 8104  df-cda 8329  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-div 9986  df-nn 10315  df-2 10372  df-3 10373  df-4 10374  df-5 10375  df-6 10376  df-7 10377  df-8 10378  df-9 10379  df-10 10380  df-n0 10572  df-z 10639  df-dec 10748  df-uz 10854  df-q 10946  df-rp 10984  df-xneg 11081  df-xadd 11082  df-xmul 11083  df-ioo 11296  df-ico 11298  df-icc 11299  df-fz 11430  df-fzo 11541  df-fl 11634  df-mod 11701  df-seq 11799  df-exp 11858  df-hash 12096  df-cj 12580  df-re 12581  df-im 12582  df-sqr 12716  df-abs 12717  df-clim 12958  df-rlim 12959  df-sum 13156  df-struct 14168  df-ndx 14169  df-slot 14170  df-base 14171  df-sets 14172  df-ress 14173  df-plusg 14243  df-mulr 14244  df-starv 14245  df-sca 14246  df-vsca 14247  df-ip 14248  df-tset 14249  df-ple 14250  df-ds 14252  df-unif 14253  df-hom 14254  df-cco 14255  df-rest 14353  df-topn 14354  df-0g 14372  df-gsum 14373  df-topgen 14374  df-pt 14375  df-prds 14378  df-xrs 14432  df-qtop 14437  df-imas 14438  df-xps 14440  df-mre 14516  df-mrc 14517  df-acs 14519  df-mnd 15407  df-submnd 15457  df-mulg 15537  df-cntz 15824  df-cmn 16268  df-psmet 17778  df-xmet 17779  df-met 17780  df-bl 17781  df-mopn 17782  df-fbas 17783  df-fg 17784  df-cnfld 17788  df-top 18472  df-bases 18474  df-topon 18475  df-topsp 18476  df-cld 18592  df-ntr 18593  df-cls 18594  df-nei 18671  df-lp 18709  df-perf 18710  df-cn 18800  df-cnp 18801  df-haus 18888  df-cmp 18959  df-tx 19104  df-hmeo 19297  df-fil 19388  df-fm 19480  df-flim 19481  df-flf 19482  df-xms 19864  df-ms 19865  df-tms 19866  df-cncf 20423  df-ovol 20917  df-vol 20918  df-mbf 21068  df-itg1 21069  df-itg2 21070  df-ibl 21071  df-itg 21072  df-0p 21117  df-limc 21310  df-dv 21311
This theorem is referenced by:  areacirc  28432
  Copyright terms: Public domain W3C validator