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

Theorem areacirc 24341
Description: The area of a circle of radius  R is  pi  x.  R ^ 2. (Contributed by Brendan Leahy, 31-Aug-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 4079 . . . . . . 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 2304 . . . . . 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 4720 . . . . . . . . . . 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 2358 . . . . . . . 8  |-  ( ( u  =  <. x ,  y >.  /\  (
( x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) ) )  ->  u  e.  ( RR  X.  RR ) )
98exlimivv 1668 . . . . . . 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 3249 . . . . . 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 3209 . . . . 5  |-  S  C_  ( RR  X.  RR )
1211a1i 10 . . . 4  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  S  C_  ( RR  X.  RR ) )
13 simp1 955 . . . . . . . 8  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  R  e.  RR )
14 simp2 956 . . . . . . . 8  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  0  <_  R )
15 simp3 957 . . . . . . . 8  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  t  e.  RR )
161, 13, 14, 15areacirclem6 24340 . . . . . . 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 ) ) ) ) ,  (/) ) )
17 resqcl 11167 . . . . . . . . . . . . . . 15  |-  ( R  e.  RR  ->  ( R ^ 2 )  e.  RR )
18173ad2ant1 976 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R ^ 2 )  e.  RR )
19 resqcl 11167 . . . . . . . . . . . . . . 15  |-  ( t  e.  RR  ->  (
t ^ 2 )  e.  RR )
20193ad2ant3 978 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t ^ 2 )  e.  RR )
2118, 20resubcld 9207 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  e.  RR )
2221adantr 451 . . . . . . . . . . . 12  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( ( R ^
2 )  -  (
t ^ 2 ) )  e.  RR )
23 absresq 11783 . . . . . . . . . . . . . . . 16  |-  ( t  e.  RR  ->  (
( abs `  t
) ^ 2 )  =  ( t ^
2 ) )
24233ad2ant3 978 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
) ^ 2 )  =  ( t ^
2 ) )
2524breq1d 4034 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( ( abs `  t
) ^ 2 )  <_  ( R ^
2 )  <->  ( t ^ 2 )  <_ 
( R ^ 2 ) ) )
26 recn 8823 . . . . . . . . . . . . . . . . 17  |-  ( t  e.  RR  ->  t  e.  CC )
2726abscld 11914 . . . . . . . . . . . . . . . 16  |-  ( t  e.  RR  ->  ( abs `  t )  e.  RR )
28273ad2ant3 978 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( abs `  t )  e.  RR )
2926absge0d 11922 . . . . . . . . . . . . . . . 16  |-  ( t  e.  RR  ->  0  <_  ( abs `  t
) )
30293ad2ant3 978 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  0  <_  ( abs `  t
) )
3128, 13, 30, 14le2sqd 11276 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  ( ( abs `  t ) ^
2 )  <_  ( R ^ 2 ) ) )
3218, 20subge0d 9358 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) )  <->  ( t ^ 2 )  <_ 
( R ^ 2 ) ) )
3325, 31, 323bitr4d 276 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )
3433biimpa 470 . . . . . . . . . . . 12  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )
3522, 34resqrcld 11896 . . . . . . . . . . 11  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
3635renegcld 9206 . . . . . . . . . 10  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  -> 
-u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
37 iccmbl 18919 . . . . . . . . . 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 )
3836, 35, 37syl2anc 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 )
39 mblvol 18885 . . . . . . . . . . . 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 ) ) ) ) ) )
4038, 39syl 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 ) ) ) ) ) )
4122, 34sqrge0d 11899 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  0  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
4235, 35, 41, 41addge0d 9344 . . . . . . . . . . . . 13  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  0  <_  ( ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  +  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
43 recn 8823 . . . . . . . . . . . . . . . . . . . . 21  |-  ( R  e.  RR  ->  R  e.  CC )
4443sqcld 11239 . . . . . . . . . . . . . . . . . . . 20  |-  ( R  e.  RR  ->  ( R ^ 2 )  e.  CC )
45443ad2ant1 976 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R ^ 2 )  e.  CC )
4626sqcld 11239 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  e.  RR  ->  (
t ^ 2 )  e.  CC )
47463ad2ant3 978 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t ^ 2 )  e.  CC )
4845, 47subcld 9153 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  e.  CC )
4948sqrcld 11915 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  CC )
5049adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  CC )
5150, 50subnegd 9160 . . . . . . . . . . . . . . 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 ) ) ) ) )
5251breq2d 4036 . . . . . . . . . . . . . 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 ) ) ) ) ) )
5335, 36subge0d 9358 . . . . . . . . . . . . . 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 ) ) ) ) )
5452, 53bitr3d 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 ) ) ) ) )
5542, 54mpbid 201 . . . . . . . . . . . 12  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  -> 
-u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
56 ovolicc 18878 . . . . . . . . . . . 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 ) ) ) ) )
5736, 35, 55, 56syl3anc 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 ) ) ) ) )
5840, 57eqtrd 2316 . . . . . . . . . 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 ) ) ) ) )
5935, 36resubcld 9207 . . . . . . . . . 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 )
6058, 59eqeltrd 2358 . . . . . . . . 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 )
61 volf 18884 . . . . . . . . . 10  |-  vol :  dom  vol --> ( 0 [,] 
+oo )
62 ffn 5355 . . . . . . . . . 10  |-  ( vol
:  dom  vol --> ( 0 [,]  +oo )  ->  vol  Fn 
dom  vol )
63 elpreima 5607 . . . . . . . . . 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 ) ) )
6461, 62, 63mp2b 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 ) )
6538, 60, 64sylanbrc 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 ) )
66 0mbl 18893 . . . . . . . . . 10  |-  (/)  e.  dom  vol
67 mblvol 18885 . . . . . . . . . . . . 13  |-  ( (/)  e.  dom  vol  ->  ( vol `  (/) )  =  ( vol * `  (/) ) )
6866, 67ax-mp 8 . . . . . . . . . . . 12  |-  ( vol `  (/) )  =  ( vol * `  (/) )
69 ovol0 18848 . . . . . . . . . . . 12  |-  ( vol
* `  (/) )  =  0
7068, 69eqtri 2304 . . . . . . . . . . 11  |-  ( vol `  (/) )  =  0
71 0re 8834 . . . . . . . . . . 11  |-  0  e.  RR
7270, 71eqeltri 2354 . . . . . . . . . 10  |-  ( vol `  (/) )  e.  RR
73 elpreima 5607 . . . . . . . . . . 11  |-  ( vol 
Fn  dom  vol  ->  ( (/) 
e.  ( `' vol " RR )  <->  ( (/)  e.  dom  vol 
/\  ( vol `  (/) )  e.  RR ) ) )
7461, 62, 73mp2b 9 . . . . . . . . . 10  |-  ( (/)  e.  ( `' vol " RR ) 
<->  ( (/)  e.  dom  vol 
/\  ( vol `  (/) )  e.  RR ) )
7566, 72, 74mpbir2an 886 . . . . . . . . 9  |-  (/)  e.  ( `' vol " RR )
7675a1i 10 . . . . . . . 8  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  -.  ( abs `  t
)  <_  R )  -> 
(/)  e.  ( `' vol " RR ) )
7765, 76ifclda 3593 . . . . . . 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 ) )
7816, 77eqeltrd 2358 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( S " { t } )  e.  ( `' vol " RR ) )
79783expa 1151 . . . . 5  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  RR )  ->  ( S " { t } )  e.  ( `' vol " RR ) )
8079ralrimiva 2627 . . . 4  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  A. t  e.  RR  ( S " { t } )  e.  ( `' vol " RR ) )
8116fveq2d 5490 . . . . . . 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 ) ) ) ) ,  (/) ) ) )
82813expa 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 ) ) ) ) ,  (/) ) ) )
8382mpteq2dva 4107 . . . . 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 ) ) ) ) ,  (/) ) ) ) )
84 renegcl 9106 . . . . . . . 8  |-  ( R  e.  RR  ->  -u R  e.  RR )
8584adantr 451 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  -u R  e.  RR )
86 simpl 443 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  R  e.  RR )
87 iccssre 10727 . . . . . . 7  |-  ( (
-u R  e.  RR  /\  R  e.  RR )  ->  ( -u R [,] R )  C_  RR )
8885, 86, 87syl2anc 642 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( -u R [,] R
)  C_  RR )
89 rembl 18894 . . . . . . 7  |-  RR  e.  dom  vol
9089a1i 10 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  RR  e.  dom  vol )
91 fvex 5500 . . . . . . 7  |-  ( vol `  if ( ( abs `  t )  <_  R ,  ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ,  (/) ) )  e.  _V
9291a1i 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 )
93 eldif 3163 . . . . . . . . 9  |-  ( t  e.  ( RR  \ 
( -u R [,] R
) )  <->  ( t  e.  RR  /\  -.  t  e.  ( -u R [,] R ) ) )
94 3anass 938 . . . . . . . . . . . . . . 15  |-  ( ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R )  <->  ( t  e.  RR  /\  ( -u R  <_  t  /\  t  <_  R ) ) )
9594a1i 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 ) ) ) )
96843ad2ant1 976 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  -u R  e.  RR )
97 elicc2 10711 . . . . . . . . . . . . . . 15  |-  ( (
-u R  e.  RR  /\  R  e.  RR )  ->  ( t  e.  ( -u R [,] R )  <->  ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R ) ) )
9896, 13, 97syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t  e.  ( -u R [,] R )  <->  ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R ) ) )
9915, 13absled 11909 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  ( -u R  <_  t  /\  t  <_  R ) ) )
10015biantrurd 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 ) ) ) )
10295, 98, 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 )
)
10793, 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 3573 . . . . . . . . 9  |-  ( -.  ( abs `  t
)  <_  R  ->  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) )  =  (/) )
110109fveq2d 5490 . . . . . . . 8  |-  ( -.  ( abs `  t
)  <_  R  ->  ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  =  ( vol `  (/) ) )
111110, 70syl6eq 2332 . . . . . . 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 )
11385, 86, 97syl2anc 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 3572 . . . . . . . . . . . 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 5490 . . . . . . . . . . 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 ) ) ) ) ) )
123173ad2ant1 976 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( R ^ 2 )  e.  RR )
12484, 87mpancom 650 . . . . . . . . . . . . . . . . . 18  |-  ( R  e.  RR  ->  ( -u R [,] R ) 
C_  RR )
125124sselda 3181 . . . . . . . . . . . . . . . . 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 11267 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( t ^ 2 )  e.  RR )
128123, 127resubcld 9207 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( ( R ^
2 )  -  (
t ^ 2 ) )  e.  RR )
12984, 97mpancom 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 ) ) )
13131, 99, 253bitr3rd 275 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( t ^ 2 )  <_  ( R ^ 2 )  <->  ( -u R  <_  t  /\  t  <_  R ) ) )
13232, 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 11896 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
140139renegcld 9206 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  ->  -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
141140, 139, 37syl2anc 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, 39syl 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 8857 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( ( R ^
2 )  -  (
t ^ 2 ) )  e.  CC )
144143sqrcld 11915 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  CC )
145144, 144subnegd 9160 . . . . . . . . . . 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 11899 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
0  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
147139, 139, 146, 146addge0d 9344 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
0  <_  ( ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  +  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
148145breq2d 4036 . . . . . . . . . . . . . 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 9358 . . . . . . . . . . . . . 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, 56syl3anc 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 9950 . . . . . . . . . . 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 2326 . . . . . . . . . 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 2320 . . . . . . . . 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 4107 . . . . . . 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 24338 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  |->  ( 2  x.  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )  e.  L ^1 )
159157, 158eqeltrd 2358 . . . . . 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 )
16088, 90, 92, 112, 159iblss2 19156 . . . . 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 )
16183, 160eqeltrd 2358 . . . 4  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  |->  ( vol `  ( S
" { t } ) ) )  e.  L ^1 )
162 dmarea 20248 . . . 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, 80, 161, 162syl3anbrc 1136 . . 3  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  S  e.  dom area )
164 areaval 20255 . . 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 simpll 730 . . . . . 6  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  ( -u R (,) R ) )  ->  R  e.  RR )
167 simplr 731 . . . . . 6  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  ( -u R (,) R ) )  ->  0  <_  R )
168 elioore 10682 . . . . . . 7  |-  ( t  e.  ( -u R (,) R )  ->  t  e.  RR )
169168adantl 452 . . . . . 6  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  ( -u R (,) R ) )  ->  t  e.  RR )
1701, 166, 167, 169areacirclem6 24340 . . . . 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 ) ) ) ) ,  (/) ) )
171170fveq2d 5490 . . . 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 ) ) ) ) ,  (/) ) ) )
172171itgeq2dv 19132 . . 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 )
173 ioossre 10708 . . . . 5  |-  ( -u R (,) R )  C_  RR
174173a1i 10 . . . 4  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( -u R (,) R
)  C_  RR )
175 eldif 3163 . . . . . 6  |-  ( t  e.  ( RR  \ 
( -u R (,) R
) )  <->  ( t  e.  RR  /\  -.  t  e.  ( -u R (,) R ) ) )
17684rexrd 8877 . . . . . . . . . . . . . 14  |-  ( R  e.  RR  ->  -u R  e.  RR* )
177 rexr 8873 . . . . . . . . . . . . . 14  |-  ( R  e.  RR  ->  R  e.  RR* )
178 elioo2 10693 . . . . . . . . . . . . . 14  |-  ( (
-u R  e.  RR*  /\  R  e.  RR* )  ->  ( t  e.  (
-u R (,) R
)  <->  ( t  e.  RR  /\  -u R  <  t  /\  t  < 
R ) ) )
179176, 177, 178syl2anc 642 . . . . . . . . . . . . 13  |-  ( R  e.  RR  ->  (
t  e.  ( -u R (,) R )  <->  ( t  e.  RR  /\  -u R  <  t  /\  t  < 
R ) ) )
1801793ad2ant1 976 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t  e.  ( -u R (,) R )  <->  ( t  e.  RR  /\  -u R  <  t  /\  t  < 
R ) ) )
18115biantrurd 494 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( -u R  <  t  /\  t  <  R )  <-> 
( t  e.  RR  /\  ( -u R  < 
t  /\  t  <  R ) ) ) )
18215, 13absltd 11908 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <  R  <->  ( -u R  <  t  /\  t  < 
R ) ) )
183 3anass 938 . . . . . . . . . . . . . 14  |-  ( ( t  e.  RR  /\  -u R  <  t  /\  t  <  R )  <->  ( t  e.  RR  /\  ( -u R  <  t  /\  t  <  R ) ) )
184183a1i 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 ) ) ) )
185181, 182, 1843bitr4rd 277 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( t  e.  RR  /\  -u R  <  t  /\  t  <  R )  <->  ( abs `  t )  <  R
) )
186180, 185bitrd 244 . . . . . . . . . . 11  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t  e.  ( -u R (,) R )  <->  ( abs `  t )  <  R
) )
187186notbid 285 . . . . . . . . . 10  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -.  t  e.  ( -u R (,) R )  <->  -.  ( abs `  t
)  <  R )
)
18813, 28lenltd 8961 . . . . . . . . . 10  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R  <_  ( abs `  t
)  <->  -.  ( abs `  t )  <  R
) )
189187, 188bitr4d 247 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -.  t  e.  ( -u R (,) R )  <-> 
R  <_  ( abs `  t ) ) )
19016adantr 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 ) ) ) ) ,  (/) ) )
191190fveq2d 5490 . . . . . . . . . . 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 ) ) ) ) ,  (/) ) ) )
19228anim1i 551 . . . . . . . . . . . . . . . 16  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( ( abs `  t )  e.  RR  /\  ( abs `  t
)  =  R ) )
193 eqle 8919 . . . . . . . . . . . . . . . 16  |-  ( ( ( abs `  t
)  e.  RR  /\  ( abs `  t )  =  R )  -> 
( abs `  t
)  <_  R )
194192, 193, 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 ) ) ) ) ) )
195 oveq1 5827 . . . . . . . . . . . . . . . . . 18  |-  ( ( abs `  t )  =  R  ->  (
( abs `  t
) ^ 2 )  =  ( R ^
2 ) )
196195adantl 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( ( abs `  t ) ^ 2 )  =  ( R ^ 2 ) )
19724adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( ( abs `  t ) ^ 2 )  =  ( t ^ 2 ) )
198196, 197eqtr3d 2318 . . . . . . . . . . . . . . . 16  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( R ^
2 )  =  ( t ^ 2 ) )
199 oveq1 5827 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R ^ 2 )  =  ( t ^
2 )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  =  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )
200199fveq2d 5490 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R ^ 2 )  =  ( t ^
2 )  ->  ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  =  ( sqr `  (
( t ^ 2 )  -  ( t ^ 2 ) ) ) )
201200negeqd 9042 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R ^ 2 )  =  ( t ^
2 )  ->  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  = 
-u ( sqr `  (
( t ^ 2 )  -  ( t ^ 2 ) ) ) )
202201, 200oveq12d 5838 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
20319recnd 8857 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  e.  RR  ->  (
t ^ 2 )  e.  CC )
204203subidd 9141 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  e.  RR  ->  (
( t ^ 2 )  -  ( t ^ 2 ) )  =  0 )
205204fveq2d 5490 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  e.  RR  ->  ( sqr `  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )  =  ( sqr `  0
) )
206205negeqd 9042 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  e.  RR  ->  -u ( sqr `  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )  = 
-u ( sqr `  0
) )
207 sqr0 11723 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( sqr `  0 )  =  0
208207negeqi 9041 . . . . . . . . . . . . . . . . . . . . . . 23  |-  -u ( sqr `  0 )  = 
-u 0
209 neg0 9089 . . . . . . . . . . . . . . . . . . . . . . 23  |-  -u 0  =  0
210208, 209eqtri 2304 . . . . . . . . . . . . . . . . . . . . . 22  |-  -u ( sqr `  0 )  =  0
211206, 210syl6eq 2332 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  e.  RR  ->  -u ( sqr `  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )  =  0 )
212205, 207syl6eq 2332 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  e.  RR  ->  ( sqr `  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )  =  0 )
213211, 212oveq12d 5838 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  e.  RR  ->  ( -u ( sqr `  (
( t ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( t ^
2 )  -  (
t ^ 2 ) ) ) )  =  ( 0 [,] 0
) )
2142133ad2ant3 978 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -u ( sqr `  (
( t ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( t ^
2 )  -  (
t ^ 2 ) ) ) )  =  ( 0 [,] 0
) )
215202, 214sylan9eqr 2338 . . . . . . . . . . . . . . . . . 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 ) )
216215fveq2d 5490 . . . . . . . . . . . . . . . . 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 ) ) )
217 iccmbl 18919 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 0  e.  RR  /\  0  e.  RR )  ->  ( 0 [,] 0
)  e.  dom  vol )
21871, 71, 217mp2an 653 . . . . . . . . . . . . . . . . . . 19  |-  ( 0 [,] 0 )  e. 
dom  vol
219 mblvol 18885 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 0 [,] 0 )  e.  dom  vol  ->  ( vol `  ( 0 [,] 0 ) )  =  ( vol * `  ( 0 [,] 0
) ) )
220218, 219ax-mp 8 . . . . . . . . . . . . . . . . . 18  |-  ( vol `  ( 0 [,] 0
) )  =  ( vol * `  (
0 [,] 0 ) )
221 0xr 8874 . . . . . . . . . . . . . . . . . . . 20  |-  0  e.  RR*
222 iccid 10697 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 0  e.  RR*  ->  ( 0 [,] 0 )  =  { 0 } )
223222fveq2d 5490 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  e.  RR*  ->  ( vol
* `  ( 0 [,] 0 ) )  =  ( vol * `  { 0 } ) )
224221, 223ax-mp 8 . . . . . . . . . . . . . . . . . . 19  |-  ( vol
* `  ( 0 [,] 0 ) )  =  ( vol * `  { 0 } )
225 ovolsn 18850 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  e.  RR  ->  ( vol * `  { 0 } )  =  0 )
22671, 225ax-mp 8 . . . . . . . . . . . . . . . . . . 19  |-  ( vol
* `  { 0 } )  =  0
227224, 226eqtri 2304 . . . . . . . . . . . . . . . . . 18  |-  ( vol
* `  ( 0 [,] 0 ) )  =  0
228220, 227eqtri 2304 . . . . . . . . . . . . . . . . 17  |-  ( vol `  ( 0 [,] 0
) )  =  0
229216, 228syl6eq 2332 . . . . . . . . . . . . . . . 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 )
230198, 229syldan 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 )
231194, 230eqtrd 2316 . . . . . . . . . . . . . 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 )
232231ex 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 ) )
233232adantr 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 ) )
23413, 28ltnled 8962 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R  <  ( abs `  t
)  <->  -.  ( abs `  t )  <_  R
) )
235234adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( R  <  ( abs `  t )  <->  -.  ( abs `  t )  <_  R ) )
236 simpl1 958 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  ->  R  e.  RR )
23728adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( abs `  t
)  e.  RR )
238 simpr 447 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  ->  R  <_  ( abs `  t
) )
239236, 237, 238leltned 8966 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( R  <  ( abs `  t )  <->  ( abs `  t )  =/=  R
) )
240235, 239bitr3d 246 . . . . . . . . . . . . 13  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( -.  ( abs `  t )  <_  R  <->  ( abs `  t )  =/=  R ) )
241240, 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 ) )
242233, 241pm2.61dne 2524 . . . . . . . . . . 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 )
243191, 242eqtrd 2316 . . . . . . . . . 10  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( vol `  ( S " { t } ) )  =  0 )
244243ex 423 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R  <_  ( abs `  t
)  ->  ( vol `  ( S " {
t } ) )  =  0 ) )
245189, 244sylbid 206 . . . . . . . 8  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -.  t  e.  ( -u R (,) R )  ->  ( vol `  ( S " { t } ) )  =  0 ) )
2462453expia 1153 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  ->  ( -.  t  e.  ( -u R (,) R )  ->  ( vol `  ( S " { t } ) )  =  0 ) ) )
247246imp3a 420 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( ( t  e.  RR  /\  -.  t  e.  ( -u R (,) R ) )  -> 
( vol `  ( S " { t } ) )  =  0 ) )
248175, 247syl5bi 208 . . . . 5  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  ( RR  \  ( -u R (,) R ) )  ->  ( vol `  ( S " { t } ) )  =  0 ) )
249248imp 418 . . . 4  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  ( RR  \  ( -u R (,) R ) ) )  ->  ( vol `  ( S " { t } ) )  =  0 )
250174, 249itgss 19162 . . 3  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  S. ( -u R (,) R ) ( vol `  ( S " {
t } ) )  _d t  =  S. RR ( vol `  ( S " { t } ) )  _d t )
251 negeq 9040 . . . . . . . . . 10  |-  ( R  =  0  ->  -u R  =  -u 0 )
252251, 209syl6eq 2332 . . . . . . . . 9  |-  ( R  =  0  ->  -u R  =  0 )
253 id 19 . . . . . . . . 9  |-  ( R  =  0  ->  R  =  0 )
254252, 253oveq12d 5838 . . . . . . . 8  |-  ( R  =  0  ->  ( -u R (,) R )  =  ( 0 (,) 0 ) )
255 iooid 10680 . . . . . . . 8  |-  ( 0 (,) 0 )  =  (/)
256254, 255syl6eq 2332 . . . . . . 7  |-  ( R  =  0  ->  ( -u R (,) R )  =  (/) )
257256adantl 452 . . . . . 6  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  R  =  0
)  ->  ( -u R (,) R )  =  (/) )
258 itgeq1 19123 . . . . . 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 )
259257, 258syl 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 )
260 itg0 19130 . . . . . 6  |-  S. (/) ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  _d t  =  0
261 sq0 11191 . . . . . . . . . . 11  |-  ( 0 ^ 2 )  =  0
262261oveq2i 5831 . . . . . . . . . 10  |-  ( pi  x.  ( 0 ^ 2 ) )  =  ( pi  x.  0 )
263 pire 19828 . . . . . . . . . . . 12  |-  pi  e.  RR
264263recni 8845 . . . . . . . . . . 11  |-  pi  e.  CC
265264mul01i 8998 . . . . . . . . . 10  |-  ( pi  x.  0 )  =  0
266262, 265eqtr2i 2305 . . . . . . . . 9  |-  0  =  ( pi  x.  ( 0 ^ 2 ) )
267266a1i 10 . . . . . . . 8  |-  ( R  =  0  ->  0  =  ( pi  x.  ( 0 ^ 2 ) ) )
268 oveq1 5827 . . . . . . . . 9  |-  ( R  =  0  ->  ( R ^ 2 )  =  ( 0 ^ 2 ) )
269268oveq2d 5836 . . . . . . . 8  |-  ( R  =  0  ->  (
pi  x.  ( R ^ 2 ) )  =  ( pi  x.  ( 0 ^ 2 ) ) )
270267, 269eqtr4d 2319 . . . . . . 7  |-  ( R  =  0  ->  0  =  ( pi  x.  ( R ^ 2 ) ) )
271270adantl 452 . . . . . 6  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  R  =  0
)  ->  0  =  ( pi  x.  ( R ^ 2 ) ) )
272260, 271syl5eq 2328 . . . . 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 ) ) )
273259, 272eqtrd 2316 . . . 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 ) ) )
274 simp1 955 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R  /\  R  =/=  0 )  ->  R  e.  RR )
27571a1i 10 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
0  e.  RR )
276 simpr 447 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
0  <_  R )
277275, 86, 276leltned 8966 . . . . . . . 8  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( 0  <  R  <->  R  =/=  0 ) )
278277biimp3ar 1282 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R  /\  R  =/=  0 )  ->  0  <  R )
279274, 278elrpd 10384 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R  /\  R  =/=  0 )  ->  R  e.  RR+ )
2802793expa 1151 . . . . 5  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  R  =/=  0
)  ->  R  e.  RR+ )
281168, 27syl 15 . . . . . . . . . . 11  |-  ( t  e.  ( -u R (,) R )  ->  ( abs `  t )  e.  RR )
282281adantl 452 . . . . . . . . . 10  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( abs `  t
)  e.  RR )
283 rpre 10356 . . . . . . . . . . 11  |-  ( R  e.  RR+  ->  R  e.  RR )
284283adantr 451 . . . . . . . . . 10  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  ->  R  e.  RR )
285283renegcld 9206 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  -u R  e.  RR )
286285rexrd 8877 . . . . . . . . . . . . 13  |-  ( R  e.  RR+  ->  -u R  e.  RR* )
287 rpxr 10357 . . . . . . . . . . . . 13  |-  ( R  e.  RR+  ->  R  e. 
RR* )
288286, 287, 178syl2anc 642 . . . . . . . . . . . 12  |-  ( R  e.  RR+  ->  ( t  e.  ( -u R (,) R )  <->  ( t  e.  RR  /\  -u R  <  t  /\  t  < 
R ) ) )
289 simpr 447 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  t  e.  RR )
290283adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  R  e.  RR )
291289, 290absltd 11908 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( abs `  t
)  <  R  <->  ( -u R  <  t  /\  t  < 
R ) ) )
292291biimprd 214 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( -u R  <  t  /\  t  <  R )  ->  ( abs `  t
)  <  R )
)
293292exp4b 590 . . . . . . . . . . . . 13  |-  ( R  e.  RR+  ->  ( t  e.  RR  ->  ( -u R  <  t  -> 
( t  <  R  ->  ( abs `  t
)  <  R )
) ) )
2942933impd 1165 . . . . . . . . . . . 12  |-  ( R  e.  RR+  ->  ( ( t  e.  RR  /\  -u R  <  t  /\  t  <  R )  -> 
( abs `  t
)  <  R )
)
295288, 294sylbid 206 . . . . . . . . . . 11  |-  ( R  e.  RR+  ->  ( t  e.  ( -u R (,) R )  ->  ( abs `  t )  < 
R ) )
296295imp 418 . . . . . . . . . 10  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( abs `  t
)  <  R )
297282, 284, 296ltled 8963 . . . . . . . . 9  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( abs `  t
)  <_  R )
298297, 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 ) ) ) ) ) )
299283resqcld 11267 . . . . . . . . . . . . . . 15  |-  ( R  e.  RR+  ->  ( R ^ 2 )  e.  RR )
300299recnd 8857 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  ( R ^ 2 )  e.  CC )
301300adantr 451 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  ( R ^ 2 )  e.  CC )
302203adantl 452 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
t ^ 2 )  e.  CC )
303301, 302subcld 9153 . . . . . . . . . . . 12  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  e.  CC )
304303sqrcld 11915 . . . . . . . . . . 11  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  CC )
305304, 304subnegd 9160 . . . . . . . . . 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 ) ) ) ) )
306168, 305sylan2 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 ) ) ) ) )
307299adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  ( R ^ 2 )  e.  RR )
30819adantl 452 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
t ^ 2 )  e.  RR )
309307, 308resubcld 9207 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  e.  RR )
310168, 309sylan2 460 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( ( R ^
2 )  -  (
t ^ 2 ) )  e.  RR )
31171a1i 10 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  e.  RR )
31227adantl 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  ( abs `  t )  e.  RR )
31329adantl 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  0  <_  ( abs `  t
) )
314 rpge0 10362 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( R  e.  RR+  ->  0  <_  R )
315314adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  0  <_  R )
316312, 290, 313, 315lt2sqd 11275 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( abs `  t
)  <  R  <->  ( ( abs `  t ) ^
2 )  <  ( R ^ 2 ) ) )
31723adantl 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( abs `  t
) ^ 2 )  =  ( t ^
2 ) )
318317breq1d 4034 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( ( abs `  t
) ^ 2 )  <  ( R ^
2 )  <->  ( t ^ 2 )  < 
( R ^ 2 ) ) )
319316, 291, 3183bitr3rd 275 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( t ^ 2 )  <  ( R ^ 2 )  <->  ( -u R  <  t  /\  t  < 
R ) ) )
320308, 307posdifd 9355 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( t ^ 2 )  <  ( R ^ 2 )  <->  0  <  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )
321319, 320bitr3d 246 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( -u R  <  t  /\  t  <  R )  <->  0  <  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) )
322321biimpd 198 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( -u R  <  t  /\  t  <  R )  ->  0  <  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) )
323322exp4b 590 . . . . . . . . . . . . . . . . . 18  |-  ( R  e.  RR+  ->  ( t  e.  RR  ->  ( -u R  <  t  -> 
( t  <  R  ->  0  <  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) ) ) )
3243233impd 1165 . . . . . . . . . . . . . . . . 17  |-  ( R  e.  RR+  ->  ( ( t  e.  RR  /\  -u R  <  t  /\  t  <  R )  -> 
0  <  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )
325288, 324sylbid 206 . . . . . . . . . . . . . . . 16  |-  ( R  e.  RR+  ->  ( t  e.  ( -u R (,) R )  ->  0  <  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
326325imp 418 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  <  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )
327311, 310, 326ltled 8963 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )
328310, 327resqrcld 11896 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
329328renegcld 9206 . . . . . . . . . . . 12  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  ->  -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
330329, 328, 37syl2anc 642 . . . . . . . . . . 11  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )  e. 
dom  vol )
331330, 39syl 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 ) ) ) ) ) )
332310, 327sqrge0d 11899 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
333328, 328, 332, 332addge0d 9344 . . . . . . . . . . . 12  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  <_  ( ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  +  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
334306breq2d 4036 . . . . . . . . . . . . 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 ) ) ) ) ) )
335328, 329subge0d 9358 . . . . . . . . . . . . 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 ) ) ) ) )
336334, 335bitr3d 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 ) ) ) ) )
337333, 336mpbid 201 . . . . . . . . . . 11  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  ->  -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
338329, 328, 337, 56syl3anc 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 ) ) ) ) )
339331, 338eqtrd 2316 . . . . . . . . 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 ) ) ) ) )
340 ax-resscn 8790 . . . . . . . . . . . . . . 15  |-  RR  C_  CC
341340a1i 10 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  RR  C_  CC )
342285, 283, 87syl2anc 642 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  ( -u R [,] R )  C_  RR )
343 rpcn 10358 . . . . . . . . . . . . . . . . 17  |-  ( R  e.  RR+  ->  R  e.  CC )
344343sqcld 11239 . . . . . . . . . . . . . . . 16  |-  ( R  e.  RR+  ->  ( R ^ 2 )  e.  CC )
345344adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( R ^ 2 )  e.  CC )
346342sselda 3181 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  ->  u  e.  RR )
347346recnd 8857 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  ->  u  e.  CC )
348343adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  ->  R  e.  CC )
349 rpne0 10365 . . . . . . . . . . . . . . . . . . 19  |-  ( R  e.  RR+  ->  R  =/=  0 )
350349adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  ->  R  =/=  0 )
351347, 348, 350divcld 9532 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( u  /  R
)  e.  CC )
352 asincl 20165 . . . . . . . . . . . . . . . . 17  |-  ( ( u  /  R )  e.  CC  ->  (arcsin `  ( u  /  R
) )  e.  CC )
353351, 352syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
(arcsin `  ( u  /  R ) )  e.  CC )
354 ax-1cn 8791 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  CC
355354a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
1  e.  CC )
356351sqcld 11239 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( ( u  /  R ) ^ 2 )  e.  CC )
357355, 356subcld 9153 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( 1  -  (
( u  /  R
) ^ 2 ) )  e.  CC )
358357sqrcld 11915 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( sqr `  (
1  -  ( ( u  /  R ) ^ 2 ) ) )  e.  CC )
359351, 358mulcld 8851 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( ( u  /  R )  x.  ( sqr `  ( 1  -  ( ( u  /  R ) ^ 2 ) ) ) )  e.  CC )
360353, 359addcld 8850 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( (arcsin `  (
u  /  R ) )  +  ( ( u  /  R )  x.  ( sqr `  (
1  -  ( ( u  /  R ) ^ 2 ) ) ) ) )  e.  CC )
361345, 360mulcld 8851 . . . . . . . . . . . . . 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 )
362 eqid 2284 . . . . . . . . . . . . . . 15  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
363362tgioo2 18305 . . . . . . . . . . . . . 14  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
364 iccntr 18322 . . . . . . . . . . . . . . 15  |-  ( (
-u R  e.  RR  /\  R  e.  RR )  ->  ( ( int `  ( topGen `  ran  (,) )
) `  ( -u R [,] R ) )  =  ( -u R (,) R ) )
365285, 283, 364syl2anc 642 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( -u R [,] R
) )  =  (
-u R (,) R
) )
366341, 342, 361, 363, 362, 365dvmptntr 19316 . . . . . . . . . . . . 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 ) ) ) ) ) ) ) ) )
367 areacirclem2 24335 . . . . . . . . . . . . 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 ) ) ) ) ) )
368366, 367eqtrd 2316 . . . . . . . . . . . 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 ) ) )