areacirclem5 - Mathbox for Brendan Leahy

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

Theorem areacirclem5 32100

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 5171	. . 3 $/\$ $/\$
3		vex 3034	. . . 4
4		imasng 5196	. . . 4 $/\$ $/\$ $/\$ $/\$
5	3, 4	ax-mp 5	. . 3 $/\$ $/\$ $/\$ $/\$
6		df-br 4396	. . . . 5 $/\$ $/\$ $/\$ $/\$
7		vex 3034	. . . . . 6
8		eleq1 2537	. . . . . . . 8
9	8	anbi1d 719	. . . . . . 7 $/\$ $/\$
10		oveq1 6315	. . . . . . . . 9
11	10	oveq1d 6323	. . . . . . . 8
12	11	breq1d 4405	. . . . . . 7
13	9, 12	anbi12d 725	. . . . . 6 $/\$ $/\$ $/\$ $/\$
14		eleq1 2537	. . . . . . . 8
15	14	anbi2d 718	. . . . . . 7 $/\$ $/\$
16		oveq1 6315	. . . . . . . . 9
17	16	oveq2d 6324	. . . . . . . 8
18	17	breq1d 4405	. . . . . . 7
19	15, 18	anbi12d 725	. . . . . 6 $/\$ $/\$ $/\$ $/\$
20	3, 7, 13, 19	opelopab 4723	. . . . 5 $/\$ $/\$ $/\$ $/\$
21		anass 661	. . . . 5 $/\$ $/\$ $/\$ $/\$
22	6, 20, 21	3bitri 279	. . . 4 $/\$ $/\$ $/\$ $/\$
23	22	abbii 2587	. . 3 $/\$ $/\$ $/\$ $/\$
24	2, 5, 23	3eqtri 2497	. 2 $/\$ $/\$
25		simp3 1032	. . . . 5 $/\$ $/\$
26	25	biantrurd 516	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
27	26	abbidv 2589	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
28		resqcl 12380	. . . . . . . . . . . 12
29	28	3ad2ant1 1051	. . . . . . . . . . 11 $/\$ $/\$
30		resqcl 12380	. . . . . . . . . . . 12
31	30	3ad2ant3 1053	. . . . . . . . . . 11 $/\$ $/\$
32	29, 31	resubcld 10068	. . . . . . . . . 10 $/\$ $/\$
33	32	adantr 472	. . . . . . . . 9 $/\$ $/\$ $/\$
34		absresq 13442	. . . . . . . . . . . . 13
35	34	3ad2ant3 1053	. . . . . . . . . . . 12 $/\$ $/\$
36	35	breq1d 4405	. . . . . . . . . . 11 $/\$ $/\$
37		recn 9647	. . . . . . . . . . . . . 14
38	37	abscld 13575	. . . . . . . . . . . . 13
39	38	3ad2ant3 1053	. . . . . . . . . . . 12 $/\$ $/\$
40		simp1 1030	. . . . . . . . . . . 12 $/\$ $/\$
41	37	absge0d 13583	. . . . . . . . . . . . 13
42	41	3ad2ant3 1053	. . . . . . . . . . . 12 $/\$ $/\$
43		simp2 1031	. . . . . . . . . . . 12 $/\$ $/\$
44	39, 40, 42, 43	le2sqd 12489	. . . . . . . . . . 11 $/\$ $/\$
45	29, 31	subge0d 10224	. . . . . . . . . . 11 $/\$ $/\$
46	36, 44, 45	3bitr4d 293	. . . . . . . . . 10 $/\$ $/\$
47	46	biimpa 492	. . . . . . . . 9 $/\$ $/\$ $/\$
48	33, 47	resqrtcld 13556	. . . . . . . 8 $/\$ $/\$ $/\$
49	48	renegcld 10067	. . . . . . 7 $/\$ $/\$ $/\$
50	49	rexrd 9708	. . . . . 6 $/\$ $/\$ $/\$
51	48	rexrd 9708	. . . . . 6 $/\$ $/\$ $/\$
52		iccval 11700	. . . . . 6 $/\$ $/\$
53	50, 51, 52	syl2anc 673	. . . . 5 $/\$ $/\$ $/\$ $/\$
54		iftrue 3878	. . . . . 6
55	54	adantl 473	. . . . 5 $/\$ $/\$ $/\$
56		absresq 13442	. . . . . . . . . . . 12
57	32	recnd 9687	. . . . . . . . . . . . . 14 $/\$ $/\$
58	57	adantr 472	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
59	58	sqsqrtd 13578	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
60	56, 59	breqan12rd 4412	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
61		recn 9647	. . . . . . . . . . . . . 14
62	61	abscld 13575	. . . . . . . . . . . . 13
63	62	adantl 473	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
64	48	adantr 472	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
65	61	absge0d 13583	. . . . . . . . . . . . 13
66	65	adantl 473	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
67	33, 47	sqrtge0d 13559	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
68	67	adantr 472	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
69	63, 64, 66, 68	le2sqd 12489	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
70	31	adantr 472	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
71		resqcl 12380	. . . . . . . . . . . . . 14
72	71	adantl 473	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
73	29	adantr 472	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
74	70, 72, 73	leaddsub2d 10236	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
75	74	adantlr 729	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
76	60, 69, 75	3bitr4rd 294	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
77		simpr 468	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
78	77, 64	absled 13569	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
79		rexr 9704	. . . . . . . . . . . 12
80	79	adantl 473	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
81	80	biantrurd 516	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
82	76, 78, 81	3bitrd 287	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
83	82	pm5.32da 653	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
84		simprl 772	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85	48	adantr 472	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86		mnfxr 11437	. . . . . . . . . . . . 13
87	86	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88	49	adantr 472	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89	88	rexrd 9708	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90		mnflt 11448	. . . . . . . . . . . . . 14
91	49, 90	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
92	91	adantr 472	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93		simprrl 782	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94	87, 89, 84, 92, 93	xrltletrd 11481	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95		simprrr 783	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96		xrre 11487	. . . . . . . . . . 11 $/\$ $/\$ $/\$
97	84, 85, 94, 95, 96	syl22anc 1293	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	97	ex 441	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
99	98	pm4.71rd 647	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100	83, 99	bitr4d 264	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101	100	abbidv 2589	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		df-rab 2765	. . . . . 6 $/\$ $/\$ $/\$
103	101, 102	syl6eqr 2523	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
104	53, 55, 103	3eqtr4rd 2516	. . . 4 $/\$ $/\$ $/\$ $/\$
105	40, 39	ltnled 9799	. . . . . . . 8 $/\$ $/\$
106	105	biimprd 231	. . . . . . 7 $/\$ $/\$
107	106	imdistani 704	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		df-rab 2765	. . . . . . 7 $/\$
109	29	3ad2ant1 1051	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
110	31	3ad2ant1 1051	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
111	71	3ad2ant3 1053	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
112	110, 111	readdcld 9688	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
113	40, 39, 43, 42	lt2sqd 12488	. . . . . . . . . . . . . . 15 $/\$ $/\$
114	35	breq2d 4407	. . . . . . . . . . . . . . 15 $/\$ $/\$
115	113, 114	bitrd 261	. . . . . . . . . . . . . 14 $/\$ $/\$
116	115	biimpa 492	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117	116	3adant3 1050	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
118		sqge0 12389	. . . . . . . . . . . . . 14
119	118	3ad2ant3 1053	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
120	110, 111	addge01d 10222	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
121	119, 120	mpbid 215	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
122	109, 110, 112, 117, 121	ltletrd 9812	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
123	109, 112	ltnled 9799	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
124	122, 123	mpbid 215	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
125	124	3expa 1231	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
126	125	ralrimiva 2809	. . . . . . . 8 $/\$ $/\$ $/\$
127		rabeq0 3757	. . . . . . . 8
128	126, 127	sylibr 217	. . . . . . 7 $/\$ $/\$ $/\$
129	108, 128	syl5eqr 2519	. . . . . 6 $/\$ $/\$ $/\$ $/\$
130	107, 129	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$
131		iffalse 3881	. . . . . 6
132	131	adantl 473	. . . . 5 $/\$ $/\$ $/\$
133	130, 132	eqtr4d 2508	. . . 4 $/\$ $/\$ $/\$ $/\$
134	104, 133	pm2.61dan 808	. . 3 $/\$ $/\$ $/\$
135	27, 134	eqtr3d 2507	. 2 $/\$ $/\$ $/\$ $/\$
136	24, 135	syl5eq 2517	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904

cab 2457

wral 2756

crab 2760

cvv 3031

c0 3722

cif 3872

csn 3959

cop 3965 class class class wbr 4395

copab 4453

cima 4842

cfv 5589 (class class class)co 6308

cc 9555

cr 9556

cc0 9557

caddc 9560

cmnf 9691

cxr 9692

clt 9693

cle 9694

cmin 9880

cneg 9881

c2 10681

cicc 11663

cexp 12310

csqrt 13373

cabs 13374

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-er 7381 df-en 7588 df-dom 7589 df-sdom 7590 df-sup 7974 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-n0 10894 df-z 10962 df-uz 11183 df-rp 11326 df-icc 11667 df-seq 12252 df-exp 12311 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376

This theorem is referenced by: areacirc 32101

W3C validator