amgm2 - Intuitionistic Logic Explorer

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

Theorem amgm2 11000

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 8887	. . . . . 6
2		simpll 519	. . . . . . . . 9 $/\$ $/\$ $/\$
3		simprl 521	. . . . . . . . 9 $/\$ $/\$ $/\$
4		remulcl 7843	. . . . . . . . 9 $/\$
5	2, 3, 4	syl2anc 409	. . . . . . . 8 $/\$ $/\$ $/\$
6		mulge0 8477	. . . . . . . 8 $/\$ $/\$ $/\$
7		resqrtcl 10911	. . . . . . . 8 $/\$
8	5, 6, 7	syl2anc 409	. . . . . . 7 $/\$ $/\$ $/\$
9	8	recnd 7889	. . . . . 6 $/\$ $/\$ $/\$
10		sqmul 10463	. . . . . 6 $/\$
11	1, 9, 10	sylancr 411	. . . . 5 $/\$ $/\$ $/\$
12		sq2 10496	. . . . . . 7
13	12	oveq1i 5828	. . . . . 6
14		resqrtth 10913	. . . . . . . 8 $/\$
15	5, 6, 14	syl2anc 409	. . . . . . 7 $/\$ $/\$ $/\$
16	15	oveq2d 5834	. . . . . 6 $/\$ $/\$ $/\$
17	13, 16	syl5eq 2202	. . . . 5 $/\$ $/\$ $/\$
18	11, 17	eqtrd 2190	. . . 4 $/\$ $/\$ $/\$
19	2, 3	resubcld 8239	. . . . . . 7 $/\$ $/\$ $/\$
20	19	sqge0d 10560	. . . . . 6 $/\$ $/\$ $/\$
21	2	recnd 7889	. . . . . . . . . 10 $/\$ $/\$ $/\$
22	3	recnd 7889	. . . . . . . . . 10 $/\$ $/\$ $/\$
23		binom2 10511	. . . . . . . . . 10 $/\$
24	21, 22, 23	syl2anc 409	. . . . . . . . 9 $/\$ $/\$ $/\$
25		binom2sub 10513	. . . . . . . . . 10 $/\$
26	21, 22, 25	syl2anc 409	. . . . . . . . 9 $/\$ $/\$ $/\$
27	24, 26	oveq12d 5836	. . . . . . . 8 $/\$ $/\$ $/\$
28	2	resqcld 10559	. . . . . . . . . . 11 $/\$ $/\$ $/\$
29		2re 8886	. . . . . . . . . . . 12
30		remulcl 7843	. . . . . . . . . . . 12 $/\$
31	29, 5, 30	sylancr 411	. . . . . . . . . . 11 $/\$ $/\$ $/\$
32	28, 31	readdcld 7890	. . . . . . . . . 10 $/\$ $/\$ $/\$
33	32	recnd 7889	. . . . . . . . 9 $/\$ $/\$ $/\$
34	28, 31	resubcld 8239	. . . . . . . . . 10 $/\$ $/\$ $/\$
35	34	recnd 7889	. . . . . . . . 9 $/\$ $/\$ $/\$
36	3	resqcld 10559	. . . . . . . . . 10 $/\$ $/\$ $/\$
37	36	recnd 7889	. . . . . . . . 9 $/\$ $/\$ $/\$
38	33, 35, 37	pnpcan2d 8207	. . . . . . . 8 $/\$ $/\$ $/\$
39	31	recnd 7889	. . . . . . . . . 10 $/\$ $/\$ $/\$
40	39	2timesd 9058	. . . . . . . . 9 $/\$ $/\$ $/\$
41		2t2e4 8970	. . . . . . . . . . 11
42	41	oveq1i 5828	. . . . . . . . . 10
43		2cnd 8889	. . . . . . . . . . 11 $/\$ $/\$ $/\$
44	5	recnd 7889	. . . . . . . . . . 11 $/\$ $/\$ $/\$
45	43, 43, 44	mulassd 7884	. . . . . . . . . 10 $/\$ $/\$ $/\$
46	42, 45	syl5eqr 2204	. . . . . . . . 9 $/\$ $/\$ $/\$
47	28	recnd 7889	. . . . . . . . . 10 $/\$ $/\$ $/\$
48	47, 39, 39	pnncand 8208	. . . . . . . . 9 $/\$ $/\$ $/\$
49	40, 46, 48	3eqtr4rd 2201	. . . . . . . 8 $/\$ $/\$ $/\$
50	27, 38, 49	3eqtrd 2194	. . . . . . 7 $/\$ $/\$ $/\$
51	2, 3	readdcld 7890	. . . . . . . . . 10 $/\$ $/\$ $/\$
52	51	resqcld 10559	. . . . . . . . 9 $/\$ $/\$ $/\$
53	52	recnd 7889	. . . . . . . 8 $/\$ $/\$ $/\$
54	19	resqcld 10559	. . . . . . . . 9 $/\$ $/\$ $/\$
55	54	recnd 7889	. . . . . . . 8 $/\$ $/\$ $/\$
56		4re 8893	. . . . . . . . . 10
57		remulcl 7843	. . . . . . . . . 10 $/\$
58	56, 5, 57	sylancr 411	. . . . . . . . 9 $/\$ $/\$ $/\$
59	58	recnd 7889	. . . . . . . 8 $/\$ $/\$ $/\$
60		subsub23 8063	. . . . . . . 8 $/\$ $/\$
61	53, 55, 59, 60	syl3anc 1220	. . . . . . 7 $/\$ $/\$ $/\$
62	50, 61	mpbid 146	. . . . . 6 $/\$ $/\$ $/\$
63	20, 62	breqtrrd 3992	. . . . 5 $/\$ $/\$ $/\$
64	52, 58	subge0d 8393	. . . . 5 $/\$ $/\$ $/\$
65	63, 64	mpbid 146	. . . 4 $/\$ $/\$ $/\$
66	18, 65	eqbrtrd 3986	. . 3 $/\$ $/\$ $/\$
67		remulcl 7843	. . . . 5 $/\$
68	29, 8, 67	sylancr 411	. . . 4 $/\$ $/\$ $/\$
69		sqrtge0 10915	. . . . . 6 $/\$
70	5, 6, 69	syl2anc 409	. . . . 5 $/\$ $/\$ $/\$
71		0le2 8906	. . . . . 6
72		mulge0 8477	. . . . . 6 $/\$ $/\$ $/\$
73	29, 71, 72	mpanl12 433	. . . . 5 $/\$
74	8, 70, 73	syl2anc 409	. . . 4 $/\$ $/\$ $/\$
75		addge0 8309	. . . . 5 $/\$ $/\$ $/\$
76	75	an4s 578	. . . 4 $/\$ $/\$ $/\$
77	68, 51, 74, 76	le2sqd 10565	. . 3 $/\$ $/\$ $/\$
78	66, 77	mpbird 166	. 2 $/\$ $/\$ $/\$
79		2pos 8907	. . . . 5
80	29, 79	pm3.2i 270	. . . 4 $/\$
81	80	a1i 9	. . 3 $/\$ $/\$ $/\$ $/\$
82		lemuldiv2 8736	. . 3 $/\$ $/\$ $/\$
83	8, 51, 81, 82	syl3anc 1220	. 2 $/\$ $/\$ $/\$
84	78, 83	mpbid 146	1 $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104

