Metamath Proof Explorer

Theorem areacirc

Description: The area of a circle of radius R is _pi x. R ^ 2 . This is Metamath 100 proof #9. (Contributed by Brendan Leahy, 31-Aug-2017) (Revised by Brendan Leahy, 22-Sep-2017) (Revised by Brendan Leahy, 11-Jul-2018)

Ref Expression
Hypothesis areacirc.1 
|- S = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) ) }
Assertion areacirc 
|- ( ( R e. RR /\ 0 <_ R ) -> ( area ` S ) = ( _pi x. ( R ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 areacirc.1 
 |-  S = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) ) }
2 opabssxp 
 |-  { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) ) } C_ ( RR X. RR )
3 1 2 eqsstri 
 |-  S C_ ( RR X. RR )
4 3 a1i 
 |-  ( ( R e. RR /\ 0 <_ R ) -> S C_ ( RR X. RR ) )
5 1 areacirclem5 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( S " { t } ) = if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) )
6 resqcl 
 |-  ( R e. RR -> ( R ^ 2 ) e. RR )
7 6 3ad2ant1 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( R ^ 2 ) e. RR )
8 resqcl 
 |-  ( t e. RR -> ( t ^ 2 ) e. RR )
9 8 3ad2ant3 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( t ^ 2 ) e. RR )
10 7 9 resubcld 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( R ^ 2 ) - ( t ^ 2 ) ) e. RR )
11 10 adantr 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( ( R ^ 2 ) - ( t ^ 2 ) ) e. RR )
12 absresq 
 |-  ( t e. RR -> ( ( abs ` t ) ^ 2 ) = ( t ^ 2 ) )
13 12 3ad2ant3 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( abs ` t ) ^ 2 ) = ( t ^ 2 ) )
14 13 breq1d 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( ( abs ` t ) ^ 2 ) <_ ( R ^ 2 ) <-> ( t ^ 2 ) <_ ( R ^ 2 ) ) )
15 recn 
 |-  ( t e. RR -> t e. CC )
16 15 abscld 
 |-  ( t e. RR -> ( abs ` t ) e. RR )
17 16 3ad2ant3 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( abs ` t ) e. RR )
18 simp1 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> R e. RR )
19 15 absge0d 
 |-  ( t e. RR -> 0 <_ ( abs ` t ) )
20 19 3ad2ant3 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> 0 <_ ( abs ` t ) )
21 simp2 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> 0 <_ R )
22 17 18 20 21 le2sqd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( abs ` t ) <_ R <-> ( ( abs ` t ) ^ 2 ) <_ ( R ^ 2 ) ) )
23 7 9 subge0d 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) <-> ( t ^ 2 ) <_ ( R ^ 2 ) ) )
24 14 22 23 3bitr4d 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( abs ` t ) <_ R <-> 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
25 24 biimpa 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) )
26 11 25 resqrtcld 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR )
27 26 renegcld 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR )
28 iccmbl 
 |-  ( ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR /\ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR ) -> ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) e. dom vol )
29 27 26 28 syl2anc 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) e. dom vol )
30 mblvol 
 |-  ( ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) e. dom vol -> ( vol ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) = ( vol* ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
31 29 30 syl 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( vol ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) = ( vol* ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
32 11 25 sqrtge0d 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> 0 <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
33 26 26 32 32 addge0d 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> 0 <_ ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) + ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
34 recn 
 |-  ( R e. RR -> R e. CC )
35 34 sqcld 
 |-  ( R e. RR -> ( R ^ 2 ) e. CC )
36 35 3ad2ant1 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( R ^ 2 ) e. CC )
37 15 sqcld 
 |-  ( t e. RR -> ( t ^ 2 ) e. CC )
38 37 3ad2ant3 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( t ^ 2 ) e. CC )
39 36 38 subcld 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( R ^ 2 ) - ( t ^ 2 ) ) e. CC )
40 39 sqrtcld 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. CC )
41 40 adantr 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. CC )
42 41 41 subnegd 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) - -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) = ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) + ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
43 42 breq2d 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( 0 <_ ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) - -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) <-> 0 <_ ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) + ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
44 26 27 subge0d 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( 0 <_ ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) - -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) <-> -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
45 43 44 bitr3d 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( 0 <_ ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) + ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) <-> -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
46 33 45 mpbid 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
47 ovolicc 
 |-  ( ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR /\ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR /\ -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) -> ( vol* ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) = ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) - -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
48 27 26 46 47 syl3anc 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( vol* ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) = ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) - -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
49 31 48 eqtrd 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( vol ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) = ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) - -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
50 26 27 resubcld 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) - -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) e. RR )
51 49 50 eqeltrd 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( vol ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) e. RR )
52 volf 
 |-  vol : dom vol --> ( 0 [,] +oo )
53 ffn 
 |-  ( vol : dom vol --> ( 0 [,] +oo ) -> vol Fn dom vol )
54 elpreima 
 |-  ( vol Fn dom vol -> ( ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) e. ( `' vol " RR ) <-> ( ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) e. dom vol /\ ( vol ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) e. RR ) ) )
55 52 53 54 mp2b 
 |-  ( ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) e. ( `' vol " RR ) <-> ( ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) e. dom vol /\ ( vol ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) e. RR ) )
56 29 51 55 sylanbrc 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) e. ( `' vol " RR ) )
57 0mbl 
 |-  (/) e. dom vol
58 mblvol 
 |-  ( (/) e. dom vol -> ( vol ` (/) ) = ( vol* ` (/) ) )
59 57 58 ax-mp 
 |-  ( vol ` (/) ) = ( vol* ` (/) )
60 ovol0 
 |-  ( vol* ` (/) ) = 0
61 59 60 eqtri 
 |-  ( vol ` (/) ) = 0
62 0re 
 |-  0 e. RR
63 61 62 eqeltri 
 |-  ( vol ` (/) ) e. RR
64 elpreima 
 |-  ( vol Fn dom vol -> ( (/) e. ( `' vol " RR ) <-> ( (/) e. dom vol /\ ( vol ` (/) ) e. RR ) ) )
65 52 53 64 mp2b 
 |-  ( (/) e. ( `' vol " RR ) <-> ( (/) e. dom vol /\ ( vol ` (/) ) e. RR ) )
66 57 63 65 mpbir2an 
 |-  (/) e. ( `' vol " RR )
67 66 a1i 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ -. ( abs ` t ) <_ R ) -> (/) e. ( `' vol " RR ) )
68 56 67 ifclda 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) e. ( `' vol " RR ) )
69 5 68 eqeltrd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( S " { t } ) e. ( `' vol " RR ) )
70 69 3expa 
 |-  ( ( ( R e. RR /\ 0 <_ R ) /\ t e. RR ) -> ( S " { t } ) e. ( `' vol " RR ) )
71 70 ralrimiva 
 |-  ( ( R e. RR /\ 0 <_ R ) -> A. t e. RR ( S " { t } ) e. ( `' vol " RR ) )
72 5 fveq2d 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( vol ` ( S " { t } ) ) = ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) )
73 72 3expa 
 |-  ( ( ( R e. RR /\ 0 <_ R ) /\ t e. RR ) -> ( vol ` ( S " { t } ) ) = ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) )
74 73 mpteq2dva 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( t e. RR |-> ( vol ` ( S " { t } ) ) ) = ( t e. RR |-> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) ) )
75 renegcl 
 |-  ( R e. RR -> -u R e. RR )
76 75 adantr 
 |-  ( ( R e. RR /\ 0 <_ R ) -> -u R e. RR )
77 simpl 
 |-  ( ( R e. RR /\ 0 <_ R ) -> R e. RR )
78 iccssre 
 |-  ( ( -u R e. RR /\ R e. RR ) -> ( -u R [,] R ) C_ RR )
79 76 77 78 syl2anc 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( -u R [,] R ) C_ RR )
80 rembl 
 |-  RR e. dom vol
81 80 a1i 
 |-  ( ( R e. RR /\ 0 <_ R ) -> RR e. dom vol )
82 fvexd 
 |-  ( ( ( R e. RR /\ 0 <_ R ) /\ t e. ( -u R [,] R ) ) -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) e. _V )
83 eldif 
 |-  ( t e. ( RR \ ( -u R [,] R ) ) <-> ( t e. RR /\ -. t e. ( -u R [,] R ) ) )
84 3anass 
 |-  ( ( t e. RR /\ -u R <_ t /\ t <_ R ) <-> ( t e. RR /\ ( -u R <_ t /\ t <_ R ) ) )
85 84 a1i 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( t e. RR /\ -u R <_ t /\ t <_ R ) <-> ( t e. RR /\ ( -u R <_ t /\ t <_ R ) ) ) )
86 75 3ad2ant1 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> -u R e. RR )
87 elicc2 
 |-  ( ( -u R e. RR /\ R e. RR ) -> ( t e. ( -u R [,] R ) <-> ( t e. RR /\ -u R <_ t /\ t <_ R ) ) )
88 86 18 87 syl2anc 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( t e. ( -u R [,] R ) <-> ( t e. RR /\ -u R <_ t /\ t <_ R ) ) )
89 simp3 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> t e. RR )
90 89 18 absled 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( abs ` t ) <_ R <-> ( -u R <_ t /\ t <_ R ) ) )
91 89 biantrurd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( -u R <_ t /\ t <_ R ) <-> ( t e. RR /\ ( -u R <_ t /\ t <_ R ) ) ) )
92 90 91 bitrd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( abs ` t ) <_ R <-> ( t e. RR /\ ( -u R <_ t /\ t <_ R ) ) ) )
93 85 88 92 3bitr4rd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( abs ` t ) <_ R <-> t e. ( -u R [,] R ) ) )
94 93 biimpd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( abs ` t ) <_ R -> t e. ( -u R [,] R ) ) )
95 94 con3d 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( -. t e. ( -u R [,] R ) -> -. ( abs ` t ) <_ R ) )
96 95 3expia 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( t e. RR -> ( -. t e. ( -u R [,] R ) -> -. ( abs ` t ) <_ R ) ) )
97 96 impd 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( ( t e. RR /\ -. t e. ( -u R [,] R ) ) -> -. ( abs ` t ) <_ R ) )
98 83 97 syl5bi 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( RR \ ( -u R [,] R ) ) -> -. ( abs ` t ) <_ R ) )
99 98 imp 
 |-  ( ( ( R e. RR /\ 0 <_ R ) /\ t e. ( RR \ ( -u R [,] R ) ) ) -> -. ( abs ` t ) <_ R )
