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 30087

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 5324	. . 3 $/\$ $/\$
3		vex 3098	. . . 4
4		imasng 5349	. . . 4 $/\$ $/\$ $/\$ $/\$
5	3, 4	ax-mp 5	. . 3 $/\$ $/\$ $/\$ $/\$
6		df-br 4438	. . . . 5 $/\$ $/\$ $/\$ $/\$
7		vex 3098	. . . . . 6
8		eleq1 2515	. . . . . . . 8
9	8	anbi1d 704	. . . . . . 7 $/\$ $/\$
10		oveq1 6288	. . . . . . . . 9
11	10	oveq1d 6296	. . . . . . . 8
12	11	breq1d 4447	. . . . . . 7
13	9, 12	anbi12d 710	. . . . . 6 $/\$ $/\$ $/\$ $/\$
14		eleq1 2515	. . . . . . . 8
15	14	anbi2d 703	. . . . . . 7 $/\$ $/\$
16		oveq1 6288	. . . . . . . . 9
17	16	oveq2d 6297	. . . . . . . 8
18	17	breq1d 4447	. . . . . . 7
19	15, 18	anbi12d 710	. . . . . 6 $/\$ $/\$ $/\$ $/\$
20	3, 7, 13, 19	opelopab 4759	. . . . 5 $/\$ $/\$ $/\$ $/\$
21		anass 649	. . . . 5 $/\$ $/\$ $/\$ $/\$
22	6, 20, 21	3bitri 271	. . . 4 $/\$ $/\$ $/\$ $/\$
23	22	abbii 2577	. . 3 $/\$ $/\$ $/\$ $/\$
24	2, 5, 23	3eqtri 2476	. 2 $/\$ $/\$
25		simp3 999	. . . . 5 $/\$ $/\$
26	25	biantrurd 508	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
27	26	abbidv 2579	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
28		resqcl 12217	. . . . . . . . . . . 12
29	28	3ad2ant1 1018	. . . . . . . . . . 11 $/\$ $/\$
30		resqcl 12217	. . . . . . . . . . . 12
31	30	3ad2ant3 1020	. . . . . . . . . . 11 $/\$ $/\$
32	29, 31	resubcld 9994	. . . . . . . . . 10 $/\$ $/\$
33	32	adantr 465	. . . . . . . . 9 $/\$ $/\$ $/\$
34		absresq 13117	. . . . . . . . . . . . 13
35	34	3ad2ant3 1020	. . . . . . . . . . . 12 $/\$ $/\$
36	35	breq1d 4447	. . . . . . . . . . 11 $/\$ $/\$
37		recn 9585	. . . . . . . . . . . . . 14
38	37	abscld 13249	. . . . . . . . . . . . 13
39	38	3ad2ant3 1020	. . . . . . . . . . . 12 $/\$ $/\$
40		simp1 997	. . . . . . . . . . . 12 $/\$ $/\$
41	37	absge0d 13257	. . . . . . . . . . . . 13
42	41	3ad2ant3 1020	. . . . . . . . . . . 12 $/\$ $/\$
43		simp2 998	. . . . . . . . . . . 12 $/\$ $/\$
44	39, 40, 42, 43	le2sqd 12327	. . . . . . . . . . 11 $/\$ $/\$
45	29, 31	subge0d 10149	. . . . . . . . . . 11 $/\$ $/\$
46	36, 44, 45	3bitr4d 285	. . . . . . . . . 10 $/\$ $/\$
47	46	biimpa 484	. . . . . . . . 9 $/\$ $/\$ $/\$
48	33, 47	resqrtcld 13231	. . . . . . . 8 $/\$ $/\$ $/\$
49	48	renegcld 9993	. . . . . . 7 $/\$ $/\$ $/\$
50	49	rexrd 9646	. . . . . 6 $/\$ $/\$ $/\$
51	48	rexrd 9646	. . . . . 6 $/\$ $/\$ $/\$
52		iccval 11579	. . . . . 6 $/\$ $/\$
53	50, 51, 52	syl2anc 661	. . . . 5 $/\$ $/\$ $/\$ $/\$
54		iftrue 3932	. . . . . 6
55	54	adantl 466	. . . . 5 $/\$ $/\$ $/\$
56		absresq 13117	. . . . . . . . . . . 12
57	32	recnd 9625	. . . . . . . . . . . . . 14 $/\$ $/\$
58	57	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
59	58	sqsqrtd 13252	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
60	56, 59	breqan12rd 4453	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
61		recn 9585	. . . . . . . . . . . . . 14
62	61	abscld 13249	. . . . . . . . . . . . 13
63	62	adantl 466	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
64	48	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
65	61	absge0d 13257	. . . . . . . . . . . . 13
66	65	adantl 466	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
67	33, 47	sqrtge0d 13234	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
68	67	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
69	63, 64, 66, 68	le2sqd 12327	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
70	31	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
71		resqcl 12217	. . . . . . . . . . . . . 14
72	71	adantl 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
73	29	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
74	70, 72, 73	leaddsub2d 10161	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
75	74	adantlr 714	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
76	60, 69, 75	3bitr4rd 286	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
77		simpr 461	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
78	77, 64	absled 13244	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
79		rexr 9642	. . . . . . . . . . . 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 756	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85	48	adantr 465	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86		mnfxr 11334	. . . . . . . . . . . . 13
87	86	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88	49	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89	88	rexrd 9646	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90		mnflt 11344	. . . . . . . . . . . . . 14
91	49, 90	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
92	91	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93		simprrl 765	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94	87, 89, 84, 92, 93	xrltletrd 11375	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95		simprrr 766	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96		xrre 11381	. . . . . . . . . . 11 $/\$ $/\$ $/\$
97	84, 85, 94, 95, 96	syl22anc 1230	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	97	ex 434	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
99	98	pm4.71rd 635	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100	83, 99	bitr4d 256	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101	100	abbidv 2579	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		df-rab 2802	. . . . . 6 $/\$ $/\$ $/\$
103	101, 102	syl6eqr 2502	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
104	53, 55, 103	3eqtr4rd 2495	. . . 4 $/\$ $/\$ $/\$ $/\$
105	40, 39	ltnled 9735	. . . . . . . 8 $/\$ $/\$
106	105	biimprd 223	. . . . . . 7 $/\$ $/\$
107	106	imdistani 690	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		df-rab 2802	. . . . . . 7 $/\$
109	29	3ad2ant1 1018	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
110	31	3ad2ant1 1018	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
111	71	3ad2ant3 1020	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
112	110, 111	readdcld 9626	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
113	40, 39, 43, 42	lt2sqd 12326	. . . . . . . . . . . . . . 15 $/\$ $/\$
114	35	breq2d 4449	. . . . . . . . . . . . . . 15 $/\$ $/\$
115	113, 114	bitrd 253	. . . . . . . . . . . . . 14 $/\$ $/\$
116	115	biimpa 484	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117	116	3adant3 1017	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
118		sqge0 12226	. . . . . . . . . . . . . 14
119	118	3ad2ant3 1020	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
120	110, 111	addge01d 10147	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
121	119, 120	mpbid 210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
122	109, 110, 112, 117, 121	ltletrd 9745	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
123	109, 112	ltnled 9735	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
124	122, 123	mpbid 210	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
125	124	3expa 1197	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
126	125	ralrimiva 2857	. . . . . . . 8 $/\$ $/\$ $/\$
127		rabeq0 3793	. . . . . . . 8
128	126, 127	sylibr 212	. . . . . . 7 $/\$ $/\$ $/\$
129	108, 128	syl5eqr 2498	. . . . . 6 $/\$ $/\$ $/\$ $/\$
130	107, 129	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$
131		iffalse 3935	. . . . . 6
132	131	adantl 466	. . . . 5 $/\$ $/\$ $/\$
133	130, 132	eqtr4d 2487	. . . 4 $/\$ $/\$ $/\$ $/\$
134	104, 133	pm2.61dan 791	. . 3 $/\$ $/\$ $/\$
135	27, 134	eqtr3d 2486	. 2 $/\$ $/\$ $/\$ $/\$
136	24, 135	syl5eq 2496	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1383

