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

Theorem areacirc 31944
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 4421 . . . . . . 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 2445 . . . . . 6  |-  S  =  { u  |  E. x E. y ( u  =  <. x ,  y
>.  /\  ( ( x  e.  RR  /\  y  e.  RR )  /\  (
( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^
2 ) ) ) }
4 simpl 458 . . . . . . . . 9  |-  ( ( u  =  <. x ,  y >.  /\  (
( x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) ) )  ->  u  =  <. x ,  y >.
)
5 opelxpi 4823 . . . . . . . . . . 11  |-  ( ( x  e.  RR  /\  y  e.  RR )  -> 
<. x ,  y >.  e.  ( RR  X.  RR ) )
65adantr 466 . . . . . . . . . 10  |-  ( ( ( x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) )  ->  <. x ,  y
>.  e.  ( RR  X.  RR ) )
76adantl 467 . . . . . . . . 9  |-  ( ( u  =  <. x ,  y >.  /\  (
( x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) ) )  ->  <. x ,  y >.  e.  ( RR  X.  RR ) )
84, 7eqeltrd 2501 . . . . . . . 8  |-  ( ( u  =  <. x ,  y >.  /\  (
( x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) ) )  ->  u  e.  ( RR  X.  RR ) )
98exlimivv 1771 . . . . . . 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 3474 . . . . . 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 3432 . . . . 5  |-  S  C_  ( RR  X.  RR )
1211a1i 11 . . . 4  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  S  C_  ( RR  X.  RR ) )
131areacirclem5 31943 . . . . . . 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 12287 . . . . . . . . . . . . . . 15  |-  ( R  e.  RR  ->  ( R ^ 2 )  e.  RR )
15143ad2ant1 1026 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R ^ 2 )  e.  RR )
16 resqcl 12287 . . . . . . . . . . . . . . 15  |-  ( t  e.  RR  ->  (
t ^ 2 )  e.  RR )
17163ad2ant3 1028 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t ^ 2 )  e.  RR )
1815, 17resubcld 9993 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  e.  RR )
1918adantr 466 . . . . . . . . . . . 12  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( ( R ^
2 )  -  (
t ^ 2 ) )  e.  RR )
20 absresq 13304 . . . . . . . . . . . . . . . 16  |-  ( t  e.  RR  ->  (
( abs `  t
) ^ 2 )  =  ( t ^
2 ) )
21203ad2ant3 1028 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
) ^ 2 )  =  ( t ^
2 ) )
2221breq1d 4371 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( ( abs `  t
) ^ 2 )  <_  ( R ^
2 )  <->  ( t ^ 2 )  <_ 
( R ^ 2 ) ) )
23 recn 9575 . . . . . . . . . . . . . . . . 17  |-  ( t  e.  RR  ->  t  e.  CC )
2423abscld 13436 . . . . . . . . . . . . . . . 16  |-  ( t  e.  RR  ->  ( abs `  t )  e.  RR )
25243ad2ant3 1028 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( abs `  t )  e.  RR )
26 simp1 1005 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  R  e.  RR )
2723absge0d 13444 . . . . . . . . . . . . . . . 16  |-  ( t  e.  RR  ->  0  <_  ( abs `  t
) )
28273ad2ant3 1028 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  0  <_  ( abs `  t
) )
29 simp2 1006 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  0  <_  R )
3025, 26, 28, 29le2sqd 12396 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  ( ( abs `  t ) ^
2 )  <_  ( R ^ 2 ) ) )
3115, 17subge0d 10149 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) )  <->  ( t ^ 2 )  <_ 
( R ^ 2 ) ) )
3222, 30, 313bitr4d 288 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )
3332biimpa 486 . . . . . . . . . . . 12  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )
3419, 33resqrtcld 13418 . . . . . . . . . . 11  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
3534renegcld 9992 . . . . . . . . . 10  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  -> 
-u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
36 iccmbl 22456 . . . . . . . . . 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 665 . . . . . . . . 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 22421 . . . . . . . . . . . 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 13421 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  0  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
4134, 34, 40, 40addge0d 10135 . . . . . . . . . . . . 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 9575 . . . . . . . . . . . . . . . . . . . . 21  |-  ( R  e.  RR  ->  R  e.  CC )
4342sqcld 12359 . . . . . . . . . . . . . . . . . . . 20  |-  ( R  e.  RR  ->  ( R ^ 2 )  e.  CC )
44433ad2ant1 1026 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R ^ 2 )  e.  CC )
4523sqcld 12359 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  e.  RR  ->  (
t ^ 2 )  e.  CC )
46453ad2ant3 1028 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t ^ 2 )  e.  CC )
4744, 46subcld 9932 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  e.  CC )
4847sqrtcld 13437 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  CC )
4948adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  CC )
5049, 49subnegd 9939 . . . . . . . . . . . . . . 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 4373 . . . . . . . . . . . . . 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 10149 . . . . . . . . . . . . . 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 258 . . . . . . . . . . . . 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 213 . . . . . . . . . . . 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 22414 . . . . . . . . . . . 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 1264 . . . . . . . . . . 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 2457 . . . . . . . . . 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 9993 . . . . . . . . . 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 2501 . . . . . . . . 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 22420 . . . . . . . . . 10  |-  vol : dom  vol --> ( 0 [,] +oo )
61 ffn 5684 . . . . . . . . . 10  |-  ( vol
: dom  vol --> ( 0 [,] +oo )  ->  vol  Fn  dom  vol )
62 elpreima 5956 . . . . . . . . . 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 668 . . . . . . . 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 22430 . . . . . . . . . 10  |-  (/)  e.  dom  vol
66 mblvol 22421 . . . . . . . . . . . . 13  |-  ( (/)  e.  dom  vol  ->  ( vol `  (/) )  =  ( vol* `  (/) ) )
6765, 66ax-mp 5 . . . . . . . . . . . 12  |-  ( vol `  (/) )  =  ( vol* `  (/) )
68 ovol0 22383 . . . . . . . . . . . 12  |-  ( vol* `  (/) )  =  0
6967, 68eqtri 2445 . . . . . . . . . . 11  |-  ( vol `  (/) )  =  0
70 0re 9589 . . . . . . . . . . 11  |-  0  e.  RR
7169, 70eqeltri 2497 . . . . . . . . . 10  |-  ( vol `  (/) )  e.  RR
72 elpreima 5956 . . . . . . . . . . 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 928 . . . . . . . . 9  |-  (/)  e.  ( `' vol " RR )
7574a1i 11 . . . . . . . 8  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  -.  ( abs `  t
)  <_  R )  -> 
(/)  e.  ( `' vol " RR ) )
7664, 75ifclda 3881 . . . . . . 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 2501 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( S " { t } )  e.  ( `' vol " RR ) )
78773expa 1205 . . . . 5  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  RR )  ->  ( S " { t } )  e.  ( `' vol " RR ) )
7978ralrimiva 2774 . . . 4  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  A. t  e.  RR  ( S " { t } )  e.  ( `' vol " RR ) )
8013fveq2d 5824 . . . . . . 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 1205 . . . . . 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 4448 . . . . 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 9883 . . . . . . . 8  |-  ( R  e.  RR  ->  -u R  e.  RR )
8483adantr 466 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  -u R  e.  RR )
85 simpl 458 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  R  e.  RR )
86 iccssre 11662 . . . . . . 7  |-  ( (
-u R  e.  RR  /\  R  e.  RR )  ->  ( -u R [,] R )  C_  RR )
8784, 85, 86syl2anc 665 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( -u R [,] R
)  C_  RR )
88 rembl 22431 . . . . . . 7  |-  RR  e.  dom  vol
8988a1i 11 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  RR  e.  dom  vol )
90 fvex 5830 . . . . . . 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 3384 . . . . . . . . 9  |-  ( t  e.  ( RR  \ 
( -u R [,] R
) )  <->  ( t  e.  RR  /\  -.  t  e.  ( -u R [,] R ) ) )
93 3anass 986 . . . . . . . . . . . . . . 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 1026 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  -u R  e.  RR )
96 elicc2 11645 . . . . . . . . . . . . . . 15  |-  ( (
-u R  e.  RR  /\  R  e.  RR )  ->  ( t  e.  ( -u R [,] R )  <->  ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R ) ) )
9795, 26, 96syl2anc 665 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t  e.  ( -u R [,] R )  <->  ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R ) ) )
98 simp3 1007 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  t  e.  RR )
9998, 26absled 13431 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  ( -u R  <_  t  /\  t  <_  R ) ) )
10098biantrurd 510 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( -u R  <_  t  /\  t  <_  R )  <-> 
( t  e.  RR  /\  ( -u R  <_ 
t  /\  t  <_  R ) ) ) )
10199, 100bitrd 256 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  ( t  e.  RR  /\  ( -u R  <_  t  /\  t  <_  R ) ) ) )
10294, 97, 1013bitr4rd 289 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  t  e.  ( -u R [,] R
) ) )
103102biimpd 210 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  ->  t  e.  ( -u R [,] R ) ) )
104103con3d 138 . . . . . . . . . . 11  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -.  t  e.  ( -u R [,] R )  ->  -.  ( abs `  t )  <_  R
) )
1051043expia 1207 . . . . . . . . . 10  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  ->  ( -.  t  e.  ( -u R [,] R )  ->  -.  ( abs `  t )  <_  R ) ) )
106105impd 432 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( ( t  e.  RR  /\  -.  t  e.  ( -u R [,] R ) )  ->  -.  ( abs `  t
)  <_  R )
)
10792, 106syl5bi 220 . . . . . . . 8  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  ( RR  \  ( -u R [,] R ) )  ->  -.  ( abs `  t )  <_  R
) )
108107imp 430 . . . . . . 7  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  ( RR  \  ( -u R [,] R ) ) )  ->  -.  ( abs `  t )  <_  R
)
109 iffalse 3858 . . . . . . . . 9  |-  ( -.  ( abs `  t
)  <_  R  ->  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) )  =  (/) )
110109fveq2d 5824 . . . . . . . 8  |-  ( -.  ( abs `  t
)  <_  R  ->  ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  =  ( vol `  (/) ) )
111110, 69syl6eq 2473 . . . . . . 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 665 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  <->  ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R ) ) )
11499biimprd 226 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( -u R  <_  t  /\  t  <_  R )  ->  ( abs `  t
)  <_  R )
)
115114expd 437 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -u R  <_  t  ->  ( t  <_  R  ->  ( abs `  t )  <_  R ) ) )
1161153expia 1207 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  ->  ( -u R  <_ 
t  ->  ( t  <_  R  ->  ( abs `  t )  <_  R
) ) ) )
1171163impd 1219 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R )  ->  ( abs `  t )  <_  R ) )
118113, 117sylbid 218 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  ->  ( abs `  t )  <_  R
) )
1191183impia 1202 . . . . . . . . . . 11  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( abs `  t
)  <_  R )
120 iftrue 3855 . . . . . . . . . . . 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 5824 . . . . . . . . . . 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 1026 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( R ^ 2 )  e.  RR )
12483, 86mpancom 673 . . . . . . . . . . . . . . . . . 18  |-  ( R  e.  RR  ->  ( -u R [,] R ) 
C_  RR )
125124sselda 3402 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR  /\  t  e.  ( -u R [,] R ) )  -> 
t  e.  RR )
1261253adant2 1024 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
t  e.  RR )
127126resqcld 12387 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( t ^ 2 )  e.  RR )
128123, 127resubcld 9993 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( ( R ^
2 )  -  (
t ^ 2 ) )  e.  RR )
12983, 96mpancom 673 . . . . . . . . . . . . . . . . 17  |-  ( R  e.  RR  ->  (
t  e.  ( -u R [,] R )  <->  ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R ) ) )
130129adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  <->  ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R ) ) )
13130, 99, 223bitr3rd 287 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( t ^ 2 )  <_  ( R ^ 2 )  <->  ( -u R  <_  t  /\  t  <_  R ) ) )
13231, 131bitrd 256 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) )  <->  ( -u R  <_  t  /\  t  <_  R ) ) )
133132biimprd 226 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( -u R  <_  t  /\  t  <_  R )  ->  0  <_  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) )
134133expd 437 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -u R  <_  t  ->  ( t  <_  R  ->  0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
1351343expia 1207 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  ->  ( -u R  <_ 
t  ->  ( t  <_  R  ->  0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ) )
1361353impd 1219 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R )  ->  0  <_  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
137130, 136sylbid 218 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  ->  0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )
1381373impia 1202 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )
139128, 138resqrtcld 13418 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
140139renegcld 9992 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  ->  -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
141140, 139, 36syl2anc 665 . . . . . . . . . . 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 9615 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( ( R ^
2 )  -  (
t ^ 2 ) )  e.  CC )
144143sqrtcld 13437 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  CC )
145144, 144subnegd 9939 . . . . . . . . . . 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 13421 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
0  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
147139, 139, 146, 146addge0d 10135 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
0  <_  ( ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  +  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
148145breq2d 4373 . . . . . . . . . . . . . 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 10149 . . . . . . . . . . . . . 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 258 . . . . . . . . . . . . 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 213 . . . . . . . . . . . 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 1264 . . . . . . . . . . 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 10801 . . . . . . . . . . 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 2467 . . . . . . . . . 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 2461 . . . . . . . . 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 1205 . . . . . . . 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 4448 . . . . . . 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 31941 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  |->  ( 2  x.  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )  e.  L^1 )
159157, 158eqeltrd 2501 . . . . . 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 22700 . . . . 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 2501 . . . 4  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  |->  ( vol `  ( S
" { t } ) ) )  e.  L^1 )
162 dmarea 23820 . . . 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 1189 . . 3  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  S  e.  dom area )
164 areaval 23827 . . 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 11612 . . . . . 6  |-  ( t  e.  ( -u R (,) R )  ->  t  e.  RR )
167133expa 1205 . . . . . 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 476 . . . . 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 5824 . . . 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 22676 . . 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 11642 . . . . 5  |-  ( -u R (,) R )  C_  RR
172171a1i 11 . . . 4  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( -u R (,) R
)  C_  RR )
173 eldif 3384 . . . . . 6  |-  ( t  e.  ( RR  \ 
( -u R (,) R
) )  <->  ( t  e.  RR  /\  -.  t  e.  ( -u R (,) R ) ) )
17483rexrd 9636 . . . . . . . . . . . . . 14  |-  ( R  e.  RR  ->  -u R  e.  RR* )
175 rexr 9632 . . . . . . . . . . . . . 14  |-  ( R  e.  RR  ->  R  e.  RR* )
176 elioo2 11623 . . . . . . . . . . . . . 14  |-  ( (
-u R  e.  RR*  /\  R  e.  RR* )  ->  ( t  e.  (
-u R (,) R
)  <->  ( t  e.  RR  /\  -u R  <  t  /\  t  < 
R ) ) )
177174, 175, 176syl2anc 665 . . . . . . . . . . . . 13  |-  ( R  e.  RR  ->  (
t  e.  ( -u R (,) R )  <->  ( t  e.  RR  /\  -u R  <  t  /\  t  < 
R ) ) )
1781773ad2ant1 1026 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t  e.  ( -u R (,) R )  <->  ( t  e.  RR  /\  -u R  <  t  /\  t  < 
R ) ) )
17998biantrurd 510 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( -u R  <  t  /\  t  <  R )  <-> 
( t  e.  RR  /\  ( -u R  < 
t  /\  t  <  R ) ) ) )
18098, 26absltd 13430 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <  R  <->  ( -u R  <  t  /\  t  < 
R ) ) )
181 3anass 986 . . . . . . . . . . . . . 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 289 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( t  e.  RR  /\  -u R  <  t  /\  t  <  R )  <->  ( abs `  t )  <  R
) )
184178, 183bitrd 256 . . . . . . . . . . 11  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t  e.  ( -u R (,) R )  <->  ( abs `  t )  <  R
) )
185184notbid 295 . . . . . . . . . 10  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -.  t  e.  ( -u R (,) R )  <->  -.  ( abs `  t
)  <  R )
)
18626, 25lenltd 9727 . . . . . . . . . 10  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R  <_  ( abs `  t
)  <->  -.  ( abs `  t )  <  R
) )
187185, 186bitr4d 259 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -.  t  e.  ( -u R (,) R )  <-> 
R  <_  ( abs `  t ) ) )
18813adantr 466 . . . . . . . . . . . 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 5824 . . . . . . . . . . 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 570 . . . . . . . . . . . . . . . 16  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( ( abs `  t )  e.  RR  /\  ( abs `  t
)  =  R ) )
191 eqle 9682 . . . . . . . . . . . . . . . 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 6251 . . . . . . . . . . . . . . . . . 18  |-  ( ( abs `  t )  =  R  ->  (
( abs `  t
) ^ 2 )  =  ( R ^
2 ) )
194193adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( ( abs `  t ) ^ 2 )  =  ( R ^ 2 ) )
19521adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( ( abs `  t ) ^ 2 )  =  ( t ^ 2 ) )
196194, 195eqtr3d 2459 . . . . . . . . . . . . . . . 16  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( R ^
2 )  =  ( t ^ 2 ) )
197 oveq1 6251 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R ^ 2 )  =  ( t ^
2 )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  =  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )
198197fveq2d 5824 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R ^ 2 )  =  ( t ^
2 )  ->  ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  =  ( sqr `  (
( t ^ 2 )  -  ( t ^ 2 ) ) ) )
199198negeqd 9815 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R ^ 2 )  =  ( t ^
2 )  ->  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  = 
-u ( sqr `  (
( t ^ 2 )  -  ( t ^ 2 ) ) ) )
200199, 198oveq12d 6262 . . . . . . . . . . . . . . . . . . 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 9615 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  e.  RR  ->  (
t ^ 2 )  e.  CC )
202201subidd 9920 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  e.  RR  ->  (
( t ^ 2 )  -  ( t ^ 2 ) )  =  0 )
203202fveq2d 5824 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  e.  RR  ->  ( sqr `  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )  =  ( sqr `  0
) )
204203negeqd 9815 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  e.  RR  ->  -u ( sqr `  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )  = 
-u ( sqr `  0
) )
205 sqrt0 13244 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( sqr `  0 )  =  0
206205negeqi 9814 . . . . . . . . . . . . . . . . . . . . . . 23  |-  -u ( sqr `  0 )  = 
-u 0
207 neg0 9866 . . . . . . . . . . . . . . . . . . . . . . 23  |-  -u 0  =  0
208206, 207eqtri 2445 . . . . . . . . . . . . . . . . . . . . . 22  |-  -u ( sqr `  0 )  =  0
209204, 208syl6eq 2473 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  e.  RR  ->  -u ( sqr `  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )  =  0 )
210203, 205syl6eq 2473 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  e.  RR  ->  ( sqr `  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )  =  0 )
211209, 210oveq12d 6262 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  e.  RR  ->  ( -u ( sqr `  (
( t ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( t ^
2 )  -  (
t ^ 2 ) ) ) )  =  ( 0 [,] 0
) )
2122113ad2ant3 1028 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -u ( sqr `  (
( t ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( t ^
2 )  -  (
t ^ 2 ) ) ) )  =  ( 0 [,] 0
) )
213200, 212sylan9eqr 2479 . . . . . . . . . . . . . . . . . 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 5824 . . . . . . . . . . . . . . . . 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 22456 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 0  e.  RR  /\  0  e.  RR )  ->  ( 0 [,] 0
)  e.  dom  vol )
21670, 70, 215mp2an 676 . . . . . . . . . . . . . . . . . . 19  |-  ( 0 [,] 0 )  e. 
dom  vol
217 mblvol 22421 . . . . . . . . . . . . . . . . . . 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 9633 . . . . . . . . . . . . . . . . . . . 20  |-  0  e.  RR*
220 iccid 11627 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 0  e.  RR*  ->  ( 0 [,] 0 )  =  { 0 } )
221220fveq2d 5824 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  e.  RR*  ->  ( vol* `  ( 0 [,] 0 ) )  =  ( vol* `  { 0 } ) )
222219, 221ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  ( vol* `  ( 0 [,] 0 ) )  =  ( vol* `  { 0 } )
223 ovolsn 22385 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  e.  RR  ->  ( vol* `  { 0 } )  =  0 )
22470, 223ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  ( vol* `  { 0 } )  =  0
225222, 224eqtri 2445 . . . . . . . . . . . . . . . . . 18  |-  ( vol* `  ( 0 [,] 0 ) )  =  0
226218, 225eqtri 2445 . . . . . . . . . . . . . . . . 17  |-  ( vol `  ( 0 [,] 0
) )  =  0
227214, 226syl6eq 2473 . . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . 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 2457 . . . . . . . . . . . . . 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 435 . . . . . . . . . . . . 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 466 . . . . . . . . . . . 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 9728 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R  <  ( abs `  t
)  <->  -.  ( abs `  t )  <_  R
) )
233232adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( R  <  ( abs `  t )  <->  -.  ( abs `  t )  <_  R ) )
234 simpl1 1008 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  ->  R  e.  RR )
23525adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( abs `  t
)  e.  RR )
236 simpr 462 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  ->  R  <_  ( abs `  t
) )
237234, 235, 236leltned 9734 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( R  <  ( abs `  t )  <->  ( abs `  t )  =/=  R
) )
238233, 237bitr3d 258 . . . . . . . . . . . . 13  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( -.  ( abs `  t )  <_  R  <->  ( abs `  t )  =/=  R ) )
239238, 111syl6bir 232 . . . . . . . . . . . 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 2682 . . . . . . . . . . 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 2457 . . . . . . . . . 10  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( vol `  ( S " { t } ) )  =  0 )
242241ex 435 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R  <_  ( abs `  t
)  ->  ( vol `  ( S " {
t } ) )  =  0 ) )
243187, 242sylbid 218 . . . . . . . 8  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -.  t  e.  ( -u R (,) R )  ->  ( vol `  ( S " { t } ) )  =  0 ) )
2442433expia 1207 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  ->  ( -.  t  e.  ( -u R (,) R )  ->  ( vol `  ( S " { t } ) )  =  0 ) ) )
245244impd 432 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( ( t  e.  RR  /\  -.  t  e.  ( -u R (,) R ) )  -> 
( vol `  ( S " { t } ) )  =  0 ) )
246173, 245syl5bi 220 . . . . 5  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  ( RR  \  ( -u R (,) R ) )  ->  ( vol `  ( S " { t } ) )  =  0 ) )
247246imp 430 . . . 4  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  ( RR  \  ( -u R (,) R ) ) )  ->  ( vol `  ( S " { t } ) )  =  0 )
248172, 247itgss 22706 . . 3  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  S. ( -u R (,) R ) ( vol `  ( S " {
t } ) )  _d t  =  S. RR ( vol `  ( S " { t } ) )  _d t )
249 negeq 9813 . . . . . . . . . 10  |-  ( R  =  0  ->  -u R  =  -u 0 )
250249, 207syl6eq 2473 . . . . . . . . 9  |-  ( R  =  0  ->  -u R  =  0 )
251 id 22 . . . . . . . . 9  |-  ( R  =  0  ->  R  =  0 )
252250, 251oveq12d 6262 . . . . . . . 8  |-  ( R  =  0  ->  ( -u R (,) R )  =  ( 0 (,) 0 ) )
253 iooid 11610 . . . . . . . 8  |-  ( 0 (,) 0 )  =  (/)
254252, 253syl6eq 2473 . . . . . . 7  |-  ( R  =  0  ->  ( -u R (,) R )  =  (/) )
255254adantl 467 . . . . . 6  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  R  =  0
)  ->  ( -u R (,) R )  =  (/) )
256 itgeq1 22667 . . . . . 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 22674 . . . . . 6  |-  S. (/) ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  _d t  =  0
259 oveq1 6251 . . . . . . . . 9  |-  ( R  =  0  ->  ( R ^ 2 )  =  ( 0 ^ 2 ) )
260259oveq2d 6260 . . . . . . . 8  |-  ( R  =  0  ->  (
pi  x.  ( R ^ 2 ) )  =  ( pi  x.  ( 0 ^ 2 ) ) )
261 sq0 12311 . . . . . . . . . 10  |-  ( 0 ^ 2 )  =  0
262261oveq2i 6255 . . . . . . . . 9  |-  ( pi  x.  ( 0 ^ 2 ) )  =  ( pi  x.  0 )
263 picn 23351 . . . . . . . . . 10  |-  pi  e.  CC
264263mul01i 9769 . . . . . . . . 9  |-  ( pi  x.  0 )  =  0
265262, 264eqtr2i 2446 . . . . . . . 8  |-  0  =  ( pi  x.  ( 0 ^ 2 ) )
266260, 265syl6reqr 2476 . . . . . . 7  |-  ( R  =  0  ->  0  =  ( pi  x.  ( R ^ 2 ) ) )
267266adantl 467 . . . . . 6  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  R  =  0
)  ->  0  =  ( pi  x.  ( R ^ 2 ) ) )
268258, 267syl5eq 2469 . . . . 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 2457 . . . 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 1005 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R  /\  R  =/=  0 )  ->  R  e.  RR )
271 0red 9590 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
0  e.  RR )
272 simpr 462 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
0  <_  R )
273271, 85, 272leltned 9734 . . . . . . . 8  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( 0  <  R  <->  R  =/=  0 ) )
274273biimp3ar 1365 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R  /\  R  =/=  0 )  ->  0  <  R )
275270, 274elrpd 11284 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R  /\  R  =/=  0 )  ->  R  e.  RR+ )
2762753expa 1205 . . . . 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 467 . . . . . . . . . 10  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( abs `  t
)  e.  RR )
279 rpre 11254 . . . . . . . . . . 11  |-  ( R  e.  RR+  ->  R  e.  RR )
280279adantr 466 . . . . . . . . . 10  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  ->  R  e.  RR )
281279renegcld 9992 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  -u R  e.  RR )
282281rexrd 9636 . . . . . . . . . . . . 13  |-  ( R  e.  RR+  ->  -u R  e.  RR* )
283 rpxr 11255 . . . . . . . . . . . . 13  |-  ( R  e.  RR+  ->  R  e. 
RR* )
284282, 283, 176syl2anc 665 . . . . . . . . . . . 12  |-  ( R  e.  RR+  ->  ( t  e.  ( -u R (,) R )  <->  ( t  e.  RR  /\  -u R  <  t  /\  t  < 
R ) ) )
285 simpr 462 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  t  e.  RR )
286279adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  R  e.  RR )
287285, 286absltd 13430 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( abs `  t
)  <  R  <->  ( -u R  <  t  /\  t  < 
R ) ) )
288287biimprd 226 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( -u R  <  t  /\  t  <  R )  ->  ( abs `  t
)  <  R )
)
289288exp4b 610 . . . . . . . . . . . . 13  |-  ( R  e.  RR+  ->  ( t  e.  RR  ->  ( -u R  <  t  -> 
( t  <  R  ->  ( abs `  t
)  <  R )
) ) )
2902893impd 1219 . . . . . . . . . . . 12  |-  ( R  e.  RR+  ->  ( ( t  e.  RR  /\  -u R  <  t  /\  t  <  R )  -> 
( abs `  t
)  <  R )
)
291284, 290sylbid 218 . . . . . . . . . . 11  |-  ( R  e.  RR+  ->  ( t  e.  ( -u R (,) R )  ->  ( abs `  t )  < 
R ) )
292291imp 430 . . . . . . . . . 10  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( abs `  t
)  <  R )
293278, 280, 292ltled 9729 . . . . . . . . 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 12387 . . . . . . . . . . . . . . 15  |-  ( R  e.  RR+  ->  ( R ^ 2 )  e.  RR )
296295recnd 9615 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  ( R ^ 2 )  e.  CC )
297296adantr 466 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  ( R ^ 2 )  e.  CC )
298201adantl 467 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
t ^ 2 )  e.  CC )
299297, 298subcld 9932 . . . . . . . . . . . 12  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  e.  CC )
300299sqrtcld 13437 . . . . . . . . . . 11  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  CC )
301300, 300subnegd 9939 . . . . . . . . . 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 476 . . . . . . . . 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 466 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  ( R ^ 2 )  e.  RR )
30416adantl 467 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
t ^ 2 )  e.  RR )
305303, 304resubcld 9993 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  e.  RR )
306166, 305sylan2 476 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( ( R ^
2 )  -  (
t ^ 2 ) )  e.  RR )
307 0red 9590 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  e.  RR )
30824adantl 467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  ( abs `  t )  e.  RR )
30927adantl 467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  0  <_  ( abs `  t
) )
310 rpge0 11260 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( R  e.  RR+  ->  0  <_  R )
311310adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  0  <_  R )
312308, 286, 309, 311lt2sqd 12395 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( abs `  t
)  <  R  <->  ( ( abs `  t ) ^
2 )  <  ( R ^ 2 ) ) )
31320adantl 467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( abs `  t
) ^ 2 )  =  ( t ^
2 ) )
314313breq1d 4371 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( ( abs `  t
) ^ 2 )  <  ( R ^
2 )  <->  ( t ^ 2 )  < 
( R ^ 2 ) ) )
315312, 287, 3143bitr3rd 287 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( t ^ 2 )  <  ( R ^ 2 )  <->  ( -u R  <  t  /\  t  < 
R ) ) )
316304, 303posdifd 10146 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( t ^ 2 )  <  ( R ^ 2 )  <->  0  <  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )
317315, 316bitr3d 258 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( -u R  <  t  /\  t  <  R )  <->  0  <  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) )
318317biimpd 210 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( -u R  <  t  /\  t  <  R )  ->  0  <  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) )
319318exp4b 610 . . . . . . . . . . . . . . . . . 18  |-  ( R  e.  RR+  ->  ( t  e.  RR  ->  ( -u R  <  t  -> 
( t  <  R  ->  0  <  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) ) ) )
3203193impd 1219 . . . . . . . . . . . . . . . . 17  |-  ( R  e.  RR+  ->  ( ( t  e.  RR  /\  -u R  <  t  /\  t  <  R )  -> 
0  <  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )
321284, 320sylbid 218 . . . . . . . . . . . . . . . 16  |-  ( R  e.  RR+  ->  ( t  e.  ( -u R (,) R )  ->  0  <  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
322321imp 430 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  <  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )
323307, 306, 322ltled 9729 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )
324306, 323resqrtcld 13418 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
325324renegcld 9992 . . . . . . . . . . . 12  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  ->  -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
326325, 324, 36syl2anc 665 . . . . . . . . . . 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 13421 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
329324, 324, 328, 328addge0d 10135 . . . . . . . . . . . 12  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  <_  ( ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  +  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
330302breq2d 4373 . . . . . . . . . . . . 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 10149 . . . . . . . . . . . . 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 258 . . . . . . . . . . . 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 213 . . . . . . . . . . 11  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  ->  -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
334325, 324, 333, 55syl3anc 1264 . . . . . . . . . 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 2457 . . . . . . . . 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 9542 . . . . . . . . . . . . . . 15  |-  RR  C_  CC
337336a1i 11 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  RR  C_  CC )
338281, 279, 86syl2anc 665 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  ( -u R [,] R )  C_  RR )
339 rpcn 11256 . . . . . . . . . . . . . . . . 17  |-  ( R  e.  RR+  ->  R  e.  CC )
340339sqcld 12359 . . . . . . . . . . . . . . . 16  |-  ( R  e.  RR+  ->  ( R ^ 2 )  e.  CC )
341340adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( R ^ 2 )  e.  CC )
342338sselda 3402 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  ->  u  e.  RR )
343342recnd 9615 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  ->  u  e.  CC )
344339adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  ->  R  e.  CC )
345 rpne0 11263 . . . . . . . . . . . . . . . . . . 19  |-  ( R  e.  RR+  ->  R  =/=  0 )
346345adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  ->  R  =/=  0 )
347343, 344, 346divcld 10329 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( u  /  R
)  e.  CC )
348 asincl 23736 . . . . . . . . . . . . . . . . 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 9605 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
1  e.  CC )
351347sqcld 12359 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( ( u  /  R ) ^ 2 )  e.  CC )
352350, 351subcld 9932 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( 1  -  (
( u  /  R
) ^ 2 ) )  e.  CC )
353352sqrtcld 13437 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( sqr `  (
1  -  ( ( u  /  R ) ^ 2 ) ) )  e.  CC )
354347, 353mulcld 9609 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( ( u  /  R )  x.  ( sqr `  ( 1  -  ( ( u  /  R ) ^ 2 ) ) ) )  e.  CC )
355349, 354addcld 9608 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( (arcsin `  (
u  /  R ) )  +  ( ( u  /  R )  x.  ( sqr `  (
1  -  ( ( u  /  R ) ^ 2 ) ) ) ) )  e.  CC )
356341, 355mulcld 9609 . . . . . . . . . . . . . 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 2423 . . . . . . . . . . . . . . 15  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
358357tgioo2 21758 . . . . . . . . . . . . . 14  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
359 iccntr 21776 . . . . . . . . . . . . . . 15  |-  ( (
-u R  e.  RR  /\  R  e.  RR )  ->  ( ( int `  ( topGen `  ran  (,) )
) `  ( -u R [,] R ) )  =  ( -u R (,) R ) )
360281, 279, 359syl2anc 665 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( -u R [,] R
) )  =  (
-u R (,) R
) )
361337, 338, 356, 358, 357, 360dvmptntr 22862 . . . . . . . . . . . . 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 31939 . . . . . . . . . . . . 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 2457 . . . . . . . . . . . 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 466 . . . . . . . . . . 11  |-  ( ( R  e.  RR+  /\  t  e.