100 iffalse 
 |-  ( -. ( abs ` t ) <_ R -> if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) = (/) )
101 100 fveq2d 
 |-  ( -. ( abs ` t ) <_ R -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) = ( vol ` (/) ) )
102 101 61 eqtrdi 
 |-  ( -. ( abs ` t ) <_ R -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) = 0 )
103 99 102 syl 
 |-  ( ( ( R e. RR /\ 0 <_ R ) /\ t e. ( RR \ ( -u R [,] R ) ) ) -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) = 0 )
104 76 77 87 syl2anc 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( -u R [,] R ) <-> ( t e. RR /\ -u R <_ t /\ t <_ R ) ) )
105 90 biimprd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( -u R <_ t /\ t <_ R ) -> ( abs ` t ) <_ R ) )
106 105 expd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( -u R <_ t -> ( t <_ R -> ( abs ` t ) <_ R ) ) )
107 106 3expia 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( t e. RR -> ( -u R <_ t -> ( t <_ R -> ( abs ` t ) <_ R ) ) ) )
108 107 3impd 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( ( t e. RR /\ -u R <_ t /\ t <_ R ) -> ( abs ` t ) <_ R ) )
109 104 108 sylbid 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( -u R [,] R ) -> ( abs ` t ) <_ R ) )
110 109 3impia 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( abs ` t ) <_ R )
111 iftrue 
 |-  ( ( abs ` t ) <_ R -> if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) = ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
112 111 fveq2d 
 |-  ( ( abs ` t ) <_ R -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) = ( vol ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
113 110 112 syl 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) = ( vol ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
114 6 3ad2ant1 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( R ^ 2 ) e. RR )
115 75 78 mpancom 
 |-  ( R e. RR -> ( -u R [,] R ) C_ RR )
116 115 sselda 
 |-  ( ( R e. RR /\ t e. ( -u R [,] R ) ) -> t e. RR )
117 116 3adant2 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> t e. RR )
118 117 resqcld 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( t ^ 2 ) e. RR )
119 114 118 resubcld 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( ( R ^ 2 ) - ( t ^ 2 ) ) e. RR )
120 75 87 mpancom 
 |-  ( R e. RR -> ( t e. ( -u R [,] R ) <-> ( t e. RR /\ -u R <_ t /\ t <_ R ) ) )
121 120 adantr 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( -u R [,] R ) <-> ( t e. RR /\ -u R <_ t /\ t <_ R ) ) )
122 22 90 14 3bitr3rd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( t ^ 2 ) <_ ( R ^ 2 ) <-> ( -u R <_ t /\ t <_ R ) ) )
123 23 122 bitrd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) <-> ( -u R <_ t /\ t <_ R ) ) )
124 123 biimprd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( -u R <_ t /\ t <_ R ) -> 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
125 124 expd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( -u R <_ t -> ( t <_ R -> 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
126 125 3expia 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( t e. RR -> ( -u R <_ t -> ( t <_ R -> 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
127 126 3impd 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( ( t e. RR /\ -u R <_ t /\ t <_ R ) -> 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
128 121 127 sylbid 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( -u R [,] R ) -> 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
129 128 3impia 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) )
130 119 129 resqrtcld 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR )
131 130 renegcld 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR )
132 131 130 28 syl2anc 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) e. dom vol )
133 132 30 syl 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( vol ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) = ( vol* ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
134 119 recnd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( ( R ^ 2 ) - ( t ^ 2 ) ) e. CC )
135 134 sqrtcld 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. CC )
136 135 135 subnegd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) - -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) = ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) + ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
137 119 129 sqrtge0d 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> 0 <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
138 130 130 137 137 addge0d 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> 0 <_ ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) + ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
139 136 breq2d 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( 0 <_ ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) - -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) <-> 0 <_ ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) + ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
140 130 131 subge0d 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( 0 <_ ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) - -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) <-> -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
141 139 140 bitr3d 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( 0 <_ ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) + ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) <-> -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
142 138 141 mpbid 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
143 131 130 142 47 syl3anc 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( vol* ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) = ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) - -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
144 135 2timesd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) = ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) + ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
145 136 143 144 3eqtr4d 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( vol* ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) = ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
146 113 133 145 3eqtrd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) = ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
147 146 3expa 
 |-  ( ( ( R e. RR /\ 0 <_ R ) /\ t e. ( -u R [,] R ) ) -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) = ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
