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

Theorem areacirc 32082
Description: The area of a circle of radius  R is  pi  x.  R ^ 2. This is Metamath 100 proof #9. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 22-Sep-2017.) (Revised by Brendan Leahy, 11-Jul-2018.)
Hypothesis
Ref Expression
areacirc.1  |-  S  =  { <. x ,  y
>.  |  ( (
x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^
2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) ) }
Assertion
Ref Expression
areacirc  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
(area `  S )  =  ( pi  x.  ( R ^ 2 ) ) )
Distinct variable group:    x, y, R
Allowed substitution hints:    S( x, y)

Proof of Theorem areacirc
Dummy variables  t  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 areacirc.1 . . . . . . 7  |-  S  =  { <. x ,  y
>.  |  ( (
x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^
2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) ) }
2 df-opab 4476 . . . . . . 7  |-  { <. x ,  y >.  |  ( ( x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) ) }  =  { u  |  E. x E. y
( u  =  <. x ,  y >.  /\  (
( x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) ) ) }
31, 2eqtri 2484 . . . . . 6  |-  S  =  { u  |  E. x E. y ( u  =  <. x ,  y
>.  /\  ( ( x  e.  RR  /\  y  e.  RR )  /\  (
( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^
2 ) ) ) }
4 simpl 463 . . . . . . . . 9  |-  ( ( u  =  <. x ,  y >.  /\  (
( x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) ) )  ->  u  =  <. x ,  y >.
)
5 opelxpi 4885 . . . . . . . . . . 11  |-  ( ( x  e.  RR  /\  y  e.  RR )  -> 
<. x ,  y >.  e.  ( RR  X.  RR ) )
65adantr 471 . . . . . . . . . 10  |-  ( ( ( x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) )  ->  <. x ,  y
>.  e.  ( RR  X.  RR ) )
76adantl 472 . . . . . . . . 9  |-  ( ( u  =  <. x ,  y >.  /\  (
( x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) ) )  ->  <. x ,  y >.  e.  ( RR  X.  RR ) )
84, 7eqeltrd 2540 . . . . . . . 8  |-  ( ( u  =  <. x ,  y >.  /\  (
( x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) ) )  ->  u  e.  ( RR  X.  RR ) )
98exlimivv 1789 . . . . . . 7  |-  ( E. x E. y ( u  =  <. x ,  y >.  /\  (
( x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) ) )  ->  u  e.  ( RR  X.  RR ) )
109abssi 3516 . . . . . 6  |-  { u  |  E. x E. y
( u  =  <. x ,  y >.  /\  (
( x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) ) ) }  C_  ( RR  X.  RR )
113, 10eqsstri 3474 . . . . 5  |-  S  C_  ( RR  X.  RR )
1211a1i 11 . . . 4  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  S  C_  ( RR  X.  RR ) )
131areacirclem5 32081 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( S " { t } )  =  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )
14 resqcl 12374 . . . . . . . . . . . . . . 15  |-  ( R  e.  RR  ->  ( R ^ 2 )  e.  RR )
15143ad2ant1 1035 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R ^ 2 )  e.  RR )
16 resqcl 12374 . . . . . . . . . . . . . . 15  |-  ( t  e.  RR  ->  (
t ^ 2 )  e.  RR )
17163ad2ant3 1037 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t ^ 2 )  e.  RR )
1815, 17resubcld 10075 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  e.  RR )
1918adantr 471 . . . . . . . . . . . 12  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( ( R ^
2 )  -  (
t ^ 2 ) )  e.  RR )
20 absresq 13414 . . . . . . . . . . . . . . . 16  |-  ( t  e.  RR  ->  (
( abs `  t
) ^ 2 )  =  ( t ^
2 ) )
21203ad2ant3 1037 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
) ^ 2 )  =  ( t ^
2 ) )
2221breq1d 4426 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( ( abs `  t
) ^ 2 )  <_  ( R ^
2 )  <->  ( t ^ 2 )  <_ 
( R ^ 2 ) ) )
23 recn 9655 . . . . . . . . . . . . . . . . 17  |-  ( t  e.  RR  ->  t  e.  CC )
2423abscld 13547 . . . . . . . . . . . . . . . 16  |-  ( t  e.  RR  ->  ( abs `  t )  e.  RR )
25243ad2ant3 1037 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( abs `  t )  e.  RR )
26 simp1 1014 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  R  e.  RR )
2723absge0d 13555 . . . . . . . . . . . . . . . 16  |-  ( t  e.  RR  ->  0  <_  ( abs `  t
) )
28273ad2ant3 1037 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  0  <_  ( abs `  t
) )
29 simp2 1015 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  0  <_  R )
3025, 26, 28, 29le2sqd 12483 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  ( ( abs `  t ) ^
2 )  <_  ( R ^ 2 ) ) )
3115, 17subge0d 10231 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) )  <->  ( t ^ 2 )  <_ 
( R ^ 2 ) ) )
3222, 30, 313bitr4d 293 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )
3332biimpa 491 . . . . . . . . . . . 12  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )
3419, 33resqrtcld 13528 . . . . . . . . . . 11  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
3534renegcld 10074 . . . . . . . . . 10  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  -> 
-u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
36 iccmbl 22568 . . . . . . . . . 10  |-  ( (
-u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR  /\  ( sqr `  ( ( R ^ 2 )  -  ( t ^
2 ) ) )  e.  RR )  -> 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )  e. 
dom  vol )
3735, 34, 36syl2anc 671 . . . . . . . . 9  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( -u ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )  e.  dom  vol )
38 mblvol 22533 . . . . . . . . . . . 12  |-  ( (
-u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )  e. 
dom  vol  ->  ( vol `  ( -u ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )  =  ( vol* `  ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ) )
3937, 38syl 17 . . . . . . . . . . 11  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( vol `  ( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )  =  ( vol* `  ( -u ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ) )
4019, 33sqrtge0d 13531 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  0  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
4134, 34, 40, 40addge0d 10217 . . . . . . . . . . . . 13  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  0  <_  ( ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  +  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
42 recn 9655 . . . . . . . . . . . . . . . . . . . . 21  |-  ( R  e.  RR  ->  R  e.  CC )
4342sqcld 12446 . . . . . . . . . . . . . . . . . . . 20  |-  ( R  e.  RR  ->  ( R ^ 2 )  e.  CC )
44433ad2ant1 1035 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R ^ 2 )  e.  CC )
4523sqcld 12446 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  e.  RR  ->  (
t ^ 2 )  e.  CC )
46453ad2ant3 1037 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t ^ 2 )  e.  CC )
4744, 46subcld 10012 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  e.  CC )
4847sqrtcld 13548 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  CC )
4948adantr 471 . . . . . . . . . . . . . . . 16  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  CC )
5049, 49subnegd 10019 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )  =  ( ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) )  +  ( sqr `  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) ) )
5150breq2d 4428 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( 0  <_  (
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )  <->  0  <_  ( ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  +  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ) )
5234, 35subge0d 10231 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( 0  <_  (
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )  <->  -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )
5351, 52bitr3d 263 . . . . . . . . . . . . 13  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( 0  <_  (
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  +  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )  <->  -u ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) )  <_  ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
5441, 53mpbid 215 . . . . . . . . . . . 12  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  -> 
-u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
55 ovolicc 22526 . . . . . . . . . . . 12  |-  ( (
-u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR  /\  ( sqr `  ( ( R ^ 2 )  -  ( t ^
2 ) ) )  e.  RR  /\  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  <_ 
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) )  ->  ( vol* `  ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) [,] ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )  =  ( ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
5635, 34, 54, 55syl3anc 1276 . . . . . . . . . . 11  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( vol* `  ( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )  =  ( ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
5739, 56eqtrd 2496 . . . . . . . . . 10  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( vol `  ( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )  =  ( ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
5834, 35resubcld 10075 . . . . . . . . . 10  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )  e.  RR )
5957, 58eqeltrd 2540 . . . . . . . . 9  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( vol `  ( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )  e.  RR )
60 volf 22532 . . . . . . . . . 10  |-  vol : dom  vol --> ( 0 [,] +oo )
61 ffn 5751 . . . . . . . . . 10  |-  ( vol
: dom  vol --> ( 0 [,] +oo )  ->  vol  Fn  dom  vol )
62 elpreima 6025 . . . . . . . . . 10  |-  ( vol 
Fn  dom  vol  ->  (
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )  e.  ( `' vol " RR ) 
<->  ( ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) )  e.  dom  vol 
/\  ( vol `  ( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )  e.  RR ) ) )
6360, 61, 62mp2b 10 . . . . . . . . 9  |-  ( (
-u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )  e.  ( `' vol " RR ) 
<->  ( ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) )  e.  dom  vol 
/\  ( vol `  ( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )  e.  RR ) )
6437, 59, 63sylanbrc 675 . . . . . . . 8  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( -u ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )  e.  ( `' vol " RR ) )
65 0mbl 22542 . . . . . . . . . 10  |-  (/)  e.  dom  vol
66 mblvol 22533 . . . . . . . . . . . . 13  |-  ( (/)  e.  dom  vol  ->  ( vol `  (/) )  =  ( vol* `  (/) ) )
6765, 66ax-mp 5 . . . . . . . . . . . 12  |-  ( vol `  (/) )  =  ( vol* `  (/) )
68 ovol0 22495 . . . . . . . . . . . 12  |-  ( vol* `  (/) )  =  0
6967, 68eqtri 2484 . . . . . . . . . . 11  |-  ( vol `  (/) )  =  0
70 0re 9669 . . . . . . . . . . 11  |-  0  e.  RR
7169, 70eqeltri 2536 . . . . . . . . . 10  |-  ( vol `  (/) )  e.  RR
72 elpreima 6025 . . . . . . . . . . 11  |-  ( vol 
Fn  dom  vol  ->  ( (/) 
e.  ( `' vol " RR )  <->  ( (/)  e.  dom  vol 
/\  ( vol `  (/) )  e.  RR ) ) )
7360, 61, 72mp2b 10 . . . . . . . . . 10  |-  ( (/)  e.  ( `' vol " RR ) 
<->  ( (/)  e.  dom  vol 
/\  ( vol `  (/) )  e.  RR ) )
7465, 71, 73mpbir2an 936 . . . . . . . . 9  |-  (/)  e.  ( `' vol " RR )
7574a1i 11 . . . . . . . 8  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  -.  ( abs `  t
)  <_  R )  -> 
(/)  e.  ( `' vol " RR ) )
7664, 75ifclda 3925 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) )  e.  ( `' vol " RR ) )
7713, 76eqeltrd 2540 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( S " { t } )  e.  ( `' vol " RR ) )
78773expa 1215 . . . . 5  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  RR )  ->  ( S " { t } )  e.  ( `' vol " RR ) )
7978ralrimiva 2814 . . . 4  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  A. t  e.  RR  ( S " { t } )  e.  ( `' vol " RR ) )
8013fveq2d 5892 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( vol `  ( S " { t } ) )  =  ( vol `  if ( ( abs `  t )  <_  R ,  ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ,  (/) ) ) )
81803expa 1215 . . . . . 6  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  RR )  ->  ( vol `  ( S " { t } ) )  =  ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) ) )
8281mpteq2dva 4503 . . . . 5  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  |->  ( vol `  ( S
" { t } ) ) )  =  ( t  e.  RR  |->  ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) ) ) )
83 renegcl 9963 . . . . . . . 8  |-  ( R  e.  RR  ->  -u R  e.  RR )
8483adantr 471 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  -u R  e.  RR )
85 simpl 463 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  R  e.  RR )
86 iccssre 11745 . . . . . . 7  |-  ( (
-u R  e.  RR  /\  R  e.  RR )  ->  ( -u R [,] R )  C_  RR )
8784, 85, 86syl2anc 671 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( -u R [,] R
)  C_  RR )
88 rembl 22543 . . . . . . 7  |-  RR  e.  dom  vol
8988a1i 11 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  RR  e.  dom  vol )
90 fvex 5898 . . . . . . 7  |-  ( vol `  if ( ( abs `  t )  <_  R ,  ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ,  (/) ) )  e.  _V
9190a1i 11 . . . . . 6  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  ( -u R [,] R ) )  ->  ( vol `  if ( ( abs `  t )  <_  R ,  ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ,  (/) ) )  e.  _V )
92 eldif 3426 . . . . . . . . 9  |-  ( t  e.  ( RR  \ 
( -u R [,] R
) )  <->  ( t  e.  RR  /\  -.  t  e.  ( -u R [,] R ) ) )
93 3anass 995 . . . . . . . . . . . . . . 15  |-  ( ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R )  <->  ( t  e.  RR  /\  ( -u R  <_  t  /\  t  <_  R ) ) )
9493a1i 11 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R )  <->  ( t  e.  RR  /\  ( -u R  <_  t  /\  t  <_  R ) ) ) )
95833ad2ant1 1035 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  -u R  e.  RR )
96 elicc2 11728 . . . . . . . . . . . . . . 15  |-  ( (
-u R  e.  RR  /\  R  e.  RR )  ->  ( t  e.  ( -u R [,] R )  <->  ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R ) ) )
9795, 26, 96syl2anc 671 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t  e.  ( -u R [,] R )  <->  ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R ) ) )
98 simp3 1016 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  t  e.  RR )
9998, 26absled 13541 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  ( -u R  <_  t  /\  t  <_  R ) ) )
10098biantrurd 515 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( -u R  <_  t  /\  t  <_  R )  <-> 
( t  e.  RR  /\  ( -u R  <_ 
t  /\  t  <_  R ) ) ) )
10199, 100bitrd 261 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  ( t  e.  RR  /\  ( -u R  <_  t  /\  t  <_  R ) ) ) )
10294, 97, 1013bitr4rd 294 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  t  e.  ( -u R [,] R
) ) )
103102biimpd 212 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  ->  t  e.  ( -u R [,] R ) ) )
104103con3d 140 . . . . . . . . . . 11  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -.  t  e.  ( -u R [,] R )  ->  -.  ( abs `  t )  <_  R
) )
1051043expia 1217 . . . . . . . . . 10  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  ->  ( -.  t  e.  ( -u R [,] R )  ->  -.  ( abs `  t )  <_  R ) ) )
106105impd 437 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( ( t  e.  RR  /\  -.  t  e.  ( -u R [,] R ) )  ->  -.  ( abs `  t
)  <_  R )
)
10792, 106syl5bi 225 . . . . . . . 8  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  ( RR  \  ( -u R [,] R ) )  ->  -.  ( abs `  t )  <_  R
) )
108107imp 435 . . . . . . 7  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  ( RR  \  ( -u R [,] R ) ) )  ->  -.  ( abs `  t )  <_  R
)
109 iffalse 3902 . . . . . . . . 9  |-  ( -.  ( abs `  t
)  <_  R  ->  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) )  =  (/) )
110109fveq2d 5892 . . . . . . . 8  |-  ( -.  ( abs `  t
)  <_  R  ->  ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  =  ( vol `  (/) ) )
111110, 69syl6eq 2512 . . . . . . 7  |-  ( -.  ( abs `  t
)  <_  R  ->  ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  =  0 )
112108, 111syl 17 . . . . . 6  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  ( RR  \  ( -u R [,] R ) ) )  ->  ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  =  0 )
11384, 85, 96syl2anc 671 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  <->  ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R ) ) )
11499biimprd 231 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( -u R  <_  t  /\  t  <_  R )  ->  ( abs `  t
)  <_  R )
)
115114expd 442 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -u R  <_  t  ->  ( t  <_  R  ->  ( abs `  t )  <_  R ) ) )
1161153expia 1217 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  ->  ( -u R  <_ 
t  ->  ( t  <_  R  ->  ( abs `  t )  <_  R
) ) ) )
1171163impd 1231 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R )  ->  ( abs `  t )  <_  R ) )
118113, 117sylbid 223 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  ->  ( abs `  t )  <_  R
) )
1191183impia 1212 . . . . . . . . . . 11  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( abs `  t
)  <_  R )
120 iftrue 3899 . . . . . . . . . . . 12  |-  ( ( abs `  t )  <_  R  ->  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) )  =  ( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )
121120fveq2d 5892 . . . . . . . . . . 11  |-  ( ( abs `  t )  <_  R  ->  ( vol `  if ( ( abs `  t )  <_  R ,  (
-u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  =  ( vol `  ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) [,] ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ) )
122119, 121syl 17 . . . . . . . . . 10  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  =  ( vol `  ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) [,] ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ) )
123143ad2ant1 1035 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( R ^ 2 )  e.  RR )
12483, 86mpancom 680 . . . . . . . . . . . . . . . . . 18  |-  ( R  e.  RR  ->  ( -u R [,] R ) 
C_  RR )
125124sselda 3444 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR  /\  t  e.  ( -u R [,] R ) )  -> 
t  e.  RR )
1261253adant2 1033 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
t  e.  RR )
127126resqcld 12474 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( t ^ 2 )  e.  RR )
128123, 127resubcld 10075 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( ( R ^
2 )  -  (
t ^ 2 ) )  e.  RR )
12983, 96mpancom 680 . . . . . . . . . . . . . . . . 17  |-  ( R  e.  RR  ->  (
t  e.  ( -u R [,] R )  <->  ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R ) ) )
130129adantr 471 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  <->  ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R ) ) )
13130, 99, 223bitr3rd 292 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( t ^ 2 )  <_  ( R ^ 2 )  <->  ( -u R  <_  t  /\  t  <_  R ) ) )
13231, 131bitrd 261 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) )  <->  ( -u R  <_  t  /\  t  <_  R ) ) )
133132biimprd 231 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( -u R  <_  t  /\  t  <_  R )  ->  0  <_  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) )
134133expd 442 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -u R  <_  t  ->  ( t  <_  R  ->  0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
1351343expia 1217 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  ->  ( -u R  <_ 
t  ->  ( t  <_  R  ->  0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ) )
1361353impd 1231 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R )  ->  0  <_  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
137130, 136sylbid 223 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  ->  0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )
1381373impia 1212 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )
139128, 138resqrtcld 13528 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
140139renegcld 10074 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  ->  -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
141140, 139, 36syl2anc 671 . . . . . . . . . . 11  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )  e. 
dom  vol )
142141, 38syl 17 . . . . . . . . . 10  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( vol `  ( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )  =  ( vol* `  ( -u ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ) )
143128recnd 9695 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( ( R ^
2 )  -  (
t ^ 2 ) )  e.  CC )
144143sqrtcld 13548 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  CC )
145144, 144subnegd 10019 . . . . . . . . . . 11  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )  =  ( ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) )  +  ( sqr `  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) ) )
146128, 138sqrtge0d 13531 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
0  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
147139, 139, 146, 146addge0d 10217 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
0  <_  ( ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  +  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
148145breq2d 4428 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( 0  <_  (
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )  <->  0  <_  ( ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  +  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ) )
149139, 140subge0d 10231 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( 0  <_  (
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )  <->  -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )
150148, 149bitr3d 263 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( 0  <_  (
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  +  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )  <->  -u ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) )  <_  ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
151147, 150mpbid 215 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  ->  -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
152140, 139, 151, 55syl3anc 1276 . . . . . . . . . . 11  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( vol* `  ( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )  =  ( ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
1531442timesd 10884 . . . . . . . . . . 11  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( 2  x.  ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )  =  ( ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) )  +  ( sqr `  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) ) )
154145, 152, 1533eqtr4d 2506 . . . . . . . . . 10  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( vol* `  ( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )  =  ( 2  x.  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
155122, 142, 1543eqtrd 2500 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  =  ( 2  x.  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )
1561553expa 1215 . . . . . . . 8  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  ( -u R [,] R ) )  ->  ( vol `  if ( ( abs `  t )  <_  R ,  ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ,  (/) ) )  =  ( 2  x.  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )
157156mpteq2dva 4503 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  |->  ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) ) )  =  ( t  e.  (
-u R [,] R
)  |->  ( 2  x.  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ) )
158 areacirclem3 32079 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  |->  ( 2  x.  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )  e.  L^1 )
159157, 158eqeltrd 2540 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  |->  ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) ) )  e.  L^1 )
16087, 89, 91, 112, 159iblss2 22812 . . . . 5  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  |->  ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) ) )  e.  L^1 )
16182, 160eqeltrd 2540 . . . 4  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  |->  ( vol `  ( S
" { t } ) ) )  e.  L^1 )
162 dmarea 23932 . . . 4  |-  ( S  e.  dom area  <->  ( S  C_  ( RR  X.  RR )  /\  A. t  e.  RR  ( S " { t } )  e.  ( `' vol " RR )  /\  (
t  e.  RR  |->  ( vol `  ( S
" { t } ) ) )  e.  L^1 ) )
16312, 79, 161, 162syl3anbrc 1198 . . 3  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  S  e.  dom area )
164 areaval 23939 . . 3  |-  ( S  e.  dom area  ->  (area `  S )  =  S. RR ( vol `  ( S " { t } ) )  _d t )
165163, 164syl 17 . 2  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
(area `  S )  =  S. RR ( vol `  ( S " {
t } ) )  _d t )
166 elioore 11695 . . . . . 6  |-  ( t  e.  ( -u R (,) R )  ->  t  e.  RR )
167133expa 1215 . . . . . 6  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  RR )  ->  ( S " { t } )  =  if ( ( abs `  t )  <_  R ,  (
-u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )
168166, 167sylan2 481 . . . . 5  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  ( -u R (,) R ) )  ->  ( S " { t } )  =  if ( ( abs `  t )  <_  R ,  (
-u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )
169168fveq2d 5892 . . . 4  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  ( -u R (,) R ) )  ->  ( vol `  ( S " {
t } ) )  =  ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) ) )
170169itgeq2dv 22788 . . 3  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  S. ( -u R (,) R ) ( vol `  ( S " {
t } ) )  _d t  =  S. ( -u R (,) R ) ( vol `  if ( ( abs `  t )  <_  R ,  ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ,  (/) ) )  _d t )
171 ioossre 11725 . . . . 5  |-  ( -u R (,) R )  C_  RR
172171a1i 11 . . . 4  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( -u R (,) R
)  C_  RR )
173 eldif 3426 . . . . . 6  |-  ( t  e.  ( RR  \ 
( -u R (,) R
) )  <->  ( t  e.  RR  /\  -.  t  e.  ( -u R (,) R ) ) )
17483rexrd 9716 . . . . . . . . . . . . . 14  |-  ( R  e.  RR  ->  -u R  e.  RR* )
175 rexr 9712 . . . . . . . . . . . . . 14  |-  ( R  e.  RR  ->  R  e.  RR* )
176 elioo2 11706 . . . . . . . . . . . . . 14  |-  ( (
-u R  e.  RR*  /\  R  e.  RR* )  ->  ( t  e.  (
-u R (,) R
)  <->  ( t  e.  RR  /\  -u R  <  t  /\  t  < 
R ) ) )
177174, 175, 176syl2anc 671 . . . . . . . . . . . . 13  |-  ( R  e.  RR  ->  (
t  e.  ( -u R (,) R )  <->  ( t  e.  RR  /\  -u R  <  t  /\  t  < 
R ) ) )
1781773ad2ant1 1035 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t  e.  ( -u R (,) R )  <->  ( t  e.  RR  /\  -u R  <  t  /\  t  < 
R ) ) )
17998biantrurd 515 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( -u R  <  t  /\  t  <  R )  <-> 
( t  e.  RR  /\  ( -u R  < 
t  /\  t  <  R ) ) ) )
18098, 26absltd 13540 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <  R  <->  ( -u R  <  t  /\  t  < 
R ) ) )
181 3anass 995 . . . . . . . . . . . . . 14  |-  ( ( t  e.  RR  /\  -u R  <  t  /\  t  <  R )  <->  ( t  e.  RR  /\  ( -u R  <  t  /\  t  <  R ) ) )
182181a1i 11 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( t  e.  RR  /\  -u R  <  t  /\  t  <  R )  <->  ( t  e.  RR  /\  ( -u R  <  t  /\  t  <  R ) ) ) )
183179, 180, 1823bitr4rd 294 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( t  e.  RR  /\  -u R  <  t  /\  t  <  R )  <->  ( abs `  t )  <  R
) )
184178, 183bitrd 261 . . . . . . . . . . 11  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t  e.  ( -u R (,) R )  <->  ( abs `  t )  <  R
) )
185184notbid 300 . . . . . . . . . 10  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -.  t  e.  ( -u R (,) R )  <->  -.  ( abs `  t
)  <  R )
)
18626, 25lenltd 9807 . . . . . . . . . 10  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R  <_  ( abs `  t
)  <->  -.  ( abs `  t )  <  R
) )
187185, 186bitr4d 264 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -.  t  e.  ( -u R (,) R )  <-> 
R  <_  ( abs `  t ) ) )
18813adantr 471 . . . . . . . . . . . 12  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( S " {
t } )  =  if ( ( abs `  t )  <_  R ,  ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ,  (/) ) )
189188fveq2d 5892 . . . . . . . . . . 11  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( vol `  ( S " { t } ) )  =  ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) ) )
19025anim1i 576 . . . . . . . . . . . . . . . 16  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( ( abs `  t )  e.  RR  /\  ( abs `  t
)  =  R ) )
191 eqle 9762 . . . . . . . . . . . . . . . 16  |-  ( ( ( abs `  t
)  e.  RR  /\  ( abs `  t )  =  R )  -> 
( abs `  t
)  <_  R )
192190, 191, 1213syl 18 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  =  ( vol `  ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) [,] ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ) )
193 oveq1 6322 . . . . . . . . . . . . . . . . . 18  |-  ( ( abs `  t )  =  R  ->  (
( abs `  t
) ^ 2 )  =  ( R ^
2 ) )
194193adantl 472 . . . . . . . . . . . . . . . . 17  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( ( abs `  t ) ^ 2 )  =  ( R ^ 2 ) )
19521adantr 471 . . . . . . . . . . . . . . . . 17  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( ( abs `  t ) ^ 2 )  =  ( t ^ 2 ) )
196194, 195eqtr3d 2498 . . . . . . . . . . . . . . . 16  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( R ^
2 )  =  ( t ^ 2 ) )
197 oveq1 6322 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R ^ 2 )  =  ( t ^
2 )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  =  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )
198197fveq2d 5892 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R ^ 2 )  =  ( t ^
2 )  ->  ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  =  ( sqr `  (
( t ^ 2 )  -  ( t ^ 2 ) ) ) )
199198negeqd 9895 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R ^ 2 )  =  ( t ^
2 )  ->  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  = 
-u ( sqr `  (
( t ^ 2 )  -  ( t ^ 2 ) ) ) )
200199, 198oveq12d 6333 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R ^ 2 )  =  ( t ^
2 )  ->  ( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )  =  ( -u ( sqr `  ( ( t ^
2 )  -  (
t ^ 2 ) ) ) [,] ( sqr `  ( ( t ^ 2 )  -  ( t ^ 2 ) ) ) ) )
20116recnd 9695 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  e.  RR  ->  (
t ^ 2 )  e.  CC )
202201subidd 10000 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  e.  RR  ->  (
( t ^ 2 )  -  ( t ^ 2 ) )  =  0 )
203202fveq2d 5892 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  e.  RR  ->  ( sqr `  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )  =  ( sqr `  0
) )
204203negeqd 9895 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  e.  RR  ->  -u ( sqr `  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )  = 
-u ( sqr `  0
) )
205 sqrt0 13354 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( sqr `  0 )  =  0
206205negeqi 9894 . . . . . . . . . . . . . . . . . . . . . . 23  |-  -u ( sqr `  0 )  = 
-u 0
207 neg0 9946 . . . . . . . . . . . . . . . . . . . . . . 23  |-  -u 0  =  0
208206, 207eqtri 2484 . . . . . . . . . . . . . . . . . . . . . 22  |-  -u ( sqr `  0 )  =  0
209204, 208syl6eq 2512 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  e.  RR  ->  -u ( sqr `  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )  =  0 )
210203, 205syl6eq 2512 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  e.  RR  ->  ( sqr `  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )  =  0 )
211209, 210oveq12d 6333 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  e.  RR  ->  ( -u ( sqr `  (
( t ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( t ^
2 )  -  (
t ^ 2 ) ) ) )  =  ( 0 [,] 0
) )
2122113ad2ant3 1037 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -u ( sqr `  (
( t ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( t ^
2 )  -  (
t ^ 2 ) ) ) )  =  ( 0 [,] 0
) )
213200, 212sylan9eqr 2518 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( R ^ 2 )  =  ( t ^ 2 ) )  ->  ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) )  =  ( 0 [,] 0 ) )
214213fveq2d 5892 . . . . . . . . . . . . . . . . 17  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( R ^ 2 )  =  ( t ^ 2 ) )  ->  ( vol `  ( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )  =  ( vol `  (
0 [,] 0 ) ) )
215 iccmbl 22568 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 0  e.  RR  /\  0  e.  RR )  ->  ( 0 [,] 0
)  e.  dom  vol )
21670, 70, 215mp2an 683 . . . . . . . . . . . . . . . . . . 19  |-  ( 0 [,] 0 )  e. 
dom  vol
217 mblvol 22533 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 0 [,] 0 )  e.  dom  vol  ->  ( vol `  ( 0 [,] 0 ) )  =  ( vol* `  ( 0 [,] 0
) ) )
218216, 217ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ( vol `  ( 0 [,] 0
) )  =  ( vol* `  (
0 [,] 0 ) )
219 0xr 9713 . . . . . . . . . . . . . . . . . . . 20  |-  0  e.  RR*
220 iccid 11710 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 0  e.  RR*  ->  ( 0 [,] 0 )  =  { 0 } )
221220fveq2d 5892 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  e.  RR*  ->  ( vol* `  ( 0 [,] 0 ) )  =  ( vol* `  { 0 } ) )
222219, 221ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  ( vol* `  ( 0 [,] 0 ) )  =  ( vol* `  { 0 } )
223 ovolsn 22497 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  e.  RR  ->  ( vol* `  { 0 } )  =  0 )
22470, 223ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  ( vol* `  { 0 } )  =  0
225222, 224eqtri 2484 . . . . . . . . . . . . . . . . . 18  |-  ( vol* `  ( 0 [,] 0 ) )  =  0
226218, 225eqtri 2484 . . . . . . . . . . . . . . . . 17  |-  ( vol `  ( 0 [,] 0
) )  =  0
227214, 226syl6eq 2512 . . . . . . . . . . . . . . . 16  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( R ^ 2 )  =  ( t ^ 2 ) )  ->  ( vol `  ( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )  =  0 )
228196, 227syldan 477 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( vol `  ( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )  =  0 )
229192, 228eqtrd 2496 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  =  0 )
230229ex 440 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  =  R  -> 
( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  =  0 ) )
231230adantr 471 . . . . . . . . . . . 12  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( ( abs `  t
)  =  R  -> 
( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  =  0 ) )
23226, 25ltnled 9808 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R  <  ( abs `  t
)  <->  -.  ( abs `  t )  <_  R
) )
233232adantr 471 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( R  <  ( abs `  t )  <->  -.  ( abs `  t )  <_  R ) )
234 simpl1 1017 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  ->  R  e.  RR )
23525adantr 471 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( abs `  t
)  e.  RR )
236 simpr 467 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  ->  R  <_  ( abs `  t
) )
237234, 235, 236leltned 9814 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( R  <  ( abs `  t )  <->  ( abs `  t )  =/=  R
) )
238233, 237bitr3d 263 . . . . . . . . . . . . 13  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( -.  ( abs `  t )  <_  R  <->  ( abs `  t )  =/=  R ) )
239238, 111syl6bir 237 . . . . . . . . . . . 12  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( ( abs `  t
)  =/=  R  -> 
( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  =  0 ) )
240231, 239pm2.61dne 2722 . . . . . . . . . . 11  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  =  0 )
241189, 240eqtrd 2496 . . . . . . . . . 10  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( vol `  ( S " { t } ) )  =  0 )
242241ex 440 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R  <_  ( abs `  t
)  ->  ( vol `  ( S " {
t } ) )  =  0 ) )
243187, 242sylbid 223 . . . . . . . 8  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -.  t  e.  ( -u R (,) R )  ->  ( vol `  ( S " { t } ) )  =  0 ) )
2442433expia 1217 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  ->  ( -.  t  e.  ( -u R (,) R )  ->  ( vol `  ( S " { t } ) )  =  0 ) ) )
245244impd 437 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( ( t  e.  RR  /\  -.  t  e.  ( -u R (,) R ) )  -> 
( vol `  ( S " { t } ) )  =  0 ) )
246173, 245syl5bi 225 . . . . 5  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  ( RR  \  ( -u R (,) R ) )  ->  ( vol `  ( S " { t } ) )  =  0 ) )
247246imp 435 . . . 4  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  ( RR  \  ( -u R (,) R ) ) )  ->  ( vol `  ( S " { t } ) )  =  0 )
248172, 247itgss 22818 . . 3  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  S. ( -u R (,) R ) ( vol `  ( S " {
t } ) )  _d t  =  S. RR ( vol `  ( S " { t } ) )  _d t )
249 negeq 9893 . . . . . . . . . 10  |-  ( R  =  0  ->  -u R  =  -u 0 )
250249, 207syl6eq 2512 . . . . . . . . 9  |-  ( R  =  0  ->  -u R  =  0 )
251 id 22 . . . . . . . . 9  |-  ( R  =  0  ->  R  =  0 )
252250, 251oveq12d 6333 . . . . . . . 8  |-  ( R  =  0  ->  ( -u R (,) R )  =  ( 0 (,) 0 ) )
253 iooid 11693 . . . . . . . 8  |-  ( 0 (,) 0 )  =  (/)
254252, 253syl6eq 2512 . . . . . . 7  |-  ( R  =  0  ->  ( -u R (,) R )  =  (/) )
255254adantl 472 . . . . . 6  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  R  =  0
)  ->  ( -u R (,) R )  =  (/) )
256 itgeq1 22779 . . . . . 6  |-  ( (
-u R (,) R
)  =  (/)  ->  S. ( -u R (,) R
) ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  _d t  =  S. (/) ( vol `  if ( ( abs `  t )  <_  R ,  ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ,  (/) ) )  _d t )
257255, 256syl 17 . . . . 5  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  R  =  0
)  ->  S. ( -u R (,) R ) ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  _d t  =  S. (/) ( vol `  if ( ( abs `  t )  <_  R ,  ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ,  (/) ) )  _d t )
258 itg0 22786 . . . . . 6  |-  S. (/) ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  _d t  =  0
259 oveq1 6322 . . . . . . . . 9  |-  ( R  =  0  ->  ( R ^ 2 )  =  ( 0 ^ 2 ) )
260259oveq2d 6331 . . . . . . . 8  |-  ( R  =  0  ->  (
pi  x.  ( R ^ 2 ) )  =  ( pi  x.  ( 0 ^ 2 ) ) )
261 sq0 12398 . . . . . . . . . 10  |-  ( 0 ^ 2 )  =  0
262261oveq2i 6326 . . . . . . . . 9  |-  ( pi  x.  ( 0 ^ 2 ) )  =  ( pi  x.  0 )
263 picn 23463 . . . . . . . . . 10  |-  pi  e.  CC
264263mul01i 9849 . . . . . . . . 9  |-  ( pi  x.  0 )  =  0
265262, 264eqtr2i 2485 . . . . . . . 8  |-  0  =  ( pi  x.  ( 0 ^ 2 ) )
266260, 265syl6reqr 2515 . . . . . . 7  |-  ( R  =  0  ->  0  =  ( pi  x.  ( R ^ 2 ) ) )
267266adantl 472 . . . . . 6  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  R  =  0
)  ->  0  =  ( pi  x.  ( R ^ 2 ) ) )
268258, 267syl5eq 2508 . . . . 5  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  R  =  0
)  ->  S. (/) ( vol `  if ( ( abs `  t )  <_  R ,  ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ,  (/) ) )  _d t  =  ( pi  x.  ( R ^ 2 ) ) )
269257, 268eqtrd 2496 . . . 4  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  R  =  0
)  ->  S. ( -u R (,) R ) ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  _d t  =  ( pi  x.  ( R ^ 2 ) ) )
270 simp1 1014 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R  /\  R  =/=  0 )  ->  R  e.  RR )
271 0red 9670 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
0  e.  RR )
272 simpr 467 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
0  <_  R )
273271, 85, 272leltned 9814 . . . . . . . 8  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( 0  <  R  <->  R  =/=  0 ) )
274273biimp3ar 1380 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R  /\  R  =/=  0 )  ->  0  <  R )
275270, 274elrpd 11367 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R  /\  R  =/=  0 )  ->  R  e.  RR+ )
2762753expa 1215 . . . . 5  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  R  =/=  0
)  ->  R  e.  RR+ )
277166, 24syl 17 . . . . . . . . . . 11  |-  ( t  e.  ( -u R (,) R )  ->  ( abs `  t )  e.  RR )
278277adantl 472 . . . . . . . . . 10  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( abs `  t
)  e.  RR )
279 rpre 11337 . . . . . . . . . . 11  |-  ( R  e.  RR+  ->  R  e.  RR )
280279adantr 471 . . . . . . . . . 10  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  ->  R  e.  RR )
281279renegcld 10074 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  -u R  e.  RR )
282281rexrd 9716 . . . . . . . . . . . . 13  |-  ( R  e.  RR+  ->  -u R  e.  RR* )
283 rpxr 11338 . . . . . . . . . . . . 13  |-  ( R  e.  RR+  ->  R  e. 
RR* )
284282, 283, 176syl2anc 671 . . . . . . . . . . . 12  |-  ( R  e.  RR+  ->  ( t  e.  ( -u R (,) R )  <->  ( t  e.  RR  /\  -u R  <  t  /\  t  < 
R ) ) )
285 simpr 467 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  t  e.  RR )
286279adantr 471 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  R  e.  RR )
287285, 286absltd 13540 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( abs `  t
)  <  R  <->  ( -u R  <  t  /\  t  < 
R ) ) )
288287biimprd 231 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( -u R  <  t  /\  t  <  R )  ->  ( abs `  t
)  <  R )
)
289288exp4b 616 . . . . . . . . . . . . 13  |-  ( R  e.  RR+  ->  ( t  e.  RR  ->  ( -u R  <  t  -> 
( t  <  R  ->  ( abs `  t
)  <  R )
) ) )
2902893impd 1231 . . . . . . . . . . . 12  |-  ( R  e.  RR+  ->  ( ( t  e.  RR  /\  -u R  <  t  /\  t  <  R )  -> 
( abs `  t
)  <  R )
)
291284, 290sylbid 223 . . . . . . . . . . 11  |-  ( R  e.  RR+  ->  ( t  e.  ( -u R (,) R )  ->  ( abs `  t )  < 
R ) )
292291imp 435 . . . . . . . . . 10  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( abs `  t
)  <  R )
293278, 280, 292ltled 9809 . . . . . . . . 9  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( abs `  t
)  <_  R )
294293, 121syl 17 . . . . . . . 8  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  =  ( vol `  ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) [,] ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ) )
295279resqcld 12474 . . . . . . . . . . . . . . 15  |-  ( R  e.  RR+  ->  ( R ^ 2 )  e.  RR )
296295recnd 9695 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  ( R ^ 2 )  e.  CC )
297296adantr 471 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  ( R ^ 2 )  e.  CC )
298201adantl 472 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
t ^ 2 )  e.  CC )
299297, 298subcld 10012 . . . . . . . . . . . 12  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  e.  CC )
300299sqrtcld 13548 . . . . . . . . . . 11  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  CC )
301300, 300subnegd 10019 . . . . . . . . . 10  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )  =  ( ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) )  +  ( sqr `  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) ) )
302166, 301sylan2 481 . . . . . . . . 9  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )  =  ( ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) )  +  ( sqr `  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) ) )
303295adantr 471 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  ( R ^ 2 )  e.  RR )
30416adantl 472 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
t ^ 2 )  e.  RR )
305303, 304resubcld 10075 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  e.  RR )
306166, 305sylan2 481 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( ( R ^
2 )  -  (
t ^ 2 ) )  e.  RR )
307 0red 9670 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  e.  RR )
30824adantl 472 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  ( abs `  t )  e.  RR )
30927adantl 472 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  0  <_  ( abs `  t
) )
310 rpge0 11343 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( R  e.  RR+  ->  0  <_  R )
311310adantr 471 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  0  <_  R )
312308, 286, 309, 311lt2sqd 12482 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( abs `  t
)  <  R  <->  ( ( abs `  t ) ^
2 )  <  ( R ^ 2 ) ) )
31320adantl 472 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( abs `  t
) ^ 2 )  =  ( t ^
2 ) )
314313breq1d 4426 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( ( abs `  t
) ^ 2 )  <  ( R ^
2 )  <->  ( t ^ 2 )  < 
( R ^ 2 ) ) )
315312, 287, 3143bitr3rd 292 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( t ^ 2 )  <  ( R ^ 2 )  <->  ( -u R  <  t  /\  t  < 
R ) ) )
316304, 303posdifd 10228 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( t ^ 2 )  <  ( R ^ 2 )  <->  0  <  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )
317315, 316bitr3d 263 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( -u R  <  t  /\  t  <  R )  <->  0  <  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) )
318317biimpd 212 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( -u R  <  t  /\  t  <  R )  ->  0  <  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) )
319318exp4b 616 . . . . . . . . . . . . . . . . . 18  |-  ( R  e.  RR+  ->  ( t  e.  RR  ->  ( -u R  <  t  -> 
( t  <  R  ->  0  <  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) ) ) )
3203193impd 1231 . . . . . . . . . . . . . . . . 17  |-  ( R  e.  RR+  ->  ( ( t  e.  RR  /\  -u R  <  t  /\  t  <  R )  -> 
0  <  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )
321284, 320sylbid 223 . . . . . . . . . . . . . . . 16  |-  ( R  e.  RR+  ->  ( t  e.  ( -u R (,) R )  ->  0  <  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
322321imp 435 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  <  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )
323307, 306, 322ltled 9809 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )
324306, 323resqrtcld 13528 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
325324renegcld 10074 . . . . . . . . . . . 12  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  ->  -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
326325, 324, 36syl2anc 671 . . . . . . . . . . 11  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )  e. 
dom  vol )
327326, 38syl 17 . . . . . . . . . 10  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( vol `  ( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )  =  ( vol* `  ( -u ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ) )
328306, 323sqrtge0d 13531 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
329324, 324, 328, 328addge0d 10217 . . . . . . . . . . . 12  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  <_  ( ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  +  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
330302breq2d 4428 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( 0  <_  (
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )  <->  0  <_  ( ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  +  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ) )
331324, 325subge0d 10231 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( 0  <_  (
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )  <->  -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )
332330, 331bitr3d 263 . . . . . . . . . . . 12  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( 0  <_  (
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  +  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )  <->  -u ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) )  <_  ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
333329, 332mpbid 215 . . . . . . . . . . 11  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  ->  -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
334325, 324, 333, 55syl3anc 1276 . . . . . . . . . 10  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( vol* `  ( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )  =  ( ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
335327, 334eqtrd 2496 . . . . . . . . 9  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( vol `  ( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )  =  ( ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
336 ax-resscn 9622 . . . . . . . . . . . . . . 15  |-  RR  C_  CC
337336a1i 11 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  RR  C_  CC )
338281, 279, 86syl2anc 671 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  ( -u R [,] R )  C_  RR )
339 rpcn 11339 . . . . . . . . . . . . . . . . 17  |-  ( R  e.  RR+  ->  R  e.  CC )
340339sqcld 12446 . . . . . . . . . . . . . . . 16  |-  ( R  e.  RR+  ->  ( R ^ 2 )  e.  CC )
341340adantr 471 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( R ^ 2 )  e.  CC )
342338sselda 3444 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  ->  u  e.  RR )
343342recnd 9695 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  ->  u  e.  CC )
344339adantr 471 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  ->  R  e.  CC )
345 rpne0 11346 . . . . . . . . . . . . . . . . . . 19  |-  ( R  e.  RR+  ->  R  =/=  0 )
346345adantr 471 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  ->  R  =/=  0 )
347343, 344, 346divcld 10411 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( u  /  R
)  e.  CC )
348 asincl 23848 . . . . . . . . . . . . . . . . 17  |-  ( ( u  /  R )  e.  CC  ->  (arcsin `  ( u  /  R
) )  e.  CC )
349347, 348syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
(arcsin `  ( u  /  R ) )  e.  CC )
350 1cnd 9685 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
1  e.  CC )
351347sqcld 12446 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( ( u  /  R ) ^ 2 )  e.  CC )
352350, 351subcld 10012 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( 1  -  (
( u  /  R
) ^ 2 ) )  e.  CC )
353352sqrtcld 13548 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( sqr `  (
1  -  ( ( u  /  R ) ^ 2 ) ) )  e.  CC )
354347, 353mulcld 9689 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( ( u  /  R )  x.  ( sqr `  ( 1  -  ( ( u  /  R ) ^ 2 ) ) ) )  e.  CC )
355349, 354addcld 9688 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( (arcsin `  (
u  /  R ) )  +  ( ( u  /  R )  x.  ( sqr `  (
1  -  ( ( u  /  R ) ^ 2 ) ) ) ) )  e.  CC )
356341, 355mulcld 9689 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( ( R ^
2 )  x.  (
(arcsin `  ( u  /  R ) )  +  ( ( u  /  R )  x.  ( sqr `  ( 1  -  ( ( u  /  R ) ^ 2 ) ) ) ) ) )  e.  CC )
357 eqid 2462 . . . . . . . . . . . . . . 15  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
358357tgioo2 21870 . . . . . . . . . . . . . 14  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
359 iccntr 21888 . . . . . . . . . . . . . . 15  |-  ( (
-u R  e.  RR  /\  R  e.  RR )  ->  ( ( int `  ( topGen `  ran  (,) )
) `  ( -u R [,] R ) )  =  ( -u R (,) R ) )
360281, 279, 359syl2anc 671 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( -u R [,] R
) )  =  (
-u R (,) R
) )
361337, 338, 356, 358, 357, 360dvmptntr 22974 . . . . . . . . . . . . 13  |-  ( R  e.  RR+  ->  ( RR 
_D  ( u  e.  ( -u R [,] R )  |->  ( ( R ^ 2 )  x.  ( (arcsin `  ( u  /  R
) )  +  ( ( u  /  R
)  x.  ( sqr `  ( 1  -  (
( u  /  R
) ^ 2 ) ) ) ) ) ) ) )  =  ( RR  _D  (
u  e.  ( -u R (,) R )  |->  ( ( R ^ 2 )  x.  ( (arcsin `  ( u  /  R
) )  +  ( ( u  /  R
)  x.  ( sqr `  ( 1  -  (
( u  /  R
) ^ 2 ) ) ) ) ) ) ) ) )
362 areacirclem1 32077 . . . . . . . . . . . . 13  |-  ( R  e.  RR+  ->  ( RR 
_D  ( u  e.  ( -u R (,) R )  |->  ( ( R ^ 2 )  x.  ( (arcsin `  ( u  /  R
) )  +  ( ( u  /  R
)  x.  ( sqr `  ( 1  -  (
( u  /  R
) ^ 2 ) ) ) ) ) ) ) )  =  ( u  e.  (
-u R (,) R
)  |->  ( 2  x.  ( sqr `  (
( R ^ 2 )  -  ( u ^ 2 ) ) ) ) ) )
363361, 362eqtrd 2496 . . . . . . . . . . . 12  |-  ( R  e.  RR+  ->  ( RR 
_D  ( u  e.  ( -u R [,] R )  |->  ( ( R ^ 2 )  x.  ( (arcsin `  ( u  /  R
) )  +  ( ( u  /  R
)  x.  ( sqr `  ( 1  -  (
( u  /  R
) ^ 2 ) ) ) ) ) ) ) )  =  ( u  e.  (
-u R (,) R
)  |->  ( 2  x.  ( sqr `  (
( R ^ 2 )  -  ( u ^ 2 ) ) ) ) ) )
364363adantr 471 . . . . . . . . . . 11  |-  ( ( R  e.  RR+