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

Theorem areacirc 24931
Description: The area of a circle of radius  R is  pi  x.  R ^ 2. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 22-Sep-2017.)
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 4078 . . . . . . 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 2303 . . . . . 6  |-  S  =  { u  |  E. x E. y ( u  =  <. x ,  y
>.  /\  ( ( x  e.  RR  /\  y  e.  RR )  /\  (
( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^
2 ) ) ) }
4 simpl 443 . . . . . . . . 9  |-  ( ( u  =  <. x ,  y >.  /\  (
( x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) ) )  ->  u  =  <. x ,  y >.
)
5 opelxpi 4721 . . . . . . . . . . 11  |-  ( ( x  e.  RR  /\  y  e.  RR )  -> 
<. x ,  y >.  e.  ( RR  X.  RR ) )
65adantr 451 . . . . . . . . . 10  |-  ( ( ( x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) )  ->  <. x ,  y
>.  e.  ( RR  X.  RR ) )
76adantl 452 . . . . . . . . 9  |-  ( ( u  =  <. x ,  y >.  /\  (
( x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) ) )  ->  <. x ,  y >.  e.  ( RR  X.  RR ) )
84, 7eqeltrd 2357 . . . . . . . 8  |-  ( ( u  =  <. x ,  y >.  /\  (
( x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) ) )  ->  u  e.  ( RR  X.  RR ) )
98exlimivv 1667 . . . . . . 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 3248 . . . . . 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 3208 . . . . 5  |-  S  C_  ( RR  X.  RR )
1211a1i 10 . . . 4  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  S  C_  ( RR  X.  RR ) )
131areacirclem6 24930 . . . . . . 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 11171 . . . . . . . . . . . . . . 15  |-  ( R  e.  RR  ->  ( R ^ 2 )  e.  RR )
15143ad2ant1 976 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R ^ 2 )  e.  RR )
16 resqcl 11171 . . . . . . . . . . . . . . 15  |-  ( t  e.  RR  ->  (
t ^ 2 )  e.  RR )
17163ad2ant3 978 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t ^ 2 )  e.  RR )
1815, 17resubcld 9211 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  e.  RR )
1918adantr 451 . . . . . . . . . . . 12  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( ( R ^
2 )  -  (
t ^ 2 ) )  e.  RR )
20 absresq 11787 . . . . . . . . . . . . . . . 16  |-  ( t  e.  RR  ->  (
( abs `  t
) ^ 2 )  =  ( t ^
2 ) )
21203ad2ant3 978 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
) ^ 2 )  =  ( t ^
2 ) )
2221breq1d 4033 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( ( abs `  t
) ^ 2 )  <_  ( R ^
2 )  <->  ( t ^ 2 )  <_ 
( R ^ 2 ) ) )
23 recn 8827 . . . . . . . . . . . . . . . . 17  |-  ( t  e.  RR  ->  t  e.  CC )
2423abscld 11918 . . . . . . . . . . . . . . . 16  |-  ( t  e.  RR  ->  ( abs `  t )  e.  RR )
25243ad2ant3 978 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( abs `  t )  e.  RR )
26 simp1 955 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  R  e.  RR )
2723absge0d 11926 . . . . . . . . . . . . . . . 16  |-  ( t  e.  RR  ->  0  <_  ( abs `  t
) )
28273ad2ant3 978 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  0  <_  ( abs `  t
) )
29 simp2 956 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  0  <_  R )
3025, 26, 28, 29le2sqd 11280 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  ( ( abs `  t ) ^
2 )  <_  ( R ^ 2 ) ) )
3115, 17subge0d 9362 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) )  <->  ( t ^ 2 )  <_ 
( R ^ 2 ) ) )
3222, 30, 313bitr4d 276 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )
3332biimpa 470 . . . . . . . . . . . 12  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )
3419, 33resqrcld 11900 . . . . . . . . . . 11  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
3534renegcld 9210 . . . . . . . . . 10  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  -> 
-u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
36 iccmbl 18923 . . . . . . . . . 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 642 . . . . . . . . 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 18889 . . . . . . . . . . . 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 15 . . . . . . . . . . 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, 33sqrge0d 11903 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  0  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
4134, 34, 40, 40addge0d 9348 . . . . . . . . . . . . 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 8827 . . . . . . . . . . . . . . . . . . . . 21  |-  ( R  e.  RR  ->  R  e.  CC )
4342sqcld 11243 . . . . . . . . . . . . . . . . . . . 20  |-  ( R  e.  RR  ->  ( R ^ 2 )  e.  CC )
44433ad2ant1 976 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R ^ 2 )  e.  CC )
4523sqcld 11243 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  e.  RR  ->  (
t ^ 2 )  e.  CC )
46453ad2ant3 978 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t ^ 2 )  e.  CC )
4744, 46subcld 9157 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  e.  CC )
4847sqrcld 11919 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  CC )
4948adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  CC )
5049, 49subnegd 9164 . . . . . . . . . . . . . . 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 4035 . . . . . . . . . . . . . 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 9362 . . . . . . . . . . . . . 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 246 . . . . . . . . . . . . 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 201 . . . . . . . . . . . 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 18882 . . . . . . . . . . . 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 1182 . . . . . . . . . . 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 2315 . . . . . . . . . 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 9211 . . . . . . . . . 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 2357 . . . . . . . . 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 18888 . . . . . . . . . 10  |-  vol : dom  vol --> ( 0 [,] 
+oo )
61 ffn 5389 . . . . . . . . . 10  |-  ( vol
: dom  vol --> ( 0 [,]  +oo )  ->  vol  Fn 
dom  vol )
62 elpreima 5645 . . . . . . . . . 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 9 . . . . . . . . 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 645 . . . . . . . 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 18897 . . . . . . . . . 10  |-  (/)  e.  dom  vol
66 mblvol 18889 . . . . . . . . . . . . 13  |-  ( (/)  e.  dom  vol  ->  ( vol `  (/) )  =  ( vol * `  (/) ) )
6765, 66ax-mp 8 . . . . . . . . . . . 12  |-  ( vol `  (/) )  =  ( vol * `  (/) )
68 ovol0 18852 . . . . . . . . . . . 12  |-  ( vol
* `  (/) )  =  0
6967, 68eqtri 2303 . . . . . . . . . . 11  |-  ( vol `  (/) )  =  0
70 0re 8838 . . . . . . . . . . 11  |-  0  e.  RR
7169, 70eqeltri 2353 . . . . . . . . . 10  |-  ( vol `  (/) )  e.  RR
72 elpreima 5645 . . . . . . . . . . 11  |-  ( vol 
Fn  dom  vol  ->  ( (/) 
e.  ( `' vol " RR )  <->  ( (/)  e.  dom  vol 
/\  ( vol `  (/) )  e.  RR ) ) )
7360, 61, 72mp2b 9 . . . . . . . . . 10  |-  ( (/)  e.  ( `' vol " RR ) 
<->  ( (/)  e.  dom  vol 
/\  ( vol `  (/) )  e.  RR ) )
7465, 71, 73mpbir2an 886 . . . . . . . . 9  |-  (/)  e.  ( `' vol " RR )
7574a1i 10 . . . . . . . 8  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  -.  ( abs `  t
)  <_  R )  -> 
(/)  e.  ( `' vol " RR ) )
7664, 75ifclda 3592 . . . . . . 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 2357 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( S " { t } )  e.  ( `' vol " RR ) )
78773expa 1151 . . . . 5  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  RR )  ->  ( S " { t } )  e.  ( `' vol " RR ) )
7978ralrimiva 2626 . . . 4  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  A. t  e.  RR  ( S " { t } )  e.  ( `' vol " RR ) )
8013fveq2d 5529 . . . . . . 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 1151 . . . . . 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 4106 . . . . 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 9110 . . . . . . . 8  |-  ( R  e.  RR  ->  -u R  e.  RR )
8483adantr 451 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  -u R  e.  RR )
85 simpl 443 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  R  e.  RR )
86 iccssre 10731 . . . . . . 7  |-  ( (
-u R  e.  RR  /\  R  e.  RR )  ->  ( -u R [,] R )  C_  RR )
8784, 85, 86syl2anc 642 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( -u R [,] R
)  C_  RR )
88 rembl 18898 . . . . . . 7  |-  RR  e.  dom  vol
8988a1i 10 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  RR  e.  dom  vol )
90 fvex 5539 . . . . . . 7  |-  ( vol `  if ( ( abs `  t )  <_  R ,  ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ,  (/) ) )  e.  _V
9190a1i 10 . . . . . 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 3162 . . . . . . . . 9  |-  ( t  e.  ( RR  \ 
( -u R [,] R
) )  <->  ( t  e.  RR  /\  -.  t  e.  ( -u R [,] R ) ) )
93 3anass 938 . . . . . . . . . . . . . . 15  |-  ( ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R )  <->  ( t  e.  RR  /\  ( -u R  <_  t  /\  t  <_  R ) ) )
9493a1i 10 . . . . . . . . . . . . . 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 976 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  -u R  e.  RR )
96 elicc2 10715 . . . . . . . . . . . . . . 15  |-  ( (
-u R  e.  RR  /\  R  e.  RR )  ->  ( t  e.  ( -u R [,] R )  <->  ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R ) ) )
9795, 26, 96syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t  e.  ( -u R [,] R )  <->  ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R ) ) )
98 simp3 957 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  t  e.  RR )
9998, 26absled 11913 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  ( -u R  <_  t  /\  t  <_  R ) ) )
10098biantrurd 494 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( -u R  <_  t  /\  t  <_  R )  <-> 
( t  e.  RR  /\  ( -u R  <_ 
t  /\  t  <_  R ) ) ) )
10199, 100bitrd 244 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  ( t  e.  RR  /\  ( -u R  <_  t  /\  t  <_  R ) ) ) )
10294, 97, 1013bitr4rd 277 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  t  e.  ( -u R [,] R
) ) )
103102biimpd 198 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  ->  t  e.  ( -u R [,] R ) ) )
104103con3d 125 . . . . . . . . . . 11  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -.  t  e.  ( -u R [,] R )  ->  -.  ( abs `  t )  <_  R
) )
1051043expia 1153 . . . . . . . . . 10  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  ->  ( -.  t  e.  ( -u R [,] R )  ->  -.  ( abs `  t )  <_  R ) ) )
106105imp3a 420 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( ( t  e.  RR  /\  -.  t  e.  ( -u R [,] R ) )  ->  -.  ( abs `  t
)  <_  R )
)
10792, 106syl5bi 208 . . . . . . . 8  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  ( RR  \  ( -u R [,] R ) )  ->  -.  ( abs `  t )  <_  R
) )
108107imp 418 . . . . . . 7  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  ( RR  \  ( -u R [,] R ) ) )  ->  -.  ( abs `  t )  <_  R
)
109 iffalse 3572 . . . . . . . . 9  |-  ( -.  ( abs `  t
)  <_  R  ->  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) )  =  (/) )
110109fveq2d 5529 . . . . . . . 8  |-  ( -.  ( abs `  t
)  <_  R  ->  ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  =  ( vol `  (/) ) )
111110, 69syl6eq 2331 . . . . . . 7  |-  ( -.  ( abs `  t
)  <_  R  ->  ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  =  0 )
112108, 111syl 15 . . . . . 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 642 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  <->  ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R ) ) )
11499biimprd 214 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( -u R  <_  t  /\  t  <_  R )  ->  ( abs `  t
)  <_  R )
)
115114exp3a 425 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -u R  <_  t  ->  ( t  <_  R  ->  ( abs `  t )  <_  R ) ) )
1161153expia 1153 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  ->  ( -u R  <_ 
t  ->  ( t  <_  R  ->  ( abs `  t )  <_  R
) ) ) )
1171163impd 1165 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R )  ->  ( abs `  t )  <_  R ) )
118113, 117sylbid 206 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  ->  ( abs `  t )  <_  R
) )
1191183impia 1148 . . . . . . . . . . 11  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( abs `  t
)  <_  R )
120 iftrue 3571 . . . . . . . . . . . 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 5529 . . . . . . . . . . 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 15 . . . . . . . . . 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 976 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( R ^ 2 )  e.  RR )
12483, 86mpancom 650 . . . . . . . . . . . . . . . . . 18  |-  ( R  e.  RR  ->  ( -u R [,] R ) 
C_  RR )
125124sselda 3180 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR  /\  t  e.  ( -u R [,] R ) )  -> 
t  e.  RR )
1261253adant2 974 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
t  e.  RR )
127126resqcld 11271 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( t ^ 2 )  e.  RR )
128123, 127resubcld 9211 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( ( R ^
2 )  -  (
t ^ 2 ) )  e.  RR )
12983, 96mpancom 650 . . . . . . . . . . . . . . . . 17  |-  ( R  e.  RR  ->  (
t  e.  ( -u R [,] R )  <->  ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R ) ) )
130129adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  <->  ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R ) ) )
13130, 99, 223bitr3rd 275 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( t ^ 2 )  <_  ( R ^ 2 )  <->  ( -u R  <_  t  /\  t  <_  R ) ) )
13231, 131bitrd 244 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) )  <->  ( -u R  <_  t  /\  t  <_  R ) ) )
133132biimprd 214 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( -u R  <_  t  /\  t  <_  R )  ->  0  <_  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) )
134133exp3a 425 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -u R  <_  t  ->  ( t  <_  R  ->  0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
1351343expia 1153 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  ->  ( -u R  <_ 
t  ->  ( t  <_  R  ->  0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ) )
1361353impd 1165 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R )  ->  0  <_  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
137130, 136sylbid 206 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  ->  0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )
1381373impia 1148 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )
139128, 138resqrcld 11900 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
140139renegcld 9210 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  ->  -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
141140, 139, 36syl2anc 642 . . . . . . . . . . 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 15 . . . . . . . . . 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 8861 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( ( R ^
2 )  -  (
t ^ 2 ) )  e.  CC )
144143sqrcld 11919 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  CC )
145144, 144subnegd 9164 . . . . . . . . . . 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, 138sqrge0d 11903 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
0  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
147139, 139, 146, 146addge0d 9348 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
0  <_  ( ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  +  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
148145breq2d 4035 . . . . . . . . . . . . . 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 9362 . . . . . . . . . . . . . 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 246 . . . . . . . . . . . . 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 201 . . . . . . . . . . . 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 1182 . . . . . . . . . . 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 9954 . . . . . . . . . . 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 2325 . . . . . . . . . 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 2319 . . . . . . . . 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 1151 . . . . . . . 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 4106 . . . . . . 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 areacirclem1 24928 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  |->  ( 2  x.  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )  e.  L ^1 )
159157, 158eqeltrd 2357 . . . . . 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 19160 . . . . 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 2357 . . . 4  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  |->  ( vol `  ( S
" { t } ) ) )  e.  L ^1 )
162 dmarea 20252 . . . 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 1136 . . 3  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  S  e.  dom area )
164 areaval 20259 . . 3  |-  ( S  e.  dom area  ->  (area `  S )  =  S. RR ( vol `  ( S " { t } ) )  _d t )
165163, 164syl 15 . 2  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
(area `  S )  =  S. RR ( vol `  ( S " {
t } ) )  _d t )
166 elioore 10686 . . . . . 6  |-  ( t  e.  ( -u R (,) R )  ->  t  e.  RR )
167133expa 1151 . . . . . 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 460 . . . . 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 5529 . . . 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 19136 . . 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 10712 . . . . 5  |-  ( -u R (,) R )  C_  RR
172171a1i 10 . . . 4  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( -u R (,) R
)  C_  RR )
173 eldif 3162 . . . . . 6  |-  ( t  e.  ( RR  \ 
( -u R (,) R
) )  <->  ( t  e.  RR  /\  -.  t  e.  ( -u R (,) R ) ) )
17483rexrd 8881 . . . . . . . . . . . . . 14  |-  ( R  e.  RR  ->  -u R  e.  RR* )
175 rexr 8877 . . . . . . . . . . . . . 14  |-  ( R  e.  RR  ->  R  e.  RR* )
176 elioo2 10697 . . . . . . . . . . . . . 14  |-  ( (
-u R  e.  RR*  /\  R  e.  RR* )  ->  ( t  e.  (
-u R (,) R
)  <->  ( t  e.  RR  /\  -u R  <  t  /\  t  < 
R ) ) )
177174, 175, 176syl2anc 642 . . . . . . . . . . . . 13  |-  ( R  e.  RR  ->  (
t  e.  ( -u R (,) R )  <->  ( t  e.  RR  /\  -u R  <  t  /\  t  < 
R ) ) )
1781773ad2ant1 976 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t  e.  ( -u R (,) R )  <->  ( t  e.  RR  /\  -u R  <  t  /\  t  < 
R ) ) )
17998biantrurd 494 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( -u R  <  t  /\  t  <  R )  <-> 
( t  e.  RR  /\  ( -u R  < 
t  /\  t  <  R ) ) ) )
18098, 26absltd 11912 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <  R  <->  ( -u R  <  t  /\  t  < 
R ) ) )
181 3anass 938 . . . . . . . . . . . . . 14  |-  ( ( t  e.  RR  /\  -u R  <  t  /\  t  <  R )  <->  ( t  e.  RR  /\  ( -u R  <  t  /\  t  <  R ) ) )
182181a1i 10 . . . . . . . . . . . . 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 277 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( t  e.  RR  /\  -u R  <  t  /\  t  <  R )  <->  ( abs `  t )  <  R
) )
184178, 183bitrd 244 . . . . . . . . . . 11  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t  e.  ( -u R (,) R )  <->  ( abs `  t )  <  R
) )
185184notbid 285 . . . . . . . . . 10  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -.  t  e.  ( -u R (,) R )  <->  -.  ( abs `  t
)  <  R )
)
18626, 25lenltd 8965 . . . . . . . . . 10  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R  <_  ( abs `  t
)  <->  -.  ( abs `  t )  <  R
) )
187185, 186bitr4d 247 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -.  t  e.  ( -u R (,) R )  <-> 
R  <_  ( abs `  t ) ) )
18813adantr 451 . . . . . . . . . . . 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 5529 . . . . . . . . . . 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 551 . . . . . . . . . . . . . . . 16  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( ( abs `  t )  e.  RR  /\  ( abs `  t
)  =  R ) )
191 eqle 8923 . . . . . . . . . . . . . . . 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 5865 . . . . . . . . . . . . . . . . . 18  |-  ( ( abs `  t )  =  R  ->  (
( abs `  t
) ^ 2 )  =  ( R ^
2 ) )
194193adantl 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( ( abs `  t ) ^ 2 )  =  ( R ^ 2 ) )
19521adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( ( abs `  t ) ^ 2 )  =  ( t ^ 2 ) )
196194, 195eqtr3d 2317 . . . . . . . . . . . . . . . 16  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( R ^
2 )  =  ( t ^ 2 ) )
197 oveq1 5865 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R ^ 2 )  =  ( t ^
2 )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  =  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )
198197fveq2d 5529 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R ^ 2 )  =  ( t ^
2 )  ->  ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  =  ( sqr `  (
( t ^ 2 )  -  ( t ^ 2 ) ) ) )
199198negeqd 9046 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R ^ 2 )  =  ( t ^
2 )  ->  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  = 
-u ( sqr `  (
( t ^ 2 )  -  ( t ^ 2 ) ) ) )
200199, 198oveq12d 5876 . . . . . . . . . . . . . . . . . . 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 8861 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  e.  RR  ->  (
t ^ 2 )  e.  CC )
202201subidd 9145 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  e.  RR  ->  (
( t ^ 2 )  -  ( t ^ 2 ) )  =  0 )
203202fveq2d 5529 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  e.  RR  ->  ( sqr `  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )  =  ( sqr `  0
) )
204203negeqd 9046 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  e.  RR  ->  -u ( sqr `  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )  = 
-u ( sqr `  0
) )
205 sqr0 11727 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( sqr `  0 )  =  0
206205negeqi 9045 . . . . . . . . . . . . . . . . . . . . . . 23  |-  -u ( sqr `  0 )  = 
-u 0
207 neg0 9093 . . . . . . . . . . . . . . . . . . . . . . 23  |-  -u 0  =  0
208206, 207eqtri 2303 . . . . . . . . . . . . . . . . . . . . . 22  |-  -u ( sqr `  0 )  =  0
209204, 208syl6eq 2331 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  e.  RR  ->  -u ( sqr `  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )  =  0 )
210203, 205syl6eq 2331 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  e.  RR  ->  ( sqr `  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )  =  0 )
211209, 210oveq12d 5876 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  e.  RR  ->  ( -u ( sqr `  (
( t ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( t ^
2 )  -  (
t ^ 2 ) ) ) )  =  ( 0 [,] 0
) )
2122113ad2ant3 978 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -u ( sqr `  (
( t ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( t ^
2 )  -  (
t ^ 2 ) ) ) )  =  ( 0 [,] 0
) )
213200, 212sylan9eqr 2337 . . . . . . . . . . . . . . . . . 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 5529 . . . . . . . . . . . . . . . . 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 18923 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 0  e.  RR  /\  0  e.  RR )  ->  ( 0 [,] 0
)  e.  dom  vol )
21670, 70, 215mp2an 653 . . . . . . . . . . . . . . . . . . 19  |-  ( 0 [,] 0 )  e. 
dom  vol
217 mblvol 18889 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 0 [,] 0 )  e.  dom  vol  ->  ( vol `  ( 0 [,] 0 ) )  =  ( vol * `  ( 0 [,] 0
) ) )
218216, 217ax-mp 8 . . . . . . . . . . . . . . . . . 18  |-  ( vol `  ( 0 [,] 0
) )  =  ( vol * `  (
0 [,] 0 ) )
219 0xr 8878 . . . . . . . . . . . . . . . . . . . 20  |-  0  e.  RR*
220 iccid 10701 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 0  e.  RR*  ->  ( 0 [,] 0 )  =  { 0 } )
221220fveq2d 5529 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  e.  RR*  ->  ( vol
* `  ( 0 [,] 0 ) )  =  ( vol * `  { 0 } ) )
222219, 221ax-mp 8 . . . . . . . . . . . . . . . . . . 19  |-  ( vol
* `  ( 0 [,] 0 ) )  =  ( vol * `  { 0 } )
223 ovolsn 18854 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  e.  RR  ->  ( vol * `  { 0 } )  =  0 )
22470, 223ax-mp 8 . . . . . . . . . . . . . . . . . . 19  |-  ( vol
* `  { 0 } )  =  0
225222, 224eqtri 2303 . . . . . . . . . . . . . . . . . 18  |-  ( vol
* `  ( 0 [,] 0 ) )  =  0
226218, 225eqtri 2303 . . . . . . . . . . . . . . . . 17  |-  ( vol `  ( 0 [,] 0
) )  =  0
227214, 226syl6eq 2331 . . . . . . . . . . . . . . . 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 456 . . . . . . . . . . . . . . 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 2315 . . . . . . . . . . . . . 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 423 . . . . . . . . . . . . 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 451 . . . . . . . . . . . 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 8966 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R  <  ( abs `  t
)  <->  -.  ( abs `  t )  <_  R
) )
233232adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( R  <  ( abs `  t )  <->  -.  ( abs `  t )  <_  R ) )
234 simpl1 958 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  ->  R  e.  RR )
23525adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( abs `  t
)  e.  RR )
236 simpr 447 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  ->  R  <_  ( abs `  t
) )
237234, 235, 236leltned 8970 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( R  <  ( abs `  t )  <->  ( abs `  t )  =/=  R
) )
238233, 237bitr3d 246 . . . . . . . . . . . . 13  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( -.  ( abs `  t )  <_  R  <->  ( abs `  t )  =/=  R ) )
239238, 111syl6bir 220 . . . . . . . . . . . 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 2523 . . . . . . . . . . 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 2315 . . . . . . . . . 10  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( vol `  ( S " { t } ) )  =  0 )
242241ex 423 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R  <_  ( abs `  t
)  ->  ( vol `  ( S " {
t } ) )  =  0 ) )
243187, 242sylbid 206 . . . . . . . 8  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -.  t  e.  ( -u R (,) R )  ->  ( vol `  ( S " { t } ) )  =  0 ) )
2442433expia 1153 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  ->  ( -.  t  e.  ( -u R (,) R )  ->  ( vol `  ( S " { t } ) )  =  0 ) ) )
245244imp3a 420 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( ( t  e.  RR  /\  -.  t  e.  ( -u R (,) R ) )  -> 
( vol `  ( S " { t } ) )  =  0 ) )
246173, 245syl5bi 208 . . . . 5  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  ( RR  \  ( -u R (,) R ) )  ->  ( vol `  ( S " { t } ) )  =  0 ) )
247246imp 418 . . . 4  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  ( RR  \  ( -u R (,) R ) ) )  ->  ( vol `  ( S " { t } ) )  =  0 )
248172, 247itgss 19166 . . 3  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  S. ( -u R (,) R ) ( vol `  ( S " {
t } ) )  _d t  =  S. RR ( vol `  ( S " { t } ) )  _d t )
249 negeq 9044 . . . . . . . . . 10  |-  ( R  =  0  ->  -u R  =  -u 0 )
250249, 207syl6eq 2331 . . . . . . . . 9  |-  ( R  =  0  ->  -u R  =  0 )
251 id 19 . . . . . . . . 9  |-  ( R  =  0  ->  R  =  0 )
252250, 251oveq12d 5876 . . . . . . . 8  |-  ( R  =  0  ->  ( -u R (,) R )  =  ( 0 (,) 0 ) )
253 iooid 10684 . . . . . . . 8  |-  ( 0 (,) 0 )  =  (/)
254252, 253syl6eq 2331 . . . . . . 7  |-  ( R  =  0  ->  ( -u R (,) R )  =  (/) )
255254adantl 452 . . . . . 6  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  R  =  0
)  ->  ( -u R (,) R )  =  (/) )
256 itgeq1 19127 . . . . . 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 15 . . . . 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 19134 . . . . . 6  |-  S. (/) ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  _d t  =  0
259 oveq1 5865 . . . . . . . . 9  |-  ( R  =  0  ->  ( R ^ 2 )  =  ( 0 ^ 2 ) )
260259oveq2d 5874 . . . . . . . 8  |-  ( R  =  0  ->  (
pi  x.  ( R ^ 2 ) )  =  ( pi  x.  ( 0 ^ 2 ) ) )
261 sq0 11195 . . . . . . . . . 10  |-  ( 0 ^ 2 )  =  0
262261oveq2i 5869 . . . . . . . . 9  |-  ( pi  x.  ( 0 ^ 2 ) )  =  ( pi  x.  0 )
263 pire 19832 . . . . . . . . . . 11  |-  pi  e.  RR
264263recni 8849 . . . . . . . . . 10  |-  pi  e.  CC
265264mul01i 9002 . . . . . . . . 9  |-  ( pi  x.  0 )  =  0
266262, 265eqtr2i 2304 . . . . . . . 8  |-  0  =  ( pi  x.  ( 0 ^ 2 ) )
267260, 266syl6reqr 2334 . . . . . . 7  |-  ( R  =  0  ->  0  =  ( pi  x.  ( R ^ 2 ) ) )
268267adantl 452 . . . . . 6  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  R  =  0
)  ->  0  =  ( pi  x.  ( R ^ 2 ) ) )
269258, 268syl5eq 2327 . . . . 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 ) ) )
270257, 269eqtrd 2315 . . . 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 ) ) )
271 simp1 955 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R  /\  R  =/=  0 )  ->  R  e.  RR )
27270a1i 10 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
0  e.  RR )
273 simpr 447 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
0  <_  R )
274272, 85, 273leltned 8970 . . . . . . . 8  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( 0  <  R  <->  R  =/=  0 ) )
275274biimp3ar 1282 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R  /\  R  =/=  0 )  ->  0  <  R )
276271, 275elrpd 10388 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R  /\  R  =/=  0 )  ->  R  e.  RR+ )
2772763expa 1151 . . . . 5  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  R  =/=  0
)  ->  R  e.  RR+ )
278166, 24syl 15 . . . . . . . . . . 11  |-  ( t  e.  ( -u R (,) R )  ->  ( abs `  t )  e.  RR )
279278adantl 452 . . . . . . . . . 10  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( abs `  t
)  e.  RR )
280 rpre 10360 . . . . . . . . . . 11  |-  ( R  e.  RR+  ->  R  e.  RR )
281280adantr 451 . . . . . . . . . 10  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  ->  R  e.  RR )
282280renegcld 9210 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  -u R  e.  RR )
283282rexrd 8881 . . . . . . . . . . . . 13  |-  ( R  e.  RR+  ->  -u R  e.  RR* )
284 rpxr 10361 . . . . . . . . . . . . 13  |-  ( R  e.  RR+  ->  R  e. 
RR* )
285283, 284, 176syl2anc 642 . . . . . . . . . . . 12  |-  ( R  e.  RR+  ->  ( t  e.  ( -u R (,) R )  <->  ( t  e.  RR  /\  -u R  <  t  /\  t  < 
R ) ) )
286 simpr 447 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  t  e.  RR )
287280adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  R  e.  RR )
288286, 287absltd 11912 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( abs `  t
)  <  R  <->  ( -u R  <  t  /\  t  < 
R ) ) )
289288biimprd 214 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( -u R  <  t  /\  t  <  R )  ->  ( abs `  t
)  <  R )
)
290289exp4b 590 . . . . . . . . . . . . 13  |-  ( R  e.  RR+  ->  ( t  e.  RR  ->  ( -u R  <  t  -> 
( t  <  R  ->  ( abs `  t
)  <  R )
) ) )
2912903impd 1165 . . . . . . . . . . . 12  |-  ( R  e.  RR+  ->  ( ( t  e.  RR  /\  -u R  <  t  /\  t  <  R )  -> 
( abs `  t
)  <  R )
)
292285, 291sylbid 206 . . . . . . . . . . 11  |-  ( R  e.  RR+  ->  ( t  e.  ( -u R (,) R )  ->  ( abs `  t )  < 
R ) )
293292imp 418 . . . . . . . . . 10  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( abs `  t
)  <  R )
294279, 281, 293ltled 8967 . . . . . . . . 9  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( abs `  t
)  <_  R )
295294, 121syl 15 . . . . . . . 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 ) ) ) ) ) )
296280resqcld 11271 . . . . . . . . . . . . . . 15  |-  ( R  e.  RR+  ->  ( R ^ 2 )  e.  RR )
297296recnd 8861 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  ( R ^ 2 )  e.  CC )
298297adantr 451 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  ( R ^ 2 )  e.  CC )
299201adantl 452 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
t ^ 2 )  e.  CC )
300298, 299subcld 9157 . . . . . . . . . . . 12  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  e.  CC )
301300sqrcld 11919 . . . . . . . . . . 11  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  CC )
302301, 301subnegd 9164 . . . . . . . . . 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 ) ) ) ) )
303166, 302sylan2 460 . . . . . . . . 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 ) ) ) ) )
304296adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  ( R ^ 2 )  e.  RR )
30516adantl 452 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
t ^ 2 )  e.  RR )
306304, 305resubcld 9211 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  e.  RR )
307166, 306sylan2 460 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( ( R ^
2 )  -  (
t ^ 2 ) )  e.  RR )
30870a1i 10 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  e.  RR )
30924adantl 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  ( abs `  t )  e.  RR )
31027adantl 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  0  <_  ( abs `  t
) )
311 rpge0 10366 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( R  e.  RR+  ->  0  <_  R )
312311adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  0  <_  R )
313309, 287, 310, 312lt2sqd 11279 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( abs `  t
)  <  R  <->  ( ( abs `  t ) ^
2 )  <  ( R ^ 2 ) ) )
31420adantl 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( abs `  t
) ^ 2 )  =  ( t ^
2 ) )
315314breq1d 4033 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( ( abs `  t
) ^ 2 )  <  ( R ^
2 )  <->  ( t ^ 2 )  < 
( R ^ 2 ) ) )
316313, 288, 3153bitr3rd 275 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( t ^ 2 )  <  ( R ^ 2 )  <->  ( -u R  <  t  /\  t  < 
R ) ) )
317305, 304posdifd 9359 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( t ^ 2 )  <  ( R ^ 2 )  <->  0  <  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )
318316, 317bitr3d 246 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( -u R  <  t  /\  t  <  R )  <->  0  <  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) )
319318biimpd 198 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( -u R  <  t  /\  t  <  R )  ->  0  <  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) )
320319exp4b 590 . . . . . . . . . . . . . . . . . 18  |-  ( R  e.  RR+  ->  ( t  e.  RR  ->  ( -u R  <  t  -> 
( t  <  R  ->  0  <  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) ) ) )
3213203impd 1165 . . . . . . . . . . . . . . . . 17  |-  ( R  e.  RR+  ->  ( ( t  e.  RR  /\  -u R  <  t  /\  t  <  R )  -> 
0  <  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )
322285, 321sylbid 206 . . . . . . . . . . . . . . . 16  |-  ( R  e.  RR+  ->  ( t  e.  ( -u R (,) R )  ->  0  <  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
323322imp 418 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  <  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )
324308, 307, 323ltled 8967 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )
325307, 324resqrcld 11900 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
326325renegcld 9210 . . . . . . . . . . . 12  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  ->  -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
327326, 325, 36syl2anc 642 . . . . . . . . . . 11  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )  e. 
dom  vol )
328327, 38syl 15 . . . . . . . . . 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 ) ) ) ) ) )
329307, 324sqrge0d 11903 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
330325, 325, 329, 329addge0d 9348 . . . . . . . . . . . 12  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  <_  ( ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  +  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
331303breq2d 4035 . . . . . . . . . . . . 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 ) ) ) ) ) )
332325, 326subge0d 9362 . . . . . . . . . . . . 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 ) ) ) ) )
333331, 332bitr3d 246 . . . . . . . . . . . 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 ) ) ) ) )
334330, 333mpbid 201 . . . . . . . . . . 11  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  ->  -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
335326, 325, 334, 55syl3anc 1182 . . . . . . . . . 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 ) ) ) ) )
336328, 335eqtrd 2315 . . . . . . . . 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 ) ) ) ) )
337 ax-resscn 8794 . . . . . . . . . . . . . . 15  |-  RR  C_  CC
338337a1i 10 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  RR  C_  CC )
339282, 280, 86syl2anc 642 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  ( -u R [,] R )  C_  RR )
340 rpcn 10362 . . . . . . . . . . . . . . . . 17  |-  ( R  e.  RR+  ->  R  e.  CC )
341340sqcld 11243 . . . . . . . . . . . . . . . 16  |-  ( R  e.  RR+  ->  ( R ^ 2 )  e.  CC )
342341adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( R ^ 2 )  e.  CC )
343339sselda 3180 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  ->  u  e.  RR )
344343recnd 8861 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  ->  u  e.  CC )
345340adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  ->  R  e.  CC )
346 rpne0 10369 . . . . . . . . . . . . . . . . . . 19  |-  ( R  e.  RR+  ->  R  =/=  0 )
347346adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  ->  R  =/=  0 )
348344, 345, 347divcld 9536 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( u  /  R
)  e.  CC )
349 asincl 20169 . . . . . . . . . . . . . . . . 17  |-  ( ( u  /  R )  e.  CC  ->  (arcsin `  ( u  /  R
) )  e.  CC )
350348, 349syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
(arcsin `  ( u  /  R ) )  e.  CC )
351 ax-1cn 8795 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  CC
352351a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
1  e.  CC )
353348sqcld 11243 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( ( u  /  R ) ^ 2 )  e.  CC )
354352, 353subcld 9157 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( 1  -  (
( u  /  R
) ^ 2 ) )  e.  CC )
355354sqrcld 11919 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( sqr `  (
1  -  ( ( u  /  R ) ^ 2 ) ) )  e.  CC )
356348, 355mulcld 8855 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( ( u  /  R )  x.  ( sqr `  ( 1  -  ( ( u  /  R ) ^ 2 ) ) ) )  e.  CC )
357350, 356addcld 8854 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( (arcsin `  (
u  /  R ) )  +  ( ( u  /  R )  x.  ( sqr `  (
1  -  ( ( u  /  R ) ^ 2 ) ) ) ) )  e.  CC )
358342, 357mulcld 8855 . . . . . . . . . . . . . 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 )
359 eqid 2283 . . . . . . . . . . . . . . 15  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
360359tgioo2 18309 . . . . . . . . . . . . . 14  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
361 iccntr 18326 . . . . . . . . . . . . . . 15  |-  ( (
-u R  e.  RR  /\  R  e.  RR )  ->  ( ( int `  ( topGen `  ran  (,) )
) `  ( -u R [,] R ) )  =  ( -u R (,) R ) )
362282, 280, 361syl2anc 642 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( -u R [,] R
) )  =  (
-u R (,) R
) )
363338, 339, 358, 360, 359, 362dvmptntr 19320 . . . . . . . . . . . . 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 ) ) ) ) ) ) ) ) )
364 areacirclem2 24925 . . . . . . . . . . . . 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 ) ) ) ) ) )
365363, 364eqtrd 2315 . . . . . . . . . . . 12  |-  ( R  e.  RR+  ->  ( RR 
_D  ( u  e.  (