148 147 mpteq2dva 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( -u R [,] R ) |-> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) ) = ( t e. ( -u R [,] R ) |-> ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
149 areacirclem3 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( -u R [,] R ) |-> ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) e. L^1 )
150 148 149 eqeltrd 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( -u R [,] R ) |-> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) ) e. L^1 )
151 79 81 82 103 150 iblss2 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( t e. RR |-> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) ) e. L^1 )
152 74 151 eqeltrd 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( t e. RR |-> ( vol ` ( S " { t } ) ) ) e. L^1 )
153 dmarea 
 |-  ( 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 ) )
154 4 71 152 153 syl3anbrc 
 |-  ( ( R e. RR /\ 0 <_ R ) -> S e. dom area )
155 areaval 
 |-  ( S e. dom area -> ( area ` S ) = S. RR ( vol ` ( S " { t } ) ) _d t )
156 154 155 syl 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( area ` S ) = S. RR ( vol ` ( S " { t } ) ) _d t )
157 elioore 
 |-  ( t e. ( -u R (,) R ) -> t e. RR )
158 5 3expa 
 |-  ( ( ( R e. RR /\ 0 <_ R ) /\ t e. RR ) -> ( S " { t } ) = if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) )
159 157 158 sylan2 
 |-  ( ( ( R e. RR /\ 0 <_ R ) /\ t e. ( -u R (,) R ) ) -> ( S " { t } ) = if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) )
160 159 fveq2d 
 |-  ( ( ( R e. RR /\ 0 <_ R ) /\ t e. ( -u R (,) R ) ) -> ( vol ` ( S " { t } ) ) = ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) )
161 160 itgeq2dv 
 |-  ( ( R e. RR /\ 0 <_ R ) -> S. ( -u R (,) R ) ( vol ` ( S " { t } ) ) _d t = S. ( -u R (,) R ) ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) _d t )
162 ioossre 
 |-  ( -u R (,) R ) C_ RR
163 162 a1i 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( -u R (,) R ) C_ RR )
164 eldif 
 |-  ( t e. ( RR \ ( -u R (,) R ) ) <-> ( t e. RR /\ -. t e. ( -u R (,) R ) ) )
165 75 rexrd 
 |-  ( R e. RR -> -u R e. RR* )
166 rexr 
 |-  ( R e. RR -> R e. RR* )
167 elioo2 
 |-  ( ( -u R e. RR* /\ R e. RR* ) -> ( t e. ( -u R (,) R ) <-> ( t e. RR /\ -u R < t /\ t < R ) ) )
168 165 166 167 syl2anc 
 |-  ( R e. RR -> ( t e. ( -u R (,) R ) <-> ( t e. RR /\ -u R < t /\ t < R ) ) )
169 168 3ad2ant1 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( t e. ( -u R (,) R ) <-> ( t e. RR /\ -u R < t /\ t < R ) ) )
170 89 biantrurd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( -u R < t /\ t < R ) <-> ( t e. RR /\ ( -u R < t /\ t < R ) ) ) )
171 89 18 absltd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( abs ` t ) < R <-> ( -u R < t /\ t < R ) ) )
172 3anass 
 |-  ( ( t e. RR /\ -u R < t /\ t < R ) <-> ( t e. RR /\ ( -u R < t /\ t < R ) ) )
173 172 a1i 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( t e. RR /\ -u R < t /\ t < R ) <-> ( t e. RR /\ ( -u R < t /\ t < R ) ) ) )
174 170 171 173 3bitr4rd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( t e. RR /\ -u R < t /\ t < R ) <-> ( abs ` t ) < R ) )
175 169 174 bitrd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( t e. ( -u R (,) R ) <-> ( abs ` t ) < R ) )
176 175 notbid 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( -. t e. ( -u R (,) R ) <-> -. ( abs ` t ) < R ) )
177 18 17 lenltd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( R <_ ( abs ` t ) <-> -. ( abs ` t ) < R ) )
178 176 177 bitr4d 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( -. t e. ( -u R (,) R ) <-> R <_ ( abs ` t ) ) )
179 5 adantr 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R <_ ( abs ` t ) ) -> ( S " { t } ) = if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) )
180 179 fveq2d 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R <_ ( abs ` t ) ) -> ( vol ` ( S " { t } ) ) = ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) )
181 17 anim1i 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) = R ) -> ( ( abs ` t ) e. RR /\ ( abs ` t ) = R ) )
182 eqle 
 |-  ( ( ( abs ` t ) e. RR /\ ( abs ` t ) = R ) -> ( abs ` t ) <_ R )
183 181 182 112 3syl 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) = R ) -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) = ( vol ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
184 oveq1 
 |-  ( ( abs ` t ) = R -> ( ( abs ` t ) ^ 2 ) = ( R ^ 2 ) )
185 184 adantl 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) = R ) -> ( ( abs ` t ) ^ 2 ) = ( R ^ 2 ) )
186 13 adantr 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) = R ) -> ( ( abs ` t ) ^ 2 ) = ( t ^ 2 ) )
187 185 186 eqtr3d 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) = R ) -> ( R ^ 2 ) = ( t ^ 2 ) )
188 fvoveq1 
 |-  ( ( R ^ 2 ) = ( t ^ 2 ) -> ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) = ( sqrt ` ( ( t ^ 2 ) - ( t ^ 2 ) ) ) )
189 188 negeqd 
 |-  ( ( R ^ 2 ) = ( t ^ 2 ) -> -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) = -u ( sqrt ` ( ( t ^ 2 ) - ( t ^ 2 ) ) ) )
190 189 188 oveq12d 
 |-  ( ( R ^ 2 ) = ( t ^ 2 ) -> ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) = ( -u ( sqrt ` ( ( t ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( t ^ 2 ) - ( t ^ 2 ) ) ) ) )
191 8 recnd 
 |-  ( t e. RR -> ( t ^ 2 ) e. CC )
192 191 subidd 
 |-  ( t e. RR -> ( ( t ^ 2 ) - ( t ^ 2 ) ) = 0 )
193 192 fveq2d 
 |-  ( t e. RR -> ( sqrt ` ( ( t ^ 2 ) - ( t ^ 2 ) ) ) = ( sqrt ` 0 ) )
194 193 negeqd 
 |-  ( t e. RR -> -u ( sqrt ` ( ( t ^ 2 ) - ( t ^ 2 ) ) ) = -u ( sqrt ` 0 ) )
195 sqrt0 
 |-  ( sqrt ` 0 ) = 0
196 195 negeqi 
 |-  -u ( sqrt ` 0 ) = -u 0
197 neg0 
 |-  -u 0 = 0
198 196 197 eqtri 
 |-  -u ( sqrt ` 0 ) = 0
199 194 198 eqtrdi 
 |-  ( t e. RR -> -u ( sqrt ` ( ( t ^ 2 ) - ( t ^ 2 ) ) ) = 0 )
200 193 195 eqtrdi 
 |-  ( t e. RR -> ( sqrt ` ( ( t ^ 2 ) - ( t ^ 2 ) ) ) = 0 )
201 199 200 oveq12d 
 |-  ( t e. RR -> ( -u ( sqrt ` ( ( t ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( t ^ 2 ) - ( t ^ 2 ) ) ) ) = ( 0 [,] 0 ) )
202 201 3ad2ant3 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( -u ( sqrt ` ( ( t ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( t ^ 2 ) - ( t ^ 2 ) ) ) ) = ( 0 [,] 0 ) )
203 190 202 sylan9eqr 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( R ^ 2 ) = ( t ^ 2 ) ) -> ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) = ( 0 [,] 0 ) )
204 203 fveq2d 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( R ^ 2 ) = ( t ^ 2 ) ) -> ( vol ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) = ( vol ` ( 0 [,] 0 ) ) )
205 iccmbl 
 |-  ( ( 0 e. RR /\ 0 e. RR ) -> ( 0 [,] 0 ) e. dom vol )
206 62 62 205 mp2an 
 |-  ( 0 [,] 0 ) e. dom vol
207 mblvol 
 |-  ( ( 0 [,] 0 ) e. dom vol -> ( vol ` ( 0 [,] 0 ) ) = ( vol* ` ( 0 [,] 0 ) ) )
208 206 207 ax-mp 
 |-  ( vol ` ( 0 [,] 0 ) ) = ( vol* ` ( 0 [,] 0 ) )
209 0xr 
 |-  0 e. RR*
210 iccid 
 |-  ( 0 e. RR* -> ( 0 [,] 0 ) = { 0 } )
211 210 fveq2d 
 |-  ( 0 e. RR* -> ( vol* ` ( 0 [,] 0 ) ) = ( vol* ` { 0 } ) )
212 209 211 ax-mp 
 |-  ( vol* ` ( 0 [,] 0 ) ) = ( vol* ` { 0 } )
213 ovolsn 
 |-  ( 0 e. RR -> ( vol* ` { 0 } ) = 0 )
