amgm2 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > amgm2		Unicode version

Theorem amgm2 10666

Description: Arithmetic-geometric mean inequality for

. (Contributed by Mario Carneiro, 2-Jul-2014.)

**Assertion**
Ref	Expression
amgm2	$/\$ $/\$ $/\$

**Proof of Theorem amgm2**
Step	Hyp	Ref	Expression
1		2cn 8591	. . . . . 6
2		simpll 497	. . . . . . . . 9 $/\$ $/\$ $/\$
3		simprl 499	. . . . . . . . 9 $/\$ $/\$ $/\$
4		remulcl 7567	. . . . . . . . 9 $/\$
5	2, 3, 4	syl2anc 404	. . . . . . . 8 $/\$ $/\$ $/\$
6		mulge0 8193	. . . . . . . 8 $/\$ $/\$ $/\$
7		resqrtcl 10577	. . . . . . . 8 $/\$
8	5, 6, 7	syl2anc 404	. . . . . . 7 $/\$ $/\$ $/\$
9	8	recnd 7613	. . . . . 6 $/\$ $/\$ $/\$
10		sqmul 10132	. . . . . 6 $/\$
11	1, 9, 10	sylancr 406	. . . . 5 $/\$ $/\$ $/\$
12		sq2 10165	. . . . . . 7
13	12	oveq1i 5700	. . . . . 6
14		resqrtth 10579	. . . . . . . 8 $/\$
15	5, 6, 14	syl2anc 404	. . . . . . 7 $/\$ $/\$ $/\$
16	15	oveq2d 5706	. . . . . 6 $/\$ $/\$ $/\$
17	13, 16	syl5eq 2139	. . . . 5 $/\$ $/\$ $/\$
18	11, 17	eqtrd 2127	. . . 4 $/\$ $/\$ $/\$
19	2, 3	resubcld 7956	. . . . . . 7 $/\$ $/\$ $/\$
20	19	sqge0d 10228	. . . . . 6 $/\$ $/\$ $/\$
21	2	recnd 7613	. . . . . . . . . 10 $/\$ $/\$ $/\$
22	3	recnd 7613	. . . . . . . . . 10 $/\$ $/\$ $/\$
23		binom2 10180	. . . . . . . . . 10 $/\$
24	21, 22, 23	syl2anc 404	. . . . . . . . 9 $/\$ $/\$ $/\$
25		binom2sub 10182	. . . . . . . . . 10 $/\$
26	21, 22, 25	syl2anc 404	. . . . . . . . 9 $/\$ $/\$ $/\$
27	24, 26	oveq12d 5708	. . . . . . . 8 $/\$ $/\$ $/\$
28	2	resqcld 10227	. . . . . . . . . . 11 $/\$ $/\$ $/\$
29		2re 8590	. . . . . . . . . . . 12
30		remulcl 7567	. . . . . . . . . . . 12 $/\$
31	29, 5, 30	sylancr 406	. . . . . . . . . . 11 $/\$ $/\$ $/\$
32	28, 31	readdcld 7614	. . . . . . . . . 10 $/\$ $/\$ $/\$
33	32	recnd 7613	. . . . . . . . 9 $/\$ $/\$ $/\$
34	28, 31	resubcld 7956	. . . . . . . . . 10 $/\$ $/\$ $/\$
35	34	recnd 7613	. . . . . . . . 9 $/\$ $/\$ $/\$
36	3	resqcld 10227	. . . . . . . . . 10 $/\$ $/\$ $/\$
37	36	recnd 7613	. . . . . . . . 9 $/\$ $/\$ $/\$
38	33, 35, 37	pnpcan2d 7928	. . . . . . . 8 $/\$ $/\$ $/\$
39	31	recnd 7613	. . . . . . . . . 10 $/\$ $/\$ $/\$
40	39	2timesd 8756	. . . . . . . . 9 $/\$ $/\$ $/\$
41		2t2e4 8668	. . . . . . . . . . 11
42	41	oveq1i 5700	. . . . . . . . . 10
43		2cnd 8593	. . . . . . . . . . 11 $/\$ $/\$ $/\$
44	5	recnd 7613	. . . . . . . . . . 11 $/\$ $/\$ $/\$
45	43, 43, 44	mulassd 7608	. . . . . . . . . 10 $/\$ $/\$ $/\$
46	42, 45	syl5eqr 2141	. . . . . . . . 9 $/\$ $/\$ $/\$
47	28	recnd 7613	. . . . . . . . . 10 $/\$ $/\$ $/\$
48	47, 39, 39	pnncand 7929	. . . . . . . . 9 $/\$ $/\$ $/\$
49	40, 46, 48	3eqtr4rd 2138	. . . . . . . 8 $/\$ $/\$ $/\$
50	27, 38, 49	3eqtrd 2131	. . . . . . 7 $/\$ $/\$ $/\$
51	2, 3	readdcld 7614	. . . . . . . . . 10 $/\$ $/\$ $/\$
52	51	resqcld 10227	. . . . . . . . 9 $/\$ $/\$ $/\$
53	52	recnd 7613	. . . . . . . 8 $/\$ $/\$ $/\$
54	19	resqcld 10227	. . . . . . . . 9 $/\$ $/\$ $/\$
55	54	recnd 7613	. . . . . . . 8 $/\$ $/\$ $/\$
56		4re 8597	. . . . . . . . . 10
57		remulcl 7567	. . . . . . . . . 10 $/\$
58	56, 5, 57	sylancr 406	. . . . . . . . 9 $/\$ $/\$ $/\$
59	58	recnd 7613	. . . . . . . 8 $/\$ $/\$ $/\$
60		subsub23 7784	. . . . . . . 8 $/\$ $/\$
61	53, 55, 59, 60	syl3anc 1181	. . . . . . 7 $/\$ $/\$ $/\$
62	50, 61	mpbid 146	. . . . . 6 $/\$ $/\$ $/\$
63	20, 62	breqtrrd 3893	. . . . 5 $/\$ $/\$ $/\$
64	52, 58	subge0d 8109	. . . . 5 $/\$ $/\$ $/\$
65	63, 64	mpbid 146	. . . 4 $/\$ $/\$ $/\$
66	18, 65	eqbrtrd 3887	. . 3 $/\$ $/\$ $/\$
67		remulcl 7567	. . . . 5 $/\$
68	29, 8, 67	sylancr 406	. . . 4 $/\$ $/\$ $/\$
69		sqrtge0 10581	. . . . . 6 $/\$
70	5, 6, 69	syl2anc 404	. . . . 5 $/\$ $/\$ $/\$
71		0le2 8610	. . . . . 6
72		mulge0 8193	. . . . . 6 $/\$ $/\$ $/\$
73	29, 71, 72	mpanl12 428	. . . . 5 $/\$
74	8, 70, 73	syl2anc 404	. . . 4 $/\$ $/\$ $/\$
75		addge0 8026	. . . . 5 $/\$ $/\$ $/\$
76	75	an4s 556	. . . 4 $/\$ $/\$ $/\$
77	68, 51, 74, 76	le2sqd 10233	. . 3 $/\$ $/\$ $/\$
78	66, 77	mpbird 166	. 2 $/\$ $/\$ $/\$
79		2pos 8611	. . . . 5
80	29, 79	pm3.2i 267	. . . 4 $/\$
81	80	a1i 9	. . 3 $/\$ $/\$ $/\$ $/\$
82		lemuldiv2 8440	. . 3 $/\$ $/\$ $/\$
83	8, 51, 81, 82	syl3anc 1181	. 2 $/\$ $/\$ $/\$
84	78, 83	mpbid 146	1 $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104

