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 31740

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 5176	. . 3 $/\$ $/\$
3		vex 3081	. . . 4
4		imasng 5201	. . . 4 $/\$ $/\$ $/\$ $/\$
5	3, 4	ax-mp 5	. . 3 $/\$ $/\$ $/\$ $/\$
6		df-br 4418	. . . . 5 $/\$ $/\$ $/\$ $/\$
7		vex 3081	. . . . . 6
8		eleq1 2492	. . . . . . . 8
9	8	anbi1d 709	. . . . . . 7 $/\$ $/\$
10		oveq1 6303	. . . . . . . . 9
11	10	oveq1d 6311	. . . . . . . 8
12	11	breq1d 4427	. . . . . . 7
13	9, 12	anbi12d 715	. . . . . 6 $/\$ $/\$ $/\$ $/\$
14		eleq1 2492	. . . . . . . 8
15	14	anbi2d 708	. . . . . . 7 $/\$ $/\$
16		oveq1 6303	. . . . . . . . 9
17	16	oveq2d 6312	. . . . . . . 8
18	17	breq1d 4427	. . . . . . 7
19	15, 18	anbi12d 715	. . . . . 6 $/\$ $/\$ $/\$ $/\$
20	3, 7, 13, 19	opelopab 4734	. . . . 5 $/\$ $/\$ $/\$ $/\$
21		anass 653	. . . . 5 $/\$ $/\$ $/\$ $/\$
22	6, 20, 21	3bitri 274	. . . 4 $/\$ $/\$ $/\$ $/\$
23	22	abbii 2554	. . 3 $/\$ $/\$ $/\$ $/\$
24	2, 5, 23	3eqtri 2453	. 2 $/\$ $/\$
25		simp3 1007	. . . . 5 $/\$ $/\$
26	25	biantrurd 510	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
27	26	abbidv 2556	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
28		resqcl 12328	. . . . . . . . . . . 12
29	28	3ad2ant1 1026	. . . . . . . . . . 11 $/\$ $/\$
30		resqcl 12328	. . . . . . . . . . . 12
31	30	3ad2ant3 1028	. . . . . . . . . . 11 $/\$ $/\$
32	29, 31	resubcld 10036	. . . . . . . . . 10 $/\$ $/\$
33	32	adantr 466	. . . . . . . . 9 $/\$ $/\$ $/\$
34		absresq 13333	. . . . . . . . . . . . 13
35	34	3ad2ant3 1028	. . . . . . . . . . . 12 $/\$ $/\$
36	35	breq1d 4427	. . . . . . . . . . 11 $/\$ $/\$
37		recn 9618	. . . . . . . . . . . . . 14
38	37	abscld 13465	. . . . . . . . . . . . 13
39	38	3ad2ant3 1028	. . . . . . . . . . . 12 $/\$ $/\$
40		simp1 1005	. . . . . . . . . . . 12 $/\$ $/\$
41	37	absge0d 13473	. . . . . . . . . . . . 13
42	41	3ad2ant3 1028	. . . . . . . . . . . 12 $/\$ $/\$
43		simp2 1006	. . . . . . . . . . . 12 $/\$ $/\$
44	39, 40, 42, 43	le2sqd 12437	. . . . . . . . . . 11 $/\$ $/\$
45	29, 31	subge0d 10192	. . . . . . . . . . 11 $/\$ $/\$
46	36, 44, 45	3bitr4d 288	. . . . . . . . . 10 $/\$ $/\$
47	46	biimpa 486	. . . . . . . . 9 $/\$ $/\$ $/\$
48	33, 47	resqrtcld 13447	. . . . . . . 8 $/\$ $/\$ $/\$
49	48	renegcld 10035	. . . . . . 7 $/\$ $/\$ $/\$
50	49	rexrd 9679	. . . . . 6 $/\$ $/\$ $/\$
51	48	rexrd 9679	. . . . . 6 $/\$ $/\$ $/\$
52		iccval 11664	. . . . . 6 $/\$ $/\$
53	50, 51, 52	syl2anc 665	. . . . 5 $/\$ $/\$ $/\$ $/\$
54		iftrue 3912	. . . . . 6
55	54	adantl 467	. . . . 5 $/\$ $/\$ $/\$
56		absresq 13333	. . . . . . . . . . . 12
57	32	recnd 9658	. . . . . . . . . . . . . 14 $/\$ $/\$
58	57	adantr 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
59	58	sqsqrtd 13468	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
60	56, 59	breqan12rd 4433	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
61		recn 9618	. . . . . . . . . . . . . 14
62	61	abscld 13465	. . . . . . . . . . . . 13
63	62	adantl 467	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
64	48	adantr 466	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
65	61	absge0d 13473	. . . . . . . . . . . . 13
66	65	adantl 467	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
67	33, 47	sqrtge0d 13450	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
68	67	adantr 466	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
69	63, 64, 66, 68	le2sqd 12437	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
70	31	adantr 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
71		resqcl 12328	. . . . . . . . . . . . . 14
72	71	adantl 467	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
73	29	adantr 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
74	70, 72, 73	leaddsub2d 10204	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
75	74	adantlr 719	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
76	60, 69, 75	3bitr4rd 289	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
77		simpr 462	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
78	77, 64	absled 13460	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
79		rexr 9675	. . . . . . . . . . . 12
80	79	adantl 467	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
81	80	biantrurd 510	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
82	76, 78, 81	3bitrd 282	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
83	82	pm5.32da 645	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
84		simprl 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85	48	adantr 466	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86		mnfxr 11403	. . . . . . . . . . . . 13
87	86	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88	49	adantr 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89	88	rexrd 9679	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90		mnflt 11414	. . . . . . . . . . . . . 14
91	49, 90	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
92	91	adantr 466	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93		simprrl 772	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94	87, 89, 84, 92, 93	xrltletrd 11447	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95		simprrr 773	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96		xrre 11453	. . . . . . . . . . 11 $/\$ $/\$ $/\$
97	84, 85, 94, 95, 96	syl22anc 1265	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	97	ex 435	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
99	98	pm4.71rd 639	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100	83, 99	bitr4d 259	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101	100	abbidv 2556	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		df-rab 2782	. . . . . 6 $/\$ $/\$ $/\$
103	101, 102	syl6eqr 2479	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
104	53, 55, 103	3eqtr4rd 2472	. . . 4 $/\$ $/\$ $/\$ $/\$
105	40, 39	ltnled 9771	. . . . . . . 8 $/\$ $/\$
106	105	biimprd 226	. . . . . . 7 $/\$ $/\$
107	106	imdistani 694	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		df-rab 2782	. . . . . . 7 $/\$
109	29	3ad2ant1 1026	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
110	31	3ad2ant1 1026	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
111	71	3ad2ant3 1028	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
112	110, 111	readdcld 9659	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
113	40, 39, 43, 42	lt2sqd 12436	. . . . . . . . . . . . . . 15 $/\$ $/\$
114	35	breq2d 4429	. . . . . . . . . . . . . . 15 $/\$ $/\$
115	113, 114	bitrd 256	. . . . . . . . . . . . . 14 $/\$ $/\$
116	115	biimpa 486	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117	116	3adant3 1025	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
118		sqge0 12337	. . . . . . . . . . . . . 14
119	118	3ad2ant3 1028	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
120	110, 111	addge01d 10190	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
121	119, 120	mpbid 213	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
122	109, 110, 112, 117, 121	ltletrd 9784	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
123	109, 112	ltnled 9771	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
124	122, 123	mpbid 213	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
125	124	3expa 1205	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
126	125	ralrimiva 2837	. . . . . . . 8 $/\$ $/\$ $/\$
127		rabeq0 3781	. . . . . . . 8
128	126, 127	sylibr 215	. . . . . . 7 $/\$ $/\$ $/\$
129	108, 128	syl5eqr 2475	. . . . . 6 $/\$ $/\$ $/\$ $/\$
130	107, 129	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$
131		iffalse 3915	. . . . . 6
132	131	adantl 467	. . . . 5 $/\$ $/\$ $/\$
133	130, 132	eqtr4d 2464	. . . 4 $/\$ $/\$ $/\$ $/\$
134	104, 133	pm2.61dan 798	. . 3 $/\$ $/\$ $/\$
135	27, 134	eqtr3d 2463	. 2 $/\$ $/\$ $/\$ $/\$
136	24, 135	syl5eq 2473	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1867

