Metamath Proof Explorer

Theorem areacirclem5

Description: Finding the cross-section of a circle. (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 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 ) ) ) ) , (/) ) )

Proof

Step Hyp Ref Expression
1 areacirc.1 
 |-  S = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) ) }
2 1 imaeq1i 
 |-  ( S " { t } ) = ( { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) ) } " { t } )
3 vex 
 |-  t e. _V
4 imasng 
 |-  ( t e. _V -> ( { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) ) } " { t } ) = { u | t { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) ) } u } )
5 3 4 ax-mp 
 |-  ( { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) ) } " { t } ) = { u | t { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) ) } u }
6 df-br 
 |-  ( t { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) ) } u <-> <. t , u >. e. { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) ) } )
7 vex 
 |-  u e. _V
8 eleq1w 
 |-  ( x = t -> ( x e. RR <-> t e. RR ) )
9 8 anbi1d 
 |-  ( x = t -> ( ( x e. RR /\ y e. RR ) <-> ( t e. RR /\ y e. RR ) ) )
10 oveq1 
 |-  ( x = t -> ( x ^ 2 ) = ( t ^ 2 ) )
11 10 oveq1d 
 |-  ( x = t -> ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( ( t ^ 2 ) + ( y ^ 2 ) ) )
12 11 breq1d 
 |-  ( x = t -> ( ( ( x ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) <-> ( ( t ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) ) )
13 9 12 anbi12d 
 |-  ( x = t -> ( ( ( x e. RR /\ y e. RR ) /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) ) <-> ( ( t e. RR /\ y e. RR ) /\ ( ( t ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) ) ) )
14 eleq1w 
 |-  ( y = u -> ( y e. RR <-> u e. RR ) )
15 14 anbi2d 
 |-  ( y = u -> ( ( t e. RR /\ y e. RR ) <-> ( t e. RR /\ u e. RR ) ) )
16 oveq1 
 |-  ( y = u -> ( y ^ 2 ) = ( u ^ 2 ) )
17 16 oveq2d 
 |-  ( y = u -> ( ( t ^ 2 ) + ( y ^ 2 ) ) = ( ( t ^ 2 ) + ( u ^ 2 ) ) )
18 17 breq1d 
 |-  ( y = u -> ( ( ( t ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) <-> ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) )
19 15 18 anbi12d 
 |-  ( y = u -> ( ( ( t e. RR /\ y e. RR ) /\ ( ( t ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) ) <-> ( ( t e. RR /\ u e. RR ) /\ ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) ) )
20 3 7 13 19 opelopab 
 |-  ( <. t , u >. e. { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) ) } <-> ( ( t e. RR /\ u e. RR ) /\ ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) )
21 anass 
 |-  ( ( ( t e. RR /\ u e. RR ) /\ ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) <-> ( t e. RR /\ ( u e. RR /\ ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) ) )
22 6 20 21 3bitri 
 |-  ( t { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) ) } u <-> ( t e. RR /\ ( u e. RR /\ ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) ) )
23 22 abbii 
 |-  { u | t { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) ) } u } = { u | ( t e. RR /\ ( u e. RR /\ ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) ) }
24 2 5 23 3eqtri 
 |-  ( S " { t } ) = { u | ( t e. RR /\ ( u e. RR /\ ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) ) }
25 simp3 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> t e. RR )
26 25 biantrurd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( u e. RR /\ ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) <-> ( t e. RR /\ ( u e. RR /\ ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) ) ) )
27 26 abbidv 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> { u | ( u e. RR /\ ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) } = { u | ( t e. RR /\ ( u e. RR /\ ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) ) } )
28 resqcl 
 |-  ( R e. RR -> ( R ^ 2 ) e. RR )
29 28 3ad2ant1 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( R ^ 2 ) e. RR )
30 resqcl 
 |-  ( t e. RR -> ( t ^ 2 ) e. RR )
