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

Theorem areacirc 28160
Description: The area of a circle of radius is 2. (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
Assertion
Ref Expression
areacirc
Distinct variable group:   , ,

Proof of Theorem areacirc
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 areacirc.1 . . . . . . 7
2 df-opab 4326 . . . . . . 7
31, 2eqtri 2442 . . . . . 6
4 simpl 447 . . . . . . . . 9
5 opelxpi 4842 . . . . . . . . . . 11
65adantr 455 . . . . . . . . . 10
76adantl 456 . . . . . . . . 9
84, 7eqeltrd 2496 . . . . . . . 8
98exlimivv 1680 . . . . . . 7
109abssi 3404 . . . . . 6
113, 10eqsstri 3363 . . . . 5
1211a1i 11 . . . 4
131areacirclem5 28159 . . . . . . 7
14 resqcl 11874 . . . . . . . . . . . . . . 15
15143ad2ant1 994 . . . . . . . . . . . . . 14
16 resqcl 11874 . . . . . . . . . . . . . . 15
17163ad2ant3 996 . . . . . . . . . . . . . 14
1815, 17resubcld 9722 . . . . . . . . . . . . 13
1918adantr 455 . . . . . . . . . . . 12
20 absresq 12732 . . . . . . . . . . . . . . . 16
21203ad2ant3 996 . . . . . . . . . . . . . . 15
2221breq1d 4277 . . . . . . . . . . . . . 14
23 recn 9318 . . . . . . . . . . . . . . . . 17
2423abscld 12863 . . . . . . . . . . . . . . . 16
25243ad2ant3 996 . . . . . . . . . . . . . . 15
26 simp1 973 . . . . . . . . . . . . . . 15
2723absge0d 12871 . . . . . . . . . . . . . . . 16
28273ad2ant3 996 . . . . . . . . . . . . . . 15
29 simp2 974 . . . . . . . . . . . . . . 15
3025, 26, 28, 29le2sqd 11984 . . . . . . . . . . . . . 14
3115, 17subge0d 9875 . . . . . . . . . . . . . 14
3222, 30, 313bitr4d 279 . . . . . . . . . . . . 13
3332biimpa 474 . . . . . . . . . . . 12
3419, 33resqrcld 12845 . . . . . . . . . . 11
3534renegcld 9721 . . . . . . . . . 10
36 iccmbl 20747 . . . . . . . . . 10
3735, 34, 36syl2anc 646 . . . . . . . . 9
38 mblvol 20713 . . . . . . . . . . . 12
3937, 38syl 16 . . . . . . . . . . 11
4019, 33sqrge0d 12848 . . . . . . . . . . . . . 14
4134, 34, 40, 40addge0d 9861 . . . . . . . . . . . . 13
42 recn 9318 . . . . . . . . . . . . . . . . . . . . 21
4342sqcld 11947 . . . . . . . . . . . . . . . . . . . 20
44433ad2ant1 994 . . . . . . . . . . . . . . . . . . 19
4523sqcld 11947 . . . . . . . . . . . . . . . . . . . 20
46453ad2ant3 996 . . . . . . . . . . . . . . . . . . 19
4744, 46subcld 9665 . . . . . . . . . . . . . . . . . 18
4847sqrcld 12864 . . . . . . . . . . . . . . . . 17
4948adantr 455 . . . . . . . . . . . . . . . 16
5049, 49subnegd 9672 . . . . . . . . . . . . . . 15
5150breq2d 4279 . . . . . . . . . . . . . 14
5234, 35subge0d 9875 . . . . . . . . . . . . . 14
5351, 52bitr3d 249 . . . . . . . . . . . . 13
5441, 53mpbid 204 . . . . . . . . . . . 12
55 ovolicc 20706 . . . . . . . . . . . 12
5635, 34, 54, 55syl3anc 1203 . . . . . . . . . . 11
5739, 56eqtrd 2454 . . . . . . . . . 10
5834, 35resubcld 9722 . . . . . . . . . 10
5957, 58eqeltrd 2496 . . . . . . . . 9
60 volf 20712 . . . . . . . . . 10
61 ffn 5529 . . . . . . . . . 10
62 elpreima 5793 . . . . . . . . . 10
6360, 61, 62mp2b 10 . . . . . . . . 9
6437, 59, 63sylanbrc 649 . . . . . . . 8
65 0mbl 20721 . . . . . . . . . 10
66 mblvol 20713 . . . . . . . . . . . . 13
6765, 66ax-mp 5 . . . . . . . . . . . 12
68 ovol0 20676 . . . . . . . . . . . 12
6967, 68eqtri 2442 . . . . . . . . . . 11
70 0re 9332 . . . . . . . . . . 11
7169, 70eqeltri 2492 . . . . . . . . . 10
72 elpreima 5793 . . . . . . . . . . 11
7360, 61, 72mp2b 10 . . . . . . . . . 10
7465, 71, 73mpbir2an 896 . . . . . . . . 9
7574a1i 11 . . . . . . . 8
7664, 75ifclda 3798 . . . . . . 7
7713, 76eqeltrd 2496 . . . . . 6
78773expa 1172 . . . . 5
7978ralrimiva 2778 . . . 4
8013fveq2d 5665 . . . . . . 7
81803expa 1172 . . . . . 6
8281mpteq2dva 4353 . . . . 5
83 renegcl 9618 . . . . . . . 8
8483adantr 455 . . . . . . 7
85 simpl 447 . . . . . . 7
86 iccssre 11322 . . . . . . 7
8784, 85, 86syl2anc 646 . . . . . 6
88 rembl 20722 . . . . . . 7
8988a1i 11 . . . . . 6
90 fvex 5671 . . . . . . 7
9190a1i 11 . . . . . 6
92 eldif 3315 . . . . . . . . 9
93 3anass 954 . . . . . . . . . . . . . . 15
9493a1i 11 . . . . . . . . . . . . . 14
95833ad2ant1 994 . . . . . . . . . . . . . . 15
96 elicc2 11305 . . . . . . . . . . . . . . 15
9795, 26, 96syl2anc 646 . . . . . . . . . . . . . 14
98 simp3 975 . . . . . . . . . . . . . . . 16
9998, 26absled 12858 . . . . . . . . . . . . . . 15
10098biantrurd 498 . . . . . . . . . . . . . . 15
10199, 100bitrd 247 . . . . . . . . . . . . . 14
10294, 97, 1013bitr4rd 280 . . . . . . . . . . . . 13
103102biimpd 201 . . . . . . . . . . . 12
104103con3d 128 . . . . . . . . . . 11
1051043expia 1174 . . . . . . . . . 10
106105imp3a 424 . . . . . . . . 9
10792, 106syl5bi 211 . . . . . . . 8
108107imp 422 . . . . . . 7
109 iffalse 3776 . . . . . . . . 9
110109fveq2d 5665 . . . . . . . 8
111110, 69syl6eq 2470 . . . . . . 7
112108, 111syl 16 . . . . . 6
11384, 85, 96syl2anc 646 . . . . . . . . . . . . 13
11499biimprd 217 . . . . . . . . . . . . . . . 16
115114exp3a 429 . . . . . . . . . . . . . . 15
1161153expia 1174 . . . . . . . . . . . . . 14
1171163impd 1186 . . . . . . . . . . . . 13
118113, 117sylbid 209 . . . . . . . . . . . 12
1191183impia 1169 . . . . . . . . . . 11
120 iftrue 3774 . . . . . . . . . . . 12
121120fveq2d 5665 . . . . . . . . . . 11
122119, 121syl 16 . . . . . . . . . 10
123143ad2ant1 994 . . . . . . . . . . . . . . 15
12483, 86mpancom 654 . . . . . . . . . . . . . . . . . 18
125124sselda 3333 . . . . . . . . . . . . . . . . 17
1261253adant2 992 . . . . . . . . . . . . . . . 16
127126resqcld 11975 . . . . . . . . . . . . . . 15
128123, 127resubcld 9722 . . . . . . . . . . . . . 14
12983, 96mpancom 654 . . . . . . . . . . . . . . . . 17
130129adantr 455 . . . . . . . . . . . . . . . 16
13130, 99, 223bitr3rd 278 . . . . . . . . . . . . . . . . . . . . 21
13231, 131bitrd 247 . . . . . . . . . . . . . . . . . . . 20
133132biimprd 217 . . . . . . . . . . . . . . . . . . 19
134133exp3a 429 . . . . . . . . . . . . . . . . . 18
1351343expia 1174 . . . . . . . . . . . . . . . . 17
1361353impd 1186 . . . . . . . . . . . . . . . 16
137130, 136sylbid 209 . . . . . . . . . . . . . . 15
1381373impia 1169 . . . . . . . . . . . . . 14
139128, 138resqrcld 12845 . . . . . . . . . . . . 13
140139renegcld 9721 . . . . . . . . . . . 12
141140, 139, 36syl2anc 646 . . . . . . . . . . 11
142141, 38syl 16 . . . . . . . . . 10
143128recnd 9358 . . . . . . . . . . . . 13
144143sqrcld 12864 . . . . . . . . . . . 12
145144, 144subnegd 9672 . . . . . . . . . . 11
146128, 138sqrge0d 12848 . . . . . . . . . . . . . 14
147139, 139, 146, 146addge0d 9861 . . . . . . . . . . . . 13
148145breq2d 4279 . . . . . . . . . . . . . 14
149139, 140subge0d 9875 . . . . . . . . . . . . . 14
150148, 149bitr3d 249 . . . . . . . . . . . . 13
151147, 150mpbid 204 . . . . . . . . . . . 12
152140, 139, 151, 55syl3anc 1203 . . . . . . . . . . 11
1531442timesd 10513 . . . . . . . . . . 11
154145, 152, 1533eqtr4d 2464 . . . . . . . . . 10
155122, 142, 1543eqtrd 2458 . . . . . . . . 9
1561553expa 1172 . . . . . . . 8
157156mpteq2dva 4353 . . . . . . 7
158 areacirclem3 28157 . . . . . . 7
159157, 158eqeltrd 2496 . . . . . 6
16087, 89, 91, 112, 159iblss2 20983 . . . . 5
16182, 160eqeltrd 2496 . . . 4
162 dmarea 22092 . . . 4
16312, 79, 161, 162syl3anbrc 1157 . . 3
164 areaval 22099 . . 3
165163, 164syl 16 . 2
166 elioore 11275 . . . . . 6
167133expa 1172 . . . . . 6
168166, 167sylan2 464 . . . . 5
169168fveq2d 5665 . . . 4
170169itgeq2dv 20959 . . 3
171 ioossre 11302 . . . . 5
172171a1i 11 . . . 4
173 eldif 3315 . . . . . 6
17483rexrd 9379 . . . . . . . . . . . . . 14
175 rexr 9375 . . . . . . . . . . . . . 14
176 elioo2 11286 . . . . . . . . . . . . . 14
177174, 175, 176syl2anc 646 . . . . . . . . . . . . 13
1781773ad2ant1 994 . . . . . . . . . . . 12
17998biantrurd 498 . . . . . . . . . . . . 13
18098, 26absltd 12857 . . . . . . . . . . . . 13
181 3anass 954 . . . . . . . . . . . . . 14
182181a1i 11 . . . . . . . . . . . . 13
183179, 180, 1823bitr4rd 280 . . . . . . . . . . . 12
184178, 183bitrd 247 . . . . . . . . . . 11
185184notbid 288 . . . . . . . . . 10
18626, 25lenltd 9466 . . . . . . . . . 10 <