Users' Mathboxes Mathbox for Jon Pennant < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  areaquad Structured version   Unicode version

Theorem areaquad 35528
Description: The area of a quadrilateral with two sides which are parallel to the y-axis in  ( RR  X.  RR ) is its width multiplied by the average height of its higher edge minus the average height of its lower edge. Co-author TA. (Contributed by Jon Pennant, 31-May-2019.)
Hypotheses
Ref Expression
areaquad.1  |-  A  e.  RR
areaquad.2  |-  B  e.  RR
areaquad.3  |-  C  e.  RR
areaquad.4  |-  D  e.  RR
areaquad.5  |-  E  e.  RR
areaquad.6  |-  F  e.  RR
areaquad.7  |-  A  < 
B
areaquad.8  |-  C  <_  E
areaquad.9  |-  D  <_  F
areaquad.10  |-  U  =  ( C  +  ( ( ( x  -  A )  /  ( B  -  A )
)  x.  ( D  -  C ) ) )
areaquad.11  |-  V  =  ( E  +  ( ( ( x  -  A )  /  ( B  -  A )
)  x.  ( F  -  E ) ) )
areaquad.12  |-  S  =  { <. x ,  y
>.  |  ( x  e.  ( A [,] B
)  /\  y  e.  ( U [,] V ) ) }
Assertion
Ref Expression
areaquad  |-  (area `  S )  =  ( ( ( ( F  +  E )  / 
2 )  -  (
( D  +  C
)  /  2 ) )  x.  ( B  -  A ) )
Distinct variable groups:    x, y, A    x, B, y    x, C    x, D    x, E    x, F    x, S    y, U    y, V
Allowed substitution hints:    C( y)    D( y)    S( y)    U( x)    E( y)    F( y)    V( x)

Proof of Theorem areaquad
StepHypRef Expression
1 areaquad.1 . . . . . . . . . 10  |-  A  e.  RR
2 areaquad.2 . . . . . . . . . 10  |-  B  e.  RR
3 iccssre 11658 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  C_  RR )
41, 2, 3mp2an 670 . . . . . . . . 9  |-  ( A [,] B )  C_  RR
54sseli 3437 . . . . . . . 8  |-  ( x  e.  ( A [,] B )  ->  x  e.  RR )
65adantr 463 . . . . . . 7  |-  ( ( x  e.  ( A [,] B )  /\  y  e.  ( U [,] V ) )  ->  x  e.  RR )
7 areaquad.3 . . . . . . . . . . . . . . . 16  |-  C  e.  RR
87recni 9637 . . . . . . . . . . . . . . 15  |-  C  e.  CC
98a1i 11 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  C  e.  CC )
10 resubcl 9918 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  RR  /\  A  e.  RR )  ->  ( x  -  A
)  e.  RR )
111, 10mpan2 669 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  RR  ->  (
x  -  A )  e.  RR )
122, 1resubcli 9916 . . . . . . . . . . . . . . . . . 18  |-  ( B  -  A )  e.  RR
1312a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  RR  ->  ( B  -  A )  e.  RR )
142recni 9637 . . . . . . . . . . . . . . . . . . . . 21  |-  B  e.  CC
1514a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( A  e.  RR  ->  B  e.  CC )
16 recn 9611 . . . . . . . . . . . . . . . . . . . 20  |-  ( A  e.  RR  ->  A  e.  CC )
17 areaquad.7 . . . . . . . . . . . . . . . . . . . . . 22  |-  A  < 
B
181, 17gtneii 9727 . . . . . . . . . . . . . . . . . . . . 21  |-  B  =/= 
A
1918a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( A  e.  RR  ->  B  =/=  A )
2015, 16, 19subne0d 9975 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  RR  ->  ( B  -  A )  =/=  0 )
211, 20ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ( B  -  A )  =/=  0
2221a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  RR  ->  ( B  -  A )  =/=  0 )
2311, 13, 22redivcld 10412 . . . . . . . . . . . . . . . 16  |-  ( x  e.  RR  ->  (
( x  -  A
)  /  ( B  -  A ) )  e.  RR )
2423recnd 9651 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  (
( x  -  A
)  /  ( B  -  A ) )  e.  CC )
25 areaquad.4 . . . . . . . . . . . . . . . . 17  |-  D  e.  RR
2625recni 9637 . . . . . . . . . . . . . . . 16  |-  D  e.  CC
2726a1i 11 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  D  e.  CC )
2824, 27mulcld 9645 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  (
( ( x  -  A )  /  ( B  -  A )
)  x.  D )  e.  CC )
2924, 9mulcld 9645 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  (
( ( x  -  A )  /  ( B  -  A )
)  x.  C )  e.  CC )
309, 28, 29addsub12d 9989 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  ( C  +  ( (
( ( x  -  A )  /  ( B  -  A )
)  x.  D )  -  ( ( ( x  -  A )  /  ( B  -  A ) )  x.  C ) ) )  =  ( ( ( ( x  -  A
)  /  ( B  -  A ) )  x.  D )  +  ( C  -  (
( ( x  -  A )  /  ( B  -  A )
)  x.  C ) ) ) )
31 areaquad.10 . . . . . . . . . . . . . 14  |-  U  =  ( C  +  ( ( ( x  -  A )  /  ( B  -  A )
)  x.  ( D  -  C ) ) )
3224, 27, 9subdid 10052 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  (
( ( x  -  A )  /  ( B  -  A )
)  x.  ( D  -  C ) )  =  ( ( ( ( x  -  A
)  /  ( B  -  A ) )  x.  D )  -  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  C
) ) )
3332oveq2d 6293 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  ( C  +  ( (
( x  -  A
)  /  ( B  -  A ) )  x.  ( D  -  C ) ) )  =  ( C  +  ( ( ( ( x  -  A )  /  ( B  -  A ) )  x.  D )  -  (
( ( x  -  A )  /  ( B  -  A )
)  x.  C ) ) ) )
3431, 33syl5eq 2455 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  U  =  ( C  +  ( ( ( ( x  -  A )  /  ( B  -  A ) )  x.  D )  -  (
( ( x  -  A )  /  ( B  -  A )
)  x.  C ) ) ) )
35 1cnd 9641 . . . . . . . . . . . . . . . 16  |-  ( x  e.  RR  ->  1  e.  CC )
3635, 24, 9subdird 10053 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  (
( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) )  x.  C )  =  ( ( 1  x.  C )  -  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  C
) ) )
378mulid2i 9628 . . . . . . . . . . . . . . . 16  |-  ( 1  x.  C )  =  C
3837oveq1i 6287 . . . . . . . . . . . . . . 15  |-  ( ( 1  x.  C )  -  ( ( ( x  -  A )  /  ( B  -  A ) )  x.  C ) )  =  ( C  -  (
( ( x  -  A )  /  ( B  -  A )
)  x.  C ) )
3936, 38syl6eq 2459 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  (
( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) )  x.  C )  =  ( C  -  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  C
) ) )
4039oveq2d 6293 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  (
( ( ( x  -  A )  / 
( B  -  A
) )  x.  D
)  +  ( ( 1  -  ( ( x  -  A )  /  ( B  -  A ) ) )  x.  C ) )  =  ( ( ( ( x  -  A
)  /  ( B  -  A ) )  x.  D )  +  ( C  -  (
( ( x  -  A )  /  ( B  -  A )
)  x.  C ) ) ) )
4130, 34, 403eqtr4d 2453 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  U  =  ( ( ( ( x  -  A
)  /  ( B  -  A ) )  x.  D )  +  ( ( 1  -  ( ( x  -  A )  /  ( B  -  A )
) )  x.  C
) ) )
42 1red 9640 . . . . . . . . . . . . . . . 16  |-  ( x  e.  RR  ->  1  e.  RR )
4342, 23resubcld 10027 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  (
1  -  ( ( x  -  A )  /  ( B  -  A ) ) )  e.  RR )
4443recnd 9651 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  (
1  -  ( ( x  -  A )  /  ( B  -  A ) ) )  e.  CC )
4544, 9mulcld 9645 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  (
( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) )  x.  C )  e.  CC )
4628, 45addcomd 9815 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  (
( ( ( x  -  A )  / 
( B  -  A
) )  x.  D
)  +  ( ( 1  -  ( ( x  -  A )  /  ( B  -  A ) ) )  x.  C ) )  =  ( ( ( 1  -  ( ( x  -  A )  /  ( B  -  A ) ) )  x.  C )  +  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  D
) ) )
4744, 9mulcomd 9646 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  (
( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) )  x.  C )  =  ( C  x.  ( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) ) ) )
4824, 27mulcomd 9646 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  (
( ( x  -  A )  /  ( B  -  A )
)  x.  D )  =  ( D  x.  ( ( x  -  A )  /  ( B  -  A )
) ) )
4947, 48oveq12d 6295 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  (
( ( 1  -  ( ( x  -  A )  /  ( B  -  A )
) )  x.  C
)  +  ( ( ( x  -  A
)  /  ( B  -  A ) )  x.  D ) )  =  ( ( C  x.  ( 1  -  ( ( x  -  A )  /  ( B  -  A )
) ) )  +  ( D  x.  (
( x  -  A
)  /  ( B  -  A ) ) ) ) )
5041, 46, 493eqtrd 2447 . . . . . . . . . . 11  |-  ( x  e.  RR  ->  U  =  ( ( C  x.  ( 1  -  ( ( x  -  A )  /  ( B  -  A )
) ) )  +  ( D  x.  (
( x  -  A
)  /  ( B  -  A ) ) ) ) )
517a1i 11 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  C  e.  RR )
5251, 43remulcld 9653 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  ( C  x.  ( 1  -  ( ( x  -  A )  / 
( B  -  A
) ) ) )  e.  RR )
5325a1i 11 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  D  e.  RR )
5453, 23remulcld 9653 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  ( D  x.  ( (
x  -  A )  /  ( B  -  A ) ) )  e.  RR )
5552, 54readdcld 9652 . . . . . . . . . . 11  |-  ( x  e.  RR  ->  (
( C  x.  (
1  -  ( ( x  -  A )  /  ( B  -  A ) ) ) )  +  ( D  x.  ( ( x  -  A )  / 
( B  -  A
) ) ) )  e.  RR )
5650, 55eqeltrd 2490 . . . . . . . . . 10  |-  ( x  e.  RR  ->  U  e.  RR )
57 areaquad.5 . . . . . . . . . . . . . . . 16  |-  E  e.  RR
5857recni 9637 . . . . . . . . . . . . . . 15  |-  E  e.  CC
5958a1i 11 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  E  e.  CC )
60 areaquad.6 . . . . . . . . . . . . . . . . 17  |-  F  e.  RR
6160recni 9637 . . . . . . . . . . . . . . . 16  |-  F  e.  CC
6261a1i 11 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  F  e.  CC )
6324, 62mulcld 9645 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  (
( ( x  -  A )  /  ( B  -  A )
)  x.  F )  e.  CC )
6424, 59mulcld 9645 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  (
( ( x  -  A )  /  ( B  -  A )
)  x.  E )  e.  CC )
6559, 63, 64addsub12d 9989 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  ( E  +  ( (
( ( x  -  A )  /  ( B  -  A )
)  x.  F )  -  ( ( ( x  -  A )  /  ( B  -  A ) )  x.  E ) ) )  =  ( ( ( ( x  -  A
)  /  ( B  -  A ) )  x.  F )  +  ( E  -  (
( ( x  -  A )  /  ( B  -  A )
)  x.  E ) ) ) )
66 areaquad.11 . . . . . . . . . . . . . 14  |-  V  =  ( E  +  ( ( ( x  -  A )  /  ( B  -  A )
)  x.  ( F  -  E ) ) )
6724, 62, 59subdid 10052 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  (
( ( x  -  A )  /  ( B  -  A )
)  x.  ( F  -  E ) )  =  ( ( ( ( x  -  A
)  /  ( B  -  A ) )  x.  F )  -  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  E
) ) )
6867oveq2d 6293 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  ( E  +  ( (
( x  -  A
)  /  ( B  -  A ) )  x.  ( F  -  E ) ) )  =  ( E  +  ( ( ( ( x  -  A )  /  ( B  -  A ) )  x.  F )  -  (
( ( x  -  A )  /  ( B  -  A )
)  x.  E ) ) ) )
6966, 68syl5eq 2455 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  V  =  ( E  +  ( ( ( ( x  -  A )  /  ( B  -  A ) )  x.  F )  -  (
( ( x  -  A )  /  ( B  -  A )
)  x.  E ) ) ) )
7035, 24, 59subdird 10053 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  (
( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) )  x.  E )  =  ( ( 1  x.  E )  -  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  E
) ) )
7158mulid2i 9628 . . . . . . . . . . . . . . . 16  |-  ( 1  x.  E )  =  E
7271oveq1i 6287 . . . . . . . . . . . . . . 15  |-  ( ( 1  x.  E )  -  ( ( ( x  -  A )  /  ( B  -  A ) )  x.  E ) )  =  ( E  -  (
( ( x  -  A )  /  ( B  -  A )
)  x.  E ) )
7370, 72syl6eq 2459 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  (
( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) )  x.  E )  =  ( E  -  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  E
) ) )
7473oveq2d 6293 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  (
( ( ( x  -  A )  / 
( B  -  A
) )  x.  F
)  +  ( ( 1  -  ( ( x  -  A )  /  ( B  -  A ) ) )  x.  E ) )  =  ( ( ( ( x  -  A
)  /  ( B  -  A ) )  x.  F )  +  ( E  -  (
( ( x  -  A )  /  ( B  -  A )
)  x.  E ) ) ) )
7565, 69, 743eqtr4d 2453 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  V  =  ( ( ( ( x  -  A
)  /  ( B  -  A ) )  x.  F )  +  ( ( 1  -  ( ( x  -  A )  /  ( B  -  A )
) )  x.  E
) ) )
7644, 59mulcld 9645 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  (
( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) )  x.  E )  e.  CC )
7763, 76addcomd 9815 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  (
( ( ( x  -  A )  / 
( B  -  A
) )  x.  F
)  +  ( ( 1  -  ( ( x  -  A )  /  ( B  -  A ) ) )  x.  E ) )  =  ( ( ( 1  -  ( ( x  -  A )  /  ( B  -  A ) ) )  x.  E )  +  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  F
) ) )
7844, 59mulcomd 9646 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  (
( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) )  x.  E )  =  ( E  x.  ( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) ) ) )
7924, 62mulcomd 9646 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  (
( ( x  -  A )  /  ( B  -  A )
)  x.  F )  =  ( F  x.  ( ( x  -  A )  /  ( B  -  A )
) ) )
8078, 79oveq12d 6295 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  (
( ( 1  -  ( ( x  -  A )  /  ( B  -  A )
) )  x.  E
)  +  ( ( ( x  -  A
)  /  ( B  -  A ) )  x.  F ) )  =  ( ( E  x.  ( 1  -  ( ( x  -  A )  /  ( B  -  A )
) ) )  +  ( F  x.  (
( x  -  A
)  /  ( B  -  A ) ) ) ) )
8175, 77, 803eqtrd 2447 . . . . . . . . . . 11  |-  ( x  e.  RR  ->  V  =  ( ( E  x.  ( 1  -  ( ( x  -  A )  /  ( B  -  A )
) ) )  +  ( F  x.  (
( x  -  A
)  /  ( B  -  A ) ) ) ) )
8257a1i 11 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  E  e.  RR )
8382, 43remulcld 9653 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  ( E  x.  ( 1  -  ( ( x  -  A )  / 
( B  -  A
) ) ) )  e.  RR )
8460a1i 11 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  F  e.  RR )
8584, 23remulcld 9653 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  ( F  x.  ( (
x  -  A )  /  ( B  -  A ) ) )  e.  RR )
8683, 85readdcld 9652 . . . . . . . . . . 11  |-  ( x  e.  RR  ->  (
( E  x.  (
1  -  ( ( x  -  A )  /  ( B  -  A ) ) ) )  +  ( F  x.  ( ( x  -  A )  / 
( B  -  A
) ) ) )  e.  RR )
8781, 86eqeltrd 2490 . . . . . . . . . 10  |-  ( x  e.  RR  ->  V  e.  RR )
88 iccssre 11658 . . . . . . . . . 10  |-  ( ( U  e.  RR  /\  V  e.  RR )  ->  ( U [,] V
)  C_  RR )
8956, 87, 88syl2anc 659 . . . . . . . . 9  |-  ( x  e.  RR  ->  ( U [,] V )  C_  RR )
905, 89syl 17 . . . . . . . 8  |-  ( x  e.  ( A [,] B )  ->  ( U [,] V )  C_  RR )
9190sselda 3441 . . . . . . 7  |-  ( ( x  e.  ( A [,] B )  /\  y  e.  ( U [,] V ) )  -> 
y  e.  RR )
926, 91jca 530 . . . . . 6  |-  ( ( x  e.  ( A [,] B )  /\  y  e.  ( U [,] V ) )  -> 
( x  e.  RR  /\  y  e.  RR ) )
9392ssopab2i 4717 . . . . 5  |-  { <. x ,  y >.  |  ( x  e.  ( A [,] B )  /\  y  e.  ( U [,] V ) ) } 
C_  { <. x ,  y >.  |  ( x  e.  RR  /\  y  e.  RR ) }
94 areaquad.12 . . . . 5  |-  S  =  { <. x ,  y
>.  |  ( x  e.  ( A [,] B
)  /\  y  e.  ( U [,] V ) ) }
95 df-xp 4828 . . . . 5  |-  ( RR 
X.  RR )  =  { <. x ,  y
>.  |  ( x  e.  RR  /\  y  e.  RR ) }
9693, 94, 953sstr4i 3480 . . . 4  |-  S  C_  ( RR  X.  RR )
97 iftrue 3890 . . . . . . . . . 10  |-  ( x  e.  ( A [,] B )  ->  if ( x  e.  ( A [,] B ) ,  ( V  -  U
) ,  0 )  =  ( V  -  U ) )
98 nfv 1728 . . . . . . . . . . . . 13  |-  F/ y  x  e.  ( A [,] B )
99 nfopab2 4461 . . . . . . . . . . . . . . 15  |-  F/_ y { <. x ,  y
>.  |  ( x  e.  ( A [,] B
)  /\  y  e.  ( U [,] V ) ) }
10094, 99nfcxfr 2562 . . . . . . . . . . . . . 14  |-  F/_ y S
101 nfcv 2564 . . . . . . . . . . . . . 14  |-  F/_ y { x }
102100, 101nfima 5164 . . . . . . . . . . . . 13  |-  F/_ y
( S " {
x } )
103 nfcv 2564 . . . . . . . . . . . . 13  |-  F/_ y
( U [,] V
)
104 vex 3061 . . . . . . . . . . . . . . . 16  |-  x  e. 
_V
105 vex 3061 . . . . . . . . . . . . . . . 16  |-  y  e. 
_V
106104, 105elimasn 5181 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( S " { x } )  <->  <. x ,  y >.  e.  S )
10794eleq2i 2480 . . . . . . . . . . . . . . 15  |-  ( <.
x ,  y >.  e.  S  <->  <. x ,  y
>.  e.  { <. x ,  y >.  |  ( x  e.  ( A [,] B )  /\  y  e.  ( U [,] V ) ) } )
108 opabid 4696 . . . . . . . . . . . . . . 15  |-  ( <.
x ,  y >.  e.  { <. x ,  y
>.  |  ( x  e.  ( A [,] B
)  /\  y  e.  ( U [,] V ) ) }  <->  ( x  e.  ( A [,] B
)  /\  y  e.  ( U [,] V ) ) )
109106, 107, 1083bitri 271 . . . . . . . . . . . . . 14  |-  ( y  e.  ( S " { x } )  <-> 
( x  e.  ( A [,] B )  /\  y  e.  ( U [,] V ) ) )
110109baib 904 . . . . . . . . . . . . 13  |-  ( x  e.  ( A [,] B )  ->  (
y  e.  ( S
" { x }
)  <->  y  e.  ( U [,] V ) ) )
11198, 102, 103, 110eqrd 3459 . . . . . . . . . . . 12  |-  ( x  e.  ( A [,] B )  ->  ( S " { x }
)  =  ( U [,] V ) )
112111fveq2d 5852 . . . . . . . . . . 11  |-  ( x  e.  ( A [,] B )  ->  ( vol `  ( S " { x } ) )  =  ( vol `  ( U [,] V
) ) )
1135, 56syl 17 . . . . . . . . . . . . 13  |-  ( x  e.  ( A [,] B )  ->  U  e.  RR )
1145, 87syl 17 . . . . . . . . . . . . 13  |-  ( x  e.  ( A [,] B )  ->  V  e.  RR )
115 iccmbl 22266 . . . . . . . . . . . . 13  |-  ( ( U  e.  RR  /\  V  e.  RR )  ->  ( U [,] V
)  e.  dom  vol )
116113, 114, 115syl2anc 659 . . . . . . . . . . . 12  |-  ( x  e.  ( A [,] B )  ->  ( U [,] V )  e. 
dom  vol )
117 mblvol 22231 . . . . . . . . . . . 12  |-  ( ( U [,] V )  e.  dom  vol  ->  ( vol `  ( U [,] V ) )  =  ( vol* `  ( U [,] V
) ) )
118116, 117syl 17 . . . . . . . . . . 11  |-  ( x  e.  ( A [,] B )  ->  ( vol `  ( U [,] V ) )  =  ( vol* `  ( U [,] V ) ) )
1195, 52syl 17 . . . . . . . . . . . . . 14  |-  ( x  e.  ( A [,] B )  ->  ( C  x.  ( 1  -  ( ( x  -  A )  / 
( B  -  A
) ) ) )  e.  RR )
1205, 54syl 17 . . . . . . . . . . . . . 14  |-  ( x  e.  ( A [,] B )  ->  ( D  x.  ( (
x  -  A )  /  ( B  -  A ) ) )  e.  RR )
1215, 83syl 17 . . . . . . . . . . . . . 14  |-  ( x  e.  ( A [,] B )  ->  ( E  x.  ( 1  -  ( ( x  -  A )  / 
( B  -  A
) ) ) )  e.  RR )
1225, 85syl 17 . . . . . . . . . . . . . 14  |-  ( x  e.  ( A [,] B )  ->  ( F  x.  ( (
x  -  A )  /  ( B  -  A ) ) )  e.  RR )
1237a1i 11 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( A [,] B )  ->  C  e.  RR )
12457a1i 11 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( A [,] B )  ->  E  e.  RR )
1255, 43syl 17 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( A [,] B )  ->  (
1  -  ( ( x  -  A )  /  ( B  -  A ) ) )  e.  RR )
1265, 23syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( A [,] B )  ->  (
( x  -  A
)  /  ( B  -  A ) )  e.  RR )
127126recnd 9651 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( A [,] B )  ->  (
( x  -  A
)  /  ( B  -  A ) )  e.  CC )
128127subidd 9954 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( A [,] B )  ->  (
( ( x  -  A )  /  ( B  -  A )
)  -  ( ( x  -  A )  /  ( B  -  A ) ) )  =  0 )
129 1red 9640 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( A [,] B )  ->  1  e.  RR )
1302a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( A [,] B )  ->  B  e.  RR )
1311a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( A [,] B )  ->  A  e.  RR )
1321rexri 9675 . . . . . . . . . . . . . . . . . . . . 21  |-  A  e. 
RR*
1332rexri 9675 . . . . . . . . . . . . . . . . . . . . 21  |-  B  e. 
RR*
134 iccleub 11632 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  x  e.  ( A [,] B
) )  ->  x  <_  B )
135132, 133, 134mp3an12 1316 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( A [,] B )  ->  x  <_  B )
1365, 130, 131, 135lesub1dd 10207 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( A [,] B )  ->  (
x  -  A )  <_  ( B  -  A ) )
1375, 1, 10sylancl 660 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( A [,] B )  ->  (
x  -  A )  e.  RR )
13812a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( A [,] B )  ->  ( B  -  A )  e.  RR )
1391recni 9637 . . . . . . . . . . . . . . . . . . . . . 22  |-  A  e.  CC
140139subidi 9925 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A  -  A )  =  0
141131, 130, 131ltsub1d 10200 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( A [,] B )  ->  ( A  <  B  <->  ( A  -  A )  <  ( B  -  A )
) )
14217, 141mpbii 211 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( A [,] B )  ->  ( A  -  A )  <  ( B  -  A
) )
143140, 142syl5eqbrr 4428 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( A [,] B )  ->  0  <  ( B  -  A
) )
144 lediv1 10447 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( x  -  A
)  e.  RR  /\  ( B  -  A
)  e.  RR  /\  ( ( B  -  A )  e.  RR  /\  0  <  ( B  -  A ) ) )  ->  ( (
x  -  A )  <_  ( B  -  A )  <->  ( (
x  -  A )  /  ( B  -  A ) )  <_ 
( ( B  -  A )  /  ( B  -  A )
) ) )
145137, 138, 138, 143, 144syl112anc 1234 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( A [,] B )  ->  (
( x  -  A
)  <_  ( B  -  A )  <->  ( (
x  -  A )  /  ( B  -  A ) )  <_ 
( ( B  -  A )  /  ( B  -  A )
) ) )
146136, 145mpbid 210 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( A [,] B )  ->  (
( x  -  A
)  /  ( B  -  A ) )  <_  ( ( B  -  A )  / 
( B  -  A
) ) )
14712recni 9637 . . . . . . . . . . . . . . . . . . 19  |-  ( B  -  A )  e.  CC
148147, 21dividi 10317 . . . . . . . . . . . . . . . . . 18  |-  ( ( B  -  A )  /  ( B  -  A ) )  =  1
149146, 148syl6breq 4433 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( A [,] B )  ->  (
( x  -  A
)  /  ( B  -  A ) )  <_  1 )
150126, 129, 126, 149lesub1dd 10207 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( A [,] B )  ->  (
( ( x  -  A )  /  ( B  -  A )
)  -  ( ( x  -  A )  /  ( B  -  A ) ) )  <_  ( 1  -  ( ( x  -  A )  /  ( B  -  A )
) ) )
151128, 150eqbrtrrd 4416 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( A [,] B )  ->  0  <_  ( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) ) )
152 areaquad.8 . . . . . . . . . . . . . . . 16  |-  C  <_  E
153152a1i 11 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( A [,] B )  ->  C  <_  E )
154123, 124, 125, 151, 153lemul1ad 10524 . . . . . . . . . . . . . 14  |-  ( x  e.  ( A [,] B )  ->  ( C  x.  ( 1  -  ( ( x  -  A )  / 
( B  -  A
) ) ) )  <_  ( E  x.  ( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) ) ) )
15525a1i 11 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( A [,] B )  ->  D  e.  RR )
15660a1i 11 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( A [,] B )  ->  F  e.  RR )
157138, 143elrpd 11300 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( A [,] B )  ->  ( B  -  A )  e.  RR+ )
158 iccgelb 11633 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  x  e.  ( A [,] B
) )  ->  A  <_  x )
159132, 133, 158mp3an12 1316 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( A [,] B )  ->  A  <_  x )
160131, 5, 131, 159lesub1dd 10207 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( A [,] B )  ->  ( A  -  A )  <_  ( x  -  A
) )
161140, 160syl5eqbrr 4428 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( A [,] B )  ->  0  <_  ( x  -  A
) )
162137, 157, 161divge0d 11339 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( A [,] B )  ->  0  <_  ( ( x  -  A )  /  ( B  -  A )
) )
163 areaquad.9 . . . . . . . . . . . . . . . 16  |-  D  <_  F
164163a1i 11 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( A [,] B )  ->  D  <_  F )
165155, 156, 126, 162, 164lemul1ad 10524 . . . . . . . . . . . . . 14  |-  ( x  e.  ( A [,] B )  ->  ( D  x.  ( (
x  -  A )  /  ( B  -  A ) ) )  <_  ( F  x.  ( ( x  -  A )  /  ( B  -  A )
) ) )
166119, 120, 121, 122, 154, 165le2addd 10209 . . . . . . . . . . . . 13  |-  ( x  e.  ( A [,] B )  ->  (
( C  x.  (
1  -  ( ( x  -  A )  /  ( B  -  A ) ) ) )  +  ( D  x.  ( ( x  -  A )  / 
( B  -  A
) ) ) )  <_  ( ( E  x.  ( 1  -  ( ( x  -  A )  /  ( B  -  A )
) ) )  +  ( F  x.  (
( x  -  A
)  /  ( B  -  A ) ) ) ) )
1675, 50syl 17 . . . . . . . . . . . . 13  |-  ( x  e.  ( A [,] B )  ->  U  =  ( ( C  x.  ( 1  -  ( ( x  -  A )  /  ( B  -  A )
) ) )  +  ( D  x.  (
( x  -  A
)  /  ( B  -  A ) ) ) ) )
1685, 81syl 17 . . . . . . . . . . . . 13  |-  ( x  e.  ( A [,] B )  ->  V  =  ( ( E  x.  ( 1  -  ( ( x  -  A )  /  ( B  -  A )
) ) )  +  ( F  x.  (
( x  -  A
)  /  ( B  -  A ) ) ) ) )
169166, 167, 1683brtr4d 4424 . . . . . . . . . . . 12  |-  ( x  e.  ( A [,] B )  ->  U  <_  V )
170 ovolicc 22224 . . . . . . . . . . . 12  |-  ( ( U  e.  RR  /\  V  e.  RR  /\  U  <_  V )  ->  ( vol* `  ( U [,] V ) )  =  ( V  -  U ) )
171113, 114, 169, 170syl3anc 1230 . . . . . . . . . . 11  |-  ( x  e.  ( A [,] B )  ->  ( vol* `  ( U [,] V ) )  =  ( V  -  U ) )
172112, 118, 1713eqtrd 2447 . . . . . . . . . 10  |-  ( x  e.  ( A [,] B )  ->  ( vol `  ( S " { x } ) )  =  ( V  -  U ) )
17397, 172eqtr4d 2446 . . . . . . . . 9  |-  ( x  e.  ( A [,] B )  ->  if ( x  e.  ( A [,] B ) ,  ( V  -  U
) ,  0 )  =  ( vol `  ( S " { x }
) ) )
174 iffalse 3893 . . . . . . . . . 10  |-  ( -.  x  e.  ( A [,] B )  ->  if ( x  e.  ( A [,] B ) ,  ( V  -  U ) ,  0 )  =  0 )
175 nfv 1728 . . . . . . . . . . . . 13  |-  F/ y  -.  x  e.  ( A [,] B )
176 nfcv 2564 . . . . . . . . . . . . 13  |-  F/_ y (/)
177109simplbi 458 . . . . . . . . . . . . . 14  |-  ( y  e.  ( S " { x } )  ->  x  e.  ( A [,] B ) )
178 noel 3741 . . . . . . . . . . . . . . 15  |-  -.  y  e.  (/)
179178pm2.21i 131 . . . . . . . . . . . . . 14  |-  ( y  e.  (/)  ->  x  e.  ( A [,] B ) )
180177, 179pm5.21ni 350 . . . . . . . . . . . . 13  |-  ( -.  x  e.  ( A [,] B )  -> 
( y  e.  ( S " { x } )  <->  y  e.  (/) ) )
181175, 102, 176, 180eqrd 3459 . . . . . . . . . . . 12  |-  ( -.  x  e.  ( A [,] B )  -> 
( S " {
x } )  =  (/) )
182181fveq2d 5852 . . . . . . . . . . 11  |-  ( -.  x  e.  ( A [,] B )  -> 
( vol `  ( S " { x }
) )  =  ( vol `  (/) ) )
183 0mbl 22240 . . . . . . . . . . . . 13  |-  (/)  e.  dom  vol
184 mblvol 22231 . . . . . . . . . . . . 13  |-  ( (/)  e.  dom  vol  ->  ( vol `  (/) )  =  ( vol* `  (/) ) )
185183, 184ax-mp 5 . . . . . . . . . . . 12  |-  ( vol `  (/) )  =  ( vol* `  (/) )
186 ovol0 22194 . . . . . . . . . . . 12  |-  ( vol* `  (/) )  =  0
187185, 186eqtri 2431 . . . . . . . . . . 11  |-  ( vol `  (/) )  =  0
188182, 187syl6eq 2459 . . . . . . . . . 10  |-  ( -.  x  e.  ( A [,] B )  -> 
( vol `  ( S " { x }
) )  =  0 )
189174, 188eqtr4d 2446 . . . . . . . . 9  |-  ( -.  x  e.  ( A [,] B )  ->  if ( x  e.  ( A [,] B ) ,  ( V  -  U ) ,  0 )  =  ( vol `  ( S " {
x } ) ) )
190173, 189pm2.61i 164 . . . . . . . 8  |-  if ( x  e.  ( A [,] B ) ,  ( V  -  U
) ,  0 )  =  ( vol `  ( S " { x }
) )
191190eqcomi 2415 . . . . . . 7  |-  ( vol `  ( S " {
x } ) )  =  if ( x  e.  ( A [,] B ) ,  ( V  -  U ) ,  0 )
19287, 56resubcld 10027 . . . . . . . 8  |-  ( x  e.  RR  ->  ( V  -  U )  e.  RR )
193 0re 9625 . . . . . . . 8  |-  0  e.  RR
194 ifcl 3926 . . . . . . . 8  |-  ( ( ( V  -  U
)  e.  RR  /\  0  e.  RR )  ->  if ( x  e.  ( A [,] B
) ,  ( V  -  U ) ,  0 )  e.  RR )
195192, 193, 194sylancl 660 . . . . . . 7  |-  ( x  e.  RR  ->  if ( x  e.  ( A [,] B ) ,  ( V  -  U
) ,  0 )  e.  RR )
196191, 195syl5eqel 2494 . . . . . 6  |-  ( x  e.  RR  ->  ( vol `  ( S " { x } ) )  e.  RR )
197 volf 22230 . . . . . . . 8  |-  vol : dom  vol --> ( 0 [,] +oo )
198 ffun 5715 . . . . . . . 8  |-  ( vol
: dom  vol --> ( 0 [,] +oo )  ->  Fun  vol )
199197, 198ax-mp 5 . . . . . . 7  |-  Fun  vol
200 iftrue 3890 . . . . . . . . . 10  |-  ( x  e.  ( A [,] B )  ->  if ( x  e.  ( A [,] B ) ,  ( U [,] V
) ,  (/) )  =  ( U [,] V
) )
201111, 200eqtr4d 2446 . . . . . . . . 9  |-  ( x  e.  ( A [,] B )  ->  ( S " { x }
)  =  if ( x  e.  ( A [,] B ) ,  ( U [,] V
) ,  (/) ) )
202 iffalse 3893 . . . . . . . . . 10  |-  ( -.  x  e.  ( A [,] B )  ->  if ( x  e.  ( A [,] B ) ,  ( U [,] V ) ,  (/) )  =  (/) )
203181, 202eqtr4d 2446 . . . . . . . . 9  |-  ( -.  x  e.  ( A [,] B )  -> 
( S " {
x } )  =  if ( x  e.  ( A [,] B
) ,  ( U [,] V ) ,  (/) ) )
204201, 203pm2.61i 164 . . . . . . . 8  |-  ( S
" { x }
)  =  if ( x  e.  ( A [,] B ) ,  ( U [,] V
) ,  (/) )
20556, 87, 115syl2anc 659 . . . . . . . . 9  |-  ( x  e.  RR  ->  ( U [,] V )  e. 
dom  vol )
206183a1i 11 . . . . . . . . 9  |-  ( x  e.  RR  ->  (/)  e.  dom  vol )
207205, 206ifcld 3927 . . . . . . . 8  |-  ( x  e.  RR  ->  if ( x  e.  ( A [,] B ) ,  ( U [,] V
) ,  (/) )  e. 
dom  vol )
208204, 207syl5eqel 2494 . . . . . . 7  |-  ( x  e.  RR  ->  ( S " { x }
)  e.  dom  vol )
209 fvimacnv 5979 . . . . . . 7  |-  ( ( Fun  vol  /\  ( S " { x }
)  e.  dom  vol )  ->  ( ( vol `  ( S " {
x } ) )  e.  RR  <->  ( S " { x } )  e.  ( `' vol " RR ) ) )
210199, 208, 209sylancr 661 . . . . . 6  |-  ( x  e.  RR  ->  (
( vol `  ( S " { x }
) )  e.  RR  <->  ( S " { x } )  e.  ( `' vol " RR ) ) )
211196, 210mpbid 210 . . . . 5  |-  ( x  e.  RR  ->  ( S " { x }
)  e.  ( `' vol " RR ) )
212211rgen 2763 . . . 4  |-  A. x  e.  RR  ( S " { x } )  e.  ( `' vol " RR )
2134a1i 11 . . . . . 6  |-  ( 0  e.  RR  ->  ( A [,] B )  C_  RR )
214 rembl 22241 . . . . . . 7  |-  RR  e.  dom  vol
215214a1i 11 . . . . . 6  |-  ( 0  e.  RR  ->  RR  e.  dom  vol )
216114, 113resubcld 10027 . . . . . . . 8  |-  ( x  e.  ( A [,] B )  ->  ( V  -  U )  e.  RR )
217172, 216eqeltrd 2490 . . . . . . 7  |-  ( x  e.  ( A [,] B )  ->  ( vol `  ( S " { x } ) )  e.  RR )
218217adantl 464 . . . . . 6  |-  ( ( 0  e.  RR  /\  x  e.  ( A [,] B ) )  -> 
( vol `  ( S " { x }
) )  e.  RR )
219 eldifn 3565 . . . . . . . 8  |-  ( x  e.  ( RR  \ 
( A [,] B
) )  ->  -.  x  e.  ( A [,] B ) )
220219, 188syl 17 . . . . . . 7  |-  ( x  e.  ( RR  \ 
( A [,] B
) )  ->  ( vol `  ( S " { x } ) )  =  0 )
221220adantl 464 . . . . . 6  |-  ( ( 0  e.  RR  /\  x  e.  ( RR  \  ( A [,] B
) ) )  -> 
( vol `  ( S " { x }
) )  =  0 )
222172mpteq2ia 4476 . . . . . . . 8  |-  ( x  e.  ( A [,] B )  |->  ( vol `  ( S " {
x } ) ) )  =  ( x  e.  ( A [,] B )  |->  ( V  -  U ) )
223 eqid 2402 . . . . . . . . . . 11  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
224223subcn 21660 . . . . . . . . . . . 12  |-  -  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) )
225224a1i 11 . . . . . . . . . . 11  |-  ( T. 
->  -  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
)  Cn  ( TopOpen ` fld )
) )
22666mpteq2i 4477 . . . . . . . . . . . 12  |-  ( x  e.  ( A [,] B )  |->  V )  =  ( x  e.  ( A [,] B
)  |->  ( E  +  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  ( F  -  E )
) ) )
227223addcn 21659 . . . . . . . . . . . . . 14  |-  +  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) )
228227a1i 11 . . . . . . . . . . . . 13  |-  ( T. 
->  +  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
)  Cn  ( TopOpen ` fld )
) )
229 ax-resscn 9578 . . . . . . . . . . . . . . . 16  |-  RR  C_  CC
2304, 229sstri 3450 . . . . . . . . . . . . . . 15  |-  ( A [,] B )  C_  CC
231 ssid 3460 . . . . . . . . . . . . . . 15  |-  CC  C_  CC
232 cncfmptc 21705 . . . . . . . . . . . . . . 15  |-  ( ( E  e.  CC  /\  ( A [,] B ) 
C_  CC  /\  CC  C_  CC )  ->  ( x  e.  ( A [,] B )  |->  E )  e.  ( ( A [,] B ) -cn-> CC ) )
23358, 230, 231, 232mp3an 1326 . . . . . . . . . . . . . 14  |-  ( x  e.  ( A [,] B )  |->  E )  e.  ( ( A [,] B ) -cn-> CC )
234233a1i 11 . . . . . . . . . . . . 13  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  E )  e.  ( ( A [,] B
) -cn-> CC ) )
235230sseli 3437 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( A [,] B )  ->  x  e.  CC )
236139a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( A [,] B )  ->  A  e.  CC )
237147a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( A [,] B )  ->  ( B  -  A )  e.  CC )
23821a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( A [,] B )  ->  ( B  -  A )  =/=  0 )
239235, 236, 237, 238divsubdird 10399 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( A [,] B )  ->  (
( x  -  A
)  /  ( B  -  A ) )  =  ( ( x  /  ( B  -  A ) )  -  ( A  /  ( B  -  A )
) ) )
240239adantl 464 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  (
( x  -  A
)  /  ( B  -  A ) )  =  ( ( x  /  ( B  -  A ) )  -  ( A  /  ( B  -  A )
) ) )
241240mpteq2dva 4480 . . . . . . . . . . . . . . 15  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( ( x  -  A )  /  ( B  -  A )
) )  =  ( x  e.  ( A [,] B )  |->  ( ( x  /  ( B  -  A )
)  -  ( A  /  ( B  -  A ) ) ) ) )
242 resmpt 5142 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A [,] B ) 
C_  CC  ->  ( ( x  e.  CC  |->  ( x  /  ( B  -  A ) ) )  |`  ( A [,] B ) )  =  ( x  e.  ( A [,] B ) 
|->  ( x  /  ( B  -  A )
) ) )
243230, 242ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  CC  |->  ( x  /  ( B  -  A ) ) )  |`  ( A [,] B ) )  =  ( x  e.  ( A [,] B ) 
|->  ( x  /  ( B  -  A )
) )
244 eqid 2402 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  CC  |->  ( x  /  ( B  -  A ) ) )  =  ( x  e.  CC  |->  ( x  / 
( B  -  A
) ) )
245244divccncf 21700 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( B  -  A
)  e.  CC  /\  ( B  -  A
)  =/=  0 )  ->  ( x  e.  CC  |->  ( x  / 
( B  -  A
) ) )  e.  ( CC -cn-> CC ) )
246147, 21, 245mp2an 670 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  CC  |->  ( x  /  ( B  -  A ) ) )  e.  ( CC -cn-> CC )
247 rescncf 21691 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A [,] B ) 
C_  CC  ->  ( ( x  e.  CC  |->  ( x  /  ( B  -  A ) ) )  e.  ( CC
-cn-> CC )  ->  (
( x  e.  CC  |->  ( x  /  ( B  -  A )
) )  |`  ( A [,] B ) )  e.  ( ( A [,] B ) -cn-> CC ) ) )
248230, 246, 247mp2 9 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  CC  |->  ( x  /  ( B  -  A ) ) )  |`  ( A [,] B ) )  e.  ( ( A [,] B ) -cn-> CC )
249243, 248eqeltrri 2487 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( A [,] B )  |->  ( x  /  ( B  -  A ) ) )  e.  ( ( A [,] B ) -cn-> CC )
250249a1i 11 . . . . . . . . . . . . . . . 16  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( x  /  ( B  -  A )
) )  e.  ( ( A [,] B
) -cn-> CC ) )
251139, 147, 21divcli 10326 . . . . . . . . . . . . . . . . . 18  |-  ( A  /  ( B  -  A ) )  e.  CC
252 cncfmptc 21705 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  /  ( B  -  A )
)  e.  CC  /\  ( A [,] B ) 
C_  CC  /\  CC  C_  CC )  ->  ( x  e.  ( A [,] B )  |->  ( A  /  ( B  -  A ) ) )  e.  ( ( A [,] B ) -cn-> CC ) )
253251, 230, 231, 252mp3an 1326 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( A [,] B )  |->  ( A  /  ( B  -  A ) ) )  e.  ( ( A [,] B ) -cn-> CC )
254253a1i 11 . . . . . . . . . . . . . . . 16  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( A  /  ( B  -  A )
) )  e.  ( ( A [,] B
) -cn-> CC ) )
255223, 225, 250, 254cncfmpt2f 21708 . . . . . . . . . . . . . . 15  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( ( x  / 
( B  -  A
) )  -  ( A  /  ( B  -  A ) ) ) )  e.  ( ( A [,] B )
-cn-> CC ) )
256241, 255eqeltrd 2490 . . . . . . . . . . . . . 14  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( ( x  -  A )  /  ( B  -  A )
) )  e.  ( ( A [,] B
) -cn-> CC ) )
257 cncfmptc 21705 . . . . . . . . . . . . . . . . 17  |-  ( ( F  e.  CC  /\  ( A [,] B ) 
C_  CC  /\  CC  C_  CC )  ->  ( x  e.  ( A [,] B )  |->  F )  e.  ( ( A [,] B ) -cn-> CC ) )
25861, 230, 231, 257mp3an 1326 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( A [,] B )  |->  F )  e.  ( ( A [,] B ) -cn-> CC )
259258a1i 11 . . . . . . . . . . . . . . 15  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  F )  e.  ( ( A [,] B
) -cn-> CC ) )
260223, 225, 259, 234cncfmpt2f 21708 . . . . . . . . . . . . . 14  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( F  -  E
) )  e.  ( ( A [,] B
) -cn-> CC ) )
261256, 260mulcncf 22149 . . . . . . . . . . . . 13  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  ( F  -  E )
) )  e.  ( ( A [,] B
) -cn-> CC ) )
262223, 228, 234, 261cncfmpt2f 21708 . . . . . . . . . . . 12  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( E  +  ( ( ( x  -  A )  /  ( B  -  A )
)  x.  ( F  -  E ) ) ) )  e.  ( ( A [,] B
) -cn-> CC ) )
263226, 262syl5eqel 2494 . . . . . . . . . . 11  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  V )  e.  ( ( A [,] B
) -cn-> CC ) )
26431mpteq2i 4477 . . . . . . . . . . . 12  |-  ( x  e.  ( A [,] B )  |->  U )  =  ( x  e.  ( A [,] B
)  |->  ( C  +  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  ( D  -  C )
) ) )
265 cncfmptc 21705 . . . . . . . . . . . . . . 15  |-  ( ( C  e.  CC  /\  ( A [,] B ) 
C_  CC  /\  CC  C_  CC )  ->  ( x  e.  ( A [,] B )  |->  C )  e.  ( ( A [,] B ) -cn-> CC ) )
2668, 230, 231, 265mp3an 1326 . . . . . . . . . . . . . 14  |-  ( x  e.  ( A [,] B )  |->  C )  e.  ( ( A [,] B ) -cn-> CC )
267266a1i 11 . . . . . . . . . . . . 13  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  C )  e.  ( ( A [,] B
) -cn-> CC ) )
268 cncfmptc 21705 . . . . . . . . . . . . . . . . 17  |-  ( ( D  e.  CC  /\  ( A [,] B ) 
C_  CC  /\  CC  C_  CC )  ->  ( x  e.  ( A [,] B )  |->  D )  e.  ( ( A [,] B ) -cn-> CC ) )
26926, 230, 231, 268mp3an 1326 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( A [,] B )  |->  D )  e.  ( ( A [,] B ) -cn-> CC )
270269a1i 11 . . . . . . . . . . . . . . 15  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  D )  e.  ( ( A [,] B
) -cn-> CC ) )
271223, 225, 270, 267cncfmpt2f 21708 . . . . . . . . . . . . . 14  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( D  -  C
) )  e.  ( ( A [,] B
) -cn-> CC ) )
272256, 271mulcncf 22149 . . . . . . . . . . . . 13  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  ( D  -  C )
) )  e.  ( ( A [,] B
) -cn-> CC ) )
273223, 228, 267, 272cncfmpt2f 21708 . . . . . . . . . . . 12  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( C  +  ( ( ( x  -  A )  /  ( B  -  A )
)  x.  ( D  -  C ) ) ) )  e.  ( ( A [,] B
) -cn-> CC ) )
274264, 273syl5eqel 2494 . . . . . . . . . . 11  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  U )  e.  ( ( A [,] B
) -cn-> CC ) )
275223, 225, 263, 274cncfmpt2f 21708 . . . . . . . . . 10  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( V  -  U
) )  e.  ( ( A [,] B
) -cn-> CC ) )
276275trud 1414 . . . . . . . . 9  |-  ( x  e.  ( A [,] B )  |->  ( V  -  U ) )  e.  ( ( A [,] B ) -cn-> CC )
277 cniccibl 22537 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  (
x  e.  ( A [,] B )  |->  ( V  -  U ) )  e.  ( ( A [,] B )
-cn-> CC ) )  -> 
( x  e.  ( A [,] B ) 
|->  ( V  -  U
) )  e.  L^1 )
2781, 2, 276, 277mp3an 1326 . . . . . . . 8  |-  ( x  e.  ( A [,] B )  |->  ( V  -  U ) )  e.  L^1
279222, 278eqeltri 2486 . . . . . . 7  |-  ( x  e.  ( A [,] B )  |->  ( vol `  ( S " {
x } ) ) )  e.  L^1
280279a1i 11 . . . . . 6  |-  ( 0  e.  RR  ->  (
x  e.  ( A [,] B )  |->  ( vol `  ( S
" { x }
) ) )  e.  L^1 )
281213, 215, 218, 221, 280iblss2 22502 . . . . 5  |-  ( 0  e.  RR  ->  (
x  e.  RR  |->  ( vol `  ( S
" { x }
) ) )  e.  L^1 )
282193, 281ax-mp 5 . . . 4  |-  ( x  e.  RR  |->  ( vol `  ( S " {
x } ) ) )  e.  L^1
283 dmarea 23611 . . . 4  |-  ( S  e.  dom area  <->  ( S  C_  ( RR  X.  RR )  /\  A. x  e.  RR  ( S " { x } )  e.  ( `' vol " RR )  /\  (
x  e.  RR  |->  ( vol `  ( S
" { x }
) ) )  e.  L^1 ) )
28496, 212, 282, 283mpbir3an 1179 . . 3  |-  S  e. 
dom area
285 areaval 23618 . . 3  |-  ( S  e.  dom area  ->  (area `  S )  =  S. RR ( vol `  ( S " { x }
) )  _d x )
286284, 285ax-mp 5 . 2  |-  (area `  S )  =  S. RR ( vol `  ( S " { x }
) )  _d x
287 itgeq2 22474 . . . 4  |-  ( A. x  e.  RR  ( vol `  ( S " { x } ) )  =  if ( x  e.  ( A [,] B ) ,  ( V  -  U
) ,  0 )  ->  S. RR ( vol `  ( S
" { x }
) )  _d x  =  S. RR if ( x  e.  ( A [,] B ) ,  ( V  -  U
) ,  0 )  _d x )
288191a1i 11 . . . 4  |-  ( x  e.  RR  ->  ( vol `  ( S " { x } ) )  =  if ( x  e.  ( A [,] B ) ,  ( V  -  U
) ,  0 ) )
289287, 288mprg 2766 . . 3  |-  S. RR ( vol `  ( S
" { x }
) )  _d x  =  S. RR if ( x  e.  ( A [,] B ) ,  ( V  -  U
) ,  0 )  _d x
290 itgss2 22509 . . . 4  |-  ( ( A [,] B ) 
C_  RR  ->  S. ( A [,] B ) ( V  -  U
)  _d x  =  S. RR if ( x  e.  ( A [,] B ) ,  ( V  -  U
) ,  0 )  _d x )
2914, 290ax-mp 5 . . 3  |-  S. ( A [,] B ) ( V  -  U
)  _d x  =  S. RR if ( x  e.  ( A [,] B ) ,  ( V  -  U
) ,  0 )  _d x
29261, 58addcli 9629 . . . . . 6  |-  ( F  +  E )  e.  CC
293 2cnne0 10790 . . . . . 6  |-  ( 2  e.  CC  /\  2  =/=  0 )
294 div32 10267 . . . . . 6  |-  ( ( ( F  +  E
)  e.  CC  /\  ( 2  e.  CC  /\  2  =/=  0 )  /\  ( B  -  A )  e.  CC )  ->  ( ( ( F  +  E )  /  2 )  x.  ( B  -  A
) )  =  ( ( F  +  E
)  x.  ( ( B  -  A )  /  2 ) ) )
295292, 293, 147, 294mp3an 1326 . . . . 5  |-  ( ( ( F  +  E
)  /  2 )  x.  ( B  -  A ) )  =  ( ( F  +  E )  x.  (
( B  -  A
)  /  2 ) )
29626, 8addcli 9629 . . . . . 6  |-  ( D  +  C )  e.  CC
297 div32 10267 . . . . . 6  |-  ( ( ( D  +  C
)  e.  CC  /\  ( 2  e.  CC  /\  2  =/=  0 )  /\  ( B  -  A )  e.  CC )  ->  ( ( ( D  +  C )  /  2 )  x.  ( B  -  A
) )  =  ( ( D  +  C
)  x.  ( ( B  -  A )  /  2 ) ) )
298296, 293, 147, 297mp3an 1326 . . . . 5  |-  ( ( ( D  +  C
)  /  2 )  x.  ( B  -  A ) )  =  ( ( D  +  C )  x.  (
( B  -  A
)  /  2 ) )
299295, 298oveq12i 6289 . . . 4  |-  ( ( ( ( F  +  E )  /  2
)  x.  ( B  -  A ) )  -  ( ( ( D  +  C )  /  2 )  x.  ( B  -  A
) ) )  =  ( ( ( F  +  E )  x.  ( ( B  -  A )  /  2
) )  -  (
( D  +  C
)  x.  ( ( B  -  A )  /  2 ) ) )
300 2cn 10646 . . . . . 6  |-  2  e.  CC
301 2ne0 10668 . . . . . 6  |-  2  =/=  0
302292, 300, 301divcli 10326 . . . . 5  |-  ( ( F  +  E )  /  2 )  e.  CC
303296, 300, 301divcli 10326 . . . . 5  |-  ( ( D  +  C )  /  2 )  e.  CC
304302, 303, 147subdiri 10046 . . . 4  |-  ( ( ( ( F  +  E )  /  2
)  -  ( ( D  +  C )  /  2 ) )  x.  ( B  -  A ) )  =  ( ( ( ( F  +  E )  /  2 )  x.  ( B  -  A
) )  -  (
( ( D  +  C )  /  2
)  x.  ( B  -  A ) ) )
305114adantl 464 . . . . . . 7  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  V  e.  RR )
306263trud 1414 . . . . . . . . 9  |-  ( x  e.  ( A [,] B )  |->  V )  e.  ( ( A [,] B ) -cn-> CC )
307 cniccibl 22537 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  (
x  e.  ( A [,] B )  |->  V )  e.  ( ( A [,] B )
-cn-> CC ) )  -> 
( x  e.  ( A [,] B ) 
|->  V )  e.  L^1 )
3081, 2, 306, 307mp3an 1326 . . . . . . . 8  |-  ( x  e.  ( A [,] B )  |->  V )  e.  L^1
309308a1i 11 . . . . . . 7  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  V )  e.  L^1 )
310113adantl 464 . . . . . . 7  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  U  e.  RR )
311274trud 1414 . . . . . . . . 9  |-  ( x  e.  ( A [,] B )  |->  U )  e.  ( ( A [,] B ) -cn-> CC )
312 cniccibl 22537 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  (
x  e.  ( A [,] B )  |->  U )  e.  ( ( A [,] B )
-cn-> CC ) )  -> 
( x  e.  ( A [,] B ) 
|->  U )  e.  L^1 )
3131, 2, 311, 312mp3an 1326 . . . . . . . 8  |-  ( x  e.  ( A [,] B )  |->  U )  e.  L^1
314313a1i 11 . . . . . . 7  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  U )  e.  L^1 )
315305, 309, 310, 314itgsub 22522 . . . . . 6  |-  ( T. 
->  S. ( A [,] B ) ( V  -  U )  _d x  =  ( S. ( A [,] B
) V  _d x  -  S. ( A [,] B ) U  _d x ) )
316315trud 1414 . . . . 5  |-  S. ( A [,] B ) ( V  -  U
)  _d x  =  ( S. ( A [,] B ) V  _d x  -  S. ( A [,] B ) U  _d x )
31758, 300, 301divcan4i 10331 . . . . . . . . . . 11  |-  ( ( E  x.  2 )  /  2 )  =  E
318317oveq1i 6287 . . . . . . . . . 10  |-  ( ( ( E  x.  2 )  /  2 )  x.  ( B  -  A ) )  =  ( E  x.  ( B  -  A )
)
31958, 300mulcli 9630 . . . . . . . . . . 11  |-  ( E  x.  2 )  e.  CC
320 div32 10267 . . . . . . . . . . 11  |-  ( ( ( E  x.  2 )  e.  CC  /\  ( 2  e.  CC  /\  2  =/=  0 )  /\  ( B  -  A )  e.  CC )  ->  ( ( ( E  x.  2 )  /  2 )  x.  ( B  -  A
) )  =  ( ( E  x.  2 )  x.  ( ( B  -  A )  /  2 ) ) )
321319, 293, 147, 320mp3an 1326 . . . . . . . . . 10  |-  ( ( ( E  x.  2 )  /  2 )  x.  ( B  -  A ) )  =  ( ( E  x.  2 )  x.  (
( B  -  A
)  /  2 ) )
322318, 321eqtr3i 2433 . . . . . . . . 9  |-  ( E  x.  ( B  -  A ) )  =  ( ( E  x.  2 )  x.  (
( B  -  A
)  /  2 ) )
323322oveq1i 6287 . . . . . . . 8  |-  ( ( E  x.  ( B  -  A ) )  +  ( ( F  -  E )  x.  ( ( B  -  A )  /  2
) ) )  =  ( ( ( E  x.  2 )  x.  ( ( B  -  A )  /  2
) )  +  ( ( F  -  E
)  x.  ( ( B  -  A )  /  2 ) ) )
324 itgeq2 22474 . . . . . . . . . 10  |-  ( A. x  e.  ( A [,] B ) V  =  ( E  +  ( ( ( x  -  A )  /  ( B  -  A )
)  x.  ( F  -  E ) ) )  ->  S. ( A [,] B ) V  _d x  =  S. ( A [,] B
) ( E  +  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  ( F  -  E )
) )  _d x )
32566a1i 11 . . . . . . . . . 10  |-  ( x  e.  ( A [,] B )  ->  V  =  ( E  +  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  ( F  -  E )
) ) )
326324, 325mprg 2766 . . . . . . . . 9  |-  S. ( A [,] B ) V  _d x  =  S. ( A [,] B ) ( E  +  ( ( ( x  -  A )  /  ( B  -  A ) )  x.  ( F  -  E
) ) )  _d x
32757a1i 11 . . . . . . . . . . 11  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  E  e.  RR )
328 cniccibl 22537 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  (
x  e.  ( A [,] B )  |->  E )  e.  ( ( A [,] B )
-cn-> CC ) )  -> 
( x  e.  ( A [,] B ) 
|->  E )  e.  L^1 )
3291, 2, 233, 328mp3an 1326 . . . . . . . . . . . 12  |-  ( x  e.  ( A [,] B )  |->  E )  e.  L^1
330329a1i 11 . . . . . . . . . . 11  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  E )  e.  L^1 )
331126adantl 464 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  (
( x  -  A
)  /  ( B  -  A ) )  e.  RR )
33260a1i 11 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  F  e.  RR )
333332, 327resubcld 10027 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  ( F  -  E )  e.  RR )
334331, 333remulcld 9653 . . . . . . . . . . 11  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  (
( ( x  -  A )  /  ( B  -  A )
)  x.  ( F  -  E ) )  e.  RR )
335261trud 1414 . . . . . . . . . . . . 13  |-  ( x  e.  ( A [,] B )  |->  ( ( ( x  -  A
)  /  ( B  -  A ) )  x.  ( F  -  E ) ) )  e.  ( ( A [,] B ) -cn-> CC )
336 cniccibl 22537 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  (
x  e.  ( A [,] B )  |->  ( ( ( x  -  A )  /  ( B  -  A )
)  x.  ( F  -  E ) ) )  e.  ( ( A [,] B )
-cn-> CC ) )  -> 
( x  e.  ( A [,] B ) 
|->  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  ( F  -  E )
) )  e.  L^1 )
3371, 2, 335, 336mp3an 1326 . . . . . . . . . . . 12  |-  ( x  e.  ( A [,] B )  |->  ( ( ( x  -  A
)  /  ( B  -  A ) )  x.  ( F  -  E ) ) )  e.  L^1
338337a1i 11 . . . . . . . . . . 11  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  ( F  -  E )
) )  e.  L^1 )
339327, 330, 334, 338itgadd 22521 . . . . . . . . . 10  |-  ( T. 
->  S. ( A [,] B ) ( E  +  ( ( ( x  -  A )  /  ( B  -  A ) )  x.  ( F  -  E
) ) )  _d x  =  ( S. ( A [,] B
) E  _d x  +  S. ( A [,] B ) ( ( ( x  -  A )  /  ( B  -  A )
)  x.  ( F  -  E ) )  _d x ) )
340339trud 1414 . . . . . . . . 9  |-  S. ( A [,] B ) ( E  +  ( ( ( x  -  A )  /  ( B  -  A )
)  x.  ( F  -  E ) ) )  _d x  =  ( S. ( A [,] B ) E  _d x  +  S. ( A [,] B ) ( ( ( x  -  A )  / 
( B  -  A
) )  x.  ( F  -  E )
)  _d x )
341 iccmbl 22266 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  e.  dom  vol )
3421, 2, 341mp2an 670 . . . . . . . . . . . 12  |-  ( A [,] B )  e. 
dom  vol
343 mblvol 22231 . . . . . . . . . . . . . . 15  |-  ( ( A [,] B )  e.  dom  vol  ->  ( vol `  ( A [,] B ) )  =  ( vol* `  ( A [,] B
) ) )
344342, 343ax-mp 5 . . . . . . . . . . . . . 14  |-  ( vol `  ( A [,] B
) )  =  ( vol* `  ( A [,] B ) )
3451, 2, 17ltleii 9738 . . . . . . . . . . . . . . 15  |-  A  <_  B
346 ovolicc 22224 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <_  B )  ->  ( vol* `  ( A [,] B ) )  =  ( B  -  A ) )
3471, 2, 345, 346mp3an 1326 . . . . . . . . . . . . . 14  |-  ( vol* `  ( A [,] B ) )  =  ( B  -  A
)
348344, 347eqtri 2431 . . . . . . . . . . . . 13  |-  ( vol `  ( A [,] B
) )  =  ( B  -  A )
349348, 12eqeltri 2486 . . . . . . . . . . . 12  |-  ( vol `  ( A [,] B
) )  e.  RR
350 itgconst 22515 . . . . . . . . . . . 12  |-  ( ( ( A [,] B
)  e.  dom  vol  /\  ( vol `  ( A [,] B ) )  e.  RR  /\  E  e.  CC )  ->  S. ( A [,] B ) E  _d x  =  ( E  x.  ( vol `  ( A [,] B ) ) ) )
351342, 349, 58, 350mp3an 1326 . . . . . . . . . . 11  |-  S. ( A [,] B ) E  _d x  =  ( E  x.  ( vol `  ( A [,] B ) ) )
352348oveq2i 6288 . . . . . . . . . . 11  |-  ( E  x.  ( vol `  ( A [,] B ) ) )  =  ( E  x.  ( B  -  A ) )
353351, 352eqtri 2431 . . . . . . . . . 10  |-  S. ( A [,] B ) E  _d x  =  ( E  x.  ( B  -  A )
)
35461a1i 11 . . . . . . . . . . . . . 14  |-  ( T. 
->  F  e.  CC )
35558a1i 11 . . . . . . . . . . . . . 14  |-  ( T. 
->  E  e.  CC )
356354, 355subcld 9966 . . . . . . . . . . . . 13  |-  ( T. 
->  ( F  -  E
)  e.  CC )
357256trud 1414 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( A [,] B )  |->  ( ( x  -  A )  /  ( B  -  A ) ) )  e.  ( ( A [,] B ) -cn-> CC )
358 cniccibl 22537 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  (
x  e.  ( A [,] B )  |->  ( ( x  -  A
)  /  ( B  -  A ) ) )  e.  ( ( A [,] B )
-cn-> CC ) )  -> 
( x  e.  ( A [,] B ) 
|->  ( ( x  -  A )  /  ( B  -  A )
) )  e.  L^1 )
3591, 2, 357, 358mp3an 1326 . . . . . . . . . . . . . 14  |-  ( x  e.  ( A [,] B )  |->  ( ( x  -  A )  /  ( B  -  A ) ) )  e.  L^1
360359a1i 11 . . . . . . . . . . . . 13  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( ( x  -  A )  /  ( B  -  A )
) )  e.  L^1 )
361356, 331, 360itgmulc2 22530 . . . . . . . . . . . 12  |-  ( T. 
->  ( ( F  -  E )  x.  S. ( A [,] B ) ( ( x  -  A )  /  ( B  -  A )
)  _d x )  =  S. ( A [,] B ) ( ( F  -  E
)  x.  ( ( x  -  A )  /  ( B  -  A ) ) )  _d x )
362361trud 1414 . . . . . . . . . . 11  |-  ( ( F  -  E )  x.  S. ( A [,] B ) ( ( x  -  A
)  /  ( B  -  A ) )  _d x )  =  S. ( A [,] B ) ( ( F  -  E )  x.  ( ( x  -  A )  / 
( B  -  A
) ) )  _d x
363 itgeq2 22474 . . . . . . . . . . . . . . 15  |-  ( A. x  e.  ( A [,] B ) ( ( x  -  A )  /  ( B  -  A ) )  =  ( ( 1  / 
( B  -  A
) )  x.  (
x  -  A ) )  ->  S. ( A [,] B ) ( ( x  -  A
)  /  ( B  -  A ) )  _d x  =  S. ( A [,] B
) ( ( 1  /  ( B  -  A ) )  x.  ( x  -  A
) )  _d x )
364137recnd 9651 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( A [,] B )  ->  (
x  -  A )  e.  CC )
365364, 237, 238divrec2d 10364 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( A [,] B )  ->  (
( x  -  A
)  /  ( B  -  A ) )  =  ( ( 1  /  ( B  -  A ) )  x.  ( x  -  A
) ) )
366363, 365mprg 2766 . . . . . . . . . . . . . 14  |-  S. ( A [,] B ) ( ( x  -  A )  /  ( B  -  A )
)  _d x  =  S. ( A [,] B ) ( ( 1  /  ( B  -  A ) )  x.  ( x  -  A ) )  _d x
3675adantl 464 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  x  e.  RR )
368 cncfmptid 21706 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( A [,] B
)  C_  CC  /\  CC  C_  CC )  ->  (
x  e.  ( A [,] B )  |->  x )  e.  ( ( A [,] B )
-cn-> CC ) )
369230, 231, 368mp2an 670 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( A [,] B )  |->  x )  e.  ( ( A [,] B ) -cn-> CC )
370 cniccibl 22537 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  (
x  e.  ( A [,] B )  |->  x )  e.  ( ( A [,] B )
-cn-> CC ) )  -> 
( x  e.  ( A [,] B ) 
|->  x )  e.  L^1 )
3711, 2, 369, 370mp3an 1326 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( A [,] B )  |->  x )  e.  L^1
372371a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  x )  e.  L^1 )
3731a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  A  e.  RR )
374 cncfmptc 21705 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  CC  /\  ( A [,] B ) 
C_  CC  /\  CC  C_  CC )  ->  ( x  e.  ( A [,] B )  |->  A )  e.  ( ( A [,] B ) -cn-> CC ) )
375139, 230, 231, 374mp3an 1326 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( A [,] B )  |->  A )  e.  ( ( A [,] B ) -cn-> CC )
376 cniccibl 22537 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  (
x  e.  ( A [,] B )  |->  A )  e.  ( ( A [,] B )
-cn-> CC ) )  -> 
( x  e.  ( A [,] B ) 
|->  A )  e.  L^1 )
3771, 2, 375, 376mp3an 1326 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( A [,] B )  |->  A )  e.  L^1
378377a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  A )  e.  L^1 )
379367, 372, 373, 378itgsub 22522 . . . . . . . . . . . . . . . . . . 19  |-  ( T. 
->  S. ( A [,] B ) ( x  -  A )  _d x  =  ( S. ( A [,] B
) x  _d x  -  S. ( A [,] B ) A  _d x ) )
380379trud 1414 . . . . . . . . . . . . . . . . . 18  |-  S. ( A [,] B ) ( x  -  A
)  _d x  =  ( S. ( A [,] B ) x  _d x  -  S. ( A [,] B ) A  _d x )
3811a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( T. 
->  A  e.  RR )
3822a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( T. 
->  B  e.  RR )
383345a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( T. 
->  A  <_  B )
384 1nn0 10851 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  1  e.  NN0
385384a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( T. 
->  1  e.  NN0 )
386381, 382, 383, 385itgpowd 35526 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T. 
->  S. ( A [,] B ) ( x ^ 1 )  _d x  =  ( ( ( B ^ (
1  +  1 ) )  -  ( A ^ ( 1  +  1 ) ) )  /  ( 1  +  1 ) ) )
387386trud 1414 . . . . . . . . . . . . . . . . . . . . 21  |-  S. ( A [,] B ) ( x ^ 1 )  _d x  =  ( ( ( B ^ ( 1  +  1 ) )  -  ( A ^ ( 1  +  1 ) ) )  /  ( 1  +  1 ) )
388 1p1e2 10689 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 1  +  1 )  =  2
389388oveq2i 6288 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( B ^ (
1  +  1 ) )  -  ( A ^ ( 1  +  1 ) ) )  /  ( 1  +  1 ) )  =  ( ( ( B ^ ( 1  +  1 ) )  -  ( A ^ ( 1  +  1 ) ) )  /  2 )
390387, 389eqtri 2431 . . . . . . . . . . . . . . . . . . . 20  |-  S. ( A [,] B ) ( x ^ 1 )  _d x  =  ( ( ( B ^ ( 1  +  1 ) )  -  ( A ^ ( 1  +  1 ) ) )  /  2 )
391 itgeq2 22474 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. x  e.  ( A [,] B ) ( x ^ 1 )  =  x  ->  S. ( A [,] B ) ( x ^ 1 )  _d x  =  S. ( A [,] B
) x  _d x )
392235exp1d 12347 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( A [,] B )  ->  (
x ^ 1 )  =  x )
393391, 392mprg 2766 . . . . . . . . . . . . . . . . . . . 20  |-  S. ( A [,] B ) ( x ^ 1 )  _d x  =  S. ( A [,] B ) x  _d x
394388oveq2i 6288 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( B ^ ( 1  +  1 ) )  =  ( B ^ 2 )
395388oveq2i 6288 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A ^ ( 1  +  1 ) )  =  ( A ^ 2 )
396394, 395oveq12i 6289 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( B ^ ( 1  +  1 ) )  -  ( A ^
( 1  +  1 ) ) )  =  ( ( B ^
2 )  -  ( A ^ 2 ) )
397396oveq1i 6287 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( B ^ (
1  +  1 ) )  -  ( A ^ ( 1  +  1 ) ) )  /  2 )  =  ( ( ( B ^ 2 )  -  ( A ^ 2 ) )  /  2 )
398390, 393, 3973eqtr3i 2439 . . . . . . . . . . . . . . . . . . 19  |-  S. ( A [,] B ) x  _d x  =  ( ( ( B ^ 2 )  -  ( A ^ 2 ) )  /  2 )
399 itgconst 22515 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( A [,] B
)  e.  dom  vol  /\  ( vol `  ( A [,] B ) )  e.  RR  /\  A  e.  CC )  ->  S. ( A [,] B ) A  _d x  =  ( A  x.  ( vol `  ( A [,] B ) ) ) )
400342, 349, 139, 399mp3an 1326 . . . . . . . . . . . . . . . . . . . 20  |-  S. ( A [,] B ) A  _d x  =  ( A  x.  ( vol `  ( A [,] B ) ) )
401348oveq2i 6288 . . . . . . . . . . . . . . . . . . . 20  |-  ( A  x.  ( vol `  ( A [,] B ) ) )  =  ( A  x.  ( B  -  A ) )
402400, 401eqtri 2431 . . . . . . . . . . . . . . . . . . 19  |-  S. ( A [,] B ) A  _d x  =  ( A  x.  ( B  -  A )
)
403398, 402oveq12i 6289 . . . . . . . . . . . . . . . . . 18  |-  ( S. ( A [,] B
) x  _d x  -  S. ( A [,] B ) A  _d x )  =  ( ( ( ( B ^ 2 )  -  ( A ^
2 ) )  / 
2 )  -  ( A  x.  ( B  -  A ) ) )
404380, 403eqtri 2431 . . . . . . . . . . . . . . . . 17  |-  S. ( A [,] B ) ( x  -  A
)  _d x  =  ( ( ( ( B ^ 2 )  -  ( A ^
2 ) )  / 
2 )  -  ( A  x.  ( B  -  A ) ) )
405404oveq2i 6288 . . . . . . . . . . . . . . . 16  |-  ( ( 1  /  ( B  -  A ) )  x.  S. ( A [,] B ) ( x  -  A )  _d x )  =  ( ( 1  / 
( B  -  A
) )  x.  (
( ( ( B ^ 2 )  -  ( A ^ 2 ) )  /  2 )  -  ( A  x.  ( B  -  A
) ) ) )
40614a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( T. 
->  B  e.  CC )
407139a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( T. 
->  A  e.  CC )
408406, 407subcld 9966 . . . . . . . . . . . . . . . . . . 19  |-  ( T. 
->  ( B  -  A
)  e.  CC )
40918a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( T. 
->  B  =/=  A
)
410406, 407, 409subne0d 9975 . . . . . . . . . . . . . . . . . . 19  |-  ( T. 
->  ( B  -  A
)  =/=  0 )
411408, 410reccld 10353 . . . . . . . . . . . . . . . . . 18  |-  ( T. 
->  ( 1  /  ( B  -  A )
)  e.  CC )
412411trud 1414 . . . . . . . . . . . . . . . . 17  |-  ( 1  /  ( B  -  A ) )  e.  CC
41314sqcli 12291 . . . . . . . . . . . . . . . . . . 19  |-  ( B ^ 2 )  e.  CC
414139sqcli 12291 . . . . . . . . . . . . . . . . . . 19  |-  ( A ^ 2 )  e.  CC
415413, 414subcli 9930 . . . . . . . . . . . . . . . . . 18  |-  ( ( B ^ 2 )  -  ( A ^
2 ) )  e.  CC
416415, 300, 301divcli 10326 . . . . . . . . . . . . . . . . 17  |-  ( ( ( B ^ 2 )  -  ( A ^ 2 ) )  /  2 )  e.  CC
417139, 147mulcli 9630 . . . . . . . . . . . . . . . . 17  |-  ( A  x.  ( B  -  A ) )  e.  CC
418412, 416, 417subdii 10045 . . . . . . . . . . . . . . . 16  |-  ( ( 1  /  ( B  -  A ) )  x.  ( ( ( ( B ^ 2 )  -  ( A ^ 2 ) )  /  2 )  -  ( A  x.  ( B  -  A )
) ) )  =  ( ( ( 1  /  ( B  -  A ) )  x.  ( ( ( B ^ 2 )  -  ( A ^ 2 ) )  /  2 ) )  -  ( ( 1  /  ( B  -  A ) )  x.  ( A  x.  ( B  -  A
) ) ) )
419405, 418eqtri 2431 . . . . . . . . . . . . . . 15  |-  ( ( 1  /  ( B  -  A ) )  x.  S. ( A [,] B ) ( x  -  A )  _d x )  =  ( ( ( 1  /  ( B  -  A ) )  x.  ( ( ( B ^ 2 )  -  ( A ^ 2 ) )  /  2 ) )  -  ( ( 1  /  ( B  -  A ) )  x.  ( A  x.  ( B  -  A
) ) ) )
420137adantl 464 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  (
x  -  A )  e.  RR )
421367, 372, 373, 378iblsub 22518 . . . . . . . . . . . . . . . . 17  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( x  -  A
) )  e.  L^1 )
422411, 420, 421itgmulc2 22530 . . . . . . . . . . . . . . . 16  |-  ( T. 
->  ( ( 1  / 
( B  -  A
) )  x.  S. ( A [,] B ) ( x  -  A
)  _d x )  =  S. ( A [,] B ) ( ( 1  /  ( B  -  A )
)  x.  ( x  -  A ) )  _d x )
423422trud 1414 . . . . . . . . . . . . . . 15  |-  ( ( 1  /  ( B  -  A ) )  x.  S. ( A [,] B ) ( x  -  A )  _d x )  =  S. ( A [,] B ) ( ( 1  /  ( B  -  A ) )  x.  ( x  -  A ) )  _d x
424412, 417mulcomi 9631 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  /  ( B  -  A ) )  x.  ( A  x.  ( B  -  A
) ) )  =  ( ( A  x.  ( B  -  A
) )  x.  (
1  /  ( B  -  A ) ) )
425417, 147, 21divreci 10329 . . . . . . . . . . . . . . . . 17  |-  ( ( A  x.  ( B  -  A ) )  /  ( B  -  A ) )  =  ( ( A  x.  ( B  -  A
) )  x.  (
1  /  ( B  -  A ) ) )
426139, 147, 21divcan4i 10331 . . . . . . . . . . . . . . . . 17  |-  ( ( A  x.  ( B  -  A ) )  /  ( B  -  A ) )  =  A
427424, 425, 4263eqtr2i 2437 . . . . . . . . . . . . . . . 16  |-  ( ( 1  /  ( B  -  A ) )  x.  ( A  x.  ( B  -  A
) ) )  =  A
428427oveq2i 6288 . . . . . . . . . . . . . . 15  |-  ( ( ( 1  /  ( B  -  A )
)  x.  ( ( ( B ^ 2 )  -  ( A ^ 2 ) )  /  2 ) )  -  ( ( 1  /  ( B  -  A ) )  x.  ( A  x.  ( B  -  A )
) ) )  =  ( ( ( 1  /  ( B  -  A ) )  x.  ( ( ( B ^ 2 )  -  ( A ^ 2 ) )  /  2 ) )  -  A )
429419, 423, 4283eqtr3i 2439 . . . . . . . . . . . . . 14  |-  S. ( A [,] B ) ( ( 1  / 
( B  -  A
) )  x.  (
x  -  A ) )  _d x  =  ( ( ( 1  /  ( B  -  A ) )  x.  ( ( ( B ^ 2 )  -  ( A ^ 2 ) )  /  2 ) )  -  A )
430366, 429eqtri 2431 . . . . . . . . . . . . 13  |-  S. ( A [,] B ) ( ( x  -  A )  /  ( B  -  A )
)  _d x  =  ( ( ( 1  /  ( B  -  A ) )  x.  ( ( ( B ^ 2 )  -  ( A ^ 2 ) )  /  2 ) )  -  A )
43114, 139subsqi 12321 . . . . . . . . . . . . . . . . 17  |-  ( ( B ^ 2 )  -  ( A ^
2 ) )  =  ( ( B  +  A )  x.  ( B  -  A )
)
432431oveq1i 6287 . . . . . . . . . . . . . . . 16  |-  ( ( ( B ^ 2 )  -  ( A ^ 2 ) )  /  2 )  =  ( ( ( B  +  A )  x.  ( B  -  A
) )  /  2
)
433432oveq2i 6288 . . . . . . . . . . . . . . 15  |-  ( ( 1  /  ( B  -  A ) )  x.  ( ( ( B ^ 2 )  -  ( A ^
2 ) )  / 
2 ) )  =  ( ( 1  / 
( B  -  A
) )  x.  (
( ( B  +  A )  x.  ( B  -  A )
)  /  2 ) )
434431, 415eqeltrri 2487 . . . . . . . . . . . . . . . 16  |-  ( ( B  +  A )  x.  ( B  -  A ) )  e.  CC
435412, 434, 300, 301divassi 10340 . . . . . . . . . . . . . . 15  |-  ( ( ( 1  /  ( B  -  A )
)  x.  ( ( B  +  A )  x.  ( B  -  A ) ) )  /  2 )  =  ( ( 1  / 
( B  -  A
) )  x.  (
( ( B  +  A )  x.  ( B  -  A )
)  /  2 ) )
436412, 434mulcomi 9631 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  /  ( B  -  A ) )  x.  ( ( B  +  A )  x.  ( B  -  A
) ) )  =  ( ( ( B  +  A )  x.  ( B  -  A
) )  x.  (
1  /  ( B  -  A ) ) )
437434, 147, 21divreci 10329 . . . . . . . . . . . . . . . . 17  |-  ( ( ( B  +  A
)  x.  ( B  -  A ) )  /  ( B  -  A ) )  =  ( ( ( B  +  A )  x.  ( B  -  A
) )  x.  (
1  /  ( B  -  A ) ) )
43814, 139addcli 9629 . . . . . . . . . . . . . . . . . 18  |-  ( B  +  A )  e.  CC
439438, 147, 21divcan4i 10331 . . . . . . . . . . . . . . . . 17  |-  ( ( ( B  +  A
)  x.  ( B  -  A ) )  /  ( B  -  A ) )  =  ( B  +  A
)
440436, 437, 4393eqtr2i 2437 . . . . . . . . . . . . . . . 16  |-  ( ( 1  /  ( B  -  A ) )  x.  ( ( B  +  A )  x.  ( B  -  A
) ) )  =  ( B  +  A
)
441440oveq1i 6287 . . . . . . . . . . . . . . 15  |-  ( ( ( 1  /  ( B  -  A )
)  x.  ( ( B  +  A )  x.  ( B  -  A ) ) )  /  2 )  =  ( ( B  +  A )  /  2
)
442433, 435, 4413eqtr2i 2437 . . . . . . . . . . . . . 14  |-  ( ( 1  /  ( B  -  A ) )  x.  ( ( ( B ^ 2 )  -  ( A ^
2 ) )  / 
2 ) )  =  ( ( B  +  A )  /  2
)
443442oveq1i 6287 . . . . . . . . . . . . 13  |-  ( ( ( 1  /  ( B  -  A )
)  x.  ( ( ( B ^ 2 )  -  ( A ^ 2 ) )  /  2 ) )  -  A )  =  ( ( ( B  +  A )  / 
2 )  -  A
)
444139, 300mulcli 9630 . . . . . . . . . . . . . . 15  |-  ( A  x.  2 )  e.  CC
445 divsubdir 10280 . . . . . . . . . . . . . . 15  |-  ( ( ( B  +  A
)  e.  CC  /\  ( A  x.  2
)  e.  CC  /\  ( 2  e.  CC  /\  2  =/=  0 ) )  ->  ( (
( B  +  A
)  -  ( A  x.  2 ) )  /  2 )  =  ( ( ( B  +  A )  / 
2 )  -  (
( A  x.  2 )  /  2 ) ) )
446438, 444, 293, 445mp3an 1326 . . . . . . . . . . . . . 14  |-  ( ( ( B  +  A
)  -  ( A  x.  2 ) )  /  2 )  =  ( ( ( B  +  A )  / 
2 )  -  (
( A  x.  2 )  /  2 ) )
44714, 139, 444addsubassi 9946 . . . . . . . . . . . . . . . 16  |-  ( ( B  +  A )  -  ( A  x.  2 ) )  =  ( B  +  ( A  -  ( A  x.  2 ) ) )
448 subsub2 9882 . . . . . . . . . . . . . . . . 17  |-  ( ( B  e.  CC  /\  ( A  x.  2
)  e.  CC  /\  A  e.  CC )  ->  ( B  -  (
( A  x.  2 )  -  A ) )  =  ( B  +  ( A  -  ( A  x.  2
) ) ) )
44914, 444, 139, 448mp3an 1326 . . . . . . . . . . . . . . . 16  |-  ( B  -  ( ( A  x.  2 )  -  A ) )  =  ( B  +  ( A  -  ( A  x.  2 ) ) )
450139times2i 10697 . . . . . . . . . . . . . . . . . . 19  |-  ( A  x.  2 )  =  ( A  +  A
)
451450oveq1i 6287 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  x.  2 )  -  A )  =  ( ( A  +  A )  -  A
)
452139, 139pncan3oi 9871 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  +  A )  -  A )  =  A
453451, 452eqtri 2431 . . . . . . . . . . . . . . . . 17  |-  ( ( A  x.  2 )  -  A )  =  A
454453oveq2i 6288 . . . . . . . . . . . . . . . 16  |-  ( B  -  ( ( A  x.  2 )  -  A ) )  =  ( B  -  A
)
455447, 449, 4543eqtr2i 2437 . . . . . . . . . . . . . . 15  |-  ( ( B  +  A )  -  ( A  x.  2 ) )  =  ( B  -  A
)
456455oveq1i 6287 . . . . . . . . . . . . . 14  |-  ( ( ( B  +  A
)  -  ( A  x.  2 ) )  /  2 )  =  ( ( B  -  A )  /  2
)
457139, 300, 301divcan4i 10331 . . . . . . . . . . . . . . 15  |-  ( ( A  x.  2 )  /  2 )  =  A
458457oveq2i 6288 . . . . . . . . . . . . . 14  |-  ( ( ( B  +  A
)  /  2 )  -  ( ( A  x.  2 )  / 
2 ) )  =  ( ( ( B  +  A )  / 
2 )  -  A
)
459446, 456, 4583eqtr3ri 2440 . . . . . . . . . . . . 13  |-  ( ( ( B  +  A
)  /  2 )  -  A )  =  ( ( B  -  A )  /  2
)
460430, 443, 4593eqtri 2435 . . . . . . . . . . . 12  |-  S. ( A [,] B ) ( ( x  -  A )  /  ( B  -  A )
)  _d x  =  ( ( B  -  A )  /  2
)
461460oveq2i 6288 . . . . . . . . . . 11  |-  ( ( F  -  E )  x.  S. ( A [,] B ) ( ( x  -  A
)  /  ( B  -  A ) )  _d x )  =  ( ( F  -  E )  x.  (
( B  -  A
)  /  2 ) )
462 itgeq2 22474 . . . . . . . . . . . 12  |-  ( A. x  e.  ( A [,] B ) ( ( F  -  E )  x.  ( ( x  -  A )  / 
( B  -  A
) ) )  =  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  ( F  -  E )
)  ->  S. ( A [,] B ) ( ( F  -  E
)  x.  ( ( x  -  A )  /  ( B  -  A ) ) )  _d x  =  S. ( A [,] B
) ( ( ( x  -  A )  /  ( B  -  A ) )  x.  ( F  -  E
) )  _d x )
46361, 58subcli 9930 . . . . . . . . . . . . . 14  |-  ( F  -  E )  e.  CC
464463a1i 11 . . . . . . . . . . . . 13  |-  ( x  e.  ( A [,] B )  ->  ( F  -  E )  e.  CC )
465464, 127mulcomd 9646 . . . . . . . . . . . 12  |-  ( x  e.  ( A [,] B )  ->  (
( F  -  E
)  x.  ( ( x  -  A )  /  ( B  -  A ) ) )  =  ( ( ( x  -  A )  /  ( B  -  A ) )  x.  ( F  -  E
) ) )
466462, 465mprg 2766 . . . . . . . . . . 11  |-  S. ( A [,] B ) ( ( F  -  E )  x.  (
( x  -  A
)  /  ( B  -  A ) ) )  _d x  =  S. ( A [,] B ) ( ( ( x  -  A
)  /  ( B  -  A ) )  x.  ( F  -  E ) )  _d x
467362, 461, 4663eqtr3ri 2440 . . . . . . . . . 10  |-  S. ( A [,] B ) ( ( ( x  -  A )  / 
( B  -  A
) )  x.  ( F  -  E )
)  _d x  =  ( ( F  -  E )  x.  (
( B  -  A
)  /  2 ) )
468353, 467oveq12i 6289 . . . . . . . . 9  |-  ( S. ( A [,] B
) E  _d x  +  S. ( A [,] B ) ( ( ( x  -  A )  /  ( B  -  A )
)  x.  ( F  -  E ) )  _d x )  =  ( ( E  x.  ( B  -  A
) )  +  ( ( F  -  E
)  x.  ( ( B  -  A )  /  2 ) ) )
469326, 340, 4683eqtri 2435 . . . . . . . 8  |-  S. ( A [,] B ) V  _d x  =  ( ( E  x.  ( B  -  A
) )  +  ( ( F  -  E
)  x.  ( ( B  -  A )  /  2 ) ) )
470147, 300, 301divcli 10326 . . . . . . . . 9  |-  ( ( B  -  A )  /  2 )  e.  CC
471319, 463, 470adddiri 9636 . . . . . . . 8  |-  ( ( ( E  x.  2 )  +  ( F  -  E ) )  x.  ( ( B  -  A )  / 
2 ) )  =  ( ( ( E  x.  2 )  x.  ( ( B  -  A )  /  2
) )  +  ( ( F  -  E
)  x.  ( ( B  -  A )  /  2 ) ) )
472323, 469, 4713eqtr4i 2441 . . . . . . 7  |-  S. ( A [,] B ) V  _d x  =  ( ( ( E  x.  2 )  +  ( F  -  E
) )  x.  (
( B  -  A
)  /  2 ) )
473 addsub12 9868 . . . . . . . . . 10  |-  ( ( F  e.  CC  /\  ( E  x.  2
)  e.  CC  /\  E  e.  CC )  ->  ( F  +  ( ( E  x.  2 )  -  E ) )  =  ( ( E  x.  2 )  +  ( F  -  E ) ) )
47461, 319, 58, 473mp3an 1326 . . . . . . . . 9  |-  ( F  +  ( ( E  x.  2 )  -  E ) )  =  ( ( E  x.  2 )  +  ( F  -  E ) )
47558times2i 10697 . . . . . . . . . . . 12  |-  ( E  x.  2 )  =  ( E  +  E
)
476475oveq1i 6287 . . . . . . . . . . 11  |-  ( ( E  x.  2 )  -  E )  =  ( ( E  +  E )  -  E
)
47758, 58pncan3oi 9871 . . . . . . . . . . 11  |-  ( ( E  +  E )  -  E )  =  E
478476, 477eqtri 2431 . . . . . . . . . 10  |-  ( ( E  x.  2 )  -  E )  =  E
479478oveq2i 6288 . . . . . . . . 9  |-  ( F  +  ( ( E  x.  2 )  -  E ) )  =  ( F  +  E
)
480474, 479eqtr3i 2433 . . . . . . . 8  |-  ( ( E  x.  2 )  +  ( F  -  E ) )  =  ( F  +  E
)
481480oveq1i 6287 . . . . . . 7  |-  ( ( ( E  x.  2 )  +  ( F  -  E ) )  x.  ( ( B  -  A )  / 
2 ) )  =  ( ( F  +  E )  x.  (
( B  -  A
)  /  2 ) )
482472, 481eqtri 2431 . . . . . 6  |-  S. ( A [,] B ) V  _d x  =  ( ( F  +  E )  x.  (
( B  -  A
)  /  2 ) )
4838, 300, 301divcan4i 10331 . . . . . . . . . . 11  |-  ( ( C  x.  2 )  /  2 )  =  C
484483oveq1i 6287 . . . . . . . . . 10  |-  ( ( ( C  x.  2 )  /  2 )  x.  ( B  -  A ) )  =  ( C  x.  ( B  -  A )
)
4858, 300mulcli 9630 . . . . . . . . . . 11  |-  ( C  x.  2 )  e.  CC
486 div32 10267 . . . . . . . . . . 11  |-  ( ( ( C  x.  2 )  e.  CC  /\  ( 2  e.  CC  /\  2  =/=  0 )  /\  ( B  -  A )  e.  CC )  ->  ( ( ( C  x.  2 )  /  2 )  x.  ( B  -  A
) )  =  ( ( C  x.  2 )  x.  ( ( B  -  A )  /  2 ) ) )
487485, 293, 147, 486mp3an 1326 . . . . . . . . . 10  |-  ( ( ( C  x.  2 )  /  2 )  x.  ( B  -  A ) )  =  ( ( C  x.  2 )  x.  (
( B  -  A
)  /  2 ) )
488484, 487eqtr3i 2433 . . . . . . . . 9  |-  ( C  x.  ( B  -  A ) )  =  ( ( C  x.  2 )  x.  (
( B  -  A
)  /  2 ) )
489488oveq1i 6287 . . . . . . . 8  |-  ( ( C  x.  ( B  -  A ) )  +  ( ( D  -  C )  x.  ( ( B  -  A )  /  2
) ) )  =  ( ( ( C  x.  2 )  x.  ( ( B  -  A )  /  2
) )  +  ( ( D  -  C
)  x.  ( ( B  -  A )  /  2 ) ) )
49031a1i 11 . . . . . . . . . . 11  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  U  =  ( C  +  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  ( D  -  C )
) ) )
491490itgeq2dv 22478 . . . . . . . . . 10  |-  ( T. 
->  S. ( A [,] B ) U  _d x  =  S. ( A [,] B ) ( C  +  ( ( ( x  -  A )  /  ( B  -  A )
)  x.  ( D  -  C ) ) )  _d x )
492491trud 1414 . . . . . . . . 9  |-  S. ( A [,] B ) U  _d x  =  S. ( A [,] B ) ( C  +  ( ( ( x  -  A )  /  ( B  -  A ) )  x.  ( D  -  C
) ) )  _d x
4937a1i 11 . . . . . . . . . . 11  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  C  e.  RR )
494 cniccibl 22537 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  (
x  e.  ( A [,] B )  |->  C )  e.  ( ( A [,] B )
-cn-> CC ) )  -> 
( x  e.  ( A [,] B ) 
|->  C )  e.  L^1 )
4951, 2, 266, 494mp3an 1326 . . . . . . . . . . . 12  |-  ( x  e.  ( A [,] B )  |->  C )  e.  L^1
496495a1i 11 . . . . . . . . . . 11  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  C )  e.  L^1 )
49725a1i 11 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  D  e.  RR )
498497, 493resubcld 10027 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  ( D  -  C )  e.  RR )
499331, 498remulcld 9653 . . . . . . . . . . 11  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  (
( ( x  -  A )  /  ( B  -  A )
)  x.  ( D  -  C ) )  e.  RR )
500272trud 1414 . . . . . . . . . . . . 13  |-  ( x  e.  ( A [,] B )  |->  ( ( ( x  -  A
)  /  ( B  -  A ) )  x.  ( D  -  C ) ) )  e.  ( ( A [,] B ) -cn-> CC )
501 cniccibl 22537 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  (
x  e.  ( A [,] B )  |->  ( (