214 62 213 ax-mp 
 |-  ( vol* ` { 0 } ) = 0
215 212 214 eqtri 
 |-  ( vol* ` ( 0 [,] 0 ) ) = 0
216 208 215 eqtri 
 |-  ( vol ` ( 0 [,] 0 ) ) = 0
217 204 216 eqtrdi 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( R ^ 2 ) = ( t ^ 2 ) ) -> ( vol ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) = 0 )
218 187 217 syldan 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) = R ) -> ( vol ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) = 0 )
219 183 218 eqtrd 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) = R ) -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) = 0 )
220 219 ex 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( abs ` t ) = R -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) = 0 ) )
221 220 adantr 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R <_ ( abs ` t ) ) -> ( ( abs ` t ) = R -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) = 0 ) )
222 18 17 ltnled 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( R < ( abs ` t ) <-> -. ( abs ` t ) <_ R ) )
223 222 adantr 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R <_ ( abs ` t ) ) -> ( R < ( abs ` t ) <-> -. ( abs ` t ) <_ R ) )
224 simpl1 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R <_ ( abs ` t ) ) -> R e. RR )
225 17 adantr 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R <_ ( abs ` t ) ) -> ( abs ` t ) e. RR )
226 simpr 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R <_ ( abs ` t ) ) -> R <_ ( abs ` t ) )
227 224 225 226 leltned 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R <_ ( abs ` t ) ) -> ( R < ( abs ` t ) <-> ( abs ` t ) =/= R ) )
228 223 227 bitr3d 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R <_ ( abs ` t ) ) -> ( -. ( abs ` t ) <_ R <-> ( abs ` t ) =/= R ) )
229 228 102 syl6bir 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R <_ ( abs ` t ) ) -> ( ( abs ` t ) =/= R -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) = 0 ) )
230 221 229 pm2.61dne 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R <_ ( abs ` t ) ) -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) = 0 )
231 180 230 eqtrd 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R <_ ( abs ` t ) ) -> ( vol ` ( S " { t } ) ) = 0 )
232 231 ex 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( R <_ ( abs ` t ) -> ( vol ` ( S " { t } ) ) = 0 ) )
233 178 232 sylbid 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( -. t e. ( -u R (,) R ) -> ( vol ` ( S " { t } ) ) = 0 ) )
234 233 3expia 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( t e. RR -> ( -. t e. ( -u R (,) R ) -> ( vol ` ( S " { t } ) ) = 0 ) ) )
235 234 impd 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( ( t e. RR /\ -. t e. ( -u R (,) R ) ) -> ( vol ` ( S " { t } ) ) = 0 ) )
236 164 235 syl5bi 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( RR \ ( -u R (,) R ) ) -> ( vol ` ( S " { t } ) ) = 0 ) )
237 236 imp 
 |-  ( ( ( R e. RR /\ 0 <_ R ) /\ t e. ( RR \ ( -u R (,) R ) ) ) -> ( vol ` ( S " { t } ) ) = 0 )
238 163 237 itgss 
 |-  ( ( R e. RR /\ 0 <_ R ) -> S. ( -u R (,) R ) ( vol ` ( S " { t } ) ) _d t = S. RR ( vol ` ( S " { t } ) ) _d t )
239 negeq 
 |-  ( R = 0 -> -u R = -u 0 )
240 239 197 eqtrdi 
 |-  ( R = 0 -> -u R = 0 )
241 id 
 |-  ( R = 0 -> R = 0 )
242 240 241 oveq12d 
 |-  ( R = 0 -> ( -u R (,) R ) = ( 0 (,) 0 ) )
243 iooid 
 |-  ( 0 (,) 0 ) = (/)
244 242 243 eqtrdi 
 |-  ( R = 0 -> ( -u R (,) R ) = (/) )
245 244 adantl 
 |-  ( ( ( R e. RR /\ 0 <_ R ) /\ R = 0 ) -> ( -u R (,) R ) = (/) )
246 itgeq1 
 |-  ( ( -u R (,) R ) = (/) -> S. ( -u R (,) R ) ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) _d t = S. (/) ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) _d t )
247 245 246 syl 
 |-  ( ( ( R e. RR /\ 0 <_ R ) /\ R = 0 ) -> S. ( -u R (,) R ) ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) _d t = S. (/) ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) _d t )
248 itg0 
 |-  S. (/) ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) _d t = 0
249 sq0 
 |-  ( 0 ^ 2 ) = 0
250 249 oveq2i 
 |-  ( _pi x. ( 0 ^ 2 ) ) = ( _pi x. 0 )
251 picn 
 |-  _pi e. CC
252 251 mul01i 
 |-  ( _pi x. 0 ) = 0
253 250 252 eqtr2i 
 |-  0 = ( _pi x. ( 0 ^ 2 ) )
254 oveq1 
 |-  ( R = 0 -> ( R ^ 2 ) = ( 0 ^ 2 ) )
255 254 oveq2d 
 |-  ( R = 0 -> ( _pi x. ( R ^ 2 ) ) = ( _pi x. ( 0 ^ 2 ) ) )
256 253 255 eqtr4id 
 |-  ( R = 0 -> 0 = ( _pi x. ( R ^ 2 ) ) )
257 256 adantl 
 |-  ( ( ( R e. RR /\ 0 <_ R ) /\ R = 0 ) -> 0 = ( _pi x. ( R ^ 2 ) ) )
258 248 257 syl5eq 
 |-  ( ( ( R e. RR /\ 0 <_ R ) /\ R = 0 ) -> S. (/) ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) _d t = ( _pi x. ( R ^ 2 ) ) )
259 247 258 eqtrd 
 |-  ( ( ( R e. RR /\ 0 <_ R ) /\ R = 0 ) -> S. ( -u R (,) R ) ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) _d t = ( _pi x. ( R ^ 2 ) ) )
260 simp1 
 |-  ( ( R e. RR /\ 0 <_ R /\ R =/= 0 ) -> R e. RR )
261 0red 
 |-  ( ( R e. RR /\ 0 <_ R ) -> 0 e. RR )
262 simpr 
 |-  ( ( R e. RR /\ 0 <_ R ) -> 0 <_ R )
263 261 77 262 leltned 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( 0 < R <-> R =/= 0 ) )
264 263 biimp3ar 
 |-  ( ( R e. RR /\ 0 <_ R /\ R =/= 0 ) -> 0 < R )
265 260 264 elrpd 
 |-  ( ( R e. RR /\ 0 <_ R /\ R =/= 0 ) -> R e. RR+ )
266 265 3expa 
 |-  ( ( ( R e. RR /\ 0 <_ R ) /\ R =/= 0 ) -> R e. RR+ )
267 157 16 syl 
 |-  ( t e. ( -u R (,) R ) -> ( abs ` t ) e. RR )
268 267 adantl 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( abs ` t ) e. RR )
269 rpre 
 |-  ( R e. RR+ -> R e. RR )
270 269 adantr 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> R e. RR )
271 269 renegcld 
 |-  ( R e. RR+ -> -u R e. RR )
272 271 rexrd 
 |-  ( R e. RR+ -> -u R e. RR* )
273 rpxr 
 |-  ( R e. RR+ -> R e. RR* )
274 272 273 167 syl2anc 
 |-  ( R e. RR+ -> ( t e. ( -u R (,) R ) <-> ( t e. RR /\ -u R < t /\ t < R ) ) )
275 simpr 
 |-  ( ( R e. RR+ /\ t e. RR ) -> t e. RR )
276 269 adantr 
 |-  ( ( R e. RR+ /\ t e. RR ) -> R e. RR )
277 275 276 absltd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) < R <-> ( -u R < t /\ t < R ) ) )
278 277 biimprd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> ( abs ` t ) < R ) )
279 278 exp4b 
 |-  ( R e. RR+ -> ( t e. RR -> ( -u R < t -> ( t < R -> ( abs ` t ) < R ) ) ) )
