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

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

Proof of Theorem areacirc
Dummy variables  t  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 areacirc.1 . . . . . . 7  |-  S  =  { <. x ,  y
>.  |  ( (
x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^
2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) ) }
2 df-opab 4259 . . . . . . 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 2455 . . . . . 6  |-  S  =  { u  |  E. x E. y ( u  =  <. x ,  y
>.  /\  ( ( x  e.  RR  /\  y  e.  RR )  /\  (
( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^
2 ) ) ) }
4 simpl 444 . . . . . . . . 9  |-  ( ( u  =  <. x ,  y >.  /\  (
( x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) ) )  ->  u  =  <. x ,  y >.
)
5 opelxpi 4902 . . . . . . . . . . 11  |-  ( ( x  e.  RR  /\  y  e.  RR )  -> 
<. x ,  y >.  e.  ( RR  X.  RR ) )
65adantr 452 . . . . . . . . . 10  |-  ( ( ( x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) )  ->  <. x ,  y
>.  e.  ( RR  X.  RR ) )
76adantl 453 . . . . . . . . 9  |-  ( ( u  =  <. x ,  y >.  /\  (
( x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) ) )  ->  <. x ,  y >.  e.  ( RR  X.  RR ) )
84, 7eqeltrd 2509 . . . . . . . 8  |-  ( ( u  =  <. x ,  y >.  /\  (
( x  e.  RR  /\  y  e.  RR )  /\  ( ( x ^ 2 )  +  ( y ^ 2 ) )  <_  ( R ^ 2 ) ) )  ->  u  e.  ( RR  X.  RR ) )
98exlimivv 1645 . . . . . . 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 3410 . . . . . 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 3370 . . . . 5  |-  S  C_  ( RR  X.  RR )
1211a1i 11 . . . 4  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  S  C_  ( RR  X.  RR ) )
131areacirclem6 26287 . . . . . . 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 11441 . . . . . . . . . . . . . . 15  |-  ( R  e.  RR  ->  ( R ^ 2 )  e.  RR )
15143ad2ant1 978 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R ^ 2 )  e.  RR )
16 resqcl 11441 . . . . . . . . . . . . . . 15  |-  ( t  e.  RR  ->  (
t ^ 2 )  e.  RR )
17163ad2ant3 980 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t ^ 2 )  e.  RR )
1815, 17resubcld 9457 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  e.  RR )
1918adantr 452 . . . . . . . . . . . 12  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( ( R ^
2 )  -  (
t ^ 2 ) )  e.  RR )
20 absresq 12099 . . . . . . . . . . . . . . . 16  |-  ( t  e.  RR  ->  (
( abs `  t
) ^ 2 )  =  ( t ^
2 ) )
21203ad2ant3 980 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
) ^ 2 )  =  ( t ^
2 ) )
2221breq1d 4214 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( ( abs `  t
) ^ 2 )  <_  ( R ^
2 )  <->  ( t ^ 2 )  <_ 
( R ^ 2 ) ) )
23 recn 9072 . . . . . . . . . . . . . . . . 17  |-  ( t  e.  RR  ->  t  e.  CC )
2423abscld 12230 . . . . . . . . . . . . . . . 16  |-  ( t  e.  RR  ->  ( abs `  t )  e.  RR )
25243ad2ant3 980 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( abs `  t )  e.  RR )
26 simp1 957 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  R  e.  RR )
2723absge0d 12238 . . . . . . . . . . . . . . . 16  |-  ( t  e.  RR  ->  0  <_  ( abs `  t
) )
28273ad2ant3 980 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  0  <_  ( abs `  t
) )
29 simp2 958 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  0  <_  R )
3025, 26, 28, 29le2sqd 11550 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  ( ( abs `  t ) ^
2 )  <_  ( R ^ 2 ) ) )
3115, 17subge0d 9608 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) )  <->  ( t ^ 2 )  <_ 
( R ^ 2 ) ) )
3222, 30, 313bitr4d 277 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )
3332biimpa 471 . . . . . . . . . . . 12  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )
3419, 33resqrcld 12212 . . . . . . . . . . 11  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
3534renegcld 9456 . . . . . . . . . 10  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  -> 
-u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
36 iccmbl 19452 . . . . . . . . . 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 643 . . . . . . . . 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 19418 . . . . . . . . . . . 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 16 . . . . . . . . . . 11  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( vol `  ( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )  =  ( vol * `  ( -u ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ) )
4019, 33sqrge0d 12215 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  0  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
4134, 34, 40, 40addge0d 9594 . . . . . . . . . . . . 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 9072 . . . . . . . . . . . . . . . . . . . . 21  |-  ( R  e.  RR  ->  R  e.  CC )
4342sqcld 11513 . . . . . . . . . . . . . . . . . . . 20  |-  ( R  e.  RR  ->  ( R ^ 2 )  e.  CC )
44433ad2ant1 978 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R ^ 2 )  e.  CC )
4523sqcld 11513 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  e.  RR  ->  (
t ^ 2 )  e.  CC )
46453ad2ant3 980 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t ^ 2 )  e.  CC )
4744, 46subcld 9403 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  e.  CC )
4847sqrcld 12231 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  CC )
4948adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  <_  R )  ->  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  CC )
5049, 49subnegd 9410 . . . . . . . . . . . . . . 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 4216 . . . . . . . . . . . . . 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 9608 . . . . . . . . . . . . . 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 247 . . . . . . . . . . . . 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 202 . . . . . . . . . . . 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 19411 . . . . . . . . . . . 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 1184 . . . . . . . . . . 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 2467 . . . . . . . . . 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 9457 . . . . . . . . . 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 2509 . . . . . . . . 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 19417 . . . . . . . . . 10  |-  vol : dom  vol --> ( 0 [,] 
+oo )
61 ffn 5583 . . . . . . . . . 10  |-  ( vol
: dom  vol --> ( 0 [,]  +oo )  ->  vol  Fn 
dom  vol )
62 elpreima 5842 . . . . . . . . . 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 646 . . . . . . . 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 19426 . . . . . . . . . 10  |-  (/)  e.  dom  vol
66 mblvol 19418 . . . . . . . . . . . . 13  |-  ( (/)  e.  dom  vol  ->  ( vol `  (/) )  =  ( vol * `  (/) ) )
6765, 66ax-mp 8 . . . . . . . . . . . 12  |-  ( vol `  (/) )  =  ( vol * `  (/) )
68 ovol0 19381 . . . . . . . . . . . 12  |-  ( vol
* `  (/) )  =  0
6967, 68eqtri 2455 . . . . . . . . . . 11  |-  ( vol `  (/) )  =  0
70 0re 9083 . . . . . . . . . . 11  |-  0  e.  RR
7169, 70eqeltri 2505 . . . . . . . . . 10  |-  ( vol `  (/) )  e.  RR
72 elpreima 5842 . . . . . . . . . . 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 887 . . . . . . . . 9  |-  (/)  e.  ( `' vol " RR )
7574a1i 11 . . . . . . . 8  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  -.  ( abs `  t
)  <_  R )  -> 
(/)  e.  ( `' vol " RR ) )
7664, 75ifclda 3758 . . . . . . 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 2509 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( S " { t } )  e.  ( `' vol " RR ) )
78773expa 1153 . . . . 5  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  RR )  ->  ( S " { t } )  e.  ( `' vol " RR ) )
7978ralrimiva 2781 . . . 4  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  A. t  e.  RR  ( S " { t } )  e.  ( `' vol " RR ) )
8013fveq2d 5724 . . . . . . 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 1153 . . . . . 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 4287 . . . . 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 9356 . . . . . . . 8  |-  ( R  e.  RR  ->  -u R  e.  RR )
8483adantr 452 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  -u R  e.  RR )
85 simpl 444 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  R  e.  RR )
86 iccssre 10984 . . . . . . 7  |-  ( (
-u R  e.  RR  /\  R  e.  RR )  ->  ( -u R [,] R )  C_  RR )
8784, 85, 86syl2anc 643 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( -u R [,] R
)  C_  RR )
88 rembl 19427 . . . . . . 7  |-  RR  e.  dom  vol
8988a1i 11 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  RR  e.  dom  vol )
90 fvex 5734 . . . . . . 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 3322 . . . . . . . . 9  |-  ( t  e.  ( RR  \ 
( -u R [,] R
) )  <->  ( t  e.  RR  /\  -.  t  e.  ( -u R [,] R ) ) )
93 3anass 940 . . . . . . . . . . . . . . 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 978 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  -u R  e.  RR )
96 elicc2 10967 . . . . . . . . . . . . . . 15  |-  ( (
-u R  e.  RR  /\  R  e.  RR )  ->  ( t  e.  ( -u R [,] R )  <->  ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R ) ) )
9795, 26, 96syl2anc 643 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t  e.  ( -u R [,] R )  <->  ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R ) ) )
98 simp3 959 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  t  e.  RR )
9998, 26absled 12225 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  ( -u R  <_  t  /\  t  <_  R ) ) )
10098biantrurd 495 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( -u R  <_  t  /\  t  <_  R )  <-> 
( t  e.  RR  /\  ( -u R  <_ 
t  /\  t  <_  R ) ) ) )
10199, 100bitrd 245 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  ( t  e.  RR  /\  ( -u R  <_  t  /\  t  <_  R ) ) ) )
10294, 97, 1013bitr4rd 278 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  <->  t  e.  ( -u R [,] R
) ) )
103102biimpd 199 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <_  R  ->  t  e.  ( -u R [,] R ) ) )
104103con3d 127 . . . . . . . . . . 11  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -.  t  e.  ( -u R [,] R )  ->  -.  ( abs `  t )  <_  R
) )
1051043expia 1155 . . . . . . . . . 10  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  ->  ( -.  t  e.  ( -u R [,] R )  ->  -.  ( abs `  t )  <_  R ) ) )
106105imp3a 421 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( ( t  e.  RR  /\  -.  t  e.  ( -u R [,] R ) )  ->  -.  ( abs `  t
)  <_  R )
)
10792, 106syl5bi 209 . . . . . . . 8  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  ( RR  \  ( -u R [,] R ) )  ->  -.  ( abs `  t )  <_  R
) )
108107imp 419 . . . . . . 7  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  ( RR  \  ( -u R [,] R ) ) )  ->  -.  ( abs `  t )  <_  R
)
109 iffalse 3738 . . . . . . . . 9  |-  ( -.  ( abs `  t
)  <_  R  ->  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) )  =  (/) )
110109fveq2d 5724 . . . . . . . 8  |-  ( -.  ( abs `  t
)  <_  R  ->  ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  =  ( vol `  (/) ) )
111110, 69syl6eq 2483 . . . . . . 7  |-  ( -.  ( abs `  t
)  <_  R  ->  ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  =  0 )
112108, 111syl 16 . . . . . 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 643 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  <->  ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R ) ) )
11499biimprd 215 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( -u R  <_  t  /\  t  <_  R )  ->  ( abs `  t
)  <_  R )
)
115114exp3a 426 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -u R  <_  t  ->  ( t  <_  R  ->  ( abs `  t )  <_  R ) ) )
1161153expia 1155 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  ->  ( -u R  <_ 
t  ->  ( t  <_  R  ->  ( abs `  t )  <_  R
) ) ) )
1171163impd 1167 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R )  ->  ( abs `  t )  <_  R ) )
118113, 117sylbid 207 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  ->  ( abs `  t )  <_  R
) )
1191183impia 1150 . . . . . . . . . . 11  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( abs `  t
)  <_  R )
120 iftrue 3737 . . . . . . . . . . . 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 5724 . . . . . . . . . . 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 16 . . . . . . . . . 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 978 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( R ^ 2 )  e.  RR )
12483, 86mpancom 651 . . . . . . . . . . . . . . . . . 18  |-  ( R  e.  RR  ->  ( -u R [,] R ) 
C_  RR )
125124sselda 3340 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR  /\  t  e.  ( -u R [,] R ) )  -> 
t  e.  RR )
1261253adant2 976 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
t  e.  RR )
127126resqcld 11541 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( t ^ 2 )  e.  RR )
128123, 127resubcld 9457 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( ( R ^
2 )  -  (
t ^ 2 ) )  e.  RR )
12983, 96mpancom 651 . . . . . . . . . . . . . . . . 17  |-  ( R  e.  RR  ->  (
t  e.  ( -u R [,] R )  <->  ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R ) ) )
130129adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  <->  ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R ) ) )
13130, 99, 223bitr3rd 276 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( t ^ 2 )  <_  ( R ^ 2 )  <->  ( -u R  <_  t  /\  t  <_  R ) ) )
13231, 131bitrd 245 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) )  <->  ( -u R  <_  t  /\  t  <_  R ) ) )
133132biimprd 215 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( -u R  <_  t  /\  t  <_  R )  ->  0  <_  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) )
134133exp3a 426 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -u R  <_  t  ->  ( t  <_  R  ->  0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
1351343expia 1155 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  ->  ( -u R  <_ 
t  ->  ( t  <_  R  ->  0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ) )
1361353impd 1167 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( ( t  e.  RR  /\  -u R  <_  t  /\  t  <_  R )  ->  0  <_  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
137130, 136sylbid 207 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  ->  0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )
1381373impia 1150 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )
139128, 138resqrcld 12212 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
140139renegcld 9456 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  ->  -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
141140, 139, 36syl2anc 643 . . . . . . . . . . 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 16 . . . . . . . . . 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 9106 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( ( R ^
2 )  -  (
t ^ 2 ) )  e.  CC )
144143sqrcld 12231 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  CC )
145144, 144subnegd 9410 . . . . . . . . . . 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 12215 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
0  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
147139, 139, 146, 146addge0d 9594 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  ( -u R [,] R ) )  -> 
0  <_  ( ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  +  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
148145breq2d 4216 . . . . . . . . . . . . . 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 9608 . . . . . . . . . . . . . 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 247 . . . . . . . . . . . . 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 202 . . . . . . . . . . . 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 1184 . . . . . . . . . . 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 10202 . . . . . . . . . . 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 2477 . . . . . . . . . 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 2471 . . . . . . . . 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 1153 . . . . . . . 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 4287 . . . . . . 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 26285 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  (
-u R [,] R
)  |->  ( 2  x.  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )  e.  L ^1 )
159157, 158eqeltrd 2509 . . . . . 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 19689 . . . . 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 2509 . . . 4  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  |->  ( vol `  ( S
" { t } ) ) )  e.  L ^1 )
162 dmarea 20788 . . . 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 1138 . . 3  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  S  e.  dom area )
164 areaval 20795 . . 3  |-  ( S  e.  dom area  ->  (area `  S )  =  S. RR ( vol `  ( S " { t } ) )  _d t )
165163, 164syl 16 . 2  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
(area `  S )  =  S. RR ( vol `  ( S " {
t } ) )  _d t )
166 elioore 10938 . . . . . 6  |-  ( t  e.  ( -u R (,) R )  ->  t  e.  RR )
167133expa 1153 . . . . . 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 461 . . . . 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 5724 . . . 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 19665 . . 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 10964 . . . . 5  |-  ( -u R (,) R )  C_  RR
172171a1i 11 . . . 4  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( -u R (,) R
)  C_  RR )
173 eldif 3322 . . . . . 6  |-  ( t  e.  ( RR  \ 
( -u R (,) R
) )  <->  ( t  e.  RR  /\  -.  t  e.  ( -u R (,) R ) ) )
17483rexrd 9126 . . . . . . . . . . . . . 14  |-  ( R  e.  RR  ->  -u R  e.  RR* )
175 rexr 9122 . . . . . . . . . . . . . 14  |-  ( R  e.  RR  ->  R  e.  RR* )
176 elioo2 10949 . . . . . . . . . . . . . 14  |-  ( (
-u R  e.  RR*  /\  R  e.  RR* )  ->  ( t  e.  (
-u R (,) R
)  <->  ( t  e.  RR  /\  -u R  <  t  /\  t  < 
R ) ) )
177174, 175, 176syl2anc 643 . . . . . . . . . . . . 13  |-  ( R  e.  RR  ->  (
t  e.  ( -u R (,) R )  <->  ( t  e.  RR  /\  -u R  <  t  /\  t  < 
R ) ) )
1781773ad2ant1 978 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t  e.  ( -u R (,) R )  <->  ( t  e.  RR  /\  -u R  <  t  /\  t  < 
R ) ) )
17998biantrurd 495 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( -u R  <  t  /\  t  <  R )  <-> 
( t  e.  RR  /\  ( -u R  < 
t  /\  t  <  R ) ) ) )
18098, 26absltd 12224 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( abs `  t
)  <  R  <->  ( -u R  <  t  /\  t  < 
R ) ) )
181 3anass 940 . . . . . . . . . . . . . 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 278 . . . . . . . . . . . 12  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
( t  e.  RR  /\  -u R  <  t  /\  t  <  R )  <->  ( abs `  t )  <  R
) )
184178, 183bitrd 245 . . . . . . . . . . 11  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  (
t  e.  ( -u R (,) R )  <->  ( abs `  t )  <  R
) )
185184notbid 286 . . . . . . . . . 10  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -.  t  e.  ( -u R (,) R )  <->  -.  ( abs `  t
)  <  R )
)
18626, 25lenltd 9211 . . . . . . . . . 10  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R  <_  ( abs `  t
)  <->  -.  ( abs `  t )  <  R
) )
187185, 186bitr4d 248 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -.  t  e.  ( -u R (,) R )  <-> 
R  <_  ( abs `  t ) ) )
18813adantr 452 . . . . . . . . . . . 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 5724 . . . . . . . . . . 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 552 . . . . . . . . . . . . . . . 16  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( ( abs `  t )  e.  RR  /\  ( abs `  t
)  =  R ) )
191 eqle 9168 . . . . . . . . . . . . . . . 16  |-  ( ( ( abs `  t
)  e.  RR  /\  ( abs `  t )  =  R )  -> 
( abs `  t
)  <_  R )
192190, 191, 1213syl 19 . . . . . . . . . . . . . . 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 6080 . . . . . . . . . . . . . . . . . 18  |-  ( ( abs `  t )  =  R  ->  (
( abs `  t
) ^ 2 )  =  ( R ^
2 ) )
194193adantl 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( ( abs `  t ) ^ 2 )  =  ( R ^ 2 ) )
19521adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( ( abs `  t ) ^ 2 )  =  ( t ^ 2 ) )
196194, 195eqtr3d 2469 . . . . . . . . . . . . . . . 16  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  ( abs `  t
)  =  R )  ->  ( R ^
2 )  =  ( t ^ 2 ) )
197 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R ^ 2 )  =  ( t ^
2 )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  =  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )
198197fveq2d 5724 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R ^ 2 )  =  ( t ^
2 )  ->  ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  =  ( sqr `  (
( t ^ 2 )  -  ( t ^ 2 ) ) ) )
199198negeqd 9292 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R ^ 2 )  =  ( t ^
2 )  ->  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  = 
-u ( sqr `  (
( t ^ 2 )  -  ( t ^ 2 ) ) ) )
200199, 198oveq12d 6091 . . . . . . . . . . . . . . . . . . 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 9106 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  e.  RR  ->  (
t ^ 2 )  e.  CC )
202201subidd 9391 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  e.  RR  ->  (
( t ^ 2 )  -  ( t ^ 2 ) )  =  0 )
203202fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  e.  RR  ->  ( sqr `  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )  =  ( sqr `  0
) )
204203negeqd 9292 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  e.  RR  ->  -u ( sqr `  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )  = 
-u ( sqr `  0
) )
205 sqr0 12039 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( sqr `  0 )  =  0
206205negeqi 9291 . . . . . . . . . . . . . . . . . . . . . . 23  |-  -u ( sqr `  0 )  = 
-u 0
207 neg0 9339 . . . . . . . . . . . . . . . . . . . . . . 23  |-  -u 0  =  0
208206, 207eqtri 2455 . . . . . . . . . . . . . . . . . . . . . 22  |-  -u ( sqr `  0 )  =  0
209204, 208syl6eq 2483 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  e.  RR  ->  -u ( sqr `  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )  =  0 )
210203, 205syl6eq 2483 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  e.  RR  ->  ( sqr `  ( ( t ^ 2 )  -  ( t ^ 2 ) ) )  =  0 )
211209, 210oveq12d 6091 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  e.  RR  ->  ( -u ( sqr `  (
( t ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( t ^
2 )  -  (
t ^ 2 ) ) ) )  =  ( 0 [,] 0
) )
2122113ad2ant3 980 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -u ( sqr `  (
( t ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( t ^
2 )  -  (
t ^ 2 ) ) ) )  =  ( 0 [,] 0
) )
213200, 212sylan9eqr 2489 . . . . . . . . . . . . . . . . . 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 5724 . . . . . . . . . . . . . . . . 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 19452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 0  e.  RR  /\  0  e.  RR )  ->  ( 0 [,] 0
)  e.  dom  vol )
21670, 70, 215mp2an 654 . . . . . . . . . . . . . . . . . . 19  |-  ( 0 [,] 0 )  e. 
dom  vol
217 mblvol 19418 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 0 [,] 0 )  e.  dom  vol  ->  ( vol `  ( 0 [,] 0 ) )  =  ( vol * `  ( 0 [,] 0
) ) )
218216, 217ax-mp 8 . . . . . . . . . . . . . . . . . 18  |-  ( vol `  ( 0 [,] 0
) )  =  ( vol * `  (
0 [,] 0 ) )
219 0xr 9123 . . . . . . . . . . . . . . . . . . . 20  |-  0  e.  RR*
220 iccid 10953 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 0  e.  RR*  ->  ( 0 [,] 0 )  =  { 0 } )
221220fveq2d 5724 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  e.  RR*  ->  ( vol
* `  ( 0 [,] 0 ) )  =  ( vol * `  { 0 } ) )
222219, 221ax-mp 8 . . . . . . . . . . . . . . . . . . 19  |-  ( vol
* `  ( 0 [,] 0 ) )  =  ( vol * `  { 0 } )
223 ovolsn 19383 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  e.  RR  ->  ( vol * `  { 0 } )  =  0 )
22470, 223ax-mp 8 . . . . . . . . . . . . . . . . . . 19  |-  ( vol
* `  { 0 } )  =  0
225222, 224eqtri 2455 . . . . . . . . . . . . . . . . . 18  |-  ( vol
* `  ( 0 [,] 0 ) )  =  0
226218, 225eqtri 2455 . . . . . . . . . . . . . . . . 17  |-  ( vol `  ( 0 [,] 0
) )  =  0
227214, 226syl6eq 2483 . . . . . . . . . . . . . . . 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 457 . . . . . . . . . . . . . . 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 2467 . . . . . . . . . . . . . 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 424 . . . . . . . . . . . . 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 452 . . . . . . . . . . . 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 9212 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R  <  ( abs `  t
)  <->  -.  ( abs `  t )  <_  R
) )
233232adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( R  <  ( abs `  t )  <->  -.  ( abs `  t )  <_  R ) )
234 simpl1 960 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  ->  R  e.  RR )
23525adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( abs `  t
)  e.  RR )
236 simpr 448 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  ->  R  <_  ( abs `  t
) )
237234, 235, 236leltned 9216 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( R  <  ( abs `  t )  <->  ( abs `  t )  =/=  R
) )
238233, 237bitr3d 247 . . . . . . . . . . . . 13  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( -.  ( abs `  t )  <_  R  <->  ( abs `  t )  =/=  R ) )
239238, 111syl6bir 221 . . . . . . . . . . . 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 2675 . . . . . . . . . . 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 2467 . . . . . . . . . 10  |-  ( ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  /\  R  <_  ( abs `  t ) )  -> 
( vol `  ( S " { t } ) )  =  0 )
242241ex 424 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( R  <_  ( abs `  t
)  ->  ( vol `  ( S " {
t } ) )  =  0 ) )
243187, 242sylbid 207 . . . . . . . 8  |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e.  RR )  ->  ( -.  t  e.  ( -u R (,) R )  ->  ( vol `  ( S " { t } ) )  =  0 ) )
2442433expia 1155 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  RR  ->  ( -.  t  e.  ( -u R (,) R )  ->  ( vol `  ( S " { t } ) )  =  0 ) ) )
245244imp3a 421 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( ( t  e.  RR  /\  -.  t  e.  ( -u R (,) R ) )  -> 
( vol `  ( S " { t } ) )  =  0 ) )
246173, 245syl5bi 209 . . . . 5  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( t  e.  ( RR  \  ( -u R (,) R ) )  ->  ( vol `  ( S " { t } ) )  =  0 ) )
247246imp 419 . . . 4  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  t  e.  ( RR  \  ( -u R (,) R ) ) )  ->  ( vol `  ( S " { t } ) )  =  0 )
248172, 247itgss 19695 . . 3  |-  ( ( R  e.  RR  /\  0  <_  R )  ->  S. ( -u R (,) R ) ( vol `  ( S " {
t } ) )  _d t  =  S. RR ( vol `  ( S " { t } ) )  _d t )
249 negeq 9290 . . . . . . . . . 10  |-  ( R  =  0  ->  -u R  =  -u 0 )
250249, 207syl6eq 2483 . . . . . . . . 9  |-  ( R  =  0  ->  -u R  =  0 )
251 id 20 . . . . . . . . 9  |-  ( R  =  0  ->  R  =  0 )
252250, 251oveq12d 6091 . . . . . . . 8  |-  ( R  =  0  ->  ( -u R (,) R )  =  ( 0 (,) 0 ) )
253 iooid 10936 . . . . . . . 8  |-  ( 0 (,) 0 )  =  (/)
254252, 253syl6eq 2483 . . . . . . 7  |-  ( R  =  0  ->  ( -u R (,) R )  =  (/) )
255254adantl 453 . . . . . 6  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  R  =  0
)  ->  ( -u R (,) R )  =  (/) )
256 itgeq1 19656 . . . . . 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 16 . . . . 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 19663 . . . . . 6  |-  S. (/) ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  _d t  =  0
259 oveq1 6080 . . . . . . . . 9  |-  ( R  =  0  ->  ( R ^ 2 )  =  ( 0 ^ 2 ) )
260259oveq2d 6089 . . . . . . . 8  |-  ( R  =  0  ->  (
pi  x.  ( R ^ 2 ) )  =  ( pi  x.  ( 0 ^ 2 ) ) )
261 sq0 11465 . . . . . . . . . 10  |-  ( 0 ^ 2 )  =  0
262261oveq2i 6084 . . . . . . . . 9  |-  ( pi  x.  ( 0 ^ 2 ) )  =  ( pi  x.  0 )
263 pire 20364 . . . . . . . . . . 11  |-  pi  e.  RR
264263recni 9094 . . . . . . . . . 10  |-  pi  e.  CC
265264mul01i 9248 . . . . . . . . 9  |-  ( pi  x.  0 )  =  0
266262, 265eqtr2i 2456 . . . . . . . 8  |-  0  =  ( pi  x.  ( 0 ^ 2 ) )
267260, 266syl6reqr 2486 . . . . . . 7  |-  ( R  =  0  ->  0  =  ( pi  x.  ( R ^ 2 ) ) )
268267adantl 453 . . . . . 6  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  R  =  0
)  ->  0  =  ( pi  x.  ( R ^ 2 ) ) )
269258, 268syl5eq 2479 . . . . 5  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  R  =  0
)  ->  S. (/) ( vol `  if ( ( abs `  t )  <_  R ,  ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ,  (/) ) )  _d t  =  ( pi  x.  ( R ^ 2 ) ) )
270257, 269eqtrd 2467 . . . 4  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  R  =  0
)  ->  S. ( -u R (,) R ) ( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  _d t  =  ( pi  x.  ( R ^ 2 ) ) )
271 simp1 957 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R  /\  R  =/=  0 )  ->  R  e.  RR )
27270a1i 11 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
0  e.  RR )
273 simpr 448 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
0  <_  R )
274272, 85, 273leltned 9216 . . . . . . . 8  |-  ( ( R  e.  RR  /\  0  <_  R )  -> 
( 0  <  R  <->  R  =/=  0 ) )
275274biimp3ar 1284 . . . . . . 7  |-  ( ( R  e.  RR  /\  0  <_  R  /\  R  =/=  0 )  ->  0  <  R )
276271, 275elrpd 10638 . . . . . 6  |-  ( ( R  e.  RR  /\  0  <_  R  /\  R  =/=  0 )  ->  R  e.  RR+ )
2772763expa 1153 . . . . 5  |-  ( ( ( R  e.  RR  /\  0  <_  R )  /\  R  =/=  0
)  ->  R  e.  RR+ )
278166, 24syl 16 . . . . . . . . . . 11  |-  ( t  e.  ( -u R (,) R )  ->  ( abs `  t )  e.  RR )
279278adantl 453 . . . . . . . . . 10  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( abs `  t
)  e.  RR )
280 rpre 10610 . . . . . . . . . . 11  |-  ( R  e.  RR+  ->  R  e.  RR )
281280adantr 452 . . . . . . . . . 10  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  ->  R  e.  RR )
282280renegcld 9456 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  -u R  e.  RR )
283282rexrd 9126 . . . . . . . . . . . . 13  |-  ( R  e.  RR+  ->  -u R  e.  RR* )
284 rpxr 10611 . . . . . . . . . . . . 13  |-  ( R  e.  RR+  ->  R  e. 
RR* )
285283, 284, 176syl2anc 643 . . . . . . . . . . . 12  |-  ( R  e.  RR+  ->  ( t  e.  ( -u R (,) R )  <->  ( t  e.  RR  /\  -u R  <  t  /\  t  < 
R ) ) )
286 simpr 448 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  t  e.  RR )
287280adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  R  e.  RR )
288286, 287absltd 12224 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( abs `  t
)  <  R  <->  ( -u R  <  t  /\  t  < 
R ) ) )
289288biimprd 215 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( -u R  <  t  /\  t  <  R )  ->  ( abs `  t
)  <  R )
)
290289exp4b 591 . . . . . . . . . . . . 13  |-  ( R  e.  RR+  ->  ( t  e.  RR  ->  ( -u R  <  t  -> 
( t  <  R  ->  ( abs `  t
)  <  R )
) ) )
2912903impd 1167 . . . . . . . . . . . 12  |-  ( R  e.  RR+  ->  ( ( t  e.  RR  /\  -u R  <  t  /\  t  <  R )  -> 
( abs `  t
)  <  R )
)
292285, 291sylbid 207 . . . . . . . . . . 11  |-  ( R  e.  RR+  ->  ( t  e.  ( -u R (,) R )  ->  ( abs `  t )  < 
R ) )
293292imp 419 . . . . . . . . . 10  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( abs `  t
)  <  R )
294279, 281, 293ltled 9213 . . . . . . . . 9  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( abs `  t
)  <_  R )
295294, 121syl 16 . . . . . . . 8  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( vol `  if ( ( abs `  t
)  <_  R , 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) ,  (/) ) )  =  ( vol `  ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) [,] ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ) )
296280resqcld 11541 . . . . . . . . . . . . . . 15  |-  ( R  e.  RR+  ->  ( R ^ 2 )  e.  RR )
297296recnd 9106 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  ( R ^ 2 )  e.  CC )
298297adantr 452 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  ( R ^ 2 )  e.  CC )
299201adantl 453 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
t ^ 2 )  e.  CC )
300298, 299subcld 9403 . . . . . . . . . . . 12  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  e.  CC )
301300sqrcld 12231 . . . . . . . . . . 11  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  CC )
302301, 301subnegd 9410 . . . . . . . . . 10  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )  =  ( ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) )  +  ( sqr `  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) ) )
303166, 302sylan2 461 . . . . . . . . 9  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )  =  ( ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) )  +  ( sqr `  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) ) )
304296adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  ( R ^ 2 )  e.  RR )
30516adantl 453 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
t ^ 2 )  e.  RR )
306304, 305resubcld 9457 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( R ^ 2 )  -  ( t ^ 2 ) )  e.  RR )
307166, 306sylan2 461 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( ( R ^
2 )  -  (
t ^ 2 ) )  e.  RR )
30870a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  e.  RR )
30924adantl 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  ( abs `  t )  e.  RR )
31027adantl 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  0  <_  ( abs `  t
) )
311 rpge0 10616 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( R  e.  RR+  ->  0  <_  R )
312311adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  0  <_  R )
313309, 287, 310, 312lt2sqd 11549 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( abs `  t
)  <  R  <->  ( ( abs `  t ) ^
2 )  <  ( R ^ 2 ) ) )
31420adantl 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( abs `  t
) ^ 2 )  =  ( t ^
2 ) )
315314breq1d 4214 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( ( abs `  t
) ^ 2 )  <  ( R ^
2 )  <->  ( t ^ 2 )  < 
( R ^ 2 ) ) )
316313, 288, 3153bitr3rd 276 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( t ^ 2 )  <  ( R ^ 2 )  <->  ( -u R  <  t  /\  t  < 
R ) ) )
317305, 304posdifd 9605 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( t ^ 2 )  <  ( R ^ 2 )  <->  0  <  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )
318316, 317bitr3d 247 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( -u R  <  t  /\  t  <  R )  <->  0  <  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) )
319318biimpd 199 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR+  /\  t  e.  RR )  ->  (
( -u R  <  t  /\  t  <  R )  ->  0  <  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) )
320319exp4b 591 . . . . . . . . . . . . . . . . . 18  |-  ( R  e.  RR+  ->  ( t  e.  RR  ->  ( -u R  <  t  -> 
( t  <  R  ->  0  <  ( ( R ^ 2 )  -  ( t ^
2 ) ) ) ) ) )
3213203impd 1167 . . . . . . . . . . . . . . . . 17  |-  ( R  e.  RR+  ->  ( ( t  e.  RR  /\  -u R  <  t  /\  t  <  R )  -> 
0  <  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )
322285, 321sylbid 207 . . . . . . . . . . . . . . . 16  |-  ( R  e.  RR+  ->  ( t  e.  ( -u R (,) R )  ->  0  <  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
323322imp 419 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  <  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )
324308, 307, 323ltled 9213 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  <_  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )
325307, 324resqrcld 12212 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
326325renegcld 9456 . . . . . . . . . . . 12  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  ->  -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  e.  RR )
327326, 325, 36syl2anc 643 . . . . . . . . . . 11  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )  e. 
dom  vol )
328327, 38syl 16 . . . . . . . . . 10  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( vol `  ( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )  =  ( vol * `  ( -u ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ) )
329307, 324sqrge0d 12215 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
330325, 325, 329, 329addge0d 9594 . . . . . . . . . . . 12  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
0  <_  ( ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  +  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
331303breq2d 4216 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( 0  <_  (
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )  <->  0  <_  ( ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) )  +  ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) ) ) )
332325, 326subge0d 9608 . . . . . . . . . . . . 13  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( 0  <_  (
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) )  <->  -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )
333331, 332bitr3d 247 . . . . . . . . . . . 12  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( 0  <_  (
( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  +  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )  <->  -u ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) )  <_  ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
334330, 333mpbid 202 . . . . . . . . . . 11  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  ->  -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) )  <_  ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) )
335326, 325, 334, 55syl3anc 1184 . . . . . . . . . 10  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( vol * `  ( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )  =  ( ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
336328, 335eqtrd 2467 . . . . . . . . 9  |-  ( ( R  e.  RR+  /\  t  e.  ( -u R (,) R ) )  -> 
( vol `  ( -u ( sqr `  (
( R ^ 2 )  -  ( t ^ 2 ) ) ) [,] ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) ) ) )  =  ( ( sqr `  ( ( R ^
2 )  -  (
t ^ 2 ) ) )  -  -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2 ) ) ) ) )
337 ax-resscn 9039 . . . . . . . . . . . . . . 15  |-  RR  C_  CC
338337a1i 11 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  RR  C_  CC )
339282, 280, 86syl2anc 643 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  ( -u R [,] R )  C_  RR )
340 rpcn 10612 . . . . . . . . . . . . . . . . 17  |-  ( R  e.  RR+  ->  R  e.  CC )
341340sqcld 11513 . . . . . . . . . . . . . . . 16  |-  ( R  e.  RR+  ->  ( R ^ 2 )  e.  CC )
342341adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( R ^ 2 )  e.  CC )
343339sselda 3340 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  ->  u  e.  RR )
344343recnd 9106 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  ->  u  e.  CC )
345340adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  ->  R  e.  CC )
346 rpne0 10619 . . . . . . . . . . . . . . . . . . 19  |-  ( R  e.  RR+  ->  R  =/=  0 )
347346adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  ->  R  =/=  0 )
348344, 345, 347divcld 9782 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( u  /  R
)  e.  CC )
349 asincl 20705 . . . . . . . . . . . . . . . . 17  |-  ( ( u  /  R )  e.  CC  ->  (arcsin `  ( u  /  R
) )  e.  CC )
350348, 349syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
(arcsin `  ( u  /  R ) )  e.  CC )
351 ax-1cn 9040 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  CC
352351a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
1  e.  CC )
353348sqcld 11513 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( ( u  /  R ) ^ 2 )  e.  CC )
354352, 353subcld 9403 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( 1  -  (
( u  /  R
) ^ 2 ) )  e.  CC )
355354sqrcld 12231 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( sqr `  (
1  -  ( ( u  /  R ) ^ 2 ) ) )  e.  CC )
356348, 355mulcld 9100 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( ( u  /  R )  x.  ( sqr `  ( 1  -  ( ( u  /  R ) ^ 2 ) ) ) )  e.  CC )
357350, 356addcld 9099 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( (arcsin `  (
u  /  R ) )  +  ( ( u  /  R )  x.  ( sqr `  (
1  -  ( ( u  /  R ) ^ 2 ) ) ) ) )  e.  CC )
358342, 357mulcld 9100 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RR+  /\  u  e.  ( -u R [,] R ) )  -> 
( ( R ^
2 )  x.  (
(arcsin `  ( u  /  R ) )  +  ( ( u  /  R )  x.  ( sqr `  ( 1  -  ( ( u  /  R ) ^ 2 ) ) ) ) ) )  e.  CC )
359 eqid 2435 . . . . . . . . . . . . . . 15  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
360359tgioo2 18826 . . . . . . . . . . . . . 14  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
361 iccntr 18844 . . . . . . . . . . . . . . 15  |-  ( (
-u R  e.  RR  /\  R  e.  RR )  ->  ( ( int `  ( topGen `  ran  (,) )
) `  ( -u R [,] R ) )  =  ( -u R (,) R ) )
362282, 280, 361syl2anc 643 . . . . . . . . . . . . . 14  |-  ( R  e.  RR+  ->  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( -u R [,] R
) )  =  (
-u R (,) R
) )
363338, 339, 358, 360, 359, 362dvmptntr 19849 . . . . . . . . . . . . 13  |-  ( R  e.  RR+  ->  ( RR 
_D  ( u  e.  ( -u R [,] R )  |->  ( ( R ^ 2 )  x.  ( (arcsin `  ( u  /  R
) )  +  ( ( u  /  R
)  x.  ( sqr `  ( 1  -  (
( u  /  R
) ^ 2 ) ) ) ) ) ) ) )  =  ( RR  _D  (
u  e.  ( -u R (,) R )  |->  ( ( R ^ 2 )  x.  ( (arcsin `  ( u  /  R
) )  +  ( ( u  /  R
)  x.  ( sqr `  ( 1  -  (
( u  /  R
) ^ 2 ) ) ) ) ) ) ) ) )
364 areacirclem2 26282 . . . . . . . . . . . . 13  |-  ( R  e.  RR+  ->  ( RR 
_D  ( u  e.  ( -u R (,) R )  |->  ( ( R ^ 2 )  x.  ( (arcsin `  ( u  /  R
) )  +  ( ( u  /  R
)  x.  ( sqr `  ( 1  -  (
( u  /  R
) ^ 2 ) ) ) ) ) ) ) )  =  ( u  e.  (
-u R (,) R
)  |->  ( 2  x.  ( sqr `  (
( R ^ 2 )  -  ( u ^ 2 ) ) ) ) ) )
365363, 364eqtrd 2467 . . . . . . . . . . . 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 ) ) ) )