wceq 1335

wcel 2128 class class class wbr 3965

cfv 5167 (class class class)co 5818

cc 7713

cr 7714

cc0 7715

caddc 7718

cmul 7720

clt 7895

cle 7896

cmin 8029

cdiv 8528

c2 8867

c4 8869

cexp 10400

csqrt 10878

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-13 2130 ax-14 2131 ax-ext 2139 ax-coll 4079 ax-sep 4082 ax-nul 4090 ax-pow 4134 ax-pr 4168 ax-un 4392 ax-setind 4494 ax-iinf 4545 ax-cnex 7806 ax-resscn 7807 ax-1cn 7808 ax-1re 7809 ax-icn 7810 ax-addcl 7811 ax-addrcl 7812 ax-mulcl 7813 ax-mulrcl 7814 ax-addcom 7815 ax-mulcom 7816 ax-addass 7817 ax-mulass 7818 ax-distr 7819 ax-i2m1 7820 ax-0lt1 7821 ax-1rid 7822 ax-0id 7823 ax-rnegex 7824 ax-precex 7825 ax-cnre 7826 ax-pre-ltirr 7827 ax-pre-ltwlin 7828 ax-pre-lttrn 7829 ax-pre-apti 7830 ax-pre-ltadd 7831 ax-pre-mulgt0 7832 ax-pre-mulext 7833 ax-arch 7834 ax-caucvg 7835

This theorem depends on definitions: df-bi 116 df-dc 821 df-3or 964 df-3an 965 df-tru 1338 df-fal 1341 df-nf 1441 df-sb 1743 df-eu 2009 df-mo 2010 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-ne 2328 df-nel 2423 df-ral 2440 df-rex 2441 df-reu 2442 df-rmo 2443 df-rab 2444 df-v 2714 df-sbc 2938 df-csb 3032 df-dif 3104 df-un 3106 df-in 3108 df-ss 3115 df-nul 3395 df-if 3506 df-pw 3545 df-sn 3566 df-pr 3567 df-op 3569 df-uni 3773 df-int 3808 df-iun 3851 df-br 3966 df-opab 4026 df-mpt 4027 df-tr 4063 df-id 4252 df-po 4255 df-iso 4256 df-iord 4325 df-on 4327 df-ilim 4328 df-suc 4330 df-iom 4548 df-xp 4589 df-rel 4590 df-cnv 4591 df-co 4592 df-dm 4593 df-rn 4594 df-res 4595 df-ima 4596 df-iota 5132 df-fun 5169 df-fn 5170 df-f 5171 df-f1 5172 df-fo 5173 df-f1o 5174 df-fv 5175 df-riota 5774 df-ov 5821 df-oprab 5822 df-mpo 5823 df-1st 6082 df-2nd 6083 df-recs 6246 df-frec 6332 df-pnf 7897 df-mnf 7898 df-xr 7899 df-ltxr 7900 df-le 7901 df-sub 8031 df-neg 8032 df-reap 8433 df-ap 8440 df-div 8529 df-inn 8817 df-2 8875 df-3 8876 df-4 8877 df-n0 9074 df-z 9151 df-uz 9423 df-rp 9543 df-seqfrec 10327 df-exp 10401 df-rsqrt 10880

This theorem is referenced by: (None)

W3C validator