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

Theorem areacirc 28949
Description: The area of a circle of radius is 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
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 4468 . . . . . . 7
31, 2eqtri 2483 . . . . . 6
4 simpl 457 . . . . . . . . 9
5 opelxpi 4988 . . . . . . . . . . 11
65adantr 465 . . . . . . . . . 10
76adantl 466 . . . . . . . . 9
84, 7eqeltrd 2542 . . . . . . . 8
98exlimivv 1690 . . . . . . 7
109abssi 3541 . . . . . 6
113, 10eqsstri 3500 . . . . 5
1211a1i 11 . . . 4
131areacirclem5 28948 . . . . . . 7
14 resqcl 12090 . . . . . . . . . . . . . . 15
15143ad2ant1 1009 . . . . . . . . . . . . . 14
16 resqcl 12090 . . . . . . . . . . . . . . 15
17163ad2ant3 1011 . . . . . . . . . . . . . 14
1815, 17resubcld 9913 . . . . . . . . . . . . 13
1918adantr 465 . . . . . . . . . . . 12
20 absresq 12949 . . . . . . . . . . . . . . . 16
21203ad2ant3 1011 . . . . . . . . . . . . . . 15
2221breq1d 4419 . . . . . . . . . . . . . 14
23 recn 9509 . . . . . . . . . . . . . . . . 17
2423abscld 13080 . . . . . . . . . . . . . . . 16
25243ad2ant3 1011 . . . . . . . . . . . . . . 15
26 simp1 988 . . . . . . . . . . . . . . 15
2723absge0d 13088 . . . . . . . . . . . . . . . 16
28273ad2ant3 1011 . . . . . . . . . . . . . . 15
29 simp2 989 . . . . . . . . . . . . . . 15
3025, 26, 28, 29le2sqd 12200 . . . . . . . . . . . . . 14
3115, 17subge0d 10066 . . . . . . . . . . . . . 14
3222, 30, 313bitr4d 285 . . . . . . . . . . . . 13
3332biimpa 484 . . . . . . . . . . . 12
3419, 33resqrcld 13062 . . . . . . . . . . 11
3534renegcld 9912 . . . . . . . . . 10
36 iccmbl 21447 . . . . . . . . . 10
3735, 34, 36syl2anc 661 . . . . . . . . 9
38 mblvol 21412 . . . . . . . . . . . 12
3937, 38syl 16 . . . . . . . . . . 11
4019, 33sqrge0d 13065 . . . . . . . . . . . . . 14
4134, 34, 40, 40addge0d 10052 . . . . . . . . . . . . 13
42 recn 9509 . . . . . . . . . . . . . . . . . . . . 21
4342sqcld 12163 . . . . . . . . . . . . . . . . . . . 20
44433ad2ant1 1009 . . . . . . . . . . . . . . . . . . 19
4523sqcld 12163 . . . . . . . . . . . . . . . . . . . 20
46453ad2ant3 1011 . . . . . . . . . . . . . . . . . . 19
4744, 46subcld 9856 . . . . . . . . . . . . . . . . . 18
4847sqrcld 13081 . . . . . . . . . . . . . . . . 17
4948adantr 465 . . . . . . . . . . . . . . . 16
5049, 49subnegd 9863 . . . . . . . . . . . . . . 15
5150breq2d 4421 . . . . . . . . . . . . . 14
5234, 35subge0d 10066 . . . . . . . . . . . . . 14
5351, 52bitr3d 255 . . . . . . . . . . . . 13
5441, 53mpbid 210 . . . . . . . . . . . 12
55 ovolicc 21405 . . . . . . . . . . . 12
5635, 34, 54, 55syl3anc 1219 . . . . . . . . . . 11
5739, 56eqtrd 2495 . . . . . . . . . 10
5834, 35resubcld 9913 . . . . . . . . . 10
5957, 58eqeltrd 2542 . . . . . . . . 9
60 volf 21411 . . . . . . . . . 10
61 ffn 5679 . . . . . . . . . 10
62 elpreima 5946 . . . . . . . . . 10
6360, 61, 62mp2b 10 . . . . . . . . 9
6437, 59, 63sylanbrc 664 . . . . . . . 8
65 0mbl 21421 . . . . . . . . . 10
66 mblvol 21412 . . . . . . . . . . . . 13
6765, 66ax-mp 5 . . . . . . . . . . . 12
68 ovol0 21375 . . . . . . . . . . . 12
6967, 68eqtri 2483 . . . . . . . . . . 11
70 0re 9523 . . . . . . . . . . 11
7169, 70eqeltri 2538 . . . . . . . . . 10
72 elpreima 5946 . . . . . . . . . . 11
7360, 61, 72mp2b 10 . . . . . . . . . 10
7465, 71, 73mpbir2an 911 . . . . . . . . 9
7574a1i 11 . . . . . . . 8
7664, 75ifclda 3937 . . . . . . 7
7713, 76eqeltrd 2542 . . . . . 6
78773expa 1188 . . . . 5
7978ralrimiva 2831 . . . 4
8013fveq2d 5817 . . . . . . 7
81803expa 1188 . . . . . 6
8281mpteq2dva 4495 . . . . 5
83 renegcl 9809 . . . . . . . 8
8483adantr 465 . . . . . . 7
85 simpl 457 . . . . . . 7
86 iccssre 11516 . . . . . . 7
8784, 85, 86syl2anc 661 . . . . . 6
88 rembl 21422 . . . . . . 7
8988a1i 11 . . . . . 6
90 fvex 5823 . . . . . . 7
9190a1i 11 . . . . . 6
92 eldif 3452 . . . . . . . . 9
93 3anass 969 . . . . . . . . . . . . . . 15
9493a1i 11 . . . . . . . . . . . . . 14
95833ad2ant1 1009 . . . . . . . . . . . . . . 15
96 elicc2 11499 . . . . . . . . . . . . . . 15
9795, 26, 96syl2anc 661 . . . . . . . . . . . . . 14
98 simp3 990 . . . . . . . . . . . . . . . 16
9998, 26absled 13075 . . . . . . . . . . . . . . 15
10098biantrurd 508 . . . . . . . . . . . . . . 15
10199, 100bitrd 253 . . . . . . . . . . . . . 14
10294, 97, 1013bitr4rd 286 . . . . . . . . . . . . 13
103102biimpd 207 . . . . . . . . . . . 12
104103con3d 133 . . . . . . . . . . 11
1051043expia 1190 . . . . . . . . . 10
106105impd 431 . . . . . . . . 9
10792, 106syl5bi 217 . . . . . . . 8
108107imp 429 . . . . . . 7
109 iffalse 3914 . . . . . . . . 9
110109fveq2d 5817 . . . . . . . 8
111110, 69syl6eq 2511 . . . . . . 7
112108, 111syl 16 . . . . . 6
11384, 85, 96syl2anc 661 . . . . . . . . . . . . 13
11499biimprd 223 . . . . . . . . . . . . . . . 16
115114expd 436 . . . . . . . . . . . . . . 15
1161153expia 1190 . . . . . . . . . . . . . 14
1171163impd 1202 . . . . . . . . . . . . 13
118113, 117sylbid 215 . . . . . . . . . . . 12
1191183impia 1185 . . . . . . . . . . 11
120 iftrue 3911 . . . . . . . . . . . 12
121120fveq2d 5817 . . . . . . . . . . 11
122119, 121syl 16 . . . . . . . . . 10
123143ad2ant1 1009 . . . . . . . . . . . . . . 15
12483, 86mpancom 669 . . . . . . . . . . . . . . . . . 18
125124sselda 3470 . . . . . . . . . . . . . . . . 17
1261253adant2 1007 . . . . . . . . . . . . . . . 16
127126resqcld 12191 . . . . . . . . . . . . . . 15
128123, 127resubcld 9913 . . . . . . . . . . . . . 14
12983, 96mpancom 669 . . . . . . . . . . . . . . . . 17
130129adantr 465 . . . . . . . . . . . . . . . 16
13130, 99, 223bitr3rd 284 . . . . . . . . . . . . . . . . . . . . 21
13231, 131bitrd 253 . . . . . . . . . . . . . . . . . . . 20
133132biimprd 223 . . . . . . . . . . . . . . . . . . 19
134133expd 436 . . . . . . . . . . . . . . . . . 18
1351343expia 1190 . . . . . . . . . . . . . . . . 17
1361353impd 1202 . . . . . . . . . . . . . . . 16
137130, 136sylbid 215 . . . . . . . . . . . . . . 15
1381373impia 1185 . . . . . . . . . . . . . 14
139128, 138resqrcld 13062 . . . . . . . . . . . . 13
140139renegcld 9912 . . . . . . . . . . . 12
141140, 139, 36syl2anc 661 . . . . . . . . . . 11
142141, 38syl 16 . . . . . . . . . 10
143128recnd 9549 . . . . . . . . . . . . 13
144143sqrcld 13081 . . . . . . . . . . . 12
145144, 144subnegd 9863 . . . . . . . . . . 11
146128, 138sqrge0d 13065 . . . . . . . . . . . . . 14
147139, 139, 146, 146addge0d 10052 . . . . . . . . . . . . 13
148145breq2d 4421 . . . . . . . . . . . . . 14
149139, 140subge0d 10066 . . . . . . . . . . . . . 14
150148, 149bitr3d 255 . . . . . . . . . . . . 13
151147, 150mpbid 210 . . . . . . . . . . . 12
152140, 139, 151, 55syl3anc 1219 . . . . . . . . . . 11
1531442timesd 10705 . . . . . . . . . . 11
154145, 152, 1533eqtr4d 2505 . . . . . . . . . 10
155122, 142, 1543eqtrd 2499 . . . . . . . . 9
1561553expa 1188 . . . . . . . 8
157156mpteq2dva 4495 . . . . . . 7
158 areacirclem3 28946 . . . . . . 7
159157, 158eqeltrd 2542 . . . . . 6
16087, 89, 91, 112, 159iblss2 21683 . . . . 5
16182, 160eqeltrd 2542 . . . 4
162 dmarea 22751 . . . 4
16312, 79, 161, 162syl3anbrc 1172 . . 3
164 areaval 22758 . . 3
165163, 164syl 16 . 2
166 elioore 11469 . . . . . 6
167133expa 1188 . . . . . 6
168166, 167sylan2 474 . . . . 5
169168fveq2d 5817 . . . 4
170169itgeq2dv 21659 . . 3
171 ioossre 11496 . . . . 5
172171a1i 11 . . . 4
173 eldif 3452 . . . . . 6
17483rexrd 9570 . . . . . . . . . . . . . 14
175 rexr 9566 . . . . . . . . . . . . . 14
176 elioo2 11480 . . . . . . . . . . . . . 14
177174, 175, 176syl2anc 661 . . . . . . . . . . . . 13
1781773ad2ant1 1009 . . . . . . . . . . . 12
17998biantrurd 508 . . . . . . . . . . . . 13
18098, 26absltd 13074 . . . . . . . . . . . . 13
181 3anass 969 . . . . . . . . . . . . . 14
182181a1i 11 . . . . . . . . . . . . 13
183179, 180, 1823bitr4rd 286 . . . . . . . . . . . 12
184178, 183bitrd 253 . . . . . . . . . . 11
185184notbid 294 . . . . . . . . . 10
18626, 25lenltd 9657 . . . . . . . . . 10