areacirclem5 - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > areacirclem5		Structured version Unicode version

Theorem areacirclem5 29688

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.)

**Hypothesis**
Ref	Expression
areacirc.1	$/\$ $/\$

**Assertion**
Ref	Expression
areacirclem5	$/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

Proof of Theorem areacirclem5 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		areacirc.1	. . . 4 $/\$ $/\$
2	1	imaeq1i 5332	. . 3 $/\$ $/\$
3		vex 3116	. . . 4
4		imasng 5357	. . . 4 $/\$ $/\$ $/\$ $/\$
5	3, 4	ax-mp 5	. . 3 $/\$ $/\$ $/\$ $/\$
6		df-br 4448	. . . . 5 $/\$ $/\$ $/\$ $/\$
7		vex 3116	. . . . . 6
8		eleq1 2539	. . . . . . . 8
9	8	anbi1d 704	. . . . . . 7 $/\$ $/\$
10		oveq1 6289	. . . . . . . . 9
11	10	oveq1d 6297	. . . . . . . 8
12	11	breq1d 4457	. . . . . . 7
13	9, 12	anbi12d 710	. . . . . 6 $/\$ $/\$ $/\$ $/\$
14		eleq1 2539	. . . . . . . 8
15	14	anbi2d 703	. . . . . . 7 $/\$ $/\$
16		oveq1 6289	. . . . . . . . 9
17	16	oveq2d 6298	. . . . . . . 8
18	17	breq1d 4457	. . . . . . 7
19	15, 18	anbi12d 710	. . . . . 6 $/\$ $/\$ $/\$ $/\$
20	3, 7, 13, 19	opelopab 4769	. . . . 5 $/\$ $/\$ $/\$ $/\$
21		anass 649	. . . . 5 $/\$ $/\$ $/\$ $/\$
22	6, 20, 21	3bitri 271	. . . 4 $/\$ $/\$ $/\$ $/\$
23	22	abbii 2601	. . 3 $/\$ $/\$ $/\$ $/\$
24	2, 5, 23	3eqtri 2500	. 2 $/\$ $/\$
25		simp3 998	. . . . 5 $/\$ $/\$
26	25	biantrurd 508	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
27	26	abbidv 2603	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
28		resqcl 12199	. . . . . . . . . . . 12
29	28	3ad2ant1 1017	. . . . . . . . . . 11 $/\$ $/\$
30		resqcl 12199	. . . . . . . . . . . 12
31	30	3ad2ant3 1019	. . . . . . . . . . 11 $/\$ $/\$
32	29, 31	resubcld 9983	. . . . . . . . . 10 $/\$ $/\$
33	32	adantr 465	. . . . . . . . 9 $/\$ $/\$ $/\$
34		absresq 13094	. . . . . . . . . . . . 13
35	34	3ad2ant3 1019	. . . . . . . . . . . 12 $/\$ $/\$
36	35	breq1d 4457	. . . . . . . . . . 11 $/\$ $/\$
37		recn 9578	. . . . . . . . . . . . . 14
38	37	abscld 13226	. . . . . . . . . . . . 13
39	38	3ad2ant3 1019	. . . . . . . . . . . 12 $/\$ $/\$
40		simp1 996	. . . . . . . . . . . 12 $/\$ $/\$
41	37	absge0d 13234	. . . . . . . . . . . . 13
42	41	3ad2ant3 1019	. . . . . . . . . . . 12 $/\$ $/\$
43		simp2 997	. . . . . . . . . . . 12 $/\$ $/\$
44	39, 40, 42, 43	le2sqd 12309	. . . . . . . . . . 11 $/\$ $/\$
45	29, 31	subge0d 10138	. . . . . . . . . . 11 $/\$ $/\$
46	36, 44, 45	3bitr4d 285	. . . . . . . . . 10 $/\$ $/\$
47	46	biimpa 484	. . . . . . . . 9 $/\$ $/\$ $/\$
48	33, 47	resqrtcld 13208	. . . . . . . 8 $/\$ $/\$ $/\$
49	48	renegcld 9982	. . . . . . 7 $/\$ $/\$ $/\$
50	49	rexrd 9639	. . . . . 6 $/\$ $/\$ $/\$
51	48	rexrd 9639	. . . . . 6 $/\$ $/\$ $/\$
52		iccval 11564	. . . . . 6 $/\$ $/\$
53	50, 51, 52	syl2anc 661	. . . . 5 $/\$ $/\$ $/\$ $/\$
54		iftrue 3945	. . . . . 6
55	54	adantl 466	. . . . 5 $/\$ $/\$ $/\$
56		absresq 13094	. . . . . . . . . . . 12
57	32	recnd 9618	. . . . . . . . . . . . . 14 $/\$ $/\$
58	57	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
59	58	sqsqrtd 13229	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
60	56, 59	breqan12rd 4463	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
61		recn 9578	. . . . . . . . . . . . . 14
62	61	abscld 13226	. . . . . . . . . . . . 13
63	62	adantl 466	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
64	48	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
65	61	absge0d 13234	. . . . . . . . . . . . 13
66	65	adantl 466	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
67	33, 47	sqrtge0d 13211	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
68	67	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
69	63, 64, 66, 68	le2sqd 12309	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
70	31	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
71		resqcl 12199	. . . . . . . . . . . . . 14
72	71	adantl 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
73	29	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
74	70, 72, 73	leaddsub2d 10150	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
75	74	adantlr 714	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
76	60, 69, 75	3bitr4rd 286	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
77		simpr 461	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
78	77, 64	absled 13221	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
79		rexr 9635	. . . . . . . . . . . 12
80	79	adantl 466	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
81	80	biantrurd 508	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
82	76, 78, 81	3bitrd 279	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
83	82	pm5.32da 641	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
84		simprl 755	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85	48	adantr 465	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86		mnfxr 11319	. . . . . . . . . . . . 13
87	86	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88	49	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89	88	rexrd 9639	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90		mnflt 11329	. . . . . . . . . . . . . 14
91	49, 90	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
92	91	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93		simprrl 763	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94	87, 89, 84, 92, 93	xrltletrd 11360	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95		simprrr 764	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96		xrre 11366	. . . . . . . . . . 11 $/\$ $/\$ $/\$
97	84, 85, 94, 95, 96	syl22anc 1229	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	97	ex 434	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
99	98	pm4.71rd 635	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100	83, 99	bitr4d 256	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101	100	abbidv 2603	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		df-rab 2823	. . . . . 6 $/\$ $/\$ $/\$
103	101, 102	syl6eqr 2526	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
104	53, 55, 103	3eqtr4rd 2519	. . . 4 $/\$ $/\$ $/\$ $/\$
105	40, 39	ltnled 9727	. . . . . . . 8 $/\$ $/\$
106	105	biimprd 223	. . . . . . 7 $/\$ $/\$
107	106	imdistani 690	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		df-rab 2823	. . . . . . 7 $/\$
109	29	3ad2ant1 1017	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
110	31	3ad2ant1 1017	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
111	71	3ad2ant3 1019	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
112	110, 111	readdcld 9619	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
113	40, 39, 43, 42	lt2sqd 12308	. . . . . . . . . . . . . . 15 $/\$ $/\$
114	35	breq2d 4459	. . . . . . . . . . . . . . 15 $/\$ $/\$
115	113, 114	bitrd 253	. . . . . . . . . . . . . 14 $/\$ $/\$
116	115	biimpa 484	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117	116	3adant3 1016	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
118		sqge0 12208	. . . . . . . . . . . . . 14
119	118	3ad2ant3 1019	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
120	110, 111	addge01d 10136	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
121	119, 120	mpbid 210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
122	109, 110, 112, 117, 121	ltletrd 9737	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
123	109, 112	ltnled 9727	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
124	122, 123	mpbid 210	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
125	124	3expa 1196	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
126	125	ralrimiva 2878	. . . . . . . 8 $/\$ $/\$ $/\$
127		rabeq0 3807	. . . . . . . 8
128	126, 127	sylibr 212	. . . . . . 7 $/\$ $/\$ $/\$
129	108, 128	syl5eqr 2522	. . . . . 6 $/\$ $/\$ $/\$ $/\$
130	107, 129	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$
131		iffalse 3948	. . . . . 6
132	131	adantl 466	. . . . 5 $/\$ $/\$ $/\$
133	130, 132	eqtr4d 2511	. . . 4 $/\$ $/\$ $/\$ $/\$
134	104, 133	pm2.61dan 789	. . 3 $/\$ $/\$ $/\$
135	27, 134	eqtr3d 2510	. 2 $/\$ $/\$ $/\$ $/\$
136	24, 135	syl5eq 2520	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 973

wceq 1379

wcel 1767

cab 2452

wral 2814

crab 2818

cvv 3113

c0 3785

cif 3939

csn 4027

cop 4033 class class class wbr 4447

copab 4504

cima 5002

cfv 5586 (class class class)co 6282

cc 9486

cr 9487

cc0 9488

caddc 9491

cmnf 9622

cxr 9623

clt 9624

cle 9625

cmin 9801

cneg 9802

c2 10581

cicc 11528

cexp 12130

csqrt 13025

cabs 13026

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565 ax-pre-sup 9566

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-om 6679 df-2nd 6782 df-recs 7039 df-rdg 7073 df-er 7308 df-en 7514 df-dom 7515 df-sdom 7516 df-sup 7897 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-div 10203 df-nn 10533 df-2 10590 df-3 10591 df-n0 10792 df-z 10861 df-uz 11079 df-rp 11217 df-icc 11532 df-seq 12072 df-exp 12131 df-cj 12891 df-re 12892 df-im 12893 df-sqrt 13027 df-abs 13028

This theorem is referenced by: areacirc 29689

W3C validator