Description: Arithmetic-geometric mean inequality for n = 3 . (Contributed by Stanislas Polu, 11-Sep-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | amgm3d.0 | |
|
amgm3d.1 | |
||
amgm3d.2 | |
||
Assertion | amgm3d | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | amgm3d.0 | |
|
2 | amgm3d.1 | |
|
3 | amgm3d.2 | |
|
4 | eqid | |
|
5 | fzofi | |
|
6 | 5 | a1i | |
7 | 3nn | |
|
8 | lbfzo0 | |
|
9 | 7 8 | mpbir | |
10 | ne0i | |
|
11 | 9 10 | mp1i | |
12 | 1 2 3 | s3cld | |
13 | wrdf | |
|
14 | s3len | |
|
15 | df-3 | |
|
16 | 14 15 | eqtri | |
17 | 16 | oveq2i | |
18 | 17 | feq2i | |
19 | 13 18 | sylib | |
20 | 15 | oveq2i | |
21 | 20 | feq2i | |
22 | 19 21 | sylibr | |
23 | 12 22 | syl | |
24 | 4 6 11 23 | amgmlem | |
25 | cnring | |
|
26 | 4 | ringmgp | |
27 | 25 26 | mp1i | |
28 | 1 | rpcnd | |
29 | 2 | rpcnd | |
30 | 3 | rpcnd | |
31 | 28 29 30 | jca32 | |
32 | cnfldbas | |
|
33 | 4 32 | mgpbas | |
34 | cnfldmul | |
|
35 | 4 34 | mgpplusg | |
36 | 33 35 | gsumws3 | |
37 | 27 31 36 | syl2anc | |
38 | 3nn0 | |
|
39 | hashfzo0 | |
|
40 | 38 39 | mp1i | |
41 | 40 | oveq2d | |
42 | 37 41 | oveq12d | |
43 | ringmnd | |
|
44 | 25 43 | mp1i | |
45 | cnfldadd | |
|
46 | 32 45 | gsumws3 | |
47 | 44 31 46 | syl2anc | |
48 | 47 40 | oveq12d | |
49 | 24 42 48 | 3brtr3d | |