Metamath Proof Explorer


Theorem amgm

Description: Inequality of arithmetic and geometric means. Here ( M gsum F ) calculates the group sum within the multiplicative monoid of the complex numbers (or in other words, it multiplies the elements F ( x ) , x e. A together), and ( CCfld gsum F ) calculates the group sum in the additive group (i.e. the sum of the elements). This is Metamath 100 proof #38. (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Hypothesis amgm.1 M = mulGrp fld
Assertion amgm A Fin A F : A 0 +∞ M F 1 A fld F A

Proof

Step Hyp Ref Expression
1 amgm.1 M = mulGrp fld
2 cnfldbas = Base fld
3 1 2 mgpbas = Base M
4 cnfld1 1 = 1 fld
5 1 4 ringidval 1 = 0 M
6 cnfldmul × = fld
7 1 6 mgpplusg × = + M
8 cncrng fld CRing
9 1 crngmgp fld CRing M CMnd
10 8 9 mp1i A Fin A F : A 0 +∞ x A F x = 0 M CMnd
11 simpl1 A Fin A F : A 0 +∞ x A F x = 0 A Fin
12 simpl3 A Fin A F : A 0 +∞ x A F x = 0 F : A 0 +∞
13 rge0ssre 0 +∞
14 ax-resscn
15 13 14 sstri 0 +∞
16 fss F : A 0 +∞ 0 +∞ F : A
17 12 15 16 sylancl A Fin A F : A 0 +∞ x A F x = 0 F : A
18 1ex 1 V
19 18 a1i A Fin A F : A 0 +∞ x A F x = 0 1 V
20 17 11 19 fdmfifsupp A Fin A F : A 0 +∞ x A F x = 0 finSupp 1 F
21 disjdif x A x =
22 21 a1i A Fin A F : A 0 +∞ x A F x = 0 x A x =
23 undif2 x A x = x A
24 simprl A Fin A F : A 0 +∞ x A F x = 0 x A
25 24 snssd A Fin A F : A 0 +∞ x A F x = 0 x A
26 ssequn1 x A x A = A
27 25 26 sylib A Fin A F : A 0 +∞ x A F x = 0 x A = A
28 23 27 eqtr2id A Fin A F : A 0 +∞ x A F x = 0 A = x A x
29 3 5 7 10 11 17 20 22 28 gsumsplit A Fin A F : A 0 +∞ x A F x = 0 M F = M F x M F A x
30 12 25 feqresmpt A Fin A F : A 0 +∞ x A F x = 0 F x = y x F y
31 30 oveq2d A Fin A F : A 0 +∞ x A F x = 0 M F x = M y x F y
32 cnring fld Ring
33 1 ringmgp fld Ring M Mnd
34 32 33 mp1i A Fin A F : A 0 +∞ x A F x = 0 M Mnd
35 17 24 ffvelrnd A Fin A F : A 0 +∞ x A F x = 0 F x
36 fveq2 y = x F y = F x
37 3 36 gsumsn M Mnd x A F x M y x F y = F x
38 34 24 35 37 syl3anc A Fin A F : A 0 +∞ x A F x = 0 M y x F y = F x
39 simprr A Fin A F : A 0 +∞ x A F x = 0 F x = 0
40 31 38 39 3eqtrd A Fin A F : A 0 +∞ x A F x = 0 M F x = 0
41 40 oveq1d A Fin A F : A 0 +∞ x A F x = 0 M F x M F A x = 0 M F A x
42 diffi A Fin A x Fin
43 11 42 syl A Fin A F : A 0 +∞ x A F x = 0 A x Fin
44 difss A x A
45 fssres F : A A x A F A x : A x
46 17 44 45 sylancl A Fin A F : A 0 +∞ x A F x = 0 F A x : A x
47 46 43 19 fdmfifsupp A Fin A F : A 0 +∞ x A F x = 0 finSupp 1 F A x
48 3 5 10 43 46 47 gsumcl A Fin A F : A 0 +∞ x A F x = 0 M F A x
49 48 mul02d A Fin A F : A 0 +∞ x A F x = 0 0 M F A x = 0
50 29 41 49 3eqtrd A Fin A F : A 0 +∞ x A F x = 0 M F = 0
51 50 oveq1d A Fin A F : A 0 +∞ x A F x = 0 M F 1 A = 0 1 A
52 simpl2 A Fin A F : A 0 +∞ x A F x = 0 A
53 hashnncl A Fin A A
54 11 53 syl A Fin A F : A 0 +∞ x A F x = 0 A A
55 52 54 mpbird A Fin A F : A 0 +∞ x A F x = 0 A
56 55 nncnd A Fin A F : A 0 +∞ x A F x = 0 A
57 55 nnne0d A Fin A F : A 0 +∞ x A F x = 0 A 0
58 56 57 reccld A Fin A F : A 0 +∞ x A F x = 0 1 A
59 56 57 recne0d A Fin A F : A 0 +∞ x A F x = 0 1 A 0
60 58 59 0cxpd A Fin A F : A 0 +∞ x A F x = 0 0 1 A = 0
61 51 60 eqtrd A Fin A F : A 0 +∞ x A F x = 0 M F 1 A = 0
62 cnfld0 0 = 0 fld
63 ringcmn fld Ring fld CMnd
64 32 63 mp1i A Fin A F : A 0 +∞ x A F x = 0 fld CMnd
65 rege0subm 0 +∞ SubMnd fld
66 65 a1i A Fin A F : A 0 +∞ x A F x = 0 0 +∞ SubMnd fld
67 c0ex 0 V
68 67 a1i A Fin A F : A 0 +∞ x A F x = 0 0 V
69 12 11 68 fdmfifsupp A Fin A F : A 0 +∞ x A F x = 0 finSupp 0 F
70 62 64 11 66 12 69 gsumsubmcl A Fin A F : A 0 +∞ x A F x = 0 fld F 0 +∞
71 elrege0 fld F 0 +∞ fld F 0 fld F
72 70 71 sylib A Fin A F : A 0 +∞ x A F x = 0 fld F 0 fld F
73 55 nnred A Fin A F : A 0 +∞ x A F x = 0 A
74 55 nngt0d A Fin A F : A 0 +∞ x A F x = 0 0 < A
75 divge0 fld F 0 fld F A 0 < A 0 fld F A
76 72 73 74 75 syl12anc A Fin A F : A 0 +∞ x A F x = 0 0 fld F A
77 61 76 eqbrtrd A Fin A F : A 0 +∞ x A F x = 0 M F 1 A fld F A
78 77 rexlimdvaa A Fin A F : A 0 +∞ x A F x = 0 M F 1 A fld F A
79 ralnex x A ¬ F x = 0 ¬ x A F x = 0
80 simpl1 A Fin A F : A 0 +∞ x A ¬ F x = 0 A Fin
81 simpl2 A Fin A F : A 0 +∞ x A ¬ F x = 0 A
82 simpl3 A Fin A F : A 0 +∞ x A ¬ F x = 0 F : A 0 +∞
83 82 ffnd A Fin A F : A 0 +∞ x A ¬ F x = 0 F Fn A
84 ffvelrn F : A 0 +∞ x A F x 0 +∞
85 84 3ad2antl3 A Fin A F : A 0 +∞ x A F x 0 +∞
86 elrege0 F x 0 +∞ F x 0 F x
87 85 86 sylib A Fin A F : A 0 +∞ x A F x 0 F x
88 87 simprd A Fin A F : A 0 +∞ x A 0 F x
89 0re 0
90 87 simpld A Fin A F : A 0 +∞ x A F x
91 leloe 0 F x 0 F x 0 < F x 0 = F x
92 89 90 91 sylancr A Fin A F : A 0 +∞ x A 0 F x 0 < F x 0 = F x
93 88 92 mpbid A Fin A F : A 0 +∞ x A 0 < F x 0 = F x
94 93 ord A Fin A F : A 0 +∞ x A ¬ 0 < F x 0 = F x
95 eqcom 0 = F x F x = 0
96 94 95 syl6ib A Fin A F : A 0 +∞ x A ¬ 0 < F x F x = 0
97 96 con1d A Fin A F : A 0 +∞ x A ¬ F x = 0 0 < F x
98 elrp F x + F x 0 < F x
99 98 baib F x F x + 0 < F x
100 90 99 syl A Fin A F : A 0 +∞ x A F x + 0 < F x
101 97 100 sylibrd A Fin A F : A 0 +∞ x A ¬ F x = 0 F x +
102 101 ralimdva A Fin A F : A 0 +∞ x A ¬ F x = 0 x A F x +
103 102 imp A Fin A F : A 0 +∞ x A ¬ F x = 0 x A F x +
104 ffnfv F : A + F Fn A x A F x +
105 83 103 104 sylanbrc A Fin A F : A 0 +∞ x A ¬ F x = 0 F : A +
106 1 80 81 105 amgmlem A Fin A F : A 0 +∞ x A ¬ F x = 0 M F 1 A fld F A
107 106 ex A Fin A F : A 0 +∞ x A ¬ F x = 0 M F 1 A fld F A
108 79 107 syl5bir A Fin A F : A 0 +∞ ¬ x A F x = 0 M F 1 A fld F A
109 78 108 pm2.61d A Fin A F : A 0 +∞ M F 1 A fld F A