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

Theorem areaquad 29589
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 11375 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  C_  RR )
41, 2, 3mp2an 672 . . . . . . . . 9  |-  ( A [,] B )  C_  RR
54sseli 3350 . . . . . . . 8  |-  ( x  e.  ( A [,] B )  ->  x  e.  RR )
65adantr 465 . . . . . . 7  |-  ( ( x  e.  ( A [,] B )  /\  y  e.  ( U [,] V ) )  ->  x  e.  RR )
7 areaquad.3 . . . . . . . . . . . . . . . 16  |-  C  e.  RR
87recni 9396 . . . . . . . . . . . . . . 15  |-  C  e.  CC
98a1i 11 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  C  e.  CC )
10 resubcl 9671 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  RR  /\  A  e.  RR )  ->  ( x  -  A
)  e.  RR )
111, 10mpan2 671 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  RR  ->  (
x  -  A )  e.  RR )
122, 1resubcli 9669 . . . . . . . . . . . . . . . . . 18  |-  ( B  -  A )  e.  RR
1312a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  RR  ->  ( B  -  A )  e.  RR )
142recni 9396 . . . . . . . . . . . . . . . . . . . . 21  |-  B  e.  CC
1514a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( A  e.  RR  ->  B  e.  CC )
161recni 9396 . . . . . . . . . . . . . . . . . . . . 21  |-  A  e.  CC
1716a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( A  e.  RR  ->  A  e.  CC )
18 areaquad.7 . . . . . . . . . . . . . . . . . . . . . 22  |-  A  < 
B
191, 18gtneii 9484 . . . . . . . . . . . . . . . . . . . . 21  |-  B  =/= 
A
2019a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( A  e.  RR  ->  B  =/=  A )
2115, 17, 20subne0d 9726 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  RR  ->  ( B  -  A )  =/=  0 )
221, 21ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ( B  -  A )  =/=  0
2322a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  RR  ->  ( B  -  A )  =/=  0 )
2411, 13, 23redivcld 10157 . . . . . . . . . . . . . . . 16  |-  ( x  e.  RR  ->  (
( x  -  A
)  /  ( B  -  A ) )  e.  RR )
2524recnd 9410 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  (
( x  -  A
)  /  ( B  -  A ) )  e.  CC )
26 areaquad.4 . . . . . . . . . . . . . . . . 17  |-  D  e.  RR
2726recni 9396 . . . . . . . . . . . . . . . 16  |-  D  e.  CC
2827a1i 11 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  D  e.  CC )
2925, 28mulcld 9404 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  (
( ( x  -  A )  /  ( B  -  A )
)  x.  D )  e.  CC )
3025, 9mulcld 9404 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  (
( ( x  -  A )  /  ( B  -  A )
)  x.  C )  e.  CC )
319, 29, 30addsub12d 9740 . . . . . . . . . . . . 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 ) ) ) )
32 areaquad.10 . . . . . . . . . . . . . 14  |-  U  =  ( C  +  ( ( ( x  -  A )  /  ( B  -  A )
)  x.  ( D  -  C ) ) )
3325, 28, 9subdid 9798 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  (
( ( x  -  A )  /  ( B  -  A )
)  x.  ( D  -  C ) )  =  ( ( ( ( x  -  A
)  /  ( B  -  A ) )  x.  D )  -  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  C
) ) )
3433oveq2d 6105 . . . . . . . . . . . . . 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 ) ) ) )
3532, 34syl5eq 2485 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  U  =  ( C  +  ( ( ( ( x  -  A )  /  ( B  -  A ) )  x.  D )  -  (
( ( x  -  A )  /  ( B  -  A )
)  x.  C ) ) ) )
36 1cnd 9400 . . . . . . . . . . . . . . . 16  |-  ( x  e.  RR  ->  1  e.  CC )
3736, 25, 9subdird 9799 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  (
( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) )  x.  C )  =  ( ( 1  x.  C )  -  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  C
) ) )
388mulid2i 9387 . . . . . . . . . . . . . . . 16  |-  ( 1  x.  C )  =  C
3938oveq1i 6099 . . . . . . . . . . . . . . 15  |-  ( ( 1  x.  C )  -  ( ( ( x  -  A )  /  ( B  -  A ) )  x.  C ) )  =  ( C  -  (
( ( x  -  A )  /  ( B  -  A )
)  x.  C ) )
4037, 39syl6eq 2489 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  (
( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) )  x.  C )  =  ( C  -  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  C
) ) )
4140oveq2d 6105 . . . . . . . . . . . . 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 ) ) ) )
4231, 35, 413eqtr4d 2483 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  U  =  ( ( ( ( x  -  A
)  /  ( B  -  A ) )  x.  D )  +  ( ( 1  -  ( ( x  -  A )  /  ( B  -  A )
) )  x.  C
) ) )
43 1red 9399 . . . . . . . . . . . . . . . 16  |-  ( x  e.  RR  ->  1  e.  RR )
4443, 24resubcld 9774 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  (
1  -  ( ( x  -  A )  /  ( B  -  A ) ) )  e.  RR )
4544recnd 9410 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  (
1  -  ( ( x  -  A )  /  ( B  -  A ) ) )  e.  CC )
4645, 9mulcld 9404 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  (
( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) )  x.  C )  e.  CC )
4729, 46addcomd 9569 . . . . . . . . . . . 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
) ) )
4845, 9mulcomd 9405 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  (
( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) )  x.  C )  =  ( C  x.  ( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) ) ) )
4925, 28mulcomd 9405 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  (
( ( x  -  A )  /  ( B  -  A )
)  x.  D )  =  ( D  x.  ( ( x  -  A )  /  ( B  -  A )
) ) )
5048, 49oveq12d 6107 . . . . . . . . . . . 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 ) ) ) ) )
5142, 47, 503eqtrd 2477 . . . . . . . . . . 11  |-  ( x  e.  RR  ->  U  =  ( ( C  x.  ( 1  -  ( ( x  -  A )  /  ( B  -  A )
) ) )  +  ( D  x.  (
( x  -  A
)  /  ( B  -  A ) ) ) ) )
527a1i 11 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  C  e.  RR )
5352, 44remulcld 9412 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  ( C  x.  ( 1  -  ( ( x  -  A )  / 
( B  -  A
) ) ) )  e.  RR )
5426a1i 11 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  D  e.  RR )
5554, 24remulcld 9412 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  ( D  x.  ( (
x  -  A )  /  ( B  -  A ) ) )  e.  RR )
5653, 55readdcld 9411 . . . . . . . . . . 11  |-  ( x  e.  RR  ->  (
( C  x.  (
1  -  ( ( x  -  A )  /  ( B  -  A ) ) ) )  +  ( D  x.  ( ( x  -  A )  / 
( B  -  A
) ) ) )  e.  RR )
5751, 56eqeltrd 2515 . . . . . . . . . 10  |-  ( x  e.  RR  ->  U  e.  RR )
58 areaquad.5 . . . . . . . . . . . . . . . 16  |-  E  e.  RR
5958recni 9396 . . . . . . . . . . . . . . 15  |-  E  e.  CC
6059a1i 11 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  E  e.  CC )
61 areaquad.6 . . . . . . . . . . . . . . . . 17  |-  F  e.  RR
6261recni 9396 . . . . . . . . . . . . . . . 16  |-  F  e.  CC
6362a1i 11 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  F  e.  CC )
6425, 63mulcld 9404 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  (
( ( x  -  A )  /  ( B  -  A )
)  x.  F )  e.  CC )
6525, 60mulcld 9404 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  (
( ( x  -  A )  /  ( B  -  A )
)  x.  E )  e.  CC )
6660, 64, 65addsub12d 9740 . . . . . . . . . . . . 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 ) ) ) )
67 areaquad.11 . . . . . . . . . . . . . 14  |-  V  =  ( E  +  ( ( ( x  -  A )  /  ( B  -  A )
)  x.  ( F  -  E ) ) )
6825, 63, 60subdid 9798 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  (
( ( x  -  A )  /  ( B  -  A )
)  x.  ( F  -  E ) )  =  ( ( ( ( x  -  A
)  /  ( B  -  A ) )  x.  F )  -  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  E
) ) )
6968oveq2d 6105 . . . . . . . . . . . . . 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 ) ) ) )
7067, 69syl5eq 2485 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  V  =  ( E  +  ( ( ( ( x  -  A )  /  ( B  -  A ) )  x.  F )  -  (
( ( x  -  A )  /  ( B  -  A )
)  x.  E ) ) ) )
7136, 25, 60subdird 9799 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  (
( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) )  x.  E )  =  ( ( 1  x.  E )  -  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  E
) ) )
7259mulid2i 9387 . . . . . . . . . . . . . . . 16  |-  ( 1  x.  E )  =  E
7372oveq1i 6099 . . . . . . . . . . . . . . 15  |-  ( ( 1  x.  E )  -  ( ( ( x  -  A )  /  ( B  -  A ) )  x.  E ) )  =  ( E  -  (
( ( x  -  A )  /  ( B  -  A )
)  x.  E ) )
7471, 73syl6eq 2489 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  (
( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) )  x.  E )  =  ( E  -  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  E
) ) )
7574oveq2d 6105 . . . . . . . . . . . . 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 ) ) ) )
7666, 70, 753eqtr4d 2483 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  V  =  ( ( ( ( x  -  A
)  /  ( B  -  A ) )  x.  F )  +  ( ( 1  -  ( ( x  -  A )  /  ( B  -  A )
) )  x.  E
) ) )
7745, 60mulcld 9404 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  (
( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) )  x.  E )  e.  CC )
7864, 77addcomd 9569 . . . . . . . . . . . 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
) ) )
7945, 60mulcomd 9405 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  (
( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) )  x.  E )  =  ( E  x.  ( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) ) ) )
8025, 63mulcomd 9405 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  (
( ( x  -  A )  /  ( B  -  A )
)  x.  F )  =  ( F  x.  ( ( x  -  A )  /  ( B  -  A )
) ) )
8179, 80oveq12d 6107 . . . . . . . . . . . 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 ) ) ) ) )
8276, 78, 813eqtrd 2477 . . . . . . . . . . 11  |-  ( x  e.  RR  ->  V  =  ( ( E  x.  ( 1  -  ( ( x  -  A )  /  ( B  -  A )
) ) )  +  ( F  x.  (
( x  -  A
)  /  ( B  -  A ) ) ) ) )
8358a1i 11 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  E  e.  RR )
8483, 44remulcld 9412 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  ( E  x.  ( 1  -  ( ( x  -  A )  / 
( B  -  A
) ) ) )  e.  RR )
8561a1i 11 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  F  e.  RR )
8685, 24remulcld 9412 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  ( F  x.  ( (
x  -  A )  /  ( B  -  A ) ) )  e.  RR )
8784, 86readdcld 9411 . . . . . . . . . . 11  |-  ( x  e.  RR  ->  (
( E  x.  (
1  -  ( ( x  -  A )  /  ( B  -  A ) ) ) )  +  ( F  x.  ( ( x  -  A )  / 
( B  -  A
) ) ) )  e.  RR )
8882, 87eqeltrd 2515 . . . . . . . . . 10  |-  ( x  e.  RR  ->  V  e.  RR )
89 iccssre 11375 . . . . . . . . . 10  |-  ( ( U  e.  RR  /\  V  e.  RR )  ->  ( U [,] V
)  C_  RR )
9057, 88, 89syl2anc 661 . . . . . . . . 9  |-  ( x  e.  RR  ->  ( U [,] V )  C_  RR )
915, 90syl 16 . . . . . . . 8  |-  ( x  e.  ( A [,] B )  ->  ( U [,] V )  C_  RR )
9291sselda 3354 . . . . . . 7  |-  ( ( x  e.  ( A [,] B )  /\  y  e.  ( U [,] V ) )  -> 
y  e.  RR )
936, 92jca 532 . . . . . 6  |-  ( ( x  e.  ( A [,] B )  /\  y  e.  ( U [,] V ) )  -> 
( x  e.  RR  /\  y  e.  RR ) )
9493ssopab2i 4614 . . . . 5  |-  { <. x ,  y >.  |  ( x  e.  ( A [,] B )  /\  y  e.  ( U [,] V ) ) } 
C_  { <. x ,  y >.  |  ( x  e.  RR  /\  y  e.  RR ) }
95 areaquad.12 . . . . 5  |-  S  =  { <. x ,  y
>.  |  ( x  e.  ( A [,] B
)  /\  y  e.  ( U [,] V ) ) }
96 df-xp 4844 . . . . 5  |-  ( RR 
X.  RR )  =  { <. x ,  y
>.  |  ( x  e.  RR  /\  y  e.  RR ) }
9794, 95, 963sstr4i 3393 . . . 4  |-  S  C_  ( RR  X.  RR )
98 iftrue 3795 . . . . . . . . . 10  |-  ( x  e.  ( A [,] B )  ->  if ( x  e.  ( A [,] B ) ,  ( V  -  U
) ,  0 )  =  ( V  -  U ) )
99 nfv 1673 . . . . . . . . . . . . 13  |-  F/ y  x  e.  ( A [,] B )
100 nfopab2 4357 . . . . . . . . . . . . . . 15  |-  F/_ y { <. x ,  y
>.  |  ( x  e.  ( A [,] B
)  /\  y  e.  ( U [,] V ) ) }
10195, 100nfcxfr 2574 . . . . . . . . . . . . . 14  |-  F/_ y S
102 nfcv 2577 . . . . . . . . . . . . . 14  |-  F/_ y { x }
103101, 102nfima 5175 . . . . . . . . . . . . 13  |-  F/_ y
( S " {
x } )
104 nfcv 2577 . . . . . . . . . . . . 13  |-  F/_ y
( U [,] V
)
105 vex 2973 . . . . . . . . . . . . . . . 16  |-  x  e. 
_V
106 vex 2973 . . . . . . . . . . . . . . . 16  |-  y  e. 
_V
107105, 106elimasn 5192 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( S " { x } )  <->  <. x ,  y >.  e.  S )
10895eleq2i 2505 . . . . . . . . . . . . . . 15  |-  ( <.
x ,  y >.  e.  S  <->  <. x ,  y
>.  e.  { <. x ,  y >.  |  ( x  e.  ( A [,] B )  /\  y  e.  ( U [,] V ) ) } )
109 opabid 4594 . . . . . . . . . . . . . . 15  |-  ( <.
x ,  y >.  e.  { <. x ,  y
>.  |  ( x  e.  ( A [,] B
)  /\  y  e.  ( U [,] V ) ) }  <->  ( x  e.  ( A [,] B
)  /\  y  e.  ( U [,] V ) ) )
110107, 108, 1093bitri 271 . . . . . . . . . . . . . 14  |-  ( y  e.  ( S " { x } )  <-> 
( x  e.  ( A [,] B )  /\  y  e.  ( U [,] V ) ) )
111110baib 896 . . . . . . . . . . . . 13  |-  ( x  e.  ( A [,] B )  ->  (
y  e.  ( S
" { x }
)  <->  y  e.  ( U [,] V ) ) )
11299, 103, 104, 111eqrd 3372 . . . . . . . . . . . 12  |-  ( x  e.  ( A [,] B )  ->  ( S " { x }
)  =  ( U [,] V ) )
113112fveq2d 5693 . . . . . . . . . . 11  |-  ( x  e.  ( A [,] B )  ->  ( vol `  ( S " { x } ) )  =  ( vol `  ( U [,] V
) ) )
1145, 57syl 16 . . . . . . . . . . . . 13  |-  ( x  e.  ( A [,] B )  ->  U  e.  RR )
1155, 88syl 16 . . . . . . . . . . . . 13  |-  ( x  e.  ( A [,] B )  ->  V  e.  RR )
116 iccmbl 21045 . . . . . . . . . . . . 13  |-  ( ( U  e.  RR  /\  V  e.  RR )  ->  ( U [,] V
)  e.  dom  vol )
117114, 115, 116syl2anc 661 . . . . . . . . . . . 12  |-  ( x  e.  ( A [,] B )  ->  ( U [,] V )  e. 
dom  vol )
118 mblvol 21011 . . . . . . . . . . . 12  |-  ( ( U [,] V )  e.  dom  vol  ->  ( vol `  ( U [,] V ) )  =  ( vol* `  ( U [,] V
) ) )
119117, 118syl 16 . . . . . . . . . . 11  |-  ( x  e.  ( A [,] B )  ->  ( vol `  ( U [,] V ) )  =  ( vol* `  ( U [,] V ) ) )
1205, 53syl 16 . . . . . . . . . . . . . 14  |-  ( x  e.  ( A [,] B )  ->  ( C  x.  ( 1  -  ( ( x  -  A )  / 
( B  -  A
) ) ) )  e.  RR )
1215, 55syl 16 . . . . . . . . . . . . . 14  |-  ( x  e.  ( A [,] B )  ->  ( D  x.  ( (
x  -  A )  /  ( B  -  A ) ) )  e.  RR )
1225, 84syl 16 . . . . . . . . . . . . . 14  |-  ( x  e.  ( A [,] B )  ->  ( E  x.  ( 1  -  ( ( x  -  A )  / 
( B  -  A
) ) ) )  e.  RR )
1235, 86syl 16 . . . . . . . . . . . . . 14  |-  ( x  e.  ( A [,] B )  ->  ( F  x.  ( (
x  -  A )  /  ( B  -  A ) ) )  e.  RR )
1247a1i 11 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( A [,] B )  ->  C  e.  RR )
12558a1i 11 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( A [,] B )  ->  E  e.  RR )
1265, 44syl 16 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( A [,] B )  ->  (
1  -  ( ( x  -  A )  /  ( B  -  A ) ) )  e.  RR )
1275, 24syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( A [,] B )  ->  (
( x  -  A
)  /  ( B  -  A ) )  e.  RR )
128127recnd 9410 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( A [,] B )  ->  (
( x  -  A
)  /  ( B  -  A ) )  e.  CC )
129128subidd 9705 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( A [,] B )  ->  (
( ( x  -  A )  /  ( B  -  A )
)  -  ( ( x  -  A )  /  ( B  -  A ) ) )  =  0 )
130 1red 9399 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( A [,] B )  ->  1  e.  RR )
1312a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( A [,] B )  ->  B  e.  RR )
1321a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( A [,] B )  ->  A  e.  RR )
1331rexri 9434 . . . . . . . . . . . . . . . . . . . . 21  |-  A  e. 
RR*
1342rexri 9434 . . . . . . . . . . . . . . . . . . . . 21  |-  B  e. 
RR*
135 iccleub 11349 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  x  e.  ( A [,] B
) )  ->  x  <_  B )
136133, 134, 135mp3an12 1304 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( A [,] B )  ->  x  <_  B )
1375, 131, 132, 136lesub1dd 9953 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( A [,] B )  ->  (
x  -  A )  <_  ( B  -  A ) )
1385, 1, 10sylancl 662 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( A [,] B )  ->  (
x  -  A )  e.  RR )
13912a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( A [,] B )  ->  ( B  -  A )  e.  RR )
14016subidi 9677 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A  -  A )  =  0
141132, 131, 132ltsub1d 9946 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( A [,] B )  ->  ( A  <  B  <->  ( A  -  A )  <  ( B  -  A )
) )
14218, 141mpbii 211 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( A [,] B )  ->  ( A  -  A )  <  ( B  -  A
) )
143140, 142syl5eqbrr 4324 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( A [,] B )  ->  0  <  ( B  -  A
) )
144 lediv1 10192 . . . . . . . . . . . . . . . . . . . 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 )
) ) )
145138, 139, 139, 143, 144syl112anc 1222 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( A [,] B )  ->  (
( x  -  A
)  <_  ( B  -  A )  <->  ( (
x  -  A )  /  ( B  -  A ) )  <_ 
( ( B  -  A )  /  ( B  -  A )
) ) )
146137, 145mpbid 210 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( A [,] B )  ->  (
( x  -  A
)  /  ( B  -  A ) )  <_  ( ( B  -  A )  / 
( B  -  A
) ) )
14712recni 9396 . . . . . . . . . . . . . . . . . . 19  |-  ( B  -  A )  e.  CC
148147, 22dividi 10062 . . . . . . . . . . . . . . . . . 18  |-  ( ( B  -  A )  /  ( B  -  A ) )  =  1
149146, 148syl6breq 4329 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( A [,] B )  ->  (
( x  -  A
)  /  ( B  -  A ) )  <_  1 )
150127, 130, 127, 149lesub1dd 9953 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( A [,] B )  ->  (
( ( x  -  A )  /  ( B  -  A )
)  -  ( ( x  -  A )  /  ( B  -  A ) ) )  <_  ( 1  -  ( ( x  -  A )  /  ( B  -  A )
) ) )
151129, 150eqbrtrrd 4312 . . . . . . . . . . . . . . 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 )
154124, 125, 126, 151, 153lemul1ad 10270 . . . . . . . . . . . . . 14  |-  ( x  e.  ( A [,] B )  ->  ( C  x.  ( 1  -  ( ( x  -  A )  / 
( B  -  A
) ) ) )  <_  ( E  x.  ( 1  -  (
( x  -  A
)  /  ( B  -  A ) ) ) ) )
15526a1i 11 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( A [,] B )  ->  D  e.  RR )
15661a1i 11 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( A [,] B )  ->  F  e.  RR )
157139, 143elrpd 11023 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( A [,] B )  ->  ( B  -  A )  e.  RR+ )
158 iccgelb 11350 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  x  e.  ( A [,] B
) )  ->  A  <_  x )
159133, 134, 158mp3an12 1304 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( A [,] B )  ->  A  <_  x )
160132, 5, 132, 159lesub1dd 9953 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( A [,] B )  ->  ( A  -  A )  <_  ( x  -  A
) )
161140, 160syl5eqbrr 4324 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( A [,] B )  ->  0  <_  ( x  -  A
) )
162138, 157, 161divge0d 11061 . . . . . . . . . . . . . . 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, 127, 162, 164lemul1ad 10270 . . . . . . . . . . . . . 14  |-  ( x  e.  ( A [,] B )  ->  ( D  x.  ( (
x  -  A )  /  ( B  -  A ) ) )  <_  ( F  x.  ( ( x  -  A )  /  ( B  -  A )
) ) )
166120, 121, 122, 123, 154, 165le2addd 9955 . . . . . . . . . . . . 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, 51syl 16 . . . . . . . . . . . . 13  |-  ( x  e.  ( A [,] B )  ->  U  =  ( ( C  x.  ( 1  -  ( ( x  -  A )  /  ( B  -  A )
) ) )  +  ( D  x.  (
( x  -  A
)  /  ( B  -  A ) ) ) ) )
1685, 82syl 16 . . . . . . . . . . . . 13  |-  ( x  e.  ( A [,] B )  ->  V  =  ( ( E  x.  ( 1  -  ( ( x  -  A )  /  ( B  -  A )
) ) )  +  ( F  x.  (
( x  -  A
)  /  ( B  -  A ) ) ) ) )
169166, 167, 1683brtr4d 4320 . . . . . . . . . . . 12  |-  ( x  e.  ( A [,] B )  ->  U  <_  V )
170 ovolicc 21004 . . . . . . . . . . . 12  |-  ( ( U  e.  RR  /\  V  e.  RR  /\  U  <_  V )  ->  ( vol* `  ( U [,] V ) )  =  ( V  -  U ) )
171114, 115, 169, 170syl3anc 1218 . . . . . . . . . . 11  |-  ( x  e.  ( A [,] B )  ->  ( vol* `  ( U [,] V ) )  =  ( V  -  U ) )
172113, 119, 1713eqtrd 2477 . . . . . . . . . 10  |-  ( x  e.  ( A [,] B )  ->  ( vol `  ( S " { x } ) )  =  ( V  -  U ) )
17398, 172eqtr4d 2476 . . . . . . . . 9  |-  ( x  e.  ( A [,] B )  ->  if ( x  e.  ( A [,] B ) ,  ( V  -  U
) ,  0 )  =  ( vol `  ( S " { x }
) ) )
174 iffalse 3797 . . . . . . . . . 10  |-  ( -.  x  e.  ( A [,] B )  ->  if ( x  e.  ( A [,] B ) ,  ( V  -  U ) ,  0 )  =  0 )
175 nfv 1673 . . . . . . . . . . . . 13  |-  F/ y  -.  x  e.  ( A [,] B )
176 nfcv 2577 . . . . . . . . . . . . 13  |-  F/_ y (/)
177110simplbi 460 . . . . . . . . . . . . . 14  |-  ( y  e.  ( S " { x } )  ->  x  e.  ( A [,] B ) )
178 noel 3639 . . . . . . . . . . . . . . 15  |-  -.  y  e.  (/)
179178pm2.21i 131 . . . . . . . . . . . . . 14  |-  ( y  e.  (/)  ->  x  e.  ( A [,] B ) )
180177, 179pm5.21ni 352 . . . . . . . . . . . . 13  |-  ( -.  x  e.  ( A [,] B )  -> 
( y  e.  ( S " { x } )  <->  y  e.  (/) ) )
181175, 103, 176, 180eqrd 3372 . . . . . . . . . . . 12  |-  ( -.  x  e.  ( A [,] B )  -> 
( S " {
x } )  =  (/) )
182181fveq2d 5693 . . . . . . . . . . 11  |-  ( -.  x  e.  ( A [,] B )  -> 
( vol `  ( S " { x }
) )  =  ( vol `  (/) ) )
183 0mbl 21019 . . . . . . . . . . . . 13  |-  (/)  e.  dom  vol
184 mblvol 21011 . . . . . . . . . . . . 13  |-  ( (/)  e.  dom  vol  ->  ( vol `  (/) )  =  ( vol* `  (/) ) )
185183, 184ax-mp 5 . . . . . . . . . . . 12  |-  ( vol `  (/) )  =  ( vol* `  (/) )
186 ovol0 20974 . . . . . . . . . . . 12  |-  ( vol* `  (/) )  =  0
187185, 186eqtri 2461 . . . . . . . . . . 11  |-  ( vol `  (/) )  =  0
188182, 187syl6eq 2489 . . . . . . . . . 10  |-  ( -.  x  e.  ( A [,] B )  -> 
( vol `  ( S " { x }
) )  =  0 )
189174, 188eqtr4d 2476 . . . . . . . . 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 2445 . . . . . . 7  |-  ( vol `  ( S " {
x } ) )  =  if ( x  e.  ( A [,] B ) ,  ( V  -  U ) ,  0 )
19288, 57resubcld 9774 . . . . . . . 8  |-  ( x  e.  RR  ->  ( V  -  U )  e.  RR )
193 0re 9384 . . . . . . . 8  |-  0  e.  RR
194 ifcl 3829 . . . . . . . 8  |-  ( ( ( V  -  U
)  e.  RR  /\  0  e.  RR )  ->  if ( x  e.  ( A [,] B
) ,  ( V  -  U ) ,  0 )  e.  RR )
195192, 193, 194sylancl 662 . . . . . . 7  |-  ( x  e.  RR  ->  if ( x  e.  ( A [,] B ) ,  ( V  -  U
) ,  0 )  e.  RR )
196191, 195syl5eqel 2525 . . . . . 6  |-  ( x  e.  RR  ->  ( vol `  ( S " { x } ) )  e.  RR )
197 volf 21010 . . . . . . . 8  |-  vol : dom  vol --> ( 0 [,] +oo )
198 ffun 5559 . . . . . . . 8  |-  ( vol
: dom  vol --> ( 0 [,] +oo )  ->  Fun  vol )
199197, 198ax-mp 5 . . . . . . 7  |-  Fun  vol
200 iftrue 3795 . . . . . . . . . 10  |-  ( x  e.  ( A [,] B )  ->  if ( x  e.  ( A [,] B ) ,  ( U [,] V
) ,  (/) )  =  ( U [,] V
) )
201112, 200eqtr4d 2476 . . . . . . . . 9  |-  ( x  e.  ( A [,] B )  ->  ( S " { x }
)  =  if ( x  e.  ( A [,] B ) ,  ( U [,] V
) ,  (/) ) )
202 iffalse 3797 . . . . . . . . . 10  |-  ( -.  x  e.  ( A [,] B )  ->  if ( x  e.  ( A [,] B ) ,  ( U [,] V ) ,  (/) )  =  (/) )
203181, 202eqtr4d 2476 . . . . . . . . 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
) ,  (/) )
20557, 88, 116syl2anc 661 . . . . . . . . 9  |-  ( x  e.  RR  ->  ( U [,] V )  e. 
dom  vol )
206183a1i 11 . . . . . . . . 9  |-  ( x  e.  RR  ->  (/)  e.  dom  vol )
207205, 206ifcld 3830 . . . . . . . 8  |-  ( x  e.  RR  ->  if ( x  e.  ( A [,] B ) ,  ( U [,] V
) ,  (/) )  e. 
dom  vol )
208204, 207syl5eqel 2525 . . . . . . 7  |-  ( x  e.  RR  ->  ( S " { x }
)  e.  dom  vol )
209 fvimacnv 5816 . . . . . . 7  |-  ( ( Fun  vol  /\  ( S " { x }
)  e.  dom  vol )  ->  ( ( vol `  ( S " {
x } ) )  e.  RR  <->  ( S " { x } )  e.  ( `' vol " RR ) ) )
210199, 208, 209sylancr 663 . . . . . 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 2779 . . . 4  |-  A. x  e.  RR  ( S " { x } )  e.  ( `' vol " RR )
2134a1i 11 . . . . . 6  |-  ( 0  e.  RR  ->  ( A [,] B )  C_  RR )
214 rembl 21020 . . . . . . 7  |-  RR  e.  dom  vol
215214a1i 11 . . . . . 6  |-  ( 0  e.  RR  ->  RR  e.  dom  vol )
216115, 114resubcld 9774 . . . . . . . 8  |-  ( x  e.  ( A [,] B )  ->  ( V  -  U )  e.  RR )
217172, 216eqeltrd 2515 . . . . . . 7  |-  ( x  e.  ( A [,] B )  ->  ( vol `  ( S " { x } ) )  e.  RR )
218217adantl 466 . . . . . 6  |-  ( ( 0  e.  RR  /\  x  e.  ( A [,] B ) )  -> 
( vol `  ( S " { x }
) )  e.  RR )
219 eldifn 3477 . . . . . . . 8  |-  ( x  e.  ( RR  \ 
( A [,] B
) )  ->  -.  x  e.  ( A [,] B ) )
220219, 188syl 16 . . . . . . 7  |-  ( x  e.  ( RR  \ 
( A [,] B
) )  ->  ( vol `  ( S " { x } ) )  =  0 )
221220adantl 466 . . . . . 6  |-  ( ( 0  e.  RR  /\  x  e.  ( RR  \  ( A [,] B
) ) )  -> 
( vol `  ( S " { x }
) )  =  0 )
222172mpteq2ia 4372 . . . . . . . 8  |-  ( x  e.  ( A [,] B )  |->  ( vol `  ( S " {
x } ) ) )  =  ( x  e.  ( A [,] B )  |->  ( V  -  U ) )
223 eqid 2441 . . . . . . . . . . 11  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
224223subcn 20440 . . . . . . . . . . . 12  |-  -  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) )
225224a1i 11 . . . . . . . . . . 11  |-  ( T. 
->  -  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
)  Cn  ( TopOpen ` fld )
) )
22667mpteq2i 4373 . . . . . . . . . . . 12  |-  ( x  e.  ( A [,] B )  |->  V )  =  ( x  e.  ( A [,] B
)  |->  ( E  +  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  ( F  -  E )
) ) )
227223addcn 20439 . . . . . . . . . . . . . 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 9337 . . . . . . . . . . . . . . . 16  |-  RR  C_  CC
2304, 229sstri 3363 . . . . . . . . . . . . . . 15  |-  ( A [,] B )  C_  CC
231 ssid 3373 . . . . . . . . . . . . . . 15  |-  CC  C_  CC
232 cncfmptc 20485 . . . . . . . . . . . . . . 15  |-  ( ( E  e.  CC  /\  ( A [,] B ) 
C_  CC  /\  CC  C_  CC )  ->  ( x  e.  ( A [,] B )  |->  E )  e.  ( ( A [,] B ) -cn-> CC ) )
23359, 230, 231, 232mp3an 1314 . . . . . . . . . . . . . 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 3350 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( A [,] B )  ->  x  e.  CC )
23616a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( A [,] B )  ->  A  e.  CC )
237147a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( A [,] B )  ->  ( B  -  A )  e.  CC )
23822a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( A [,] B )  ->  ( B  -  A )  =/=  0 )
239235, 236, 237, 238divsubdird 10144 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( A [,] B )  ->  (
( x  -  A
)  /  ( B  -  A ) )  =  ( ( x  /  ( B  -  A ) )  -  ( A  /  ( B  -  A )
) ) )
240239adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  (
( x  -  A
)  /  ( B  -  A ) )  =  ( ( x  /  ( B  -  A ) )  -  ( A  /  ( B  -  A )
) ) )
241240mpteq2dva 4376 . . . . . . . . . . . . . . 15  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( ( x  -  A )  /  ( B  -  A )
) )  =  ( x  e.  ( A [,] B )  |->  ( ( x  /  ( B  -  A )
)  -  ( A  /  ( B  -  A ) ) ) ) )
242 resmpt 5154 . . . . . . . . . . . . . . . . . . 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 2441 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  CC  |->  ( x  /  ( B  -  A ) ) )  =  ( x  e.  CC  |->  ( x  / 
( B  -  A
) ) )
245244divccncf 20480 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( B  -  A
)  e.  CC  /\  ( B  -  A
)  =/=  0 )  ->  ( x  e.  CC  |->  ( x  / 
( B  -  A
) ) )  e.  ( CC -cn-> CC ) )
246147, 22, 245mp2an 672 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  CC  |->  ( x  /  ( B  -  A ) ) )  e.  ( CC -cn-> CC )
247 rescncf 20471 . . . . . . . . . . . . . . . . . . 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 2512 . . . . . . . . . . . . . . . . 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 ) )
25116, 147, 22divcli 10071 . . . . . . . . . . . . . . . . . 18  |-  ( A  /  ( B  -  A ) )  e.  CC
252 cncfmptc 20485 . . . . . . . . . . . . . . . . . 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 1314 . . . . . . . . . . . . . . . . 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 20488 . . . . . . . . . . . . . . 15  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( ( x  / 
( B  -  A
) )  -  ( A  /  ( B  -  A ) ) ) )  e.  ( ( A [,] B )
-cn-> CC ) )
256241, 255eqeltrd 2515 . . . . . . . . . . . . . 14  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( ( x  -  A )  /  ( B  -  A )
) )  e.  ( ( A [,] B
) -cn-> CC ) )
257 cncfmptc 20485 . . . . . . . . . . . . . . . . 17  |-  ( ( F  e.  CC  /\  ( A [,] B ) 
C_  CC  /\  CC  C_  CC )  ->  ( x  e.  ( A [,] B )  |->  F )  e.  ( ( A [,] B ) -cn-> CC ) )
25862, 230, 231, 257mp3an 1314 . . . . . . . . . . . . . . . 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 20488 . . . . . . . . . . . . . 14  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( F  -  E
) )  e.  ( ( A [,] B
) -cn-> CC ) )
261256, 260mulcncf 20929 . . . . . . . . . . . . 13  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  ( F  -  E )
) )  e.  ( ( A [,] B
) -cn-> CC ) )
262223, 228, 234, 261cncfmpt2f 20488 . . . . . . . . . . . 12  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( E  +  ( ( ( x  -  A )  /  ( B  -  A )
)  x.  ( F  -  E ) ) ) )  e.  ( ( A [,] B
) -cn-> CC ) )
263226, 262syl5eqel 2525 . . . . . . . . . . 11  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  V )  e.  ( ( A [,] B
) -cn-> CC ) )
26432mpteq2i 4373 . . . . . . . . . . . 12  |-  ( x  e.  ( A [,] B )  |->  U )  =  ( x  e.  ( A [,] B
)  |->  ( C  +  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  ( D  -  C )
) ) )
265 cncfmptc 20485 . . . . . . . . . . . . . . 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 1314 . . . . . . . . . . . . . 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 20485 . . . . . . . . . . . . . . . . 17  |-  ( ( D  e.  CC  /\  ( A [,] B ) 
C_  CC  /\  CC  C_  CC )  ->  ( x  e.  ( A [,] B )  |->  D )  e.  ( ( A [,] B ) -cn-> CC ) )
26927, 230, 231, 268mp3an 1314 . . . . . . . . . . . . . . . 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 20488 . . . . . . . . . . . . . 14  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( D  -  C
) )  e.  ( ( A [,] B
) -cn-> CC ) )
272256, 271mulcncf 20929 . . . . . . . . . . . . 13  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  ( D  -  C )
) )  e.  ( ( A [,] B
) -cn-> CC ) )
273223, 228, 267, 272cncfmpt2f 20488 . . . . . . . . . . . 12  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( C  +  ( ( ( x  -  A )  /  ( B  -  A )
)  x.  ( D  -  C ) ) ) )  e.  ( ( A [,] B
) -cn-> CC ) )
274264, 273syl5eqel 2525 . . . . . . . . . . 11  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  U )  e.  ( ( A [,] B
) -cn-> CC ) )
275223, 225, 263, 274cncfmpt2f 20488 . . . . . . . . . 10  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( V  -  U
) )  e.  ( ( A [,] B
) -cn-> CC ) )
276275trud 1378 . . . . . . . . 9  |-  ( x  e.  ( A [,] B )  |->  ( V  -  U ) )  e.  ( ( A [,] B ) -cn-> CC )
277 cniccibl 21316 . . . . . . . . 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 1314 . . . . . . . 8  |-  ( x  e.  ( A [,] B )  |->  ( V  -  U ) )  e.  L^1
279222, 278eqeltri 2511 . . . . . . 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 21281 . . . . 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 22349 . . . 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 ) )
28497, 212, 282, 283mpbir3an 1170 . . 3  |-  S  e. 
dom area
285 areaval 22356 . . 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 21253 . . . 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 2783 . . 3  |-  S. RR ( vol `  ( S
" { x }
) )  _d x  =  S. RR if ( x  e.  ( A [,] B ) ,  ( V  -  U
) ,  0 )  _d x
290 itgss2 21288 . . . 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
29262, 59addcli 9388 . . . . . 6  |-  ( F  +  E )  e.  CC
293 2cnne0 10534 . . . . . 6  |-  ( 2  e.  CC  /\  2  =/=  0 )
294 div32 10012 . . . . . 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 1314 . . . . 5  |-  ( ( ( F  +  E
)  /  2 )  x.  ( B  -  A ) )  =  ( ( F  +  E )  x.  (
( B  -  A
)  /  2 ) )
29627, 8addcli 9388 . . . . . 6  |-  ( D  +  C )  e.  CC
297 div32 10012 . . . . . 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 1314 . . . . 5  |-  ( ( ( D  +  C
)  /  2 )  x.  ( B  -  A ) )  =  ( ( D  +  C )  x.  (
( B  -  A
)  /  2 ) )
299295, 298oveq12i 6101 . . . 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 10390 . . . . . 6  |-  2  e.  CC
301 2ne0 10412 . . . . . 6  |-  2  =/=  0
302292, 300, 301divcli 10071 . . . . 5  |-  ( ( F  +  E )  /  2 )  e.  CC
303296, 300, 301divcli 10071 . . . . 5  |-  ( ( D  +  C )  /  2 )  e.  CC
304302, 303, 147subdiri 9792 . . . 4  |-  ( ( ( ( F  +  E )  /  2
)  -  ( ( D  +  C )  /  2 ) )  x.  ( B  -  A ) )  =  ( ( ( ( F  +  E )  /  2 )  x.  ( B  -  A
) )  -  (
( ( D  +  C )  /  2
)  x.  ( B  -  A ) ) )
305115adantl 466 . . . . . . 7  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  V  e.  RR )
306263trud 1378 . . . . . . . . 9  |-  ( x  e.  ( A [,] B )  |->  V )  e.  ( ( A [,] B ) -cn-> CC )
307 cniccibl 21316 . . . . . . . . 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 1314 . . . . . . . 8  |-  ( x  e.  ( A [,] B )  |->  V )  e.  L^1
309308a1i 11 . . . . . . 7  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  V )  e.  L^1 )
310114adantl 466 . . . . . . 7  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  U  e.  RR )
311274trud 1378 . . . . . . . . 9  |-  ( x  e.  ( A [,] B )  |->  U )  e.  ( ( A [,] B ) -cn-> CC )
312 cniccibl 21316 . . . . . . . . 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 1314 . . . . . . . 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 21301 . . . . . 6  |-  ( T. 
->  S. ( A [,] B ) ( V  -  U )  _d x  =  ( S. ( A [,] B
) V  _d x  -  S. ( A [,] B ) U  _d x ) )
316315trud 1378 . . . . 5  |-  S. ( A [,] B ) ( V  -  U
)  _d x  =  ( S. ( A [,] B ) V  _d x  -  S. ( A [,] B ) U  _d x )
31759, 300, 301divcan4i 10076 . . . . . . . . . . 11  |-  ( ( E  x.  2 )  /  2 )  =  E
318317oveq1i 6099 . . . . . . . . . 10  |-  ( ( ( E  x.  2 )  /  2 )  x.  ( B  -  A ) )  =  ( E  x.  ( B  -  A )
)
31959, 300mulcli 9389 . . . . . . . . . . 11  |-  ( E  x.  2 )  e.  CC
320 div32 10012 . . . . . . . . . . 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 1314 . . . . . . . . . 10  |-  ( ( ( E  x.  2 )  /  2 )  x.  ( B  -  A ) )  =  ( ( E  x.  2 )  x.  (
( B  -  A
)  /  2 ) )
322318, 321eqtr3i 2463 . . . . . . . . 9  |-  ( E  x.  ( B  -  A ) )  =  ( ( E  x.  2 )  x.  (
( B  -  A
)  /  2 ) )
323322oveq1i 6099 . . . . . . . 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 21253 . . . . . . . . . 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 )
32567a1i 11 . . . . . . . . . 10  |-  ( x  e.  ( A [,] B )  ->  V  =  ( E  +  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  ( F  -  E )
) ) )
326324, 325mprg 2783 . . . . . . . . 9  |-  S. ( A [,] B ) V  _d x  =  S. ( A [,] B ) ( E  +  ( ( ( x  -  A )  /  ( B  -  A ) )  x.  ( F  -  E
) ) )  _d x
32758a1i 11 . . . . . . . . . . 11  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  E  e.  RR )
328 cniccibl 21316 . . . . . . . . . . . . 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 1314 . . . . . . . . . . . 12  |-  ( x  e.  ( A [,] B )  |->  E )  e.  L^1
330329a1i 11 . . . . . . . . . . 11  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  E )  e.  L^1 )
331127adantl 466 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  (
( x  -  A
)  /  ( B  -  A ) )  e.  RR )
33261a1i 11 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  F  e.  RR )
333332, 327resubcld 9774 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  ( F  -  E )  e.  RR )
334331, 333remulcld 9412 . . . . . . . . . . 11  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  (
( ( x  -  A )  /  ( B  -  A )
)  x.  ( F  -  E ) )  e.  RR )
335261trud 1378 . . . . . . . . . . . . 13  |-  ( x  e.  ( A [,] B )  |->  ( ( ( x  -  A
)  /  ( B  -  A ) )  x.  ( F  -  E ) ) )  e.  ( ( A [,] B ) -cn-> CC )
336 cniccibl 21316 . . . . . . . . . . . . 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 1314 . . . . . . . . . . . 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 21300 . . . . . . . . . 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 1378 . . . . . . . . 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 21045 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  e.  dom  vol )
3421, 2, 341mp2an 672 . . . . . . . . . . . 12  |-  ( A [,] B )  e. 
dom  vol
343 mblvol 21011 . . . . . . . . . . . . . . 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, 18ltleii 9495 . . . . . . . . . . . . . . 15  |-  A  <_  B
346 ovolicc 21004 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <_  B )  ->  ( vol* `  ( A [,] B ) )  =  ( B  -  A ) )
3471, 2, 345, 346mp3an 1314 . . . . . . . . . . . . . 14  |-  ( vol* `  ( A [,] B ) )  =  ( B  -  A
)
348344, 347eqtri 2461 . . . . . . . . . . . . 13  |-  ( vol `  ( A [,] B
) )  =  ( B  -  A )
349348, 12eqeltri 2511 . . . . . . . . . . . 12  |-  ( vol `  ( A [,] B
) )  e.  RR
350 itgconst 21294 . . . . . . . . . . . 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, 59, 350mp3an 1314 . . . . . . . . . . 11  |-  S. ( A [,] B ) E  _d x  =  ( E  x.  ( vol `  ( A [,] B ) ) )
352348oveq2i 6100 . . . . . . . . . . 11  |-  ( E  x.  ( vol `  ( A [,] B ) ) )  =  ( E  x.  ( B  -  A ) )
353351, 352eqtri 2461 . . . . . . . . . 10  |-  S. ( A [,] B ) E  _d x  =  ( E  x.  ( B  -  A )
)
35462a1i 11 . . . . . . . . . . . . . 14  |-  ( T. 
->  F  e.  CC )
35559a1i 11 . . . . . . . . . . . . . 14  |-  ( T. 
->  E  e.  CC )
356354, 355subcld 9717 . . . . . . . . . . . . 13  |-  ( T. 
->  ( F  -  E
)  e.  CC )
357256trud 1378 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( A [,] B )  |->  ( ( x  -  A )  /  ( B  -  A ) ) )  e.  ( ( A [,] B ) -cn-> CC )
358 cniccibl 21316 . . . . . . . . . . . . . . 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 1314 . . . . . . . . . . . . . 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 21309 . . . . . . . . . . . 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 1378 . . . . . . . . . . 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 21253 . . . . . . . . . . . . . . 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 )
364138recnd 9410 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( A [,] B )  ->  (
x  -  A )  e.  CC )
365364, 237, 238divrec2d 10109 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( A [,] B )  ->  (
( x  -  A
)  /  ( B  -  A ) )  =  ( ( 1  /  ( B  -  A ) )  x.  ( x  -  A
) ) )
366363, 365mprg 2783 . . . . . . . . . . . . . 14  |-  S. ( A [,] B ) ( ( x  -  A )  /  ( B  -  A )
)  _d x  =  S. ( A [,] B ) ( ( 1  /  ( B  -  A ) )  x.  ( x  -  A ) )  _d x
3675adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  x  e.  RR )
368 cncfmptid 20486 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( A [,] B
)  C_  CC  /\  CC  C_  CC )  ->  (
x  e.  ( A [,] B )  |->  x )  e.  ( ( A [,] B )
-cn-> CC ) )
369230, 231, 368mp2an 672 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( A [,] B )  |->  x )  e.  ( ( A [,] B ) -cn-> CC )
370 cniccibl 21316 . . . . . . . . . . . . . . . . . . . . . 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 1314 . . . . . . . . . . . . . . . . . . . . 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 20485 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  CC  /\  ( A [,] B ) 
C_  CC  /\  CC  C_  CC )  ->  ( x  e.  ( A [,] B )  |->  A )  e.  ( ( A [,] B ) -cn-> CC ) )
37516, 230, 231, 374mp3an 1314 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( A [,] B )  |->  A )  e.  ( ( A [,] B ) -cn-> CC )
376 cniccibl 21316 . . . . . . . . . . . . . . . . . . . . . 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 1314 . . . . . . . . . . . . . . . . . . . . 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 21301 . . . . . . . . . . . . . . . . . . 19  |-  ( T. 
->  S. ( A [,] B ) ( x  -  A )  _d x  =  ( S. ( A [,] B
) x  _d x  -  S. ( A [,] B ) A  _d x ) )
380379trud 1378 . . . . . . . . . . . . . . . . . 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 10593 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  1  e.  NN0
385384a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( T. 
->  1  e.  NN0 )
386381, 382, 383, 385itgpowd 29587 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T. 
->  S. ( A [,] B ) ( x ^ 1 )  _d x  =  ( ( ( B ^ (
1  +  1 ) )  -  ( A ^ ( 1  +  1 ) ) )  /  ( 1  +  1 ) ) )
387386trud 1378 . . . . . . . . . . . . . . . . . . . . 21  |-  S. ( A [,] B ) ( x ^ 1 )  _d x  =  ( ( ( B ^ ( 1  +  1 ) )  -  ( A ^ ( 1  +  1 ) ) )  /  ( 1  +  1 ) )
388 1p1e2 10433 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 1  +  1 )  =  2
389388oveq2i 6100 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( B ^ (
1  +  1 ) )  -  ( A ^ ( 1  +  1 ) ) )  /  ( 1  +  1 ) )  =  ( ( ( B ^ ( 1  +  1 ) )  -  ( A ^ ( 1  +  1 ) ) )  /  2 )
390387, 389eqtri 2461 . . . . . . . . . . . . . . . . . . . 20  |-  S. ( A [,] B ) ( x ^ 1 )  _d x  =  ( ( ( B ^ ( 1  +  1 ) )  -  ( A ^ ( 1  +  1 ) ) )  /  2 )
391 itgeq2 21253 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. x  e.  ( A [,] B ) ( x ^ 1 )  =  x  ->  S. ( A [,] B ) ( x ^ 1 )  _d x  =  S. ( A [,] B
) x  _d x )
392235exp1d 12001 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( A [,] B )  ->  (
x ^ 1 )  =  x )
393391, 392mprg 2783 . . . . . . . . . . . . . . . . . . . 20  |-  S. ( A [,] B ) ( x ^ 1 )  _d x  =  S. ( A [,] B ) x  _d x
394388oveq2i 6100 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( B ^ ( 1  +  1 ) )  =  ( B ^ 2 )
395388oveq2i 6100 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A ^ ( 1  +  1 ) )  =  ( A ^ 2 )
396394, 395oveq12i 6101 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( B ^ ( 1  +  1 ) )  -  ( A ^
( 1  +  1 ) ) )  =  ( ( B ^
2 )  -  ( A ^ 2 ) )
397396oveq1i 6099 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( B ^ (
1  +  1 ) )  -  ( A ^ ( 1  +  1 ) ) )  /  2 )  =  ( ( ( B ^ 2 )  -  ( A ^ 2 ) )  /  2 )
398390, 393, 3973eqtr3i 2469 . . . . . . . . . . . . . . . . . . 19  |-  S. ( A [,] B ) x  _d x  =  ( ( ( B ^ 2 )  -  ( A ^ 2 ) )  /  2 )
399 itgconst 21294 . . . . . . . . . . . . . . . . . . . . 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, 16, 399mp3an 1314 . . . . . . . . . . . . . . . . . . . 20  |-  S. ( A [,] B ) A  _d x  =  ( A  x.  ( vol `  ( A [,] B ) ) )
401348oveq2i 6100 . . . . . . . . . . . . . . . . . . . 20  |-  ( A  x.  ( vol `  ( A [,] B ) ) )  =  ( A  x.  ( B  -  A ) )
402400, 401eqtri 2461 . . . . . . . . . . . . . . . . . . 19  |-  S. ( A [,] B ) A  _d x  =  ( A  x.  ( B  -  A )
)
403398, 402oveq12i 6101 . . . . . . . . . . . . . . . . . 18  |-  ( S. ( A [,] B
) x  _d x  -  S. ( A [,] B ) A  _d x )  =  ( ( ( ( B ^ 2 )  -  ( A ^
2 ) )  / 
2 )  -  ( A  x.  ( B  -  A ) ) )
404380, 403eqtri 2461 . . . . . . . . . . . . . . . . 17  |-  S. ( A [,] B ) ( x  -  A
)  _d x  =  ( ( ( ( B ^ 2 )  -  ( A ^
2 ) )  / 
2 )  -  ( A  x.  ( B  -  A ) ) )
405404oveq2i 6100 . . . . . . . . . . . . . . . 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 )
40716a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( T. 
->  A  e.  CC )
408406, 407subcld 9717 . . . . . . . . . . . . . . . . . . 19  |-  ( T. 
->  ( B  -  A
)  e.  CC )
40919a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( T. 
->  B  =/=  A
)
410406, 407, 409subne0d 9726 . . . . . . . . . . . . . . . . . . 19  |-  ( T. 
->  ( B  -  A
)  =/=  0 )
411408, 410reccld 10098 . . . . . . . . . . . . . . . . . 18  |-  ( T. 
->  ( 1  /  ( B  -  A )
)  e.  CC )
412411trud 1378 . . . . . . . . . . . . . . . . 17  |-  ( 1  /  ( B  -  A ) )  e.  CC
41314sqcli 11944 . . . . . . . . . . . . . . . . . . 19  |-  ( B ^ 2 )  e.  CC
41416sqcli 11944 . . . . . . . . . . . . . . . . . . 19  |-  ( A ^ 2 )  e.  CC
415413, 414subcli 9682 . . . . . . . . . . . . . . . . . 18  |-  ( ( B ^ 2 )  -  ( A ^
2 ) )  e.  CC
416415, 300, 301divcli 10071 . . . . . . . . . . . . . . . . 17  |-  ( ( ( B ^ 2 )  -  ( A ^ 2 ) )  /  2 )  e.  CC
41716, 147mulcli 9389 . . . . . . . . . . . . . . . . 17  |-  ( A  x.  ( B  -  A ) )  e.  CC
418412, 416, 417subdii 9791 . . . . . . . . . . . . . . . 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 2461 . . . . . . . . . . . . . . 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
) ) ) )
420138adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  (
x  -  A )  e.  RR )
421367, 372, 373, 378iblsub 21297 . . . . . . . . . . . . . . . . 17  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  ( x  -  A
) )  e.  L^1 )
422411, 420, 421itgmulc2 21309 . . . . . . . . . . . . . . . 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 1378 . . . . . . . . . . . . . . 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 9390 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  /  ( B  -  A ) )  x.  ( A  x.  ( B  -  A
) ) )  =  ( ( A  x.  ( B  -  A
) )  x.  (
1  /  ( B  -  A ) ) )
425417, 147, 22divreci 10074 . . . . . . . . . . . . . . . . 17  |-  ( ( A  x.  ( B  -  A ) )  /  ( B  -  A ) )  =  ( ( A  x.  ( B  -  A
) )  x.  (
1  /  ( B  -  A ) ) )
42616, 147, 22divcan4i 10076 . . . . . . . . . . . . . . . . 17  |-  ( ( A  x.  ( B  -  A ) )  /  ( B  -  A ) )  =  A
427424, 425, 4263eqtr2i 2467 . . . . . . . . . . . . . . . 16  |-  ( ( 1  /  ( B  -  A ) )  x.  ( A  x.  ( B  -  A
) ) )  =  A
428427oveq2i 6100 . . . . . . . . . . . . . . 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 2469 . . . . . . . . . . . . . 14  |-  S. ( A [,] B ) ( ( 1  / 
( B  -  A
) )  x.  (
x  -  A ) )  _d x  =  ( ( ( 1  /  ( B  -  A ) )  x.  ( ( ( B ^ 2 )  -  ( A ^ 2 ) )  /  2 ) )  -  A )
430366, 429eqtri 2461 . . . . . . . . . . . . 13  |-  S. ( A [,] B ) ( ( x  -  A )  /  ( B  -  A )
)  _d x  =  ( ( ( 1  /  ( B  -  A ) )  x.  ( ( ( B ^ 2 )  -  ( A ^ 2 ) )  /  2 ) )  -  A )
43114, 16subsqi 11975 . . . . . . . . . . . . . . . . 17  |-  ( ( B ^ 2 )  -  ( A ^
2 ) )  =  ( ( B  +  A )  x.  ( B  -  A )
)
432431oveq1i 6099 . . . . . . . . . . . . . . . 16  |-  ( ( ( B ^ 2 )  -  ( A ^ 2 ) )  /  2 )  =  ( ( ( B  +  A )  x.  ( B  -  A
) )  /  2
)
433432oveq2i 6100 . . . . . . . . . . . . . . 15  |-  ( ( 1  /  ( B  -  A ) )  x.  ( ( ( B ^ 2 )  -  ( A ^
2 ) )  / 
2 ) )  =  ( ( 1  / 
( B  -  A
) )  x.  (
( ( B  +  A )  x.  ( B  -  A )
)  /  2 ) )
434431, 415eqeltrri 2512 . . . . . . . . . . . . . . . 16  |-  ( ( B  +  A )  x.  ( B  -  A ) )  e.  CC
435412, 434, 300, 301divassi 10085 . . . . . . . . . . . . . . 15  |-  ( ( ( 1  /  ( B  -  A )
)  x.  ( ( B  +  A )  x.  ( B  -  A ) ) )  /  2 )  =  ( ( 1  / 
( B  -  A
) )  x.  (
( ( B  +  A )  x.  ( B  -  A )
)  /  2 ) )
436412, 434mulcomi 9390 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  /  ( B  -  A ) )  x.  ( ( B  +  A )  x.  ( B  -  A
) ) )  =  ( ( ( B  +  A )  x.  ( B  -  A
) )  x.  (
1  /  ( B  -  A ) ) )
437434, 147, 22divreci 10074 . . . . . . . . . . . . . . . . 17  |-  ( ( ( B  +  A
)  x.  ( B  -  A ) )  /  ( B  -  A ) )  =  ( ( ( B  +  A )  x.  ( B  -  A
) )  x.  (
1  /  ( B  -  A ) ) )
43814, 16addcli 9388 . . . . . . . . . . . . . . . . . 18  |-  ( B  +  A )  e.  CC
439438, 147, 22divcan4i 10076 . . . . . . . . . . . . . . . . 17  |-  ( ( ( B  +  A
)  x.  ( B  -  A ) )  /  ( B  -  A ) )  =  ( B  +  A
)
440436, 437, 4393eqtr2i 2467 . . . . . . . . . . . . . . . 16  |-  ( ( 1  /  ( B  -  A ) )  x.  ( ( B  +  A )  x.  ( B  -  A
) ) )  =  ( B  +  A
)
441440oveq1i 6099 . . . . . . . . . . . . . . 15  |-  ( ( ( 1  /  ( B  -  A )
)  x.  ( ( B  +  A )  x.  ( B  -  A ) ) )  /  2 )  =  ( ( B  +  A )  /  2
)
442433, 435, 4413eqtr2i 2467 . . . . . . . . . . . . . 14  |-  ( ( 1  /  ( B  -  A ) )  x.  ( ( ( B ^ 2 )  -  ( A ^
2 ) )  / 
2 ) )  =  ( ( B  +  A )  /  2
)
443442oveq1i 6099 . . . . . . . . . . . . 13  |-  ( ( ( 1  /  ( B  -  A )
)  x.  ( ( ( B ^ 2 )  -  ( A ^ 2 ) )  /  2 ) )  -  A )  =  ( ( ( B  +  A )  / 
2 )  -  A
)
44416, 300mulcli 9389 . . . . . . . . . . . . . . 15  |-  ( A  x.  2 )  e.  CC
445 divsubdir 10025 . . . . . . . . . . . . . . 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 1314 . . . . . . . . . . . . . 14  |-  ( ( ( B  +  A
)  -  ( A  x.  2 ) )  /  2 )  =  ( ( ( B  +  A )  / 
2 )  -  (
( A  x.  2 )  /  2 ) )
44714, 16, 444addsubassi 9697 . . . . . . . . . . . . . . . 16  |-  ( ( B  +  A )  -  ( A  x.  2 ) )  =  ( B  +  ( A  -  ( A  x.  2 ) ) )
448 subsub2 9635 . . . . . . . . . . . . . . . . 17  |-  ( ( B  e.  CC  /\  ( A  x.  2
)  e.  CC  /\  A  e.  CC )  ->  ( B  -  (
( A  x.  2 )  -  A ) )  =  ( B  +  ( A  -  ( A  x.  2
) ) ) )
44914, 444, 16, 448mp3an 1314 . . . . . . . . . . . . . . . 16  |-  ( B  -  ( ( A  x.  2 )  -  A ) )  =  ( B  +  ( A  -  ( A  x.  2 ) ) )
45016times2i 10441 . . . . . . . . . . . . . . . . . . 19  |-  ( A  x.  2 )  =  ( A  +  A
)
451450oveq1i 6099 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  x.  2 )  -  A )  =  ( ( A  +  A )  -  A
)
45216, 16pncan3oi 9624 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  +  A )  -  A )  =  A
453451, 452eqtri 2461 . . . . . . . . . . . . . . . . 17  |-  ( ( A  x.  2 )  -  A )  =  A
454453oveq2i 6100 . . . . . . . . . . . . . . . 16  |-  ( B  -  ( ( A  x.  2 )  -  A ) )  =  ( B  -  A
)
455447, 449, 4543eqtr2i 2467 . . . . . . . . . . . . . . 15  |-  ( ( B  +  A )  -  ( A  x.  2 ) )  =  ( B  -  A
)
456455oveq1i 6099 . . . . . . . . . . . . . 14  |-  ( ( ( B  +  A
)  -  ( A  x.  2 ) )  /  2 )  =  ( ( B  -  A )  /  2
)
45716, 300, 301divcan4i 10076 . . . . . . . . . . . . . . 15  |-  ( ( A  x.  2 )  /  2 )  =  A
458457oveq2i 6100 . . . . . . . . . . . . . 14  |-  ( ( ( B  +  A
)  /  2 )  -  ( ( A  x.  2 )  / 
2 ) )  =  ( ( ( B  +  A )  / 
2 )  -  A
)
459446, 456, 4583eqtr3ri 2470 . . . . . . . . . . . . 13  |-  ( ( ( B  +  A
)  /  2 )  -  A )  =  ( ( B  -  A )  /  2
)
460430, 443, 4593eqtri 2465 . . . . . . . . . . . 12  |-  S. ( A [,] B ) ( ( x  -  A )  /  ( B  -  A )
)  _d x  =  ( ( B  -  A )  /  2
)
461460oveq2i 6100 . . . . . . . . . . 11  |-  ( ( F  -  E )  x.  S. ( A [,] B ) ( ( x  -  A
)  /  ( B  -  A ) )  _d x )  =  ( ( F  -  E )  x.  (
( B  -  A
)  /  2 ) )
462 itgeq2 21253 . . . . . . . . . . . 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 )
46362, 59subcli 9682 . . . . . . . . . . . . . 14  |-  ( F  -  E )  e.  CC
464463a1i 11 . . . . . . . . . . . . 13  |-  ( x  e.  ( A [,] B )  ->  ( F  -  E )  e.  CC )
465464, 128mulcomd 9405 . . . . . . . . . . . 12  |-  ( x  e.  ( A [,] B )  ->  (
( F  -  E
)  x.  ( ( x  -  A )  /  ( B  -  A ) ) )  =  ( ( ( x  -  A )  /  ( B  -  A ) )  x.  ( F  -  E
) ) )
466462, 465mprg 2783 . . . . . . . . . . 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 2470 . . . . . . . . . 10  |-  S. ( A [,] B ) ( ( ( x  -  A )  / 
( B  -  A
) )  x.  ( F  -  E )
)  _d x  =  ( ( F  -  E )  x.  (
( B  -  A
)  /  2 ) )
468353, 467oveq12i 6101 . . . . . . . . 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 2465 . . . . . . . 8  |-  S. ( A [,] B ) V  _d x  =  ( ( E  x.  ( B  -  A
) )  +  ( ( F  -  E
)  x.  ( ( B  -  A )  /  2 ) ) )
470147, 300, 301divcli 10071 . . . . . . . . 9  |-  ( ( B  -  A )  /  2 )  e.  CC
471319, 463, 470adddiri 9395 . . . . . . . 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 2471 . . . . . . 7  |-  S. ( A [,] B ) V  _d x  =  ( ( ( E  x.  2 )  +  ( F  -  E
) )  x.  (
( B  -  A
)  /  2 ) )
473 addsub12 9621 . . . . . . . . . 10  |-  ( ( F  e.  CC  /\  ( E  x.  2
)  e.  CC  /\  E  e.  CC )  ->  ( F  +  ( ( E  x.  2 )  -  E ) )  =  ( ( E  x.  2 )  +  ( F  -  E ) ) )
47462, 319, 59, 473mp3an 1314 . . . . . . . . 9  |-  ( F  +  ( ( E  x.  2 )  -  E ) )  =  ( ( E  x.  2 )  +  ( F  -  E ) )
47559times2i 10441 . . . . . . . . . . . 12  |-  ( E  x.  2 )  =  ( E  +  E
)
476475oveq1i 6099 . . . . . . . . . . 11  |-  ( ( E  x.  2 )  -  E )  =  ( ( E  +  E )  -  E
)
47759, 59pncan3oi 9624 . . . . . . . . . . 11  |-  ( ( E  +  E )  -  E )  =  E
478476, 477eqtri 2461 . . . . . . . . . 10  |-  ( ( E  x.  2 )  -  E )  =  E
479478oveq2i 6100 . . . . . . . . 9  |-  ( F  +  ( ( E  x.  2 )  -  E ) )  =  ( F  +  E
)
480474, 479eqtr3i 2463 . . . . . . . 8  |-  ( ( E  x.  2 )  +  ( F  -  E ) )  =  ( F  +  E
)
481480oveq1i 6099 . . . . . . 7  |-  ( ( ( E  x.  2 )  +  ( F  -  E ) )  x.  ( ( B  -  A )  / 
2 ) )  =  ( ( F  +  E )  x.  (
( B  -  A
)  /  2 ) )
482472, 481eqtri 2461 . . . . . 6  |-  S. ( A [,] B ) V  _d x  =  ( ( F  +  E )  x.  (
( B  -  A
)  /  2 ) )
4838, 300, 301divcan4i 10076 . . . . . . . . . . 11  |-  ( ( C  x.  2 )  /  2 )  =  C
484483oveq1i 6099 . . . . . . . . . 10  |-  ( ( ( C  x.  2 )  /  2 )  x.  ( B  -  A ) )  =  ( C  x.  ( B  -  A )
)
4858, 300mulcli 9389 . . . . . . . . . . 11  |-  ( C  x.  2 )  e.  CC
486 div32 10012 . . . . . . . . . . 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 1314 . . . . . . . . . 10  |-  ( ( ( C  x.  2 )  /  2 )  x.  ( B  -  A ) )  =  ( ( C  x.  2 )  x.  (
( B  -  A
)  /  2 ) )
488484, 487eqtr3i 2463 . . . . . . . . 9  |-  ( C  x.  ( B  -  A ) )  =  ( ( C  x.  2 )  x.  (
( B  -  A
)  /  2 ) )
489488oveq1i 6099 . . . . . . . 8  |-  ( ( C  x.  ( B  -  A ) )  +  ( ( D  -  C )  x.  ( ( B  -  A )  /  2
) ) )  =  ( ( ( C  x.  2 )  x.  ( ( B  -  A )  /  2
) )  +  ( ( D  -  C
)  x.  ( ( B  -  A )  /  2 ) ) )
49032a1i 11 . . . . . . . . . . 11  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  U  =  ( C  +  ( ( ( x  -  A )  / 
( B  -  A
) )  x.  ( D  -  C )
) ) )
491490itgeq2dv 21257 . . . . . . . . . 10  |-  ( T. 
->  S. ( A [,] B ) U  _d x  =  S. ( A [,] B ) ( C  +  ( ( ( x  -  A )  /  ( B  -  A )
)  x.  ( D  -  C ) ) )  _d x )
492491trud 1378 . . . . . . . . 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 21316 . . . . . . . . . . . . 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 1314 . . . . . . . . . . . 12  |-  ( x  e.  ( A [,] B )  |->  C )  e.  L^1
496495a1i 11 . . . . . . . . . . 11  |-  ( T. 
->  ( x  e.  ( A [,] B ) 
|->  C )  e.  L^1 )
49726a1i 11 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  D  e.  RR )
498497, 493resubcld 9774 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  ( D  -  C )  e.  RR )
499331, 498remulcld 9412 . . . . . . . . . . 11  |-  ( ( T.  /\  x  e.  ( A [,] B
) )  ->  (
( ( x  -  A )  /  ( B  -  A )
)  x.  ( D  -  C ) )  e.  RR )
500272trud 1378 . . . . . . . . . . . . 13  |-  ( x  e.  ( A [,] B )  |->  ( ( ( x  -  A
)  /  ( B  -  A ) )  x.  ( D  -  C ) ) )  e.  ( ( A [,] B ) -cn-> CC )
501 cniccibl 21316 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  (
x  e.  ( A [,] B )  |->  ( ( (