cab 2405

wral 2773

crab 2777

cvv 3078

c0 3758

cif 3906

csn 3993

cop 3999 class class class wbr 4417

copab 4474

cima 4848

cfv 5592 (class class class)co 6296

cc 9526

cr 9527

cc0 9528

caddc 9531

cmnf 9662

cxr 9663

clt 9664

cle 9665

cmin 9849

cneg 9850

c2 10648

cicc 11627

cexp 12258

csqrt 13264

cabs 13265

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1838 ax-8 1869 ax-9 1871 ax-10 1886 ax-11 1891 ax-12 1904 ax-13 2052 ax-ext 2398 ax-sep 4539 ax-nul 4547 ax-pow 4594 ax-pr 4652 ax-un 6588 ax-cnex 9584 ax-resscn 9585 ax-1cn 9586 ax-icn 9587 ax-addcl 9588 ax-addrcl 9589 ax-mulcl 9590 ax-mulrcl 9591 ax-mulcom 9592 ax-addass 9593 ax-mulass 9594 ax-distr 9595 ax-i2m1 9596 ax-1ne0 9597 ax-1rid 9598 ax-rnegex 9599 ax-rrecex 9600 ax-cnre 9601 ax-pre-lttri 9602 ax-pre-lttrn 9603 ax-pre-ltadd 9604 ax-pre-mulgt0 9605 ax-pre-sup 9606

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2267 df-mo 2268 df-clab 2406 df-cleq 2412 df-clel 2415 df-nfc 2570 df-ne 2618 df-nel 2619 df-ral 2778 df-rex 2779 df-reu 2780 df-rmo 2781 df-rab 2782 df-v 3080 df-sbc 3297 df-csb 3393 df-dif 3436 df-un 3438 df-in 3440 df-ss 3447 df-pss 3449 df-nul 3759 df-if 3907 df-pw 3978 df-sn 3994 df-pr 3996 df-tp 3998 df-op 4000 df-uni 4214 df-iun 4295 df-br 4418 df-opab 4476 df-mpt 4477 df-tr 4512 df-eprel 4756 df-id 4760 df-po 4766 df-so 4767 df-fr 4804 df-we 4806 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-pred 5390 df-ord 5436 df-on 5437 df-lim 5438 df-suc 5439 df-iota 5556 df-fun 5594 df-fn 5595 df-f 5596 df-f1 5597 df-fo 5598 df-f1o 5599 df-fv 5600 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6698 df-2nd 6799 df-wrecs 7027 df-recs 7089 df-rdg 7127 df-er 7362 df-en 7569 df-dom 7570 df-sdom 7571 df-sup 7953 df-pnf 9666 df-mnf 9667 df-xr 9668 df-ltxr 9669 df-le 9670 df-sub 9851 df-neg 9852 df-div 10259 df-nn 10599 df-2 10657 df-3 10658 df-n0 10859 df-z 10927 df-uz 11149 df-rp 11292 df-icc 11631 df-seq 12200 df-exp 12259 df-cj 13130 df-re 13131 df-im 13132 df-sqrt 13266 df-abs 13267

This theorem is referenced by: areacirc 31741

W3C validator