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 32029

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 5164	. . 3 $/\$ $/\$
3		vex 3047	. . . 4
4		imasng 5189	. . . 4 $/\$ $/\$ $/\$ $/\$
5	3, 4	ax-mp 5	. . 3 $/\$ $/\$ $/\$ $/\$
6		df-br 4402	. . . . 5 $/\$ $/\$ $/\$ $/\$
7		vex 3047	. . . . . 6
8		eleq1 2516	. . . . . . . 8
9	8	anbi1d 710	. . . . . . 7 $/\$ $/\$
10		oveq1 6295	. . . . . . . . 9
11	10	oveq1d 6303	. . . . . . . 8
12	11	breq1d 4411	. . . . . . 7
13	9, 12	anbi12d 716	. . . . . 6 $/\$ $/\$ $/\$ $/\$
14		eleq1 2516	. . . . . . . 8
15	14	anbi2d 709	. . . . . . 7 $/\$ $/\$
16		oveq1 6295	. . . . . . . . 9
17	16	oveq2d 6304	. . . . . . . 8
18	17	breq1d 4411	. . . . . . 7
19	15, 18	anbi12d 716	. . . . . 6 $/\$ $/\$ $/\$ $/\$
20	3, 7, 13, 19	opelopab 4722	. . . . 5 $/\$ $/\$ $/\$ $/\$
21		anass 654	. . . . 5 $/\$ $/\$ $/\$ $/\$
22	6, 20, 21	3bitri 275	. . . 4 $/\$ $/\$ $/\$ $/\$
23	22	abbii 2566	. . 3 $/\$ $/\$ $/\$ $/\$
24	2, 5, 23	3eqtri 2476	. 2 $/\$ $/\$
25		simp3 1009	. . . . 5 $/\$ $/\$
26	25	biantrurd 511	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
27	26	abbidv 2568	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
28		resqcl 12339	. . . . . . . . . . . 12
29	28	3ad2ant1 1028	. . . . . . . . . . 11 $/\$ $/\$
30		resqcl 12339	. . . . . . . . . . . 12
31	30	3ad2ant3 1030	. . . . . . . . . . 11 $/\$ $/\$
32	29, 31	resubcld 10044	. . . . . . . . . 10 $/\$ $/\$
33	32	adantr 467	. . . . . . . . 9 $/\$ $/\$ $/\$
34		absresq 13358	. . . . . . . . . . . . 13
35	34	3ad2ant3 1030	. . . . . . . . . . . 12 $/\$ $/\$
36	35	breq1d 4411	. . . . . . . . . . 11 $/\$ $/\$
37		recn 9626	. . . . . . . . . . . . . 14
38	37	abscld 13491	. . . . . . . . . . . . 13
39	38	3ad2ant3 1030	. . . . . . . . . . . 12 $/\$ $/\$
40		simp1 1007	. . . . . . . . . . . 12 $/\$ $/\$
41	37	absge0d 13499	. . . . . . . . . . . . 13
42	41	3ad2ant3 1030	. . . . . . . . . . . 12 $/\$ $/\$
43		simp2 1008	. . . . . . . . . . . 12 $/\$ $/\$
44	39, 40, 42, 43	le2sqd 12448	. . . . . . . . . . 11 $/\$ $/\$
45	29, 31	subge0d 10200	. . . . . . . . . . 11 $/\$ $/\$
46	36, 44, 45	3bitr4d 289	. . . . . . . . . 10 $/\$ $/\$
47	46	biimpa 487	. . . . . . . . 9 $/\$ $/\$ $/\$
48	33, 47	resqrtcld 13472	. . . . . . . 8 $/\$ $/\$ $/\$
49	48	renegcld 10043	. . . . . . 7 $/\$ $/\$ $/\$
50	49	rexrd 9687	. . . . . 6 $/\$ $/\$ $/\$
51	48	rexrd 9687	. . . . . 6 $/\$ $/\$ $/\$
52		iccval 11672	. . . . . 6 $/\$ $/\$
53	50, 51, 52	syl2anc 666	. . . . 5 $/\$ $/\$ $/\$ $/\$
54		iftrue 3886	. . . . . 6
55	54	adantl 468	. . . . 5 $/\$ $/\$ $/\$
56		absresq 13358	. . . . . . . . . . . 12
57	32	recnd 9666	. . . . . . . . . . . . . 14 $/\$ $/\$
58	57	adantr 467	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
59	58	sqsqrtd 13494	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
60	56, 59	breqan12rd 4418	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
61		recn 9626	. . . . . . . . . . . . . 14
62	61	abscld 13491	. . . . . . . . . . . . 13
63	62	adantl 468	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
64	48	adantr 467	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
65	61	absge0d 13499	. . . . . . . . . . . . 13
66	65	adantl 468	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
67	33, 47	sqrtge0d 13475	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
68	67	adantr 467	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
69	63, 64, 66, 68	le2sqd 12448	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
70	31	adantr 467	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
71		resqcl 12339	. . . . . . . . . . . . . 14
72	71	adantl 468	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
73	29	adantr 467	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
74	70, 72, 73	leaddsub2d 10212	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
75	74	adantlr 720	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
76	60, 69, 75	3bitr4rd 290	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
77		simpr 463	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
78	77, 64	absled 13485	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
79		rexr 9683	. . . . . . . . . . . 12
80	79	adantl 468	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
81	80	biantrurd 511	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
82	76, 78, 81	3bitrd 283	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
83	82	pm5.32da 646	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
84		simprl 763	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85	48	adantr 467	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86		mnfxr 11411	. . . . . . . . . . . . 13
87	86	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88	49	adantr 467	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89	88	rexrd 9687	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90		mnflt 11422	. . . . . . . . . . . . . 14
91	49, 90	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
92	91	adantr 467	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93		simprrl 773	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94	87, 89, 84, 92, 93	xrltletrd 11455	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95		simprrr 774	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96		xrre 11461	. . . . . . . . . . 11 $/\$ $/\$ $/\$
97	84, 85, 94, 95, 96	syl22anc 1268	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	97	ex 436	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
99	98	pm4.71rd 640	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100	83, 99	bitr4d 260	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101	100	abbidv 2568	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		df-rab 2745	. . . . . 6 $/\$ $/\$ $/\$
103	101, 102	syl6eqr 2502	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
104	53, 55, 103	3eqtr4rd 2495	. . . 4 $/\$ $/\$ $/\$ $/\$
105	40, 39	ltnled 9779	. . . . . . . 8 $/\$ $/\$
106	105	biimprd 227	. . . . . . 7 $/\$ $/\$
107	106	imdistani 695	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		df-rab 2745	. . . . . . 7 $/\$
109	29	3ad2ant1 1028	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
110	31	3ad2ant1 1028	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
111	71	3ad2ant3 1030	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
112	110, 111	readdcld 9667	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
113	40, 39, 43, 42	lt2sqd 12447	. . . . . . . . . . . . . . 15 $/\$ $/\$
114	35	breq2d 4413	. . . . . . . . . . . . . . 15 $/\$ $/\$
115	113, 114	bitrd 257	. . . . . . . . . . . . . 14 $/\$ $/\$
116	115	biimpa 487	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117	116	3adant3 1027	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
118		sqge0 12348	. . . . . . . . . . . . . 14
119	118	3ad2ant3 1030	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
120	110, 111	addge01d 10198	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
121	119, 120	mpbid 214	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
122	109, 110, 112, 117, 121	ltletrd 9792	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
123	109, 112	ltnled 9779	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
124	122, 123	mpbid 214	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
125	124	3expa 1207	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
126	125	ralrimiva 2801	. . . . . . . 8 $/\$ $/\$ $/\$
127		rabeq0 3753	. . . . . . . 8
128	126, 127	sylibr 216	. . . . . . 7 $/\$ $/\$ $/\$
129	108, 128	syl5eqr 2498	. . . . . 6 $/\$ $/\$ $/\$ $/\$
130	107, 129	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$
131		iffalse 3889	. . . . . 6
132	131	adantl 468	. . . . 5 $/\$ $/\$ $/\$
133	130, 132	eqtr4d 2487	. . . 4 $/\$ $/\$ $/\$ $/\$
134	104, 133	pm2.61dan 799	. . 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 188 $/\$ wa 371 $/\$ w3a 984

wceq 1443

wcel 1886

cab 2436

wral 2736

crab 2740

cvv 3044

c0 3730

cif 3880

csn 3967

cop 3973 class class class wbr 4401

copab 4459

cima 4836

cfv 5581 (class class class)co 6288

cc 9534

cr 9535

cc0 9536

caddc 9539

cmnf 9670

cxr 9671

clt 9672

cle 9673

cmin 9857

cneg 9858

c2 10656

cicc 11635

cexp 12269

csqrt 13289

cabs 13290

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613 ax-pre-sup 9614

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-uni 4198 df-iun 4279 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-om 6690 df-2nd 6791 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-er 7360 df-en 7567 df-dom 7568 df-sdom 7569 df-sup 7953 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-div 10267 df-nn 10607 df-2 10665 df-3 10666 df-n0 10867 df-z 10935 df-uz 11157 df-rp 11300 df-icc 11639 df-seq 12211 df-exp 12270 df-cj 13155 df-re 13156 df-im 13157 df-sqrt 13291 df-abs 13292

This theorem is referenced by: areacirc 32030

W3C validator