280 279 3impd 
 |-  ( R e. RR+ -> ( ( t e. RR /\ -u R < t /\ t < R ) -> ( abs ` t ) < R ) )
281 274 280 sylbid 
 |-  ( R e. RR+ -> ( t e. ( -u R (,) R ) -> ( abs ` t ) < R ) )
282 281 imp 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( abs ` t ) < R )
283 268 270 282 ltled 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( abs ` t ) <_ R )
284 283 112 syl 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) = ( vol ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
285 269 resqcld 
 |-  ( R e. RR+ -> ( R ^ 2 ) e. RR )
286 285 recnd 
 |-  ( R e. RR+ -> ( R ^ 2 ) e. CC )
287 286 adantr 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( R ^ 2 ) e. CC )
288 191 adantl 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( t ^ 2 ) e. CC )
289 287 288 subcld 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( R ^ 2 ) - ( t ^ 2 ) ) e. CC )
290 289 sqrtcld 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. CC )
291 290 290 subnegd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) - -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) = ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) + ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
292 157 291 sylan2 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) - -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) = ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) + ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
293 285 adantr 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( R ^ 2 ) e. RR )
294 8 adantl 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( t ^ 2 ) e. RR )
295 293 294 resubcld 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( R ^ 2 ) - ( t ^ 2 ) ) e. RR )
296 157 295 sylan2 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) - ( t ^ 2 ) ) e. RR )
297 0red 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 e. RR )
298 16 adantl 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( abs ` t ) e. RR )
299 19 adantl 
 |-  ( ( R e. RR+ /\ t e. RR ) -> 0 <_ ( abs ` t ) )
300 rpge0 
 |-  ( R e. RR+ -> 0 <_ R )
301 300 adantr 
 |-  ( ( R e. RR+ /\ t e. RR ) -> 0 <_ R )
302 298 276 299 301 lt2sqd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) < R <-> ( ( abs ` t ) ^ 2 ) < ( R ^ 2 ) ) )
303 12 adantl 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) ^ 2 ) = ( t ^ 2 ) )
304 303 breq1d 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( ( abs ` t ) ^ 2 ) < ( R ^ 2 ) <-> ( t ^ 2 ) < ( R ^ 2 ) ) )
305 302 277 304 3bitr3rd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( t ^ 2 ) < ( R ^ 2 ) <-> ( -u R < t /\ t < R ) ) )
306 294 293 posdifd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( t ^ 2 ) < ( R ^ 2 ) <-> 0 < ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
307 305 306 bitr3d 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) <-> 0 < ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
308 307 biimpd 
 |-  ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> 0 < ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
309 308 exp4b 
 |-  ( R e. RR+ -> ( t e. RR -> ( -u R < t -> ( t < R -> 0 < ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
310 309 3impd 
 |-  ( R e. RR+ -> ( ( t e. RR /\ -u R < t /\ t < R ) -> 0 < ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
311 274 310 sylbid 
 |-  ( R e. RR+ -> ( t e. ( -u R (,) R ) -> 0 < ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
312 311 imp 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 < ( ( R ^ 2 ) - ( t ^ 2 ) ) )
313 297 296 312 ltled 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) )
314 296 313 resqrtcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR )
315 314 renegcld 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR )
316 315 314 28 syl2anc 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) e. dom vol )
317 316 30 syl 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( vol ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) = ( vol* ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
318 296 313 sqrtge0d 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
319 314 314 318 318 addge0d 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 <_ ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) + ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
320 292 breq2d 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 0 <_ ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) - -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) <-> 0 <_ ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) + ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
321 314 315 subge0d 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 0 <_ ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) - -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) <-> -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
322 320 321 bitr3d 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 0 <_ ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) + ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) <-> -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
323 319 322 mpbid 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
324 315 314 323 47 syl3anc 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( vol* ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) = ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) - -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
325 317 324 eqtrd 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( vol ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) = ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) - -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
326 ax-resscn 
 |-  RR C_ CC
327 326 a1i 
 |-  ( R e. RR+ -> RR C_ CC )
328 271 269 78 syl2anc 
 |-  ( R e. RR+ -> ( -u R [,] R ) C_ RR )
329 rpcn 
 |-  ( R e. RR+ -> R e. CC )
330 329 sqcld 
 |-  ( R e. RR+ -> ( R ^ 2 ) e. CC )
331 330 adantr 
 |-  ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> ( R ^ 2 ) e. CC )
332 328 sselda 
 |-  ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> u e. RR )
333 332 recnd 
 |-  ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> u e. CC )
334 329 adantr 
 |-  ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> R e. CC )
335 rpne0 
 |-  ( R e. RR+ -> R =/= 0 )
336 335 adantr 
 |-  ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> R =/= 0 )
337 333 334 336 divcld 
 |-  ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> ( u / R ) e. CC )
338 asincl 
 |-  ( ( u / R ) e. CC -> ( arcsin ` ( u / R ) ) e. CC )
339 337 338 syl 
 |-  ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> ( arcsin ` ( u / R ) ) e. CC )
340 1cnd 
 |-  ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> 1 e. CC )
341 337 sqcld 
 |-  ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> ( ( u / R ) ^ 2 ) e. CC )
342 340 341 subcld 
 |-  ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> ( 1 - ( ( u / R ) ^ 2 ) ) e. CC )
343 342 sqrtcld 
 |-  ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) e. CC )
344 337 343 mulcld 
 |-  ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) e. CC )
345 339 344 addcld 
 |-  ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) e. CC )
346 331 345 mulcld 
 |-  ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) e. CC )
347 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
348 347 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
349 iccntr 
 |-  ( ( -u R e. RR /\ R e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( -u R [,] R ) ) = ( -u R (,) R ) )