31 30 3ad2ant3 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( t ^ 2 ) e. RR )
32 29 31 resubcld 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( R ^ 2 ) - ( t ^ 2 ) ) e. RR )
33 32 adantr 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( ( R ^ 2 ) - ( t ^ 2 ) ) e. RR )
34 absresq 
 |-  ( t e. RR -> ( ( abs ` t ) ^ 2 ) = ( t ^ 2 ) )
35 34 3ad2ant3 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( abs ` t ) ^ 2 ) = ( t ^ 2 ) )
36 35 breq1d 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( ( abs ` t ) ^ 2 ) <_ ( R ^ 2 ) <-> ( t ^ 2 ) <_ ( R ^ 2 ) ) )
37 recn 
 |-  ( t e. RR -> t e. CC )
38 37 abscld 
 |-  ( t e. RR -> ( abs ` t ) e. RR )
39 38 3ad2ant3 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( abs ` t ) e. RR )
40 simp1 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> R e. RR )
41 37 absge0d 
 |-  ( t e. RR -> 0 <_ ( abs ` t ) )
42 41 3ad2ant3 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> 0 <_ ( abs ` t ) )
43 simp2 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> 0 <_ R )
44 39 40 42 43 le2sqd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( abs ` t ) <_ R <-> ( ( abs ` t ) ^ 2 ) <_ ( R ^ 2 ) ) )
45 29 31 subge0d 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) <-> ( t ^ 2 ) <_ ( R ^ 2 ) ) )
46 36 44 45 3bitr4d 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( abs ` t ) <_ R <-> 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
47 46 biimpa 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> 0 <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) )
48 33 47 resqrtcld 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR )
49 48 renegcld 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR )
50 49 rexrd 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR* )
51 48 rexrd 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR* )
52 iccval 
 |-  ( ( -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 ) ) ) ) = { u e. RR* | ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) } )
53 50 51 52 syl2anc 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) = { u e. RR* | ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) } )
54 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 ) ) ) ) )
55 54 adantl 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( 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 ) ) ) ) )
56 absresq 
 |-  ( u e. RR -> ( ( abs ` u ) ^ 2 ) = ( u ^ 2 ) )
57 32 recnd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( R ^ 2 ) - ( t ^ 2 ) ) e. CC )
58 57 adantr 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( ( R ^ 2 ) - ( t ^ 2 ) ) e. CC )
59 58 sqsqrtd 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ^ 2 ) = ( ( R ^ 2 ) - ( t ^ 2 ) ) )
60 56 59 breqan12rd 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ u e. RR ) -> ( ( ( abs ` u ) ^ 2 ) <_ ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ^ 2 ) <-> ( u ^ 2 ) <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
61 recn 
 |-  ( u e. RR -> u e. CC )
62 61 abscld 
 |-  ( u e. RR -> ( abs ` u ) e. RR )
63 62 adantl 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ u e. RR ) -> ( abs ` u ) e. RR )
64 48 adantr 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ u e. RR ) -> ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR )
65 61 absge0d 
 |-  ( u e. RR -> 0 <_ ( abs ` u ) )
66 65 adantl 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ u e. RR ) -> 0 <_ ( abs ` u ) )
67 33 47 sqrtge0d 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> 0 <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
68 67 adantr 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ u e. RR ) -> 0 <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
69 63 64 66 68 le2sqd 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ u e. RR ) -> ( ( abs ` u ) <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <-> ( ( abs ` u ) ^ 2 ) <_ ( ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ^ 2 ) ) )
70 31 adantr 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ u e. RR ) -> ( t ^ 2 ) e. RR )
71 resqcl 
 |-  ( u e. RR -> ( u ^ 2 ) e. RR )