wcel 1804

cab 2428

wral 2793

crab 2797

cvv 3095

c0 3770

cif 3926

csn 4014

cop 4020 class class class wbr 4437

copab 4494

cima 4992

cfv 5578 (class class class)co 6281

cc 9493

cr 9494

cc0 9495

caddc 9498

cmnf 9629

cxr 9630

clt 9631

cle 9632

cmin 9810

cneg 9811

c2 10592

cicc 11543

cexp 12148

csqrt 13048

cabs 13049

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-8 1806 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-sep 4558 ax-nul 4566 ax-pow 4615 ax-pr 4676 ax-un 6577 ax-cnex 9551 ax-resscn 9552 ax-1cn 9553 ax-icn 9554 ax-addcl 9555 ax-addrcl 9556 ax-mulcl 9557 ax-mulrcl 9558 ax-mulcom 9559 ax-addass 9560 ax-mulass 9561 ax-distr 9562 ax-i2m1 9563 ax-1ne0 9564 ax-1rid 9565 ax-rnegex 9566 ax-rrecex 9567 ax-cnre 9568 ax-pre-lttri 9569 ax-pre-lttrn 9570 ax-pre-ltadd 9571 ax-pre-mulgt0 9572 ax-pre-sup 9573

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 975 df-3an 976 df-tru 1386 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-nel 2641 df-ral 2798 df-rex 2799 df-reu 2800 df-rmo 2801 df-rab 2802 df-v 3097 df-sbc 3314 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3771 df-if 3927 df-pw 3999 df-sn 4015 df-pr 4017 df-tp 4019 df-op 4021 df-uni 4235 df-iun 4317 df-br 4438 df-opab 4496 df-mpt 4497 df-tr 4531 df-eprel 4781 df-id 4785 df-po 4790 df-so 4791 df-fr 4828 df-we 4830 df-ord 4871 df-on 4872 df-lim 4873 df-suc 4874 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-res 5001 df-ima 5002 df-iota 5541 df-fun 5580 df-fn 5581 df-f 5582 df-f1 5583 df-fo 5584 df-f1o 5585 df-fv 5586 df-riota 6242 df-ov 6284 df-oprab 6285 df-mpt2 6286 df-om 6686 df-2nd 6786 df-recs 7044 df-rdg 7078 df-er 7313 df-en 7519 df-dom 7520 df-sdom 7521 df-sup 7903 df-pnf 9633 df-mnf 9634 df-xr 9635 df-ltxr 9636 df-le 9637 df-sub 9812 df-neg 9813 df-div 10214 df-nn 10544 df-2 10601 df-3 10602 df-n0 10803 df-z 10872 df-uz 11093 df-rp 11232 df-icc 11547 df-seq 12090 df-exp 12149 df-cj 12914 df-re 12915 df-im 12916 df-sqrt 13050 df-abs 13051

This theorem is referenced by: areacirc 30088

W3C validator