350 271 269 349 syl2anc 
 |-  ( R e. RR+ -> ( ( int ` ( topGen ` ran (,) ) ) ` ( -u R [,] R ) ) = ( -u R (,) R ) )
351 327 328 346 348 347 350 dvmptntr 
 |-  ( R e. RR+ -> ( RR _D ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ) = ( RR _D ( u e. ( -u R (,) R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ) )
352 areacirclem1 
 |-  ( R e. RR+ -> ( RR _D ( u e. ( -u R (,) R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ) = ( u e. ( -u R (,) R ) |-> ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) ) )
353 351 352 eqtrd 
 |-  ( R e. RR+ -> ( RR _D ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ) = ( u e. ( -u R (,) R ) |-> ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) ) )
354 353 adantr 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( RR _D ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ) = ( u e. ( -u R (,) R ) |-> ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) ) )
355 oveq1 
 |-  ( u = t -> ( u ^ 2 ) = ( t ^ 2 ) )
356 355 oveq2d 
 |-  ( u = t -> ( ( R ^ 2 ) - ( u ^ 2 ) ) = ( ( R ^ 2 ) - ( t ^ 2 ) ) )
357 356 fveq2d 
 |-  ( u = t -> ( sqrt ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) = ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
358 357 oveq2d 
 |-  ( u = t -> ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) = ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
359 358 adantl 
 |-  ( ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) /\ u = t ) -> ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) = ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
360 simpr 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> t e. ( -u R (,) R ) )
361 ovexd 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) e. _V )
362 354 359 360 361 fvmptd 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( RR _D ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ) ` t ) = ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
363 157 290 sylan2 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. CC )
364 363 2timesd 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) = ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) + ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
365 362 364 eqtrd 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( RR _D ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ) ` t ) = ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) + ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
366 292 325 365 3eqtr4rd 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( RR _D ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ) ` t ) = ( vol ` ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
367 284 366 eqtr4d 
 |-  ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) = ( ( RR _D ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ) ` t ) )
368 367 itgeq2dv 
 |-  ( R e. RR+ -> S. ( -u R (,) R ) ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) _d t = S. ( -u R (,) R ) ( ( RR _D ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ) ` t ) _d t )
369 269 269 300 300 addge0d 
 |-  ( R e. RR+ -> 0 <_ ( R + R ) )
370 329 329 subnegd 
 |-  ( R e. RR+ -> ( R - -u R ) = ( R + R ) )
371 370 breq2d 
 |-  ( R e. RR+ -> ( 0 <_ ( R - -u R ) <-> 0 <_ ( R + R ) ) )
372 269 271 subge0d 
 |-  ( R e. RR+ -> ( 0 <_ ( R - -u R ) <-> -u R <_ R ) )
373 371 372 bitr3d 
 |-  ( R e. RR+ -> ( 0 <_ ( R + R ) <-> -u R <_ R ) )
374 369 373 mpbid 
 |-  ( R e. RR+ -> -u R <_ R )
375 2cn 
 |-  2 e. CC
376 162 326 sstri 
 |-  ( -u R (,) R ) C_ CC
377 ssid 
 |-  CC C_ CC
378 375 376 377 3pm3.2i 
 |-  ( 2 e. CC /\ ( -u R (,) R ) C_ CC /\ CC C_ CC )
379 cncfmptc 
 |-  ( ( 2 e. CC /\ ( -u R (,) R ) C_ CC /\ CC C_ CC ) -> ( u e. ( -u R (,) R ) |-> 2 ) e. ( ( -u R (,) R ) -cn-> CC ) )
380 378 379 mp1i 
 |-  ( R e. RR+ -> ( u e. ( -u R (,) R ) |-> 2 ) e. ( ( -u R (,) R ) -cn-> CC ) )
381 ioossicc 
 |-  ( -u R (,) R ) C_ ( -u R [,] R )
382 resmpt 
 |-  ( ( -u R (,) R ) C_ ( -u R [,] R ) -> ( ( u e. ( -u R [,] R ) |-> ( sqrt ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) |` ( -u R (,) R ) ) = ( u e. ( -u R (,) R ) |-> ( sqrt ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) )
383 381 382 ax-mp 
 |-  ( ( u e. ( -u R [,] R ) |-> ( sqrt ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) |` ( -u R (,) R ) ) = ( u e. ( -u R (,) R ) |-> ( sqrt ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) )
384 areacirclem2 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( u e. ( -u R [,] R ) |-> ( sqrt ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
385 269 300 384 syl2anc 
 |-  ( R e. RR+ -> ( u e. ( -u R [,] R ) |-> ( sqrt ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
386 rescncf 
 |-  ( ( -u R (,) R ) C_ ( -u R [,] R ) -> ( ( u e. ( -u R [,] R ) |-> ( sqrt ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) -> ( ( u e. ( -u R [,] R ) |-> ( sqrt ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) |` ( -u R (,) R ) ) e. ( ( -u R (,) R ) -cn-> CC ) ) )
387 381 385 386 mpsyl 
 |-  ( R e. RR+ -> ( ( u e. ( -u R [,] R ) |-> ( sqrt ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) |` ( -u R (,) R ) ) e. ( ( -u R (,) R ) -cn-> CC ) )
388 383 387 eqeltrrid 
 |-  ( R e. RR+ -> ( u e. ( -u R (,) R ) |-> ( sqrt ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) e. ( ( -u R (,) R ) -cn-> CC ) )
389 380 388 mulcncf 
 |-  ( R e. RR+ -> ( u e. ( -u R (,) R ) |-> ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) ) e. ( ( -u R (,) R ) -cn-> CC ) )
390 353 389 eqeltrd 
 |-  ( R e. RR+ -> ( RR _D ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ) e. ( ( -u R (,) R ) -cn-> CC ) )
391 381 a1i 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( -u R (,) R ) C_ ( -u R [,] R ) )
392 ioombl 
 |-  ( -u R (,) R ) e. dom vol
393 392 a1i 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( -u R (,) R ) e. dom vol )
394 ovexd 
 |-  ( ( ( R e. RR /\ 0 <_ R ) /\ u e. ( -u R [,] R ) ) -> ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) e. _V )
395 areacirclem3 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( u e. ( -u R [,] R ) |-> ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) ) e. L^1 )
396 391 393 394 395 iblss 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( u e. ( -u R (,) R ) |-> ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) ) e. L^1 )
397 269 300 396 syl2anc 
 |-  ( R e. RR+ -> ( u e. ( -u R (,) R ) |-> ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) ) e. L^1 )
398 353 397 eqeltrd 
 |-  ( R e. RR+ -> ( RR _D ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ) e. L^1 )
399 areacirclem4 
 |-  ( R e. RR+ -> ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
400 271 269 374 390 398 399 ftc2nc 
 |-  ( R e. RR+ -> S. ( -u R (,) R ) ( ( RR _D ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ) ` t ) _d t = ( ( ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ` R ) - ( ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ` -u R ) ) )
401 eqidd 
 |-  ( R e. RR+ -> ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) = ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) )
402 fvoveq1 
 |-  ( u = R -> ( arcsin ` ( u / R ) ) = ( arcsin ` ( R / R ) ) )
403 oveq1 
 |-  ( u = R -> ( u / R ) = ( R / R ) )
404 403 oveq1d 
 |-  ( u = R -> ( ( u / R ) ^ 2 ) = ( ( R / R ) ^ 2 ) )
405 404 oveq2d 
 |-  ( u = R -> ( 1 - ( ( u / R ) ^ 2 ) ) = ( 1 - ( ( R / R ) ^ 2 ) ) )
406 405 fveq2d 
 |-  ( u = R -> ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) = ( sqrt ` ( 1 - ( ( R / R ) ^ 2 ) ) ) )
407 403 406 oveq12d 
 |-  ( u = R -> ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) = ( ( R / R ) x. ( sqrt ` ( 1 - ( ( R / R ) ^ 2 ) ) ) ) )