72 71 adantl 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ u e. RR ) -> ( u ^ 2 ) e. RR )
73 29 adantr 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ u e. RR ) -> ( R ^ 2 ) e. RR )
74 70 72 73 leaddsub2d 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ u e. RR ) -> ( ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) <-> ( u ^ 2 ) <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
75 74 adantlr 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ u e. RR ) -> ( ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) <-> ( u ^ 2 ) <_ ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
76 60 69 75 3bitr4rd 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ u e. RR ) -> ( ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) <-> ( abs ` u ) <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) )
77 simpr 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ u e. RR ) -> u e. RR )
78 77 64 absled 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ u e. RR ) -> ( ( abs ` u ) <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <-> ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) )
79 rexr 
 |-  ( u e. RR -> u e. RR* )
80 79 adantl 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ u e. RR ) -> u e. RR* )
81 80 biantrurd 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ u e. RR ) -> ( ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) <-> ( u e. RR* /\ ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) ) )
82 76 78 81 3bitrd 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ u e. RR ) -> ( ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) <-> ( u e. RR* /\ ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) ) )
83 82 pm5.32da 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( ( u e. RR /\ ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) <-> ( u e. RR /\ ( u e. RR* /\ ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) ) ) )
84 simprl 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ ( u e. RR* /\ ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) ) -> u e. RR* )
85 48 adantr 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ ( u e. RR* /\ ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) ) -> ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR )
86 mnfxr 
 |-  -oo e. RR*
87 86 a1i 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ ( u e. RR* /\ ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) ) -> -oo e. RR* )
88 49 adantr 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ ( u e. RR* /\ ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) ) -> -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR )
89 88 rexrd 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ ( u e. RR* /\ ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) ) -> -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR* )
90 49 mnfltd 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> -oo < -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
91 90 adantr 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ ( u e. RR* /\ ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) ) -> -oo < -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
92 simprrl 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ ( u e. RR* /\ ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) ) -> -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u )
93 87 89 84 91 92 xrltletrd 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ ( u e. RR* /\ ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) ) -> -oo < u )
94 simprrr 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ ( u e. RR* /\ ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) ) -> u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) )
95 xrre 
 |-  ( ( ( u e. RR* /\ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) e. RR ) /\ ( -oo < u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) -> u e. RR )
96 84 85 93 94 95 syl22anc 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) /\ ( u e. RR* /\ ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) ) -> u e. RR )
97 96 ex 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( ( u e. RR* /\ ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) -> u e. RR ) )
98 97 pm4.71rd 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( ( u e. RR* /\ ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) <-> ( u e. RR /\ ( u e. RR* /\ ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) ) ) )
99 83 98 bitr4d 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> ( ( u e. RR /\ ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) <-> ( u e. RR* /\ ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) ) )
100 99 abbidv 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> { u | ( u e. RR /\ ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) } = { u | ( u e. RR* /\ ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) } )
101 df-rab 
 |-  { u e. RR* | ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) } = { u | ( u e. RR* /\ ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) }
