Theorem areacirc 33505

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

Hypothesis

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

Assertion

Ref	Expression
areacirc	|- ( ( R e. RR /\ 0 <_ R ) -> (area ` S ) = ( pi x. ( R ^ 2 ) ) )

Distinct variable group:   x, y, R

Allowed substitution hints:   S( x, y)

Proof of Theorem areacirc

Dummy variables t u are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		areacirc.1	. . . . . 6 |- S = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) ) }
2		opabssxp 5193	. . . . . 6 |- { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) ) } C_ ( RR X. RR )
3	1, 2	eqsstri 3635	. . . . 5 |- S C_ ( RR X. RR )
4	3	a1i 11	. . . 4 |- ( ( R e. RR /\ 0 <_ R ) -> S C_ ( RR X. RR ) )
5	1	areacirclem5 33504	. . . . . . 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 ) ) ) ) , (/) ) )
6		resqcl 12931	. . . . . . . . . . . . . . 15 |- ( R e. RR -> ( R ^ 2 ) e. RR )
7	6	3ad2ant1 1082	. . . . . . . . . . . . . 14 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( R ^ 2 ) e. RR )
8		resqcl 12931	. . . . . . . . . . . . . . 15 |- ( t e. RR -> ( t ^ 2 ) e. RR )
9	8	3ad2ant3 1084	. . . . . . . . . . . . . 14 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( t ^ 2 ) e. RR )
10	7, 9	resubcld 10458	. . . . . . . . . . . . 13 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( R ^ 2 ) - ( t ^ 2 ) ) e. RR )
11	10	adantr 481	. . . . . . . . . . . 12 |- ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( ( R ^ 2 ) - ( t ^ 2 ) ) e. RR )
12		absresq 14042	. . . . . . . . . . . . . . . 16 |- ( t e. RR -> ( ( abs ` t ) ^ 2 ) = ( t ^ 2 ) )
13	12	3ad2ant3 1084	. . . . . . . . . . . . . . 15 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( abs ` t ) ^ 2 ) = ( t ^ 2 ) )
14	13	breq1d 4663	. . . . . . . . . . . . . 14 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( ( abs ` t ) ^ 2 ) <_ ( R ^ 2 ) <-> ( t ^ 2 ) <_ ( R ^ 2 ) ) )
15		recn 10026	. . . . . . . . . . . . . . . . 17 |- ( t e. RR -> t e. CC )
16	15	abscld 14175	. . . . . . . . . . . . . . . 16 |- ( t e. RR -> ( abs ` t ) e. RR )
17	16	3ad2ant3 1084	. . . . . . . . . . . . . . 15 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( abs ` t ) e. RR )
18		simp1 1061	. . . . . . . . . . . . . . 15 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> R e. RR )
19	15	absge0d 14183	. . . . . . . . . . . . . . . 16 |- ( t e. RR -> 0 <_ ( abs ` t ) )
20	19	3ad2ant3 1084	. . . . . . . . . . . . . . 15 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> 0 <_ ( abs ` t ) )
21		simp2 1062	. . . . . . . . . . . . . . 15 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> 0 <_ R )
22	17, 18, 20, 21	le2sqd 13044	. . . . . . . . . . . . . 14 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( abs ` t ) <_ R <-> ( ( abs ` t ) ^ 2 ) <_ ( R ^ 2 ) ) )
23	7, 9	subge0d 10617	. . . . . . . . . . . . . 14 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) <-> ( t ^ 2 ) <_ ( R ^ 2 ) ) )
24	14, 22, 23	3bitr4d 300	. . . . . . . . . . . . 13 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( abs ` t ) <_ R <-> 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
25	24	biimpa 501	. . . . . . . . . . . 12 |- ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) )
26	11, 25	resqrtcld 14156	. . . . . . . . . . 11 |- ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR )
27	26	renegcld 10457	. . . . . . . . . 10 |- ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR )
28		iccmbl 23334	. . . . . . . . . 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 )
29	27, 26, 28	syl2anc 693	. . . . . . . . 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 )
30		mblvol 23298	. . . . . . . . . . . 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 ) ) ) ) ) )
31	29, 30	syl 17	. . . . . . . . . . 11 |- ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( vol ` ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) = ( vol* ` ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
32	11, 25	sqrtge0d 14159	. . . . . . . . . . . . . 14 |- ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> 0 <_ ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
33	26, 26, 32, 32	addge0d 10603	. . . . . . . . . . . . 13 |- ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> 0 <_ ( ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) + ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
34		recn 10026	. . . . . . . . . . . . . . . . . . . . 21 |- ( R e. RR -> R e. CC )
35	34	sqcld 13006	. . . . . . . . . . . . . . . . . . . 20 |- ( R e. RR -> ( R ^ 2 ) e. CC )
36	35	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . 19 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( R ^ 2 ) e. CC )
37	15	sqcld 13006	. . . . . . . . . . . . . . . . . . . 20 |- ( t e. RR -> ( t ^ 2 ) e. CC )
38	37	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . 19 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( t ^ 2 ) e. CC )
39	36, 38	subcld 10392	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( R ^ 2 ) - ( t ^ 2 ) ) e. CC )
40	39	sqrtcld 14176	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. CC )
41	40	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. CC )
42	41, 41	subnegd 10399	. . . . . . . . . . . . . . 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 ) ) ) ) )
43	42	breq2d 4665	. . . . . . . . . . . . . 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 ) ) ) ) ) )
44	26, 27	subge0d 10617	. . . . . . . . . . . . . 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 ) ) ) ) )
45	43, 44	bitr3d 270	. . . . . . . . . . . . 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 ) ) ) ) )
46	33, 45	mpbid 222	. . . . . . . . . . . 12 |- ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
47		ovolicc 23291	. . . . . . . . . . . 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 ) ) ) ) )
48	27, 26, 46, 47	syl3anc 1326	. . . . . . . . . . 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 ) ) ) ) )
49	31, 48	eqtrd 2656	. . . . . . . . . 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 ) ) ) ) )
50	26, 27	resubcld 10458	. . . . . . . . . 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 )
51	49, 50	eqeltrd 2701	. . . . . . . . 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 )
52		volf 23297	. . . . . . . . . 10 |- vol : dom vol --> ( 0 [,] +oo )
53		ffn 6045	. . . . . . . . . 10 |- ( vol : dom vol --> ( 0 [,] +oo ) -> vol Fn dom vol )
54		elpreima 6337	. . . . . . . . . 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 ) ) )
55	52, 53, 54	mp2b 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 ) )
56	29, 51, 55	sylanbrc 698	. . . . . . . 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 ) )
57		0mbl 23307	. . . . . . . . . 10 |- (/) e. dom vol
58		mblvol 23298	. . . . . . . . . . . . 13 |- ( (/) e. dom vol -> ( vol ` (/) ) = ( vol* ` (/) ) )
59	57, 58	ax-mp 5	. . . . . . . . . . . 12 |- ( vol ` (/) ) = ( vol* ` (/) )
60		ovol0 23261	. . . . . . . . . . . 12 |- ( vol* ` (/) ) = 0
61	59, 60	eqtri 2644	. . . . . . . . . . 11 |- ( vol ` (/) ) = 0
62		0re 10040	. . . . . . . . . . 11 |- 0 e. RR
63	61, 62	eqeltri 2697	. . . . . . . . . 10 |- ( vol ` (/) ) e. RR
64		elpreima 6337	. . . . . . . . . . 11 |- ( vol Fn dom vol -> ( (/) e. ( `' vol " RR ) <-> ( (/) e. dom vol /\ ( vol ` (/) ) e. RR ) ) )
65	52, 53, 64	mp2b 10	. . . . . . . . . 10 |- ( (/) e. ( `' vol " RR ) <-> ( (/) e. dom vol /\ ( vol ` (/) ) e. RR ) )
66	57, 63, 65	mpbir2an 955	. . . . . . . . 9 |- (/) e. ( `' vol " RR )
67	66	a1i 11	. . . . . . . 8 |- ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ -. ( abs ` t ) <_ R ) -> (/) e. ( `' vol " RR ) )
68	56, 67	ifclda 4120	. . . . . . 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 ) )
69	5, 68	eqeltrd 2701	. . . . . 6 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( S " { t } ) e. ( `' vol " RR ) )
70	69	3expa 1265	. . . . 5 |- ( ( ( R e. RR /\ 0 <_ R ) /\ t e. RR ) -> ( S " { t } ) e. ( `' vol " RR ) )
71	70	ralrimiva 2966	. . . 4 |- ( ( R e. RR /\ 0 <_ R ) -> A. t e. RR ( S " { t } ) e. ( `' vol " RR ) )
72	5	fveq2d 6195	. . . . . . 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 ) ) ) ) , (/) ) ) )
73	72	3expa 1265	. . . . . 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 ) ) ) ) , (/) ) ) )
74	73	mpteq2dva 4744	. . . . 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 ) ) ) ) , (/) ) ) ) )
75		renegcl 10344	. . . . . . . 8 |- ( R e. RR -> -u R e. RR )
76	75	adantr 481	. . . . . . 7 |- ( ( R e. RR /\ 0 <_ R ) -> -u R e. RR )
77		simpl 473	. . . . . . 7 |- ( ( R e. RR /\ 0 <_ R ) -> R e. RR )
78		iccssre 12255	. . . . . . 7 |- ( ( -u R e. RR /\ R e. RR ) -> ( -u R [,] R ) C_ RR )
79	76, 77, 78	syl2anc 693	. . . . . 6 |- ( ( R e. RR /\ 0 <_ R ) -> ( -u R [,] R ) C_ RR )
80		rembl 23308	. . . . . . 7 |- RR e. dom vol
81	80	a1i 11	. . . . . 6 |- ( ( R e. RR /\ 0 <_ R ) -> RR e. dom vol )
82		fvexd 6203	. . . . . 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 )
83		eldif 3584	. . . . . . . . 9 |- ( t e. ( RR \ ( -u R [,] R ) ) <-> ( t e. RR /\ -. t e. ( -u R [,] R ) ) )
84		3anass 1042	. . . . . . . . . . . . . . 15 |- ( ( t e. RR /\ -u R <_ t /\ t <_ R ) <-> ( t e. RR /\ ( -u R <_ t /\ t <_ R ) ) )
85	84	a1i 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 ) ) ) )
86	75	3ad2ant1 1082	. . . . . . . . . . . . . . 15 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> -u R e. RR )
87		elicc2 12238	. . . . . . . . . . . . . . 15 |- ( ( -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 693	. . . . . . . . . . . . . 14 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( t e. ( -u R [,] R ) <-> ( t e. RR /\ -u R <_ t /\ t <_ R ) ) )
89		simp3 1063	. . . . . . . . . . . . . . . 16 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> t e. RR )
90	89, 18	absled 14169	. . . . . . . . . . . . . . 15 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( abs ` t ) <_ R <-> ( -u R <_ t /\ t <_ R ) ) )
91	89	biantrurd 529	. . . . . . . . . . . . . . 15 |- ( ( 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 268	. . . . . . . . . . . . . 14 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( abs ` t ) <_ R <-> ( t e. RR /\ ( -u R <_ t /\ t <_ R ) ) ) )
93	85, 88, 92	3bitr4rd 301	. . . . . . . . . . . . 13 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( abs ` t ) <_ R <-> t e. ( -u R [,] R ) ) )
94	93	biimpd 219	. . . . . . . . . . . 12 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( abs ` t ) <_ R -> t e. ( -u R [,] R ) ) )
95	94	con3d 148	. . . . . . . . . . 11 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( -. t e. ( -u R [,] R ) -> -. ( abs ` t ) <_ R ) )
96	95	3expia 1267	. . . . . . . . . 10 |- ( ( R e. RR /\ 0 <_ R ) -> ( t e. RR -> ( -. t e. ( -u R [,] R ) -> -. ( abs ` t ) <_ R ) ) )
97	96	impd 447	. . . . . . . . 9 |- ( ( R e. RR /\ 0 <_ R ) -> ( ( t e. RR /\ -. t e. ( -u R [,] R ) ) -> -. ( abs ` t ) <_ R ) )
98	83, 97	syl5bi 232	. . . . . . . 8 |- ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( RR \ ( -u R [,] R ) ) -> -. ( abs ` t ) <_ R ) )
99	98	imp 445	. . . . . . 7 |- ( ( ( R e. RR /\ 0 <_ R ) /\ t e. ( RR \ ( -u R [,] R ) ) ) -> -. ( abs ` t ) <_ R )
100		iffalse 4095	. . . . . . . . 9 |- ( -. ( abs ` t ) <_ R -> if ( ( abs ` t ) <_ R , ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) = (/) )
101	100	fveq2d 6195	. . . . . . . 8 |- ( -. ( abs ` t ) <_ R -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) = ( vol ` (/) ) )
102	101, 61	syl6eq 2672	. . . . . . 7 |- ( -. ( abs ` t ) <_ R -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) = 0 )
103	99, 102	syl 17	. . . . . 6 |- ( ( ( R e. RR /\ 0 <_ R ) /\ t e. ( RR \ ( -u R [,] R ) ) ) -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) = 0 )
104	76, 77, 87	syl2anc 693	. . . . . . . . . . . . 13 |- ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( -u R [,] R ) <-> ( t e. RR /\ -u R <_ t /\ t <_ R ) ) )
105	90	biimprd 238	. . . . . . . . . . . . . . . 16 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( -u R <_ t /\ t <_ R ) -> ( abs ` t ) <_ R ) )
106	105	expd 452	. . . . . . . . . . . . . . 15 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( -u R <_ t -> ( t <_ R -> ( abs ` t ) <_ R ) ) )
107	106	3expia 1267	. . . . . . . . . . . . . 14 |- ( ( R e. RR /\ 0 <_ R ) -> ( t e. RR -> ( -u R <_ t -> ( t <_ R -> ( abs ` t ) <_ R ) ) ) )
108	107	3impd 1281	. . . . . . . . . . . . 13 |- ( ( R e. RR /\ 0 <_ R ) -> ( ( t e. RR /\ -u R <_ t /\ t <_ R ) -> ( abs ` t ) <_ R ) )
109	104, 108	sylbid 230	. . . . . . . . . . . 12 |- ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( -u R [,] R ) -> ( abs ` t ) <_ R ) )
110	109	3impia 1261	. . . . . . . . . . 11 |- ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( abs ` t ) <_ R )
111		iftrue 4092	. . . . . . . . . . . 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 ) ) ) ) )
112	111	fveq2d 6195	. . . . . . . . . . 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 ) ) ) ) ) )
113	110, 112	syl 17	. . . . . . . . . 10 |- ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) = ( vol ` ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
114	6	3ad2ant1 1082	. . . . . . . . . . . . . . 15 |- ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( R ^ 2 ) e. RR )
115	75, 78	mpancom 703	. . . . . . . . . . . . . . . . . 18 |- ( R e. RR -> ( -u R [,] R ) C_ RR )
116	115	sselda 3603	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR /\ t e. ( -u R [,] R ) ) -> t e. RR )
117	116	3adant2 1080	. . . . . . . . . . . . . . . 16 |- ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> t e. RR )
118	117	resqcld 13035	. . . . . . . . . . . . . . 15 |- ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( t ^ 2 ) e. RR )
119	114, 118	resubcld 10458	. . . . . . . . . . . . . 14 |- ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( ( R ^ 2 ) - ( t ^ 2 ) ) e. RR )
120	75, 87	mpancom 703	. . . . . . . . . . . . . . . . 17 |- ( R e. RR -> ( t e. ( -u R [,] R ) <-> ( t e. RR /\ -u R <_ t /\ t <_ R ) ) )
121	120	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( -u R [,] R ) <-> ( t e. RR /\ -u R <_ t /\ t <_ R ) ) )
122	22, 90, 14	3bitr3rd 299	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( t ^ 2 ) <_ ( R ^ 2 ) <-> ( -u R <_ t /\ t <_ R ) ) )
123	23, 122	bitrd 268	. . . . . . . . . . . . . . . . . . . 20 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) <-> ( -u R <_ t /\ t <_ R ) ) )
124	123	biimprd 238	. . . . . . . . . . . . . . . . . . 19 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( -u R <_ t /\ t <_ R ) -> 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
125	124	expd 452	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( -u R <_ t -> ( t <_ R -> 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
126	125	3expia 1267	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR /\ 0 <_ R ) -> ( t e. RR -> ( -u R <_ t -> ( t <_ R -> 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
127	126	3impd 1281	. . . . . . . . . . . . . . . 16 |- ( ( R e. RR /\ 0 <_ R ) -> ( ( t e. RR /\ -u R <_ t /\ t <_ R ) -> 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
128	121, 127	sylbid 230	. . . . . . . . . . . . . . 15 |- ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( -u R [,] R ) -> 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
129	128	3impia 1261	. . . . . . . . . . . . . 14 |- ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) )
130	119, 129	resqrtcld 14156	. . . . . . . . . . . . 13 |- ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR )
131	130	renegcld 10457	. . . . . . . . . . . 12 |- ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR )
132	131, 130, 28	syl2anc 693	. . . . . . . . . . 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 )
133	132, 30	syl 17	. . . . . . . . . 10 |- ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( vol ` ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) = ( vol* ` ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
134	119	recnd 10068	. . . . . . . . . . . . 13 |- ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( ( R ^ 2 ) - ( t ^ 2 ) ) e. CC )
135	134	sqrtcld 14176	. . . . . . . . . . . 12 |- ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. CC )
136	135, 135	subnegd 10399	. . . . . . . . . . 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 ) ) ) ) )
137	119, 129	sqrtge0d 14159	. . . . . . . . . . . . . 14 |- ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> 0 <_ ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
138	130, 130, 137, 137	addge0d 10603	. . . . . . . . . . . . 13 |- ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> 0 <_ ( ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) + ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
139	136	breq2d 4665	. . . . . . . . . . . . . 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 ) ) ) ) ) )
140	130, 131	subge0d 10617	. . . . . . . . . . . . . 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 ) ) ) ) )
141	139, 140	bitr3d 270	. . . . . . . . . . . . 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 ) ) ) ) )
142	138, 141	mpbid 222	. . . . . . . . . . . 12 |- ( ( R e. RR /\ 0 <_ R /\ t e. ( -u R [,] R ) ) -> -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
143	131, 130, 142, 47	syl3anc 1326	. . . . . . . . . . 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 ) ) ) ) )
144	135	2timesd 11275	. . . . . . . . . . 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 ) ) ) ) )
145	136, 143, 144	3eqtr4d 2666	. . . . . . . . . 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 ) ) ) ) )
146	113, 133, 145	3eqtrd 2660	. . . . . . . . 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 ) ) ) ) )
147	146	3expa 1265	. . . . . . . 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 ) ) ) ) )
148	147	mpteq2dva 4744	. . . . . . 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 ) ) ) ) ) )
149		areacirclem3 33502	. . . . . . 7 |- ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( -u R [,] R ) |-> ( 2 x. ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) e. L^1 )
150	148, 149	eqeltrd 2701	. . . . . 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 )
151	79, 81, 82, 103, 150	iblss2 23572	. . . . 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 )
152	74, 151	eqeltrd 2701	. . . 4 |- ( ( R e. RR /\ 0 <_ R ) -> ( t e. RR |-> ( vol ` ( S " { t } ) ) ) e. L^1 )
153		dmarea 24684	. . . 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 ) )
154	4, 71, 152, 153	syl3anbrc 1246	. . 3 |- ( ( R e. RR /\ 0 <_ R ) -> S e. dom area )
155		areaval 24691	. . 3 |- ( S e. dom area -> (area ` S ) = S. RR ( vol ` ( S " { t } ) ) _d t )
156	154, 155	syl 17	. 2 |- ( ( R e. RR /\ 0 <_ R ) -> (area ` S ) = S. RR ( vol ` ( S " { t } ) ) _d t )
157		elioore 12205	. . . . . 6 |- ( t e. ( -u R (,) R ) -> t e. RR )
158	5	3expa 1265	. . . . . 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 ) ) ) ) , (/) ) )
159	157, 158	sylan2 491	. . . . 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 ) ) ) ) , (/) ) )
160	159	fveq2d 6195	. . . 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 ) ) ) ) , (/) ) ) )
161	160	itgeq2dv 23548	. . 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 )
162		ioossre 12235	. . . . 5 |- ( -u R (,) R ) C_ RR
163	162	a1i 11	. . . 4 |- ( ( R e. RR /\ 0 <_ R ) -> ( -u R (,) R ) C_ RR )
164		eldif 3584	. . . . . 6 |- ( t e. ( RR \ ( -u R (,) R ) ) <-> ( t e. RR /\ -. t e. ( -u R (,) R ) ) )
165	75	rexrd 10089	. . . . . . . . . . . . . 14 |- ( R e. RR -> -u R e. RR* )
166		rexr 10085	. . . . . . . . . . . . . 14 |- ( R e. RR -> R e. RR* )
167		elioo2 12216	. . . . . . . . . . . . . 14 |- ( ( -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 693	. . . . . . . . . . . . 13 |- ( R e. RR -> ( t e. ( -u R (,) R ) <-> ( t e. RR /\ -u R < t /\ t < R ) ) )
169	168	3ad2ant1 1082	. . . . . . . . . . . 12 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( t e. ( -u R (,) R ) <-> ( t e. RR /\ -u R < t /\ t < R ) ) )
170	89	biantrurd 529	. . . . . . . . . . . . 13 |- ( ( 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 14168	. . . . . . . . . . . . 13 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( abs ` t ) < R <-> ( -u R < t /\ t < R ) ) )
172		3anass 1042	. . . . . . . . . . . . . 14 |- ( ( t e. RR /\ -u R < t /\ t < R ) <-> ( t e. RR /\ ( -u R < t /\ t < R ) ) )
173	172	a1i 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 ) ) ) )
174	170, 171, 173	3bitr4rd 301	. . . . . . . . . . . 12 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( t e. RR /\ -u R < t /\ t < R ) <-> ( abs ` t ) < R ) )
175	169, 174	bitrd 268	. . . . . . . . . . 11 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( t e. ( -u R (,) R ) <-> ( abs ` t ) < R ) )
176	175	notbid 308	. . . . . . . . . 10 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( -. t e. ( -u R (,) R ) <-> -. ( abs ` t ) < R ) )
177	18, 17	lenltd 10183	. . . . . . . . . 10 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( R <_ ( abs ` t ) <-> -. ( abs ` t ) < R ) )
178	176, 177	bitr4d 271	. . . . . . . . 9 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( -. t e. ( -u R (,) R ) <-> R <_ ( abs ` t ) ) )
179	5	adantr 481	. . . . . . . . . . . 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 ) ) ) ) , (/) ) )
180	179	fveq2d 6195	. . . . . . . . . . 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 ) ) ) ) , (/) ) ) )
181	17	anim1i 592	. . . . . . . . . . . . . . . 16 |- ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) = R ) -> ( ( abs ` t ) e. RR /\ ( abs ` t ) = R ) )
182		eqle 10139	. . . . . . . . . . . . . . . 16 |- ( ( ( abs ` t ) e. RR /\ ( abs ` t ) = R ) -> ( abs ` t ) <_ R )
183	181, 182, 112	3syl 18	. . . . . . . . . . . . . . 15 |- ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) = R ) -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) = ( vol ` ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
184		oveq1 6657	. . . . . . . . . . . . . . . . . 18 |- ( ( abs ` t ) = R -> ( ( abs ` t ) ^ 2 ) = ( R ^ 2 ) )
185	184	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) = R ) -> ( ( abs ` t ) ^ 2 ) = ( R ^ 2 ) )
186	13	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) = R ) -> ( ( abs ` t ) ^ 2 ) = ( t ^ 2 ) )
187	185, 186	eqtr3d 2658	. . . . . . . . . . . . . . . 16 |- ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) = R ) -> ( R ^ 2 ) = ( t ^ 2 ) )
188		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( R ^ 2 ) = ( t ^ 2 ) -> ( ( R ^ 2 ) - ( t ^ 2 ) ) = ( ( t ^ 2 ) - ( t ^ 2 ) ) )
189	188	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( R ^ 2 ) = ( t ^ 2 ) -> ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) = ( sqr ` ( ( t ^ 2 ) - ( t ^ 2 ) ) ) )
190	189	negeqd 10275	. . . . . . . . . . . . . . . . . . . 20 |- ( ( R ^ 2 ) = ( t ^ 2 ) -> -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) = -u ( sqr ` ( ( t ^ 2 ) - ( t ^ 2 ) ) ) )
191	190, 189	oveq12d 6668	. . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
192	8	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( t e. RR -> ( t ^ 2 ) e. CC )
193	192	subidd 10380	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( t e. RR -> ( ( t ^ 2 ) - ( t ^ 2 ) ) = 0 )
194	193	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( t e. RR -> ( sqr ` ( ( t ^ 2 ) - ( t ^ 2 ) ) ) = ( sqr ` 0 ) )
195	194	negeqd 10275	. . . . . . . . . . . . . . . . . . . . . 22 |- ( t e. RR -> -u ( sqr ` ( ( t ^ 2 ) - ( t ^ 2 ) ) ) = -u ( sqr ` 0 ) )
196		sqrt0 13982	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( sqr ` 0 ) = 0
197	196	negeqi 10274	. . . . . . . . . . . . . . . . . . . . . . 23 |- -u ( sqr ` 0 ) = -u 0
198		neg0 10327	. . . . . . . . . . . . . . . . . . . . . . 23 |- -u 0 = 0
199	197, 198	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . 22 |- -u ( sqr ` 0 ) = 0
200	195, 199	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . 21 |- ( t e. RR -> -u ( sqr ` ( ( t ^ 2 ) - ( t ^ 2 ) ) ) = 0 )
201	194, 196	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . 21 |- ( t e. RR -> ( sqr ` ( ( t ^ 2 ) - ( t ^ 2 ) ) ) = 0 )
202	200, 201	oveq12d 6668	. . . . . . . . . . . . . . . . . . . 20 |- ( t e. RR -> ( -u ( sqr ` ( ( t ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( t ^ 2 ) - ( t ^ 2 ) ) ) ) = ( 0 [,] 0 ) )
203	202	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . 19 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( -u ( sqr ` ( ( t ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( t ^ 2 ) - ( t ^ 2 ) ) ) ) = ( 0 [,] 0 ) )
204	191, 203	sylan9eqr 2678	. . . . . . . . . . . . . . . . . 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 ) )
205	204	fveq2d 6195	. . . . . . . . . . . . . . . . 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 ) ) )
206		iccmbl 23334	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 0 e. RR /\ 0 e. RR ) -> ( 0 [,] 0 ) e. dom vol )
207	62, 62, 206	mp2an 708	. . . . . . . . . . . . . . . . . . 19 |- ( 0 [,] 0 ) e. dom vol
208		mblvol 23298	. . . . . . . . . . . . . . . . . . 19 |- ( ( 0 [,] 0 ) e. dom vol -> ( vol ` ( 0 [,] 0 ) ) = ( vol* ` ( 0 [,] 0 ) ) )
209	207, 208	ax-mp 5	. . . . . . . . . . . . . . . . . 18 |- ( vol ` ( 0 [,] 0 ) ) = ( vol* ` ( 0 [,] 0 ) )
210		0xr 10086	. . . . . . . . . . . . . . . . . . . 20 |- 0 e. RR*
211		iccid 12220	. . . . . . . . . . . . . . . . . . . . 21 |- ( 0 e. RR* -> ( 0 [,] 0 ) = { 0 } )
212	211	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20 |- ( 0 e. RR* -> ( vol* ` ( 0 [,] 0 ) ) = ( vol* ` { 0 } ) )
213	210, 212	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 |- ( vol* ` ( 0 [,] 0 ) ) = ( vol* ` { 0 } )
214		ovolsn 23263	. . . . . . . . . . . . . . . . . . . 20 |- ( 0 e. RR -> ( vol* ` { 0 } ) = 0 )
215	62, 214	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 |- ( vol* ` { 0 } ) = 0
216	213, 215	eqtri 2644	. . . . . . . . . . . . . . . . . 18 |- ( vol* ` ( 0 [,] 0 ) ) = 0
217	209, 216	eqtri 2644	. . . . . . . . . . . . . . . . 17 |- ( vol ` ( 0 [,] 0 ) ) = 0
218	205, 217	syl6eq 2672	. . . . . . . . . . . . . . . 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 )
219	187, 218	syldan 487	. . . . . . . . . . . . . . 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 )
220	183, 219	eqtrd 2656	. . . . . . . . . . . . . 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 )
221	220	ex 450	. . . . . . . . . . . . 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 ) )
222	221	adantr 481	. . . . . . . . . . . 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 ) )
223	18, 17	ltnled 10184	. . . . . . . . . . . . . . 15 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( R < ( abs ` t ) <-> -. ( abs ` t ) <_ R ) )
224	223	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R <_ ( abs ` t ) ) -> ( R < ( abs ` t ) <-> -. ( abs ` t ) <_ R ) )
225		simpl1 1064	. . . . . . . . . . . . . . 15 |- ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R <_ ( abs ` t ) ) -> R e. RR )
226	17	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R <_ ( abs ` t ) ) -> ( abs ` t ) e. RR )
227		simpr 477	. . . . . . . . . . . . . . 15 |- ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R <_ ( abs ` t ) ) -> R <_ ( abs ` t ) )
228	225, 226, 227	leltned 10190	. . . . . . . . . . . . . 14 |- ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R <_ ( abs ` t ) ) -> ( R < ( abs ` t ) <-> ( abs ` t ) =/= R ) )
229	224, 228	bitr3d 270	. . . . . . . . . . . . 13 |- ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R <_ ( abs ` t ) ) -> ( -. ( abs ` t ) <_ R <-> ( abs ` t ) =/= R ) )
230	229, 102	syl6bir 244	. . . . . . . . . . . 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 ) )
231	222, 230	pm2.61dne 2880	. . . . . . . . . . 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 )
232	180, 231	eqtrd 2656	. . . . . . . . . 10 |- ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R <_ ( abs ` t ) ) -> ( vol ` ( S " { t } ) ) = 0 )
233	232	ex 450	. . . . . . . . 9 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( R <_ ( abs ` t ) -> ( vol ` ( S " { t } ) ) = 0 ) )
234	178, 233	sylbid 230	. . . . . . . 8 |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( -. t e. ( -u R (,) R ) -> ( vol ` ( S " { t } ) ) = 0 ) )
235	234	3expia 1267	. . . . . . 7 |- ( ( R e. RR /\ 0 <_ R ) -> ( t e. RR -> ( -. t e. ( -u R (,) R ) -> ( vol ` ( S " { t } ) ) = 0 ) ) )
236	235	impd 447	. . . . . 6 |- ( ( R e. RR /\ 0 <_ R ) -> ( ( t e. RR /\ -. t e. ( -u R (,) R ) ) -> ( vol ` ( S " { t } ) ) = 0 ) )
237	164, 236	syl5bi 232	. . . . 5 |- ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( RR \ ( -u R (,) R ) ) -> ( vol ` ( S " { t } ) ) = 0 ) )
238	237	imp 445	. . . 4 |- ( ( ( R e. RR /\ 0 <_ R ) /\ t e. ( RR \ ( -u R (,) R ) ) ) -> ( vol ` ( S " { t } ) ) = 0 )
239	163, 238	itgss 23578	. . 3 |- ( ( R e. RR /\ 0 <_ R ) -> S. ( -u R (,) R ) ( vol ` ( S " { t } ) ) _d t = S. RR ( vol ` ( S " { t } ) ) _d t )
240		negeq 10273	. . . . . . . . . 10 |- ( R = 0 -> -u R = -u 0 )
241	240, 198	syl6eq 2672	. . . . . . . . 9 |- ( R = 0 -> -u R = 0 )
242		id 22	. . . . . . . . 9 |- ( R = 0 -> R = 0 )
243	241, 242	oveq12d 6668	. . . . . . . 8 |- ( R = 0 -> ( -u R (,) R ) = ( 0 (,) 0 ) )
244		iooid 12203	. . . . . . . 8 |- ( 0 (,) 0 ) = (/)
245	243, 244	syl6eq 2672	. . . . . . 7 |- ( R = 0 -> ( -u R (,) R ) = (/) )
246	245	adantl 482	. . . . . 6 |- ( ( ( R e. RR /\ 0 <_ R ) /\ R = 0 ) -> ( -u R (,) R ) = (/) )
247		itgeq1 23539	. . . . . 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 )
248	246, 247	syl 17	. . . . 5 |- ( ( ( R e. RR /\ 0 <_ R ) /\ R = 0 ) -> S. ( -u R (,) R ) ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) _d t = S. (/) ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) _d t )
249		itg0 23546	. . . . . 6 |- S. (/) ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) _d t = 0
250		oveq1 6657	. . . . . . . . 9 |- ( R = 0 -> ( R ^ 2 ) = ( 0 ^ 2 ) )
251	250	oveq2d 6666	. . . . . . . 8 |- ( R = 0 -> ( pi x. ( R ^ 2 ) ) = ( pi x. ( 0 ^ 2 ) ) )
252		sq0 12955	. . . . . . . . . 10 |- ( 0 ^ 2 ) = 0
253	252	oveq2i 6661	. . . . . . . . 9 |- ( pi x. ( 0 ^ 2 ) ) = ( pi x. 0 )
254		picn 24211	. . . . . . . . . 10 |- pi e. CC
255	254	mul01i 10226	. . . . . . . . 9 |- ( pi x. 0 ) = 0
256	253, 255	eqtr2i 2645	. . . . . . . 8 |- 0 = ( pi x. ( 0 ^ 2 ) )
257	251, 256	syl6reqr 2675	. . . . . . 7 |- ( R = 0 -> 0 = ( pi x. ( R ^ 2 ) ) )
258	257	adantl 482	. . . . . 6 |- ( ( ( R e. RR /\ 0 <_ R ) /\ R = 0 ) -> 0 = ( pi x. ( R ^ 2 ) ) )
259	249, 258	syl5eq 2668	. . . . 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 ) ) )
260	248, 259	eqtrd 2656	. . . 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 ) ) )
261		simp1 1061	. . . . . . 7 |- ( ( R e. RR /\ 0 <_ R /\ R =/= 0 ) -> R e. RR )
262		0red 10041	. . . . . . . . 9 |- ( ( R e. RR /\ 0 <_ R ) -> 0 e. RR )
263		simpr 477	. . . . . . . . 9 |- ( ( R e. RR /\ 0 <_ R ) -> 0 <_ R )
264	262, 77, 263	leltned 10190	. . . . . . . 8 |- ( ( R e. RR /\ 0 <_ R ) -> ( 0 < R <-> R =/= 0 ) )
265	264	biimp3ar 1433	. . . . . . 7 |- ( ( R e. RR /\ 0 <_ R /\ R =/= 0 ) -> 0 < R )
266	261, 265	elrpd 11869	. . . . . 6 |- ( ( R e. RR /\ 0 <_ R /\ R =/= 0 ) -> R e. RR+ )
267	266	3expa 1265	. . . . 5 |- ( ( ( R e. RR /\ 0 <_ R ) /\ R =/= 0 ) -> R e. RR+ )
268	157, 16	syl 17	. . . . . . . . . . 11 |- ( t e. ( -u R (,) R ) -> ( abs ` t ) e. RR )
269	268	adantl 482	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( abs ` t ) e. RR )
270		rpre 11839	. . . . . . . . . . 11 |- ( R e. RR+ -> R e. RR )
271	270	adantr 481	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> R e. RR )
272	270	renegcld 10457	. . . . . . . . . . . . . 14 |- ( R e. RR+ -> -u R e. RR )
273	272	rexrd 10089	. . . . . . . . . . . . 13 |- ( R e. RR+ -> -u R e. RR* )
274		rpxr 11840	. . . . . . . . . . . . 13 |- ( R e. RR+ -> R e. RR* )
275	273, 274, 167	syl2anc 693	. . . . . . . . . . . 12 |- ( R e. RR+ -> ( t e. ( -u R (,) R ) <-> ( t e. RR /\ -u R < t /\ t < R ) ) )
276		simpr 477	. . . . . . . . . . . . . . . 16 |- ( ( R e. RR+ /\ t e. RR ) -> t e. RR )
277	270	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( R e. RR+ /\ t e. RR ) -> R e. RR )
278	276, 277	absltd 14168	. . . . . . . . . . . . . . 15 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) < R <-> ( -u R < t /\ t < R ) ) )
279	278	biimprd 238	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> ( abs ` t ) < R ) )
280	279	exp4b 632	. . . . . . . . . . . . 13 |- ( R e. RR+ -> ( t e. RR -> ( -u R < t -> ( t < R -> ( abs ` t ) < R ) ) ) )
281	280	3impd 1281	. . . . . . . . . . . 12 |- ( R e. RR+ -> ( ( t e. RR /\ -u R < t /\ t < R ) -> ( abs ` t ) < R ) )
282	275, 281	sylbid 230	. . . . . . . . . . 11 |- ( R e. RR+ -> ( t e. ( -u R (,) R ) -> ( abs ` t ) < R ) )
283	282	imp 445	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( abs ` t ) < R )
284	269, 271, 283	ltled 10185	. . . . . . . . 9 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( abs ` t ) <_ R )
285	284, 112	syl 17	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) = ( vol ` ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
286	270	resqcld 13035	. . . . . . . . . . . . . . 15 |- ( R e. RR+ -> ( R ^ 2 ) e. RR )
287	286	recnd 10068	. . . . . . . . . . . . . 14 |- ( R e. RR+ -> ( R ^ 2 ) e. CC )
288	287	adantr 481	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ t e. RR ) -> ( R ^ 2 ) e. CC )
289	192	adantl 482	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ t e. RR ) -> ( t ^ 2 ) e. CC )
290	288, 289	subcld 10392	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( R ^ 2 ) - ( t ^ 2 ) ) e. CC )
291	290	sqrtcld 14176	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. RR ) -> ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. CC )
292	291, 291	subnegd 10399	. . . . . . . . . 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 ) ) ) ) )
293	157, 292	sylan2 491	. . . . . . . . 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 ) ) ) ) )
294	286	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( R e. RR+ /\ t e. RR ) -> ( R ^ 2 ) e. RR )
295	8	adantl 482	. . . . . . . . . . . . . . . 16 |- ( ( R e. RR+ /\ t e. RR ) -> ( t ^ 2 ) e. RR )
296	294, 295	resubcld 10458	. . . . . . . . . . . . . . 15 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( R ^ 2 ) - ( t ^ 2 ) ) e. RR )
297	157, 296	sylan2 491	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( R ^ 2 ) - ( t ^ 2 ) ) e. RR )
298		0red 10041	. . . . . . . . . . . . . . 15 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 e. RR )
299	16	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( R e. RR+ /\ t e. RR ) -> ( abs ` t ) e. RR )
300	19	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( R e. RR+ /\ t e. RR ) -> 0 <_ ( abs ` t ) )
301		rpge0 11845	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( R e. RR+ -> 0 <_ R )
302	301	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( R e. RR+ /\ t e. RR ) -> 0 <_ R )
303	299, 277, 300, 302	lt2sqd 13043	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) < R <-> ( ( abs ` t ) ^ 2 ) < ( R ^ 2 ) ) )
304	12	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( abs ` t ) ^ 2 ) = ( t ^ 2 ) )
305	304	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( ( abs ` t ) ^ 2 ) < ( R ^ 2 ) <-> ( t ^ 2 ) < ( R ^ 2 ) ) )
306	303, 278, 305	3bitr3rd 299	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( t ^ 2 ) < ( R ^ 2 ) <-> ( -u R < t /\ t < R ) ) )
307	295, 294	posdifd 10614	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( t ^ 2 ) < ( R ^ 2 ) <-> 0 < ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
308	306, 307	bitr3d 270	. . . . . . . . . . . . . . . . . . . 20 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) <-> 0 < ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
309	308	biimpd 219	. . . . . . . . . . . . . . . . . . 19 |- ( ( R e. RR+ /\ t e. RR ) -> ( ( -u R < t /\ t < R ) -> 0 < ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
310	309	exp4b 632	. . . . . . . . . . . . . . . . . 18 |- ( R e. RR+ -> ( t e. RR -> ( -u R < t -> ( t < R -> 0 < ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
311	310	3impd 1281	. . . . . . . . . . . . . . . . 17 |- ( R e. RR+ -> ( ( t e. RR /\ -u R < t /\ t < R ) -> 0 < ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
312	275, 311	sylbid 230	. . . . . . . . . . . . . . . 16 |- ( R e. RR+ -> ( t e. ( -u R (,) R ) -> 0 < ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
313	312	imp 445	. . . . . . . . . . . . . . 15 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 < ( ( R ^ 2 ) - ( t ^ 2 ) ) )
314	298, 297, 313	ltled 10185	. . . . . . . . . . . . . 14 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) )
315	297, 314	resqrtcld 14156	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR )
316	315	renegcld 10457	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR )
317	316, 315, 28	syl2anc 693	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) e. dom vol )
318	317, 30	syl 17	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( vol ` ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) = ( vol* ` ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
319	297, 314	sqrtge0d 14159	. . . . . . . . . . . . 13 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 <_ ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
320	315, 315, 319, 319	addge0d 10603	. . . . . . . . . . . 12 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> 0 <_ ( ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) + ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
321	293	breq2d 4665	. . . . . . . . . . . . 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 ) ) ) ) ) )
322	315, 316	subge0d 10617	. . . . . . . . . . . . 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 ) ) ) ) )
323	321, 322	bitr3d 270	. . . . . . . . . . . 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 ) ) ) ) )
324	320, 323	mpbid 222	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
325	316, 315, 324, 47	syl3anc 1326	. . . . . . . . . 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 ) ) ) ) )
326	318, 325	eqtrd 2656	. . . . . . . . 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 ) ) ) ) )
327		ax-resscn 9993	. . . . . . . . . . . . . . 15 |- RR C_ CC
328	327	a1i 11	. . . . . . . . . . . . . 14 |- ( R e. RR+ -> RR C_ CC )
329	272, 270, 78	syl2anc 693	. . . . . . . . . . . . . 14 |- ( R e. RR+ -> ( -u R [,] R ) C_ RR )
330		rpcn 11841	. . . . . . . . . . . . . . . . 17 |- ( R e. RR+ -> R e. CC )
331	330	sqcld 13006	. . . . . . . . . . . . . . . 16 |- ( R e. RR+ -> ( R ^ 2 ) e. CC )
332	331	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> ( R ^ 2 ) e. CC )
333	329	sselda 3603	. . . . . . . . . . . . . . . . . . 19 |- ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> u e. RR )
334	333	recnd 10068	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> u e. CC )
335	330	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> R e. CC )
336		rpne0 11848	. . . . . . . . . . . . . . . . . . 19 |- ( R e. RR+ -> R =/= 0 )
337	336	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> R =/= 0 )
338	334, 335, 337	divcld 10801	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> ( u / R ) e. CC )
339		asincl 24600	. . . . . . . . . . . . . . . . 17 |- ( ( u / R ) e. CC -> (arcsin ` ( u / R ) ) e. CC )
340	338, 339	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> (arcsin ` ( u / R ) ) e. CC )
341		1cnd 10056	. . . . . . . . . . . . . . . . . . 19 |- ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> 1 e. CC )
342	338	sqcld 13006	. . . . . . . . . . . . . . . . . . 19 |- ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> ( ( u / R ) ^ 2 ) e. CC )
343	341, 342	subcld 10392	. . . . . . . . . . . . . . . . . 18 |- ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> ( 1 - ( ( u / R ) ^ 2 ) ) e. CC )
344	343	sqrtcld 14176	. . . . . . . . . . . . . . . . 17 |- ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) e. CC )
345	338, 344	mulcld 10060	. . . . . . . . . . . . . . . 16 |- ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) e. CC )
346	340, 345	addcld 10059	. . . . . . . . . . . . . . 15 |- ( ( R e. RR+ /\ u e. ( -u R [,] R ) ) -> ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) e. CC )
347	332, 346	mulcld 10060	. . . . . . . . . . . . . 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 )
348		eqid 2622	. . . . . . . . . . . . . . 15 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
349	348	tgioo2 22606	. . . . . . . . . . . . . 14 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
350		iccntr 22624	. . . . . . . . . . . . . . 15 |- ( ( -u R e. RR /\ R e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( -u R [,] R ) ) = ( -u R (,) R ) )
351	272, 270, 350	syl2anc 693	. . . . . . . . . . . . . 14 |- ( R e. RR+ -> ( ( int ` ( topGen ` ran (,) ) ) ` ( -u R [,] R ) ) = ( -u R (,) R ) )
352	328, 329, 347, 349, 348, 351	dvmptntr 23734	. . . . . . . . . . . . 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 ) ) ) ) ) ) ) ) )
353		areacirclem1 33500	. . . . . . . . . . . . 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 ) ) ) ) ) )
354	352, 353	eqtrd 2656	. . . . . . . . . . . 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 ) ) ) ) ) )
355	354	adantr 481	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 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 ) ) ) ) ) )
356		oveq1 6657	. . . . . . . . . . . . . . 15 |- ( u = t -> ( u ^ 2 ) = ( t ^ 2 ) )
357	356	oveq2d 6666	. . . . . . . . . . . . . 14 |- ( u = t -> ( ( R ^ 2 ) - ( u ^ 2 ) ) = ( ( R ^ 2 ) - ( t ^ 2 ) ) )
358	357	fveq2d 6195	. . . . . . . . . . . . 13 |- ( u = t -> ( sqr ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) = ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
359	358	oveq2d 6666	. . . . . . . . . . . 12 |- ( u = t -> ( 2 x. ( sqr ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) = ( 2 x. ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
360	359	adantl 482	. . . . . . . . . . 11 |- ( ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) /\ u = t ) -> ( 2 x. ( sqr ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) = ( 2 x. ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
361		simpr 477	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> t e. ( -u R (,) R ) )
362		ovexd 6680	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 2 x. ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) e. _V )
363	355, 360, 361, 362	fvmptd 6288	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( RR _D ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ) ` t ) = ( 2 x. ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
364	157, 291	sylan2 491	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. CC )
365	364	2timesd 11275	. . . . . . . . . 10 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( 2 x. ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) = ( ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) + ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
366	363, 365	eqtrd 2656	. . . . . . . . 9 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( RR _D ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ) ` t ) = ( ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) + ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
367	293, 326, 366	3eqtr4rd 2667	. . . . . . . 8 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( ( RR _D ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ) ` t ) = ( vol ` ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
368	285, 367	eqtr4d 2659	. . . . . . 7 |- ( ( R e. RR+ /\ t e. ( -u R (,) R ) ) -> ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) ) = ( ( RR _D ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ) ` t ) )
369	368	itgeq2dv 23548	. . . . . 6 |- ( R e. RR+ -> S. ( -u R (,) R ) ( vol ` if ( ( abs ` t ) <_ R , ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( 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. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ) ` t ) _d t )
370	270, 270, 301, 301	addge0d 10603	. . . . . . . 8 |- ( R e. RR+ -> 0 <_ ( R + R ) )
371	330, 330	subnegd 10399	. . . . . . . . . 10 |- ( R e. RR+ -> ( R - -u R ) = ( R + R ) )
372	371	breq2d 4665	. . . . . . . . 9 |- ( R e. RR+ -> ( 0 <_ ( R - -u R ) <-> 0 <_ ( R + R ) ) )
373	270, 272	subge0d 10617	. . . . . . . . 9 |- ( R e. RR+ -> ( 0 <_ ( R - -u R ) <-> -u R <_ R ) )
374	372, 373	bitr3d 270	. . . . . . . 8 |- ( R e. RR+ -> ( 0 <_ ( R + R ) <-> -u R <_ R ) )
375	370, 374	mpbid 222	. . . . . . 7 |- ( R e. RR+ -> -u R <_ R )
376		2cn 11091	. . . . . . . . . . 11 |- 2 e. CC
377	162, 327	sstri 3612	. . . . . . . . . . 11 |- ( -u R (,) R ) C_ CC
378		ssid 3624	. . . . . . . . . . 11 |- CC C_ CC
379	376, 377, 378	3pm3.2i 1239	. . . . . . . . . 10 |- ( 2 e. CC /\ ( -u R (,) R ) C_ CC /\ CC C_ CC )
380		cncfmptc 22714	. . . . . . . . . 10 |- ( ( 2 e. CC /\ ( -u R (,) R ) C_ CC /\ CC C_ CC ) -> ( u e. ( -u R (,) R ) |-> 2 ) e. ( ( -u R (,) R ) -cn-> CC ) )
381	379, 380	mp1i 13	. . . . . . . . 9 |- ( R e. RR+ -> ( u e. ( -u R (,) R ) |-> 2 ) e. ( ( -u R (,) R ) -cn-> CC ) )
382		ioossicc 12259	. . . . . . . . . . 11 |- ( -u R (,) R ) C_ ( -u R [,] R )
383		resmpt 5449	. . . . . . . . . . 11 |- ( ( -u R (,) R ) C_ ( -u R [,] R ) -> ( ( u e. ( -u R [,] R ) |-> ( sqr ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) |` ( -u R (,) R ) ) = ( u e. ( -u R (,) R ) |-> ( sqr ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) )
384	382, 383	ax-mp 5	. . . . . . . . . 10 |- ( ( u e. ( -u R [,] R ) |-> ( sqr ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) |` ( -u R (,) R ) ) = ( u e. ( -u R (,) R ) |-> ( sqr ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) )
385		areacirclem2 33501	. . . . . . . . . . . 12 |- ( ( R e. RR /\ 0 <_ R ) -> ( u e. ( -u R [,] R ) |-> ( sqr ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
386	270, 301, 385	syl2anc 693	. . . . . . . . . . 11 |- ( R e. RR+ -> ( u e. ( -u R [,] R ) |-> ( sqr ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
387		rescncf 22700	. . . . . . . . . . 11 |- ( ( -u R (,) R ) C_ ( -u R [,] R ) -> ( ( u e. ( -u R [,] R ) |-> ( sqr ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) -> ( ( u e. ( -u R [,] R ) |-> ( sqr ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) |` ( -u R (,) R ) ) e. ( ( -u R (,) R ) -cn-> CC ) ) )
388	382, 386, 387	mpsyl 68	. . . . . . . . . 10 |- ( R e. RR+ -> ( ( u e. ( -u R [,] R ) |-> ( sqr ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) |` ( -u R (,) R ) ) e. ( ( -u R (,) R ) -cn-> CC ) )
389	384, 388	syl5eqelr 2706	. . . . . . . . 9 |- ( R e. RR+ -> ( u e. ( -u R (,) R ) |-> ( sqr ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) e. ( ( -u R (,) R ) -cn-> CC ) )
390	381, 389	mulcncf 23215	. . . . . . . 8 |- ( R e. RR+ -> ( u e. ( -u R (,) R ) |-> ( 2 x. ( sqr ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) ) e. ( ( -u R (,) R ) -cn-> CC ) )
391	354, 390	eqeltrd 2701	. . . . . . 7 |- ( R e. RR+ -> ( RR _D ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ) e. ( ( -u R (,) R ) -cn-> CC ) )
392	382	a1i 11	. . . . . . . . . 10 |- ( ( R e. RR /\ 0 <_ R ) -> ( -u R (,) R ) C_ ( -u R [,] R ) )
393		ioombl 23333	. . . . . . . . . . 11 |- ( -u R (,) R ) e. dom vol
394	393	a1i 11	. . . . . . . . . 10 |- ( ( R e. RR /\ 0 <_ R ) -> ( -u R (,) R ) e. dom vol )
395		ovexd 6680	. . . . . . . . . 10 |- ( ( ( R e. RR /\ 0 <_ R ) /\ u e. ( -u R [,] R ) ) -> ( 2 x. ( sqr ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) e. _V )
396		areacirclem3 33502	. . . . . . . . . 10 |- ( ( R e. RR /\ 0 <_ R ) -> ( u e. ( -u R [,] R ) |-> ( 2 x. ( sqr ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) ) e. L^1 )
397	392, 394, 395, 396	iblss 23571	. . . . . . . . 9 |- ( ( R e. RR /\ 0 <_ R ) -> ( u e. ( -u R (,) R ) |-> ( 2 x. ( sqr ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) ) e. L^1 )
398	270, 301, 397	syl2anc 693	. . . . . . . 8 |- ( R e. RR+ -> ( u e. ( -u R (,) R ) |-> ( 2 x. ( sqr ` ( ( R ^ 2 ) - ( u ^ 2 ) ) ) ) ) e. L^1 )
399	354, 398	eqeltrd 2701	. . . . . . 7 |- ( R e. RR+ -> ( RR _D ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ) e. L^1 )
400		areacirclem4 33503	. . . . . . 7 |- ( R e. RR+ -> ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
401	272, 270, 375, 391, 399, 400	ftc2nc 33494	. . . . . 6 |- ( R e. RR+ -> S. ( -u R (,) R ) ( ( RR _D ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ) ` t ) _d t = ( ( ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ` R ) - ( ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ` -u R ) ) )
402		eqidd 2623	. . . . . . . . . 10 |- ( R e. RR+ -> ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) = ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) )
403		oveq1 6657	. . . . . . . . . . . . . 14 |- ( u = R -> ( u / R ) = ( R / R ) )
404	403	fveq2d 6195	. . . . . . . . . . . . 13 |- ( u = R -> (arcsin ` ( u / R ) ) = (arcsin ` ( R / R ) ) )
405	403	oveq1d 6665	. . . . . . . . . . . . . . . 16 |- ( u = R -> ( ( u / R ) ^ 2 ) = ( ( R / R ) ^ 2 ) )
406	405	oveq2d 6666	. . . . . . . . . . . . . . 15 |- ( u = R -> ( 1 - ( ( u / R ) ^ 2 ) ) = ( 1 - ( ( R / R ) ^ 2 ) ) )
407	406	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( u = R -> ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) = ( sqr ` ( 1 - ( ( R / R ) ^ 2 ) ) ) )
408	403, 407	oveq12d 6668	. . . . . . . . . . . . 13 |- ( u = R -> ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) = ( ( R / R ) x. ( sqr ` ( 1 - ( ( R / R ) ^ 2 ) ) ) ) )
409	404, 408	oveq12d 6668	. . . . . . . . . . . 12 |- ( u = R -> ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) = ( (arcsin ` ( R / R ) ) + ( ( R / R ) x. ( sqr ` ( 1 - ( ( R / R ) ^ 2 ) ) ) ) ) )
410	409	oveq2d 6666	. . . . . . . . . . 11 |- ( u = R -> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) = ( ( R ^ 2 ) x. ( (arcsin ` ( R / R ) ) + ( ( R / R ) x. ( sqr ` ( 1 - ( ( R / R ) ^ 2 ) ) ) ) ) ) )
411	410	adantl 482	. . . . . . . . . 10 |- ( ( R e. RR+ /\ u = R ) -> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) = ( ( R ^ 2 ) x. ( (arcsin ` ( R / R ) ) + ( ( R / R ) x. ( sqr ` ( 1 - ( ( R / R ) ^ 2 ) ) ) ) ) ) )
412		ubicc2 12289	. . . . . . . . . . 11 |- ( ( -u R e. RR* /\ R e. RR* /\ -u R <_ R ) -> R e. ( -u R [,] R ) )
413	273, 274, 375, 412	syl3anc 1326	. . . . . . . . . 10 |- ( R e. RR+ -> R e. ( -u R [,] R ) )
414		ovexd 6680	. . . . . . . . . 10 |- ( R e. RR+ -> ( ( R ^ 2 ) x. ( (arcsin ` ( R / R ) ) + ( ( R / R ) x. ( sqr ` ( 1 - ( ( R / R ) ^ 2 ) ) ) ) ) ) e. _V )
415	402, 411, 413, 414	fvmptd 6288	. . . . . . . . 9 |- ( R e. RR+ -> ( ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ` R ) = ( ( R ^ 2 ) x. ( (arcsin ` ( R / R ) ) + ( ( R / R ) x. ( sqr ` ( 1 - ( ( R / R ) ^ 2 ) ) ) ) ) ) )
416	330, 336	dividd 10799	. . . . . . . . . . . . . 14 |- ( R e. RR+ -> ( R / R ) = 1 )
417	416	fveq2d 6195	. . . . . . . . . . . . 13 |- ( R e. RR+ -> (arcsin ` ( R / R ) ) = (arcsin ` 1 ) )
418		asin1 24621	. . . . . . . . . . . . 13 |- (arcsin ` 1 ) = ( pi / 2 )
419	417, 418	syl6eq 2672	. . . . . . . . . . . 12 |- ( R e. RR+ -> (arcsin ` ( R / R ) ) = ( pi / 2 ) )
420	416	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19 |- ( R e. RR+ -> ( ( R / R ) ^ 2 ) = ( 1 ^ 2 ) )
421		sq1 12958	. . . . . . . . . . . . . . . . . . 19 |- ( 1 ^ 2 ) = 1
422	420, 421	syl6eq 2672	. . . . . . . . . . . . . . . . . 18 |- ( R e. RR+ -> ( ( R / R ) ^ 2 ) = 1 )
423	422	oveq2d 6666	. . . . . . . . . . . . . . . . 17 |- ( R e. RR+ -> ( 1 - ( ( R / R ) ^ 2 ) ) = ( 1 - 1 ) )
424		1cnd 10056	. . . . . . . . . . . . . . . . . 18 |- ( R e. RR+ -> 1 e. CC )
425	424	subidd 10380	. . . . . . . . . . . . . . . . 17 |- ( R e. RR+ -> ( 1 - 1 ) = 0 )
426	423, 425	eqtrd 2656	. . . . . . . . . . . . . . . 16 |- ( R e. RR+ -> ( 1 - ( ( R / R ) ^ 2 ) ) = 0 )
427	426	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( R e. RR+ -> ( sqr ` ( 1 - ( ( R / R ) ^ 2 ) ) ) = ( sqr ` 0 ) )
428	427, 196	syl6eq 2672	. . . . . . . . . . . . . 14 |- ( R e. RR+ -> ( sqr ` ( 1 - ( ( R / R ) ^ 2 ) ) ) = 0 )
429	428	oveq2d 6666	. . . . . . . . . . . . 13 |- ( R e. RR+ -> ( ( R / R ) x. ( sqr ` ( 1 - ( ( R / R ) ^ 2 ) ) ) ) = ( ( R / R ) x. 0 ) )
430	330, 330, 336	divcld 10801	. . . . . . . . . . . . . 14 |- ( R e. RR+ -> ( R / R ) e. CC )
431	430	mul01d 10235	. . . . . . . . . . . . 13 |- ( R e. RR+ -> ( ( R / R ) x. 0 ) = 0 )
432	429, 431	eqtrd 2656	. . . . . . . . . . . 12 |- ( R e. RR+ -> ( ( R / R ) x. ( sqr ` ( 1 - ( ( R / R ) ^ 2 ) ) ) ) = 0 )
433	419, 432	oveq12d 6668	. . . . . . . . . . 11 |- ( R e. RR+ -> ( (arcsin ` ( R / R ) ) + ( ( R / R ) x. ( sqr ` ( 1 - ( ( R / R ) ^ 2 ) ) ) ) ) = ( ( pi / 2 ) + 0 ) )
434		2ne0 11113	. . . . . . . . . . . . . 14 |- 2 =/= 0
435	254, 376, 434	divcli 10767	. . . . . . . . . . . . 13 |- ( pi / 2 ) e. CC
436	435	a1i 11	. . . . . . . . . . . 12 |- ( R e. RR+ -> ( pi / 2 ) e. CC )
437	436	addid1d 10236	. . . . . . . . . . 11 |- ( R e. RR+ -> ( ( pi / 2 ) + 0 ) = ( pi / 2 ) )
438	433, 437	eqtrd 2656	. . . . . . . . . 10 |- ( R e. RR+ -> ( (arcsin ` ( R / R ) ) + ( ( R / R ) x. ( sqr ` ( 1 - ( ( R / R ) ^ 2 ) ) ) ) ) = ( pi / 2 ) )
439	438	oveq2d 6666	. . . . . . . . 9 |- ( R e. RR+ -> ( ( R ^ 2 ) x. ( (arcsin ` ( R / R ) ) + ( ( R / R ) x. ( sqr ` ( 1 - ( ( R / R ) ^ 2 ) ) ) ) ) ) = ( ( R ^ 2 ) x. ( pi / 2 ) ) )
440	415, 439	eqtrd 2656	. . . . . . . 8 |- ( R e. RR+ -> ( ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ` R ) = ( ( R ^ 2 ) x. ( pi / 2 ) ) )
441		oveq1 6657	. . . . . . . . . . . . . 14 |- ( u = -u R -> ( u / R ) = ( -u R / R ) )
442	441	fveq2d 6195	. . . . . . . . . . . . 13 |- ( u = -u R -> (arcsin ` ( u / R ) ) = (arcsin ` ( -u R / R ) ) )
443	441	oveq1d 6665	. . . . . . . . . . . . . . . 16 |- ( u = -u R -> ( ( u / R ) ^ 2 ) = ( ( -u R / R ) ^ 2 ) )
444	443	oveq2d 6666	. . . . . . . . . . . . . . 15 |- ( u = -u R -> ( 1 - ( ( u / R ) ^ 2 ) ) = ( 1 - ( ( -u R / R ) ^ 2 ) ) )
445	444	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( u = -u R -> ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) = ( sqr ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) )
446	441, 445	oveq12d 6668	. . . . . . . . . . . . 13 |- ( u = -u R -> ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) = ( ( -u R / R ) x. ( sqr ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) ) )
447	442, 446	oveq12d 6668	. . . . . . . . . . . 12 |- ( u = -u R -> ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) = ( (arcsin ` ( -u R / R ) ) + ( ( -u R / R ) x. ( sqr ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) ) ) )
448	447	adantl 482	. . . . . . . . . . 11 |- ( ( R e. RR+ /\ u = -u R ) -> ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) = ( (arcsin ` ( -u R / R ) ) + ( ( -u R / R ) x. ( sqr ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) ) ) )
449	448	oveq2d 6666	. . . . . . . . . 10 |- ( ( R e. RR+ /\ u = -u R ) -> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) = ( ( R ^ 2 ) x. ( (arcsin ` ( -u R / R ) ) + ( ( -u R / R ) x. ( sqr ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) ) ) ) )
450		lbicc2 12288	. . . . . . . . . . 11 |- ( ( -u R e. RR* /\ R e. RR* /\ -u R <_ R ) -> -u R e. ( -u R [,] R ) )
451	273, 274, 375, 450	syl3anc 1326	. . . . . . . . . 10 |- ( R e. RR+ -> -u R e. ( -u R [,] R ) )
452		ovexd 6680	. . . . . . . . . 10 |- ( R e. RR+ -> ( ( R ^ 2 ) x. ( (arcsin ` ( -u R / R ) ) + ( ( -u R / R ) x. ( sqr ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) ) ) ) e. _V )
453	402, 449, 451, 452	fvmptd 6288	. . . . . . . . 9 |- ( R e. RR+ -> ( ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ` -u R ) = ( ( R ^ 2 ) x. ( (arcsin ` ( -u R / R ) ) + ( ( -u R / R ) x. ( sqr ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) ) ) ) )
454	330, 330, 336	divnegd 10814	. . . . . . . . . . . . . . 15 |- ( R e. RR+ -> -u ( R / R ) = ( -u R / R ) )
455	416	negeqd 10275	. . . . . . . . . . . . . . 15 |- ( R e. RR+ -> -u ( R / R ) = -u 1 )
456	454, 455	eqtr3d 2658	. . . . . . . . . . . . . 14 |- ( R e. RR+ -> ( -u R / R ) = -u 1 )
457	456	fveq2d 6195	. . . . . . . . . . . . 13 |- ( R e. RR+ -> (arcsin ` ( -u R / R ) ) = (arcsin ` -u 1 ) )
458		ax-1cn 9994	. . . . . . . . . . . . . . 15 |- 1 e. CC
459		asinneg 24613	. . . . . . . . . . . . . . 15 |- ( 1 e. CC -> (arcsin ` -u 1 ) = -u (arcsin ` 1 ) )
460	458, 459	ax-mp 5	. . . . . . . . . . . . . 14 |- (arcsin ` -u 1 ) = -u (arcsin ` 1 )
461	418	negeqi 10274	. . . . . . . . . . . . . 14 |- -u (arcsin ` 1 ) = -u ( pi / 2 )
462	460, 461	eqtri 2644	. . . . . . . . . . . . 13 |- (arcsin ` -u 1 ) = -u ( pi / 2 )
463	457, 462	syl6eq 2672	. . . . . . . . . . . 12 |- ( R e. RR+ -> (arcsin ` ( -u R / R ) ) = -u ( pi / 2 ) )
464	456	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19 |- ( R e. RR+ -> ( ( -u R / R ) ^ 2 ) = ( -u 1 ^ 2 ) )
465		neg1sqe1 12959	. . . . . . . . . . . . . . . . . . 19 |- ( -u 1 ^ 2 ) = 1
466	464, 465	syl6eq 2672	. . . . . . . . . . . . . . . . . 18 |- ( R e. RR+ -> ( ( -u R / R ) ^ 2 ) = 1 )
467	466	oveq2d 6666	. . . . . . . . . . . . . . . . 17 |- ( R e. RR+ -> ( 1 - ( ( -u R / R ) ^ 2 ) ) = ( 1 - 1 ) )
468	467, 425	eqtrd 2656	. . . . . . . . . . . . . . . 16 |- ( R e. RR+ -> ( 1 - ( ( -u R / R ) ^ 2 ) ) = 0 )
469	468	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( R e. RR+ -> ( sqr ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) = ( sqr ` 0 ) )
470	469, 196	syl6eq 2672	. . . . . . . . . . . . . 14 |- ( R e. RR+ -> ( sqr ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) = 0 )
471	470	oveq2d 6666	. . . . . . . . . . . . 13 |- ( R e. RR+ -> ( ( -u R / R ) x. ( sqr ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) ) = ( ( -u R / R ) x. 0 ) )
472	272	recnd 10068	. . . . . . . . . . . . . . 15 |- ( R e. RR+ -> -u R e. CC )
473	472, 330, 336	divcld 10801	. . . . . . . . . . . . . 14 |- ( R e. RR+ -> ( -u R / R ) e. CC )
474	473	mul01d 10235	. . . . . . . . . . . . 13 |- ( R e. RR+ -> ( ( -u R / R ) x. 0 ) = 0 )
475	471, 474	eqtrd 2656	. . . . . . . . . . . 12 |- ( R e. RR+ -> ( ( -u R / R ) x. ( sqr ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) ) = 0 )
476	463, 475	oveq12d 6668	. . . . . . . . . . 11 |- ( R e. RR+ -> ( (arcsin ` ( -u R / R ) ) + ( ( -u R / R ) x. ( sqr ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) ) ) = ( -u ( pi / 2 ) + 0 ) )
477	435	negcli 10349	. . . . . . . . . . . . 13 |- -u ( pi / 2 ) e. CC
478	477	a1i 11	. . . . . . . . . . . 12 |- ( R e. RR+ -> -u ( pi / 2 ) e. CC )
479	478	addid1d 10236	. . . . . . . . . . 11 |- ( R e. RR+ -> ( -u ( pi / 2 ) + 0 ) = -u ( pi / 2 ) )
480	476, 479	eqtrd 2656	. . . . . . . . . 10 |- ( R e. RR+ -> ( (arcsin ` ( -u R / R ) ) + ( ( -u R / R ) x. ( sqr ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) ) ) = -u ( pi / 2 ) )
481	480	oveq2d 6666	. . . . . . . . 9 |- ( R e. RR+ -> ( ( R ^ 2 ) x. ( (arcsin ` ( -u R / R ) ) + ( ( -u R / R ) x. ( sqr ` ( 1 - ( ( -u R / R ) ^ 2 ) ) ) ) ) ) = ( ( R ^ 2 ) x. -u ( pi / 2 ) ) )
482	453, 481	eqtrd 2656	. . . . . . . 8 |- ( R e. RR+ -> ( ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ` -u R ) = ( ( R ^ 2 ) x. -u ( pi / 2 ) ) )
483	440, 482	oveq12d 6668	. . . . . . 7 |- ( R e. RR+ -> ( ( ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ` R ) - ( ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ` -u R ) ) = ( ( ( R ^ 2 ) x. ( pi / 2 ) ) - ( ( R ^ 2 ) x. -u ( pi / 2 ) ) ) )
484	435, 435	subnegi 10360	. . . . . . . . . . 11 |- ( ( pi / 2 ) - -u ( pi / 2 ) ) = ( ( pi / 2 ) + ( pi / 2 ) )
485		pidiv2halves 24219	. . . . . . . . . . 11 |- ( ( pi / 2 ) + ( pi / 2 ) ) = pi
486	484, 485	eqtri 2644	. . . . . . . . . 10 |- ( ( pi / 2 ) - -u ( pi / 2 ) ) = pi
487	486	a1i 11	. . . . . . . . 9 |- ( R e. RR+ -> ( ( pi / 2 ) - -u ( pi / 2 ) ) = pi )
488	487	oveq2d 6666	. . . . . . . 8 |- ( R e. RR+ -> ( ( R ^ 2 ) x. ( ( pi / 2 ) - -u ( pi / 2 ) ) ) = ( ( R ^ 2 ) x. pi ) )
489	331, 436, 478	subdid 10486	. . . . . . . 8 |- ( R e. RR+ -> ( ( R ^ 2 ) x. ( ( pi / 2 ) - -u ( pi / 2 ) ) ) = ( ( ( R ^ 2 ) x. ( pi / 2 ) ) - ( ( R ^ 2 ) x. -u ( pi / 2 ) ) ) )
490	254	a1i 11	. . . . . . . . 9 |- ( R e. RR+ -> pi e. CC )
491	331, 490	mulcomd 10061	. . . . . . . 8 |- ( R e. RR+ -> ( ( R ^ 2 ) x. pi ) = ( pi x. ( R ^ 2 ) ) )
492	488, 489, 491	3eqtr3d 2664	. . . . . . 7 |- ( R e. RR+ -> ( ( ( R ^ 2 ) x. ( pi / 2 ) ) - ( ( R ^ 2 ) x. -u ( pi / 2 ) ) ) = ( pi x. ( R ^ 2 ) ) )
493	483, 492	eqtrd 2656	. . . . . 6 |- ( R e. RR+ -> ( ( ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ` R ) - ( ( u e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( u / R ) ) + ( ( u / R ) x. ( sqr ` ( 1 - ( ( u / R ) ^ 2 ) ) ) ) ) ) ) ` -u R ) ) = ( pi x. ( R ^ 2 ) ) )
494	369, 401, 493	3eqtrd 2660	. . . . 5 |- ( R e. RR+ -> 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 ) ) )
495	267, 494	syl 17	. . . 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 ) ) )
496	260, 495	pm2.61dane 2881	. . 3 |- ( ( R e. RR /\ 0 <_ R ) -> 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 ) ) )
497	161, 239, 496	3eqtr3d 2664	. 2 |- ( ( R e. RR /\ 0 <_ R ) -> S. RR ( vol ` ( S " { t } ) ) _d t = ( pi x. ( R ^ 2 ) ) )
498	156, 497	eqtrd 2656	1 |- ( ( R e. RR /\ 0 <_ R ) -> (area ` S ) = ( pi x. ( R ^ 2 ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   _Vcvv 3200   \ cdif 3571   C_ wss 3574   (/)c0 3915   ifcif 4086   {csn 4177   class class class wbr 4653   {copab 4712   |-> cmpt 4729   X. cxp 5112   `'ccnv 5113   dom cdm 5114   ran crn 5115   |` cres 5116   "cima 5117   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   +oocpnf 10071   RR*cxr 10073   < clt 10074   <_ cle 10075   - cmin 10266   -ucneg 10267   / cdiv 10684   2c2 11070   RR+crp 11832   (,)cioo 12175   [,]cicc 12178   ^cexp 12860   sqrcsqrt 13973   abscabs 13974   picpi 14797   TopOpenctopn 16082   topGenctg 16098  ℂ_fldccnfld 19746   intcnt 20821   -cn->ccncf 22679   vol*covol 23231   volcvol 23232   L^1cibl 23386   S.citg 23387   _D cdv 23627  arcsincasin 24589  areacarea 24682

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015  ax-mulf 10016

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-disj 4621  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-ofr 6898  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-omul 7565  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-fi 8317  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-acn 8768  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-ioc 12180  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-fl 12593  df-mod 12669  df-seq 12802  df-exp 12861  df-fac 13061  df-bc 13090  df-hash 13118  df-shft 13807  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-limsup 14202  df-clim 14219  df-rlim 14220  df-sum 14417  df-ef 14798  df-sin 14800  df-cos 14801  df-tan 14802  df-pi 14803  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-hom 15966  df-cco 15967  df-rest 16083  df-topn 16084  df-0g 16102  df-gsum 16103  df-topgen 16104  df-pt 16105  df-prds 16108  df-xrs 16162  df-qtop 16167  df-imas 16168  df-xps 16170  df-mre 16246  df-mrc 16247  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-submnd 17336  df-mulg 17541  df-cntz 17750  df-cmn 18195  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-fbas 19743  df-fg 19744  df-cnfld 19747  df-top 20699  df-topon 20716  df-topsp 20737  df-bases 20750  df-cld 20823  df-ntr 20824  df-cls 20825  df-nei 20902  df-lp 20940  df-perf 20941  df-cn 21031  df-cnp 21032  df-haus 21119  df-cmp 21190  df-tx 21365  df-hmeo 21558  df-fil 21650  df-fm 21742  df-flim 21743  df-flf 21744  df-xms 22125  df-ms 22126  df-tms 22127  df-cncf 22681  df-ovol 23233  df-vol 23234  df-mbf 23388  df-itg1 23389  df-itg2 23390  df-ibl 23391  df-itg 23392  df-0p 23437  df-limc 23630  df-dv 23631  df-log 24303  df-cxp 24304  df-asin 24592  df-area 24683

This theorem is referenced by: (None)