408 402 407 oveq12d 
 |-  ( u = R -> ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) = ( ( arcsin ` ( R / R ) ) + ( ( R / R ) x. ( sqrt ` ( 1 - ( ( R / R ) ^ 2 ) ) ) ) ) )
409 408 oveq2d 
 |-  ( u = R -> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) = ( ( R ^ 2 ) x. ( ( arcsin ` ( R / R ) ) + ( ( R / R ) x. ( sqrt ` ( 1 - ( ( R / R ) ^ 2 ) ) ) ) ) ) )
410 409 adantl 
 |-  ( ( R e. RR+ /\ u = R ) -> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) = ( ( R ^ 2 ) x. ( ( arcsin ` ( R / R ) ) + ( ( R / R ) x. ( sqrt ` ( 1 - ( ( R / R ) ^ 2 ) ) ) ) ) ) )
411 ubicc2 
 |-  ( ( -u R e. RR* /\ R e. RR* /\ -u R <_ R ) -> R e. ( -u R [,] R ) )
412 272 273 374 411 syl3anc 
 |-  ( R e. RR+ -> R e. ( -u R [,] R ) )
413 ovexd 
 |-  ( R e. RR+ -> ( ( R ^ 2 ) x. ( ( arcsin ` ( R / R ) ) + ( ( R / R ) x. ( sqrt ` ( 1 - ( ( R / R ) ^ 2 ) ) ) ) ) ) e. _V )
414 401 410 412 413 fvmptd 
 |-  ( R e. RR+ -> ( ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ` R ) = ( ( R ^ 2 ) x. ( ( arcsin ` ( R / R ) ) + ( ( R / R ) x. ( sqrt ` ( 1 - ( ( R / R ) ^ 2 ) ) ) ) ) ) )
415 329 335 dividd 
 |-  ( R e. RR+ -> ( R / R ) = 1 )
416 415 fveq2d 
 |-  ( R e. RR+ -> ( arcsin ` ( R / R ) ) = ( arcsin ` 1 ) )
417 asin1 
 |-  ( arcsin ` 1 ) = ( _pi / 2 )
418 416 417 eqtrdi 
 |-  ( R e. RR+ -> ( arcsin ` ( R / R ) ) = ( _pi / 2 ) )
419 415 oveq1d 
 |-  ( R e. RR+ -> ( ( R / R ) ^ 2 ) = ( 1 ^ 2 ) )
420 sq1 
 |-  ( 1 ^ 2 ) = 1
421 419 420 eqtrdi 
 |-  ( R e. RR+ -> ( ( R / R ) ^ 2 ) = 1 )
422 421 oveq2d 
 |-  ( R e. RR+ -> ( 1 - ( ( R / R ) ^ 2 ) ) = ( 1 - 1 ) )
423 1cnd 
 |-  ( R e. RR+ -> 1 e. CC )
424 423 subidd 
 |-  ( R e. RR+ -> ( 1 - 1 ) = 0 )
425 422 424 eqtrd 
 |-  ( R e. RR+ -> ( 1 - ( ( R / R ) ^ 2 ) ) = 0 )
426 425 fveq2d 
 |-  ( R e. RR+ -> ( sqrt ` ( 1 - ( ( R / R ) ^ 2 ) ) ) = ( sqrt ` 0 ) )
427 426 195 eqtrdi 
 |-  ( R e. RR+ -> ( sqrt ` ( 1 - ( ( R / R ) ^ 2 ) ) ) = 0 )
428 427 oveq2d 
 |-  ( R e. RR+ -> ( ( R / R ) x. ( sqrt ` ( 1 - ( ( R / R ) ^ 2 ) ) ) ) = ( ( R / R ) x. 0 ) )
429 329 329 335 divcld 
 |-  ( R e. RR+ -> ( R / R ) e. CC )
430 429 mul01d 
 |-  ( R e. RR+ -> ( ( R / R ) x. 0 ) = 0 )
431 428 430 eqtrd 
 |-  ( R e. RR+ -> ( ( R / R ) x. ( sqrt ` ( 1 - ( ( R / R ) ^ 2 ) ) ) ) = 0 )
432 418 431 oveq12d 
 |-  ( R e. RR+ -> ( ( arcsin ` ( R / R ) ) + ( ( R / R ) x. ( sqrt ` ( 1 - ( ( R / R ) ^ 2 ) ) ) ) ) = ( ( _pi / 2 ) + 0 ) )
433 2ne0 
 |-  2 =/= 0
434 251 375 433 divcli 
 |-  ( _pi / 2 ) e. CC
435 434 a1i 
 |-  ( R e. RR+ -> ( _pi / 2 ) e. CC )
436 435 addid1d 
 |-  ( R e. RR+ -> ( ( _pi / 2 ) + 0 ) = ( _pi / 2 ) )
437 432 436 eqtrd 
 |-  ( R e. RR+ -> ( ( arcsin ` ( R / R ) ) + ( ( R / R ) x. ( sqrt ` ( 1 - ( ( R / R ) ^ 2 ) ) ) ) ) = ( _pi / 2 ) )
438 437 oveq2d 
 |-  ( R e. RR+ -> ( ( R ^ 2 ) x. ( ( arcsin ` ( R / R ) ) + ( ( R / R ) x. ( sqrt ` ( 1 - ( ( R / R ) ^ 2 ) ) ) ) ) ) = ( ( R ^ 2 ) x. ( _pi / 2 ) ) )
439 414 438 eqtrd 
 |-  ( R e. RR+ -> ( ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ` R ) = ( ( R ^ 2 ) x. ( _pi / 2 ) ) )
440 fvoveq1 
 |-  ( u = -u R -> ( arcsin ` ( u / R ) ) = ( arcsin ` ( -u R / R ) ) )
441 oveq1 
 |-  ( u = -u R -> ( u / R ) = ( -u R / R ) )
442 441 oveq1d 
 |-  ( u = -u R -> ( ( u / R ) ^ 2 ) = ( ( -u R / R ) ^ 2 ) )
443 442 oveq2d 
 |-  ( u = -u R -> ( 1 - ( ( u / R ) ^ 2 ) ) = ( 1 - ( ( -u R / R ) ^ 2 ) ) )
444 443 fveq2d 
 |-  ( u = -u R -> ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) = ( sqrt ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) )
445 441 444 oveq12d 
 |-  ( u = -u R -> ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) = ( ( -u R / R ) x. ( sqrt ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) ) )
446 440 445 oveq12d 
 |-  ( u = -u R -> ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) = ( ( arcsin ` ( -u R / R ) ) + ( ( -u R / R ) x. ( sqrt ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) ) ) )
447 446 adantl 
 |-  ( ( R e. RR+ /\ u = -u R ) -> ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) = ( ( arcsin ` ( -u R / R ) ) + ( ( -u R / R ) x. ( sqrt ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) ) ) )
448 447 oveq2d 
 |-  ( ( R e. RR+ /\ u = -u R ) -> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) = ( ( R ^ 2 ) x. ( ( arcsin ` ( -u R / R ) ) + ( ( -u R / R ) x. ( sqrt ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) ) ) ) )
449 lbicc2 
 |-  ( ( -u R e. RR* /\ R e. RR* /\ -u R <_ R ) -> -u R e. ( -u R [,] R ) )
450 272 273 374 449 syl3anc 
 |-  ( R e. RR+ -> -u R e. ( -u R [,] R ) )