wceq 1296

wcel 1445 class class class wbr 3867

cfv 5049 (class class class)co 5690

cc 7445

cr 7446

cc0 7447

caddc 7450

cmul 7452

clt 7619

cle 7620

cmin 7750

cdiv 8236

c2 8571

c4 8573

cexp 10069

csqrt 10544

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 582 ax-in2 583 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-13 1456 ax-14 1457 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-coll 3975 ax-sep 3978 ax-nul 3986 ax-pow 4030 ax-pr 4060 ax-un 4284 ax-setind 4381 ax-iinf 4431 ax-cnex 7533 ax-resscn 7534 ax-1cn 7535 ax-1re 7536 ax-icn 7537 ax-addcl 7538 ax-addrcl 7539 ax-mulcl 7540 ax-mulrcl 7541 ax-addcom 7542 ax-mulcom 7543 ax-addass 7544 ax-mulass 7545 ax-distr 7546 ax-i2m1 7547 ax-0lt1 7548 ax-1rid 7549 ax-0id 7550 ax-rnegex 7551 ax-precex 7552 ax-cnre 7553 ax-pre-ltirr 7554 ax-pre-ltwlin 7555 ax-pre-lttrn 7556 ax-pre-apti 7557 ax-pre-ltadd 7558 ax-pre-mulgt0 7559 ax-pre-mulext 7560 ax-arch 7561 ax-caucvg 7562

This theorem depends on definitions: df-bi 116 df-dc 784 df-3or 928 df-3an 929 df-tru 1299 df-fal 1302 df-nf 1402 df-sb 1700 df-eu 1958 df-mo 1959 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-ne 2263 df-nel 2358 df-ral 2375 df-rex 2376 df-reu 2377 df-rmo 2378 df-rab 2379 df-v 2635 df-sbc 2855 df-csb 2948 df-dif 3015 df-un 3017 df-in 3019 df-ss 3026 df-nul 3303 df-if 3414 df-pw 3451 df-sn 3472 df-pr 3473 df-op 3475 df-uni 3676 df-int 3711 df-iun 3754 df-br 3868 df-opab 3922 df-mpt 3923 df-tr 3959 df-id 4144 df-po 4147 df-iso 4148 df-iord 4217 df-on 4219 df-ilim 4220 df-suc 4222 df-iom 4434 df-xp 4473 df-rel 4474 df-cnv 4475 df-co 4476 df-dm 4477 df-rn 4478 df-res 4479 df-ima 4480 df-iota 5014 df-fun 5051 df-fn 5052 df-f 5053 df-f1 5054 df-fo 5055 df-f1o 5056 df-fv 5057 df-riota 5646 df-ov 5693 df-oprab 5694 df-mpt2 5695 df-1st 5949 df-2nd 5950 df-recs 6108 df-frec 6194 df-pnf 7621 df-mnf 7622 df-xr 7623 df-ltxr 7624 df-le 7625 df-sub 7752 df-neg 7753 df-reap 8149 df-ap 8156 df-div 8237 df-inn 8521 df-2 8579 df-3 8580 df-4 8581 df-n0 8772 df-z 8849 df-uz 9119 df-rp 9234 df-seqfrec 10001 df-exp 10070 df-rsqrt 10546

This theorem is referenced by: (None)

W3C validator