102 100 101 eqtr4di 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> { u | ( u e. RR /\ ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) } = { u e. RR* | ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) <_ u /\ u <_ ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) } )
103 53 55 102 3eqtr4rd 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ ( abs ` t ) <_ R ) -> { u | ( u e. RR /\ ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) } = if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) )
104 40 39 ltnled 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( R < ( abs ` t ) <-> -. ( abs ` t ) <_ R ) )
105 104 biimprd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( -. ( abs ` t ) <_ R -> R < ( abs ` t ) ) )
106 105 imdistani 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ -. ( abs ` t ) <_ R ) -> ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R < ( abs ` t ) ) )
107 df-rab 
 |-  { u e. RR | ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) } = { u | ( u e. RR /\ ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) }
108 29 3ad2ant1 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R < ( abs ` t ) /\ u e. RR ) -> ( R ^ 2 ) e. RR )
109 31 3ad2ant1 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R < ( abs ` t ) /\ u e. RR ) -> ( t ^ 2 ) e. RR )
110 71 3ad2ant3 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R < ( abs ` t ) /\ u e. RR ) -> ( u ^ 2 ) e. RR )
111 109 110 readdcld 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R < ( abs ` t ) /\ u e. RR ) -> ( ( t ^ 2 ) + ( u ^ 2 ) ) e. RR )
112 40 39 43 42 lt2sqd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( R < ( abs ` t ) <-> ( R ^ 2 ) < ( ( abs ` t ) ^ 2 ) ) )
113 35 breq2d 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( ( R ^ 2 ) < ( ( abs ` t ) ^ 2 ) <-> ( R ^ 2 ) < ( t ^ 2 ) ) )
114 112 113 bitrd 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( R < ( abs ` t ) <-> ( R ^ 2 ) < ( t ^ 2 ) ) )
115 114 biimpa 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R < ( abs ` t ) ) -> ( R ^ 2 ) < ( t ^ 2 ) )
116 115 3adant3 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R < ( abs ` t ) /\ u e. RR ) -> ( R ^ 2 ) < ( t ^ 2 ) )
117 sqge0 
 |-  ( u e. RR -> 0 <_ ( u ^ 2 ) )
118 117 3ad2ant3 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R < ( abs ` t ) /\ u e. RR ) -> 0 <_ ( u ^ 2 ) )
119 109 110 addge01d 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R < ( abs ` t ) /\ u e. RR ) -> ( 0 <_ ( u ^ 2 ) <-> ( t ^ 2 ) <_ ( ( t ^ 2 ) + ( u ^ 2 ) ) ) )
120 118 119 mpbid 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R < ( abs ` t ) /\ u e. RR ) -> ( t ^ 2 ) <_ ( ( t ^ 2 ) + ( u ^ 2 ) ) )
121 108 109 111 116 120 ltletrd 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R < ( abs ` t ) /\ u e. RR ) -> ( R ^ 2 ) < ( ( t ^ 2 ) + ( u ^ 2 ) ) )
122 108 111 ltnled 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R < ( abs ` t ) /\ u e. RR ) -> ( ( R ^ 2 ) < ( ( t ^ 2 ) + ( u ^ 2 ) ) <-> -. ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) )
123 121 122 mpbid 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R < ( abs ` t ) /\ u e. RR ) -> -. ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) )
124 123 3expa 
 |-  ( ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R < ( abs ` t ) ) /\ u e. RR ) -> -. ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) )
125 124 ralrimiva 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R < ( abs ` t ) ) -> A. u e. RR -. ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) )
126 rabeq0 
 |-  ( { u e. RR | ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) } = (/) <-> A. u e. RR -. ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) )
127 125 126 sylibr 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R < ( abs ` t ) ) -> { u e. RR | ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) } = (/) )
128 107 127 eqtr3id 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ R < ( abs ` t ) ) -> { u | ( u e. RR /\ ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) } = (/) )
129 106 128 syl 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ -. ( abs ` t ) <_ R ) -> { u | ( u e. RR /\ ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) } = (/) )
130 iffalse 
 |-  ( -. ( abs ` t ) <_ R -> if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) = (/) )
131 130 adantl 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ -. ( abs ` t ) <_ R ) -> if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) = (/) )
132 129 131 eqtr4d 
 |-  ( ( ( R e. RR /\ 0 <_ R /\ t e. RR ) /\ -. ( abs ` t ) <_ R ) -> { u | ( u e. RR /\ ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) } = if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) )
133 103 132 pm2.61dan 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> { u | ( u e. RR /\ ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) } = if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) )
134 27 133 eqtr3d 
 |-  ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> { u | ( t e. RR /\ ( u e. RR /\ ( ( t ^ 2 ) + ( u ^ 2 ) ) <_ ( R ^ 2 ) ) ) } = if ( ( abs ` t ) <_ R , ( -u ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) )
135 24 134 eqtrid 
 |-  ( ( 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 ) ) ) ) , (/) ) )