451 ovexd 
 |-  ( R e. RR+ -> ( ( R ^ 2 ) x. ( ( arcsin ` ( -u R / R ) ) + ( ( -u R / R ) x. ( sqrt ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) ) ) ) e. _V )
452 401 448 450 451 fvmptd 
 |-  ( R e. RR+ -> ( ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ` -u R ) = ( ( R ^ 2 ) x. ( ( arcsin ` ( -u R / R ) ) + ( ( -u R / R ) x. ( sqrt ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) ) ) ) )
453 329 329 335 divnegd 
 |-  ( R e. RR+ -> -u ( R / R ) = ( -u R / R ) )
454 415 negeqd 
 |-  ( R e. RR+ -> -u ( R / R ) = -u 1 )
455 453 454 eqtr3d 
 |-  ( R e. RR+ -> ( -u R / R ) = -u 1 )
456 455 fveq2d 
 |-  ( R e. RR+ -> ( arcsin ` ( -u R / R ) ) = ( arcsin ` -u 1 ) )
457 ax-1cn 
 |-  1 e. CC
458 asinneg 
 |-  ( 1 e. CC -> ( arcsin ` -u 1 ) = -u ( arcsin ` 1 ) )
459 457 458 ax-mp 
 |-  ( arcsin ` -u 1 ) = -u ( arcsin ` 1 )
460 417 negeqi 
 |-  -u ( arcsin ` 1 ) = -u ( _pi / 2 )
461 459 460 eqtri 
 |-  ( arcsin ` -u 1 ) = -u ( _pi / 2 )
462 456 461 eqtrdi 
 |-  ( R e. RR+ -> ( arcsin ` ( -u R / R ) ) = -u ( _pi / 2 ) )
463 455 oveq1d 
 |-  ( R e. RR+ -> ( ( -u R / R ) ^ 2 ) = ( -u 1 ^ 2 ) )
464 neg1sqe1 
 |-  ( -u 1 ^ 2 ) = 1
465 463 464 eqtrdi 
 |-  ( R e. RR+ -> ( ( -u R / R ) ^ 2 ) = 1 )
466 465 oveq2d 
 |-  ( R e. RR+ -> ( 1 - ( ( -u R / R ) ^ 2 ) ) = ( 1 - 1 ) )
467 466 424 eqtrd 
 |-  ( R e. RR+ -> ( 1 - ( ( -u R / R ) ^ 2 ) ) = 0 )
468 467 fveq2d 
 |-  ( R e. RR+ -> ( sqrt ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) = ( sqrt ` 0 ) )
469 468 195 eqtrdi 
 |-  ( R e. RR+ -> ( sqrt ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) = 0 )
470 469 oveq2d 
 |-  ( R e. RR+ -> ( ( -u R / R ) x. ( sqrt ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) ) = ( ( -u R / R ) x. 0 ) )
471 271 recnd 
 |-  ( R e. RR+ -> -u R e. CC )
472 471 329 335 divcld 
 |-  ( R e. RR+ -> ( -u R / R ) e. CC )
473 472 mul01d 
 |-  ( R e. RR+ -> ( ( -u R / R ) x. 0 ) = 0 )
474 470 473 eqtrd 
 |-  ( R e. RR+ -> ( ( -u R / R ) x. ( sqrt ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) ) = 0 )
475 462 474 oveq12d 
 |-  ( R e. RR+ -> ( ( arcsin ` ( -u R / R ) ) + ( ( -u R / R ) x. ( sqrt ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) ) ) = ( -u ( _pi / 2 ) + 0 ) )
476 434 negcli 
 |-  -u ( _pi / 2 ) e. CC
477 476 a1i 
 |-  ( R e. RR+ -> -u ( _pi / 2 ) e. CC )
478 477 addid1d 
 |-  ( R e. RR+ -> ( -u ( _pi / 2 ) + 0 ) = -u ( _pi / 2 ) )
479 475 478 eqtrd 
 |-  ( R e. RR+ -> ( ( arcsin ` ( -u R / R ) ) + ( ( -u R / R ) x. ( sqrt ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) ) ) = -u ( _pi / 2 ) )
480 479 oveq2d 
 |-  ( R e. RR+ -> ( ( R ^ 2 ) x. ( ( arcsin ` ( -u R / R ) ) + ( ( -u R / R ) x. ( sqrt ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) ) ) ) = ( ( R ^ 2 ) x. -u ( _pi / 2 ) ) )
481 452 480 eqtrd 
 |-  ( R e. RR+ -> ( ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ` -u R ) = ( ( R ^ 2 ) x. -u ( _pi / 2 ) ) )
482 439 481 oveq12d 
 |-  ( R e. RR+ -> ( ( ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ` R ) - ( ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ` -u R ) ) = ( ( ( R ^ 2 ) x. ( _pi / 2 ) ) - ( ( R ^ 2 ) x. -u ( _pi / 2 ) ) ) )
483 434 434 subnegi 
 |-  ( ( _pi / 2 ) - -u ( _pi / 2 ) ) = ( ( _pi / 2 ) + ( _pi / 2 ) )
484 pidiv2halves 
 |-  ( ( _pi / 2 ) + ( _pi / 2 ) ) = _pi
485 483 484 eqtri 
 |-  ( ( _pi / 2 ) - -u ( _pi / 2 ) ) = _pi
486 485 a1i 
 |-  ( R e. RR+ -> ( ( _pi / 2 ) - -u ( _pi / 2 ) ) = _pi )
487 486 oveq2d 
 |-  ( R e. RR+ -> ( ( R ^ 2 ) x. ( ( _pi / 2 ) - -u ( _pi / 2 ) ) ) = ( ( R ^ 2 ) x. _pi ) )
488 330 435 477 subdid 
 |-  ( R e. RR+ -> ( ( R ^ 2 ) x. ( ( _pi / 2 ) - -u ( _pi / 2 ) ) ) = ( ( ( R ^ 2 ) x. ( _pi / 2 ) ) - ( ( R ^ 2 ) x. -u ( _pi / 2 ) ) ) )
489 251 a1i 
 |-  ( R e. RR+ -> _pi e. CC )
490 330 489 mulcomd 
 |-  ( R e. RR+ -> ( ( R ^ 2 ) x. _pi ) = ( _pi x. ( R ^ 2 ) ) )
491 487 488 490 3eqtr3d 
 |-  ( R e. RR+ -> ( ( ( R ^ 2 ) x. ( _pi / 2 ) ) - ( ( R ^ 2 ) x. -u ( _pi / 2 ) ) ) = ( _pi x. ( R ^ 2 ) ) )
492 482 491 eqtrd 
 |-  ( R e. RR+ -> ( ( ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ` R ) - ( ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( ( arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqrt ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ` -u R ) ) = ( _pi x. ( R ^ 2 ) ) )
493 368 400 492 3eqtrd 
 |-  ( R e. RR+ -> S. ( -u R (,) R ) ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) _d t = ( _pi x. ( R ^ 2 ) ) )
494 266 493 syl 
 |-  ( ( ( R e. RR /\ 0 <_ R ) /\ R =/= 0 ) -> S. ( -u R (,) R ) ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) _d t = ( _pi x. ( R ^ 2 ) ) )
495 259 494 pm2.61dane 
 |-  ( ( R e. RR /\ 0 <_ R ) -> S. ( -u R (,) R ) ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) _d t = ( _pi x. ( R ^ 2 ) ) )
496 161 238 495 3eqtr3d 
 |-  ( ( R e. RR /\ 0 <_ R ) -> S. RR ( vol ` ( S " { t } ) ) _d t = ( _pi x. ( R ^ 2 ) ) )
497 156 496 eqtrd 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( area ` S ) = ( _pi x. ( R ^ 2 ) ) )