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