MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  amgmlem Structured version   Visualization version   GIF version

Theorem amgmlem 25578
Description: Lemma for amgm 25579. (Contributed by Mario Carneiro, 21-Jun-2015.)
Hypotheses
Ref Expression
amgm.1 𝑀 = (mulGrp‘ℂfld)
amgm.2 (𝜑𝐴 ∈ Fin)
amgm.3 (𝜑𝐴 ≠ ∅)
amgm.4 (𝜑𝐹:𝐴⟶ℝ+)
Assertion
Ref Expression
amgmlem (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 / (♯‘𝐴))) ≤ ((ℂfld Σg 𝐹) / (♯‘𝐴)))

Proof of Theorem amgmlem
Dummy variables 𝑎 𝑏 𝑘 𝑠 𝑢 𝑣 𝑤 𝑥 𝑦 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnfld0 20118 . . . . . . . 8 0 = (0g‘ℂfld)
2 cnring 20116 . . . . . . . . 9 fld ∈ Ring
3 ringabl 19329 . . . . . . . . 9 (ℂfld ∈ Ring → ℂfld ∈ Abel)
42, 3mp1i 13 . . . . . . . 8 (𝜑 → ℂfld ∈ Abel)
5 amgm.2 . . . . . . . 8 (𝜑𝐴 ∈ Fin)
6 resubdrg 20300 . . . . . . . . . 10 (ℝ ∈ (SubRing‘ℂfld) ∧ ℝfld ∈ DivRing)
76simpli 487 . . . . . . . . 9 ℝ ∈ (SubRing‘ℂfld)
8 subrgsubg 19537 . . . . . . . . 9 (ℝ ∈ (SubRing‘ℂfld) → ℝ ∈ (SubGrp‘ℂfld))
97, 8mp1i 13 . . . . . . . 8 (𝜑 → ℝ ∈ (SubGrp‘ℂfld))
10 amgm.4 . . . . . . . . . . . 12 (𝜑𝐹:𝐴⟶ℝ+)
1110ffvelrnda 6832 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
1211relogcld 25217 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (log‘(𝐹𝑘)) ∈ ℝ)
1312renegcld 11060 . . . . . . . . 9 ((𝜑𝑘𝐴) → -(log‘(𝐹𝑘)) ∈ ℝ)
1413fmpttd 6860 . . . . . . . 8 (𝜑 → (𝑘𝐴 ↦ -(log‘(𝐹𝑘))):𝐴⟶ℝ)
15 c0ex 10628 . . . . . . . . . 10 0 ∈ V
1615a1i 11 . . . . . . . . 9 (𝜑 → 0 ∈ V)
1714, 5, 16fdmfifsupp 8831 . . . . . . . 8 (𝜑 → (𝑘𝐴 ↦ -(log‘(𝐹𝑘))) finSupp 0)
181, 4, 5, 9, 14, 17gsumsubgcl 19036 . . . . . . 7 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) ∈ ℝ)
1918recnd 10662 . . . . . 6 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) ∈ ℂ)
20 amgm.3 . . . . . . . 8 (𝜑𝐴 ≠ ∅)
21 hashnncl 13727 . . . . . . . . 9 (𝐴 ∈ Fin → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
225, 21syl 17 . . . . . . . 8 (𝜑 → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
2320, 22mpbird 260 . . . . . . 7 (𝜑 → (♯‘𝐴) ∈ ℕ)
2423nncnd 11645 . . . . . 6 (𝜑 → (♯‘𝐴) ∈ ℂ)
2523nnne0d 11679 . . . . . 6 (𝜑 → (♯‘𝐴) ≠ 0)
2619, 24, 25divnegd 11422 . . . . 5 (𝜑 → -((ℂfld Σg (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) / (♯‘𝐴)) = (-(ℂfld Σg (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) / (♯‘𝐴)))
2712recnd 10662 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (log‘(𝐹𝑘)) ∈ ℂ)
285, 27gsumfsum 20161 . . . . . . . . 9 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ (log‘(𝐹𝑘)))) = Σ𝑘𝐴 (log‘(𝐹𝑘)))
2927negnegd 10981 . . . . . . . . . 10 ((𝜑𝑘𝐴) → --(log‘(𝐹𝑘)) = (log‘(𝐹𝑘)))
3029sumeq2dv 15055 . . . . . . . . 9 (𝜑 → Σ𝑘𝐴 --(log‘(𝐹𝑘)) = Σ𝑘𝐴 (log‘(𝐹𝑘)))
3113recnd 10662 . . . . . . . . . 10 ((𝜑𝑘𝐴) → -(log‘(𝐹𝑘)) ∈ ℂ)
325, 31fsumneg 15137 . . . . . . . . 9 (𝜑 → Σ𝑘𝐴 --(log‘(𝐹𝑘)) = -Σ𝑘𝐴 -(log‘(𝐹𝑘)))
3328, 30, 323eqtr2rd 2843 . . . . . . . 8 (𝜑 → -Σ𝑘𝐴 -(log‘(𝐹𝑘)) = (ℂfld Σg (𝑘𝐴 ↦ (log‘(𝐹𝑘)))))
345, 31gsumfsum 20161 . . . . . . . . 9 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) = Σ𝑘𝐴 -(log‘(𝐹𝑘)))
3534negeqd 10873 . . . . . . . 8 (𝜑 → -(ℂfld Σg (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) = -Σ𝑘𝐴 -(log‘(𝐹𝑘)))
3610feqmptd 6712 . . . . . . . . . 10 (𝜑𝐹 = (𝑘𝐴 ↦ (𝐹𝑘)))
37 relogf1o 25161 . . . . . . . . . . . . 13 (log ↾ ℝ+):ℝ+1-1-onto→ℝ
38 f1of 6594 . . . . . . . . . . . . 13 ((log ↾ ℝ+):ℝ+1-1-onto→ℝ → (log ↾ ℝ+):ℝ+⟶ℝ)
3937, 38mp1i 13 . . . . . . . . . . . 12 (𝜑 → (log ↾ ℝ+):ℝ+⟶ℝ)
4039feqmptd 6712 . . . . . . . . . . 11 (𝜑 → (log ↾ ℝ+) = (𝑥 ∈ ℝ+ ↦ ((log ↾ ℝ+)‘𝑥)))
41 fvres 6668 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+ → ((log ↾ ℝ+)‘𝑥) = (log‘𝑥))
4241mpteq2ia 5124 . . . . . . . . . . 11 (𝑥 ∈ ℝ+ ↦ ((log ↾ ℝ+)‘𝑥)) = (𝑥 ∈ ℝ+ ↦ (log‘𝑥))
4340, 42eqtrdi 2852 . . . . . . . . . 10 (𝜑 → (log ↾ ℝ+) = (𝑥 ∈ ℝ+ ↦ (log‘𝑥)))
44 fveq2 6649 . . . . . . . . . 10 (𝑥 = (𝐹𝑘) → (log‘𝑥) = (log‘(𝐹𝑘)))
4511, 36, 43, 44fmptco 6872 . . . . . . . . 9 (𝜑 → ((log ↾ ℝ+) ∘ 𝐹) = (𝑘𝐴 ↦ (log‘(𝐹𝑘))))
4645oveq2d 7155 . . . . . . . 8 (𝜑 → (ℂfld Σg ((log ↾ ℝ+) ∘ 𝐹)) = (ℂfld Σg (𝑘𝐴 ↦ (log‘(𝐹𝑘)))))
4733, 35, 463eqtr4d 2846 . . . . . . 7 (𝜑 → -(ℂfld Σg (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) = (ℂfld Σg ((log ↾ ℝ+) ∘ 𝐹)))
48 amgm.1 . . . . . . . . . . . . . . 15 𝑀 = (mulGrp‘ℂfld)
4948oveq1i 7149 . . . . . . . . . . . . . 14 (𝑀s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
5049rpmsubg 20158 . . . . . . . . . . . . 13 + ∈ (SubGrp‘(𝑀s (ℂ ∖ {0})))
51 subgsubm 18296 . . . . . . . . . . . . 13 (ℝ+ ∈ (SubGrp‘(𝑀s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))))
5250, 51ax-mp 5 . . . . . . . . . . . 12 + ∈ (SubMnd‘(𝑀s (ℂ ∖ {0})))
53 cnfldbas 20098 . . . . . . . . . . . . . . 15 ℂ = (Base‘ℂfld)
54 cndrng 20123 . . . . . . . . . . . . . . 15 fld ∈ DivRing
5553, 1, 54drngui 19504 . . . . . . . . . . . . . 14 (ℂ ∖ {0}) = (Unit‘ℂfld)
5655, 48unitsubm 19419 . . . . . . . . . . . . 13 (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
57 eqid 2801 . . . . . . . . . . . . . 14 (𝑀s (ℂ ∖ {0})) = (𝑀s (ℂ ∖ {0}))
5857subsubm 17976 . . . . . . . . . . . . 13 ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
592, 56, 58mp2b 10 . . . . . . . . . . . 12 (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
6052, 59mpbi 233 . . . . . . . . . . 11 (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
6160simpli 487 . . . . . . . . . 10 + ∈ (SubMnd‘𝑀)
62 eqid 2801 . . . . . . . . . . 11 (𝑀s+) = (𝑀s+)
6362submbas 17974 . . . . . . . . . 10 (ℝ+ ∈ (SubMnd‘𝑀) → ℝ+ = (Base‘(𝑀s+)))
6461, 63ax-mp 5 . . . . . . . . 9 + = (Base‘(𝑀s+))
65 cnfld1 20119 . . . . . . . . . . . 12 1 = (1r‘ℂfld)
6648, 65ringidval 19249 . . . . . . . . . . 11 1 = (0g𝑀)
6762, 66subm0 17975 . . . . . . . . . 10 (ℝ+ ∈ (SubMnd‘𝑀) → 1 = (0g‘(𝑀s+)))
6861, 67ax-mp 5 . . . . . . . . 9 1 = (0g‘(𝑀s+))
69 cncrng 20115 . . . . . . . . . . 11 fld ∈ CRing
7048crngmgp 19301 . . . . . . . . . . 11 (ℂfld ∈ CRing → 𝑀 ∈ CMnd)
7169, 70mp1i 13 . . . . . . . . . 10 (𝜑𝑀 ∈ CMnd)
7262submmnd 17973 . . . . . . . . . . 11 (ℝ+ ∈ (SubMnd‘𝑀) → (𝑀s+) ∈ Mnd)
7361, 72mp1i 13 . . . . . . . . . 10 (𝜑 → (𝑀s+) ∈ Mnd)
7462subcmn 18953 . . . . . . . . . 10 ((𝑀 ∈ CMnd ∧ (𝑀s+) ∈ Mnd) → (𝑀s+) ∈ CMnd)
7571, 73, 74syl2anc 587 . . . . . . . . 9 (𝜑 → (𝑀s+) ∈ CMnd)
76 df-refld 20297 . . . . . . . . . . . 12 fld = (ℂflds ℝ)
7776subrgring 19534 . . . . . . . . . . 11 (ℝ ∈ (SubRing‘ℂfld) → ℝfld ∈ Ring)
787, 77ax-mp 5 . . . . . . . . . 10 fld ∈ Ring
79 ringmnd 19303 . . . . . . . . . 10 (ℝfld ∈ Ring → ℝfld ∈ Mnd)
8078, 79mp1i 13 . . . . . . . . 9 (𝜑 → ℝfld ∈ Mnd)
8148oveq1i 7149 . . . . . . . . . . . 12 (𝑀s+) = ((mulGrp‘ℂfld) ↾s+)
8281reloggim 25193 . . . . . . . . . . 11 (log ↾ ℝ+) ∈ ((𝑀s+) GrpIso ℝfld)
83 gimghm 18399 . . . . . . . . . . 11 ((log ↾ ℝ+) ∈ ((𝑀s+) GrpIso ℝfld) → (log ↾ ℝ+) ∈ ((𝑀s+) GrpHom ℝfld))
8482, 83ax-mp 5 . . . . . . . . . 10 (log ↾ ℝ+) ∈ ((𝑀s+) GrpHom ℝfld)
85 ghmmhm 18363 . . . . . . . . . 10 ((log ↾ ℝ+) ∈ ((𝑀s+) GrpHom ℝfld) → (log ↾ ℝ+) ∈ ((𝑀s+) MndHom ℝfld))
8684, 85mp1i 13 . . . . . . . . 9 (𝜑 → (log ↾ ℝ+) ∈ ((𝑀s+) MndHom ℝfld))
87 1ex 10630 . . . . . . . . . . 11 1 ∈ V
8887a1i 11 . . . . . . . . . 10 (𝜑 → 1 ∈ V)
8910, 5, 88fdmfifsupp 8831 . . . . . . . . 9 (𝜑𝐹 finSupp 1)
9064, 68, 75, 80, 5, 86, 10, 89gsummhm 19054 . . . . . . . 8 (𝜑 → (ℝfld Σg ((log ↾ ℝ+) ∘ 𝐹)) = ((log ↾ ℝ+)‘((𝑀s+) Σg 𝐹)))
91 subgsubm 18296 . . . . . . . . . 10 (ℝ ∈ (SubGrp‘ℂfld) → ℝ ∈ (SubMnd‘ℂfld))
929, 91syl 17 . . . . . . . . 9 (𝜑 → ℝ ∈ (SubMnd‘ℂfld))
93 fco 6509 . . . . . . . . . 10 (((log ↾ ℝ+):ℝ+⟶ℝ ∧ 𝐹:𝐴⟶ℝ+) → ((log ↾ ℝ+) ∘ 𝐹):𝐴⟶ℝ)
9439, 10, 93syl2anc 587 . . . . . . . . 9 (𝜑 → ((log ↾ ℝ+) ∘ 𝐹):𝐴⟶ℝ)
955, 92, 94, 76gsumsubm 17994 . . . . . . . 8 (𝜑 → (ℂfld Σg ((log ↾ ℝ+) ∘ 𝐹)) = (ℝfld Σg ((log ↾ ℝ+) ∘ 𝐹)))
9661a1i 11 . . . . . . . . . 10 (𝜑 → ℝ+ ∈ (SubMnd‘𝑀))
975, 96, 10, 62gsumsubm 17994 . . . . . . . . 9 (𝜑 → (𝑀 Σg 𝐹) = ((𝑀s+) Σg 𝐹))
9897fveq2d 6653 . . . . . . . 8 (𝜑 → ((log ↾ ℝ+)‘(𝑀 Σg 𝐹)) = ((log ↾ ℝ+)‘((𝑀s+) Σg 𝐹)))
9990, 95, 983eqtr4d 2846 . . . . . . 7 (𝜑 → (ℂfld Σg ((log ↾ ℝ+) ∘ 𝐹)) = ((log ↾ ℝ+)‘(𝑀 Σg 𝐹)))
10066, 71, 5, 96, 10, 89gsumsubmcl 19035 . . . . . . . 8 (𝜑 → (𝑀 Σg 𝐹) ∈ ℝ+)
101100fvresd 6669 . . . . . . 7 (𝜑 → ((log ↾ ℝ+)‘(𝑀 Σg 𝐹)) = (log‘(𝑀 Σg 𝐹)))
10247, 99, 1013eqtrd 2840 . . . . . 6 (𝜑 → -(ℂfld Σg (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) = (log‘(𝑀 Σg 𝐹)))
103102oveq1d 7154 . . . . 5 (𝜑 → (-(ℂfld Σg (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) / (♯‘𝐴)) = ((log‘(𝑀 Σg 𝐹)) / (♯‘𝐴)))
104100relogcld 25217 . . . . . . 7 (𝜑 → (log‘(𝑀 Σg 𝐹)) ∈ ℝ)
105104recnd 10662 . . . . . 6 (𝜑 → (log‘(𝑀 Σg 𝐹)) ∈ ℂ)
106105, 24, 25divrec2d 11413 . . . . 5 (𝜑 → ((log‘(𝑀 Σg 𝐹)) / (♯‘𝐴)) = ((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹))))
10726, 103, 1063eqtrd 2840 . . . 4 (𝜑 → -((ℂfld Σg (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) / (♯‘𝐴)) = ((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹))))
10836oveq2d 7155 . . . . . . . . 9 (𝜑 → (ℂfld Σg 𝐹) = (ℂfld Σg (𝑘𝐴 ↦ (𝐹𝑘))))
10911rpcnd 12425 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℂ)
1105, 109gsumfsum 20161 . . . . . . . . 9 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ (𝐹𝑘))) = Σ𝑘𝐴 (𝐹𝑘))
111108, 110eqtrd 2836 . . . . . . . 8 (𝜑 → (ℂfld Σg 𝐹) = Σ𝑘𝐴 (𝐹𝑘))
1125, 20, 11fsumrpcl 15089 . . . . . . . 8 (𝜑 → Σ𝑘𝐴 (𝐹𝑘) ∈ ℝ+)
113111, 112eqeltrd 2893 . . . . . . 7 (𝜑 → (ℂfld Σg 𝐹) ∈ ℝ+)
11423nnrpd 12421 . . . . . . 7 (𝜑 → (♯‘𝐴) ∈ ℝ+)
115113, 114rpdivcld 12440 . . . . . 6 (𝜑 → ((ℂfld Σg 𝐹) / (♯‘𝐴)) ∈ ℝ+)
116115relogcld 25217 . . . . 5 (𝜑 → (log‘((ℂfld Σg 𝐹) / (♯‘𝐴))) ∈ ℝ)
11718, 23nndivred 11683 . . . . 5 (𝜑 → ((ℂfld Σg (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) / (♯‘𝐴)) ∈ ℝ)
118 rpssre 12388 . . . . . . . . 9 + ⊆ ℝ
119118a1i 11 . . . . . . . 8 (𝜑 → ℝ+ ⊆ ℝ)
120 relogcl 25170 . . . . . . . . . . 11 (𝑤 ∈ ℝ+ → (log‘𝑤) ∈ ℝ)
121120adantl 485 . . . . . . . . . 10 ((𝜑𝑤 ∈ ℝ+) → (log‘𝑤) ∈ ℝ)
122121renegcld 11060 . . . . . . . . 9 ((𝜑𝑤 ∈ ℝ+) → -(log‘𝑤) ∈ ℝ)
123122fmpttd 6860 . . . . . . . 8 (𝜑 → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)):ℝ+⟶ℝ)
124 ioorp 12807 . . . . . . . . . . . 12 (0(,)+∞) = ℝ+
125124eleq2i 2884 . . . . . . . . . . 11 (𝑎 ∈ (0(,)+∞) ↔ 𝑎 ∈ ℝ+)
126124eleq2i 2884 . . . . . . . . . . 11 (𝑏 ∈ (0(,)+∞) ↔ 𝑏 ∈ ℝ+)
127 iccssioo2 12802 . . . . . . . . . . 11 ((𝑎 ∈ (0(,)+∞) ∧ 𝑏 ∈ (0(,)+∞)) → (𝑎[,]𝑏) ⊆ (0(,)+∞))
128125, 126, 127syl2anbr 601 . . . . . . . . . 10 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → (𝑎[,]𝑏) ⊆ (0(,)+∞))
129128, 124sseqtrdi 3968 . . . . . . . . 9 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → (𝑎[,]𝑏) ⊆ ℝ+)
130129adantl 485 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) → (𝑎[,]𝑏) ⊆ ℝ+)
13123nnrecred 11680 . . . . . . . . . 10 (𝜑 → (1 / (♯‘𝐴)) ∈ ℝ)
132114rpreccld 12433 . . . . . . . . . . 11 (𝜑 → (1 / (♯‘𝐴)) ∈ ℝ+)
133132rpge0d 12427 . . . . . . . . . 10 (𝜑 → 0 ≤ (1 / (♯‘𝐴)))
134 elrege0 12836 . . . . . . . . . 10 ((1 / (♯‘𝐴)) ∈ (0[,)+∞) ↔ ((1 / (♯‘𝐴)) ∈ ℝ ∧ 0 ≤ (1 / (♯‘𝐴))))
135131, 133, 134sylanbrc 586 . . . . . . . . 9 (𝜑 → (1 / (♯‘𝐴)) ∈ (0[,)+∞))
136 fconst6g 6546 . . . . . . . . 9 ((1 / (♯‘𝐴)) ∈ (0[,)+∞) → (𝐴 × {(1 / (♯‘𝐴))}):𝐴⟶(0[,)+∞))
137135, 136syl 17 . . . . . . . 8 (𝜑 → (𝐴 × {(1 / (♯‘𝐴))}):𝐴⟶(0[,)+∞))
138 0lt1 11155 . . . . . . . . 9 0 < 1
139 fconstmpt 5582 . . . . . . . . . . 11 (𝐴 × {(1 / (♯‘𝐴))}) = (𝑘𝐴 ↦ (1 / (♯‘𝐴)))
140139oveq2i 7150 . . . . . . . . . 10 (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))})) = (ℂfld Σg (𝑘𝐴 ↦ (1 / (♯‘𝐴))))
141 ringmnd 19303 . . . . . . . . . . . . 13 (ℂfld ∈ Ring → ℂfld ∈ Mnd)
1422, 141mp1i 13 . . . . . . . . . . . 12 (𝜑 → ℂfld ∈ Mnd)
143131recnd 10662 . . . . . . . . . . . 12 (𝜑 → (1 / (♯‘𝐴)) ∈ ℂ)
144 eqid 2801 . . . . . . . . . . . . 13 (.g‘ℂfld) = (.g‘ℂfld)
14553, 144gsumconst 19050 . . . . . . . . . . . 12 ((ℂfld ∈ Mnd ∧ 𝐴 ∈ Fin ∧ (1 / (♯‘𝐴)) ∈ ℂ) → (ℂfld Σg (𝑘𝐴 ↦ (1 / (♯‘𝐴)))) = ((♯‘𝐴)(.g‘ℂfld)(1 / (♯‘𝐴))))
146142, 5, 143, 145syl3anc 1368 . . . . . . . . . . 11 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ (1 / (♯‘𝐴)))) = ((♯‘𝐴)(.g‘ℂfld)(1 / (♯‘𝐴))))
14723nnzd 12078 . . . . . . . . . . . 12 (𝜑 → (♯‘𝐴) ∈ ℤ)
148 cnfldmulg 20126 . . . . . . . . . . . 12 (((♯‘𝐴) ∈ ℤ ∧ (1 / (♯‘𝐴)) ∈ ℂ) → ((♯‘𝐴)(.g‘ℂfld)(1 / (♯‘𝐴))) = ((♯‘𝐴) · (1 / (♯‘𝐴))))
149147, 143, 148syl2anc 587 . . . . . . . . . . 11 (𝜑 → ((♯‘𝐴)(.g‘ℂfld)(1 / (♯‘𝐴))) = ((♯‘𝐴) · (1 / (♯‘𝐴))))
15024, 25recidd 11404 . . . . . . . . . . 11 (𝜑 → ((♯‘𝐴) · (1 / (♯‘𝐴))) = 1)
151146, 149, 1503eqtrd 2840 . . . . . . . . . 10 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ (1 / (♯‘𝐴)))) = 1)
152140, 151syl5eq 2848 . . . . . . . . 9 (𝜑 → (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))})) = 1)
153138, 152breqtrrid 5071 . . . . . . . 8 (𝜑 → 0 < (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))})))
154 logccv 25257 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
1551543adant1 1127 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
156 ioossre 12790 . . . . . . . . . . . . . . 15 (0(,)1) ⊆ ℝ
157 simp3 1135 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ (0(,)1))
158156, 157sseldi 3916 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ)
159 simp21 1203 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑥 ∈ ℝ+)
160159relogcld 25217 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈ ℝ)
161158, 160remulcld 10664 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℝ)
162 1re 10634 . . . . . . . . . . . . . . 15 1 ∈ ℝ
163 resubcl 10943 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 − 𝑡) ∈ ℝ)
164162, 158, 163sylancr 590 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℝ)
165 simp22 1204 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑦 ∈ ℝ+)
166165relogcld 25217 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈ ℝ)
167164, 166remulcld 10664 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈ ℝ)
168161, 167readdcld 10663 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) ∈ ℝ)
169 simp1 1133 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝜑)
170 ioossicc 12815 . . . . . . . . . . . . . . 15 (0(,)1) ⊆ (0[,]1)
171170, 157sseldi 3916 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ (0[,]1))
172119, 130cvxcl 25573 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ+)
173169, 159, 165, 171, 172syl13anc 1369 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ+)
174173relogcld 25217 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ ℝ)
175168, 174ltnegd 11211 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ↔ -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦)))))
176155, 175mpbid 235 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))))
177 fveq2 6649 . . . . . . . . . . . . 13 (𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) → (log‘𝑤) = (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
178177negeqd 10873 . . . . . . . . . . . 12 (𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) → -(log‘𝑤) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
179 eqid 2801 . . . . . . . . . . . 12 (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤))
180 negex 10877 . . . . . . . . . . . 12 -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ V
181178, 179, 180fvmpt 6749 . . . . . . . . . . 11 (((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ+ → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
182173, 181syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
183 fveq2 6649 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑥 → (log‘𝑤) = (log‘𝑥))
184183negeqd 10873 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑥 → -(log‘𝑤) = -(log‘𝑥))
185 negex 10877 . . . . . . . . . . . . . . . 16 -(log‘𝑥) ∈ V
186184, 179, 185fvmpt 6749 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ+ → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥) = -(log‘𝑥))
187159, 186syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥) = -(log‘𝑥))
188187oveq2d 7155 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) = (𝑡 · -(log‘𝑥)))
189158recnd 10662 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℂ)
190160recnd 10662 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈ ℂ)
191189, 190mulneg2d 11087 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · -(log‘𝑥)) = -(𝑡 · (log‘𝑥)))
192188, 191eqtrd 2836 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) = -(𝑡 · (log‘𝑥)))
193 fveq2 6649 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑦 → (log‘𝑤) = (log‘𝑦))
194193negeqd 10873 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑦 → -(log‘𝑤) = -(log‘𝑦))
195 negex 10877 . . . . . . . . . . . . . . . 16 -(log‘𝑦) ∈ V
196194, 179, 195fvmpt 6749 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℝ+ → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦) = -(log‘𝑦))
197165, 196syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦) = -(log‘𝑦))
198197oveq2d 7155 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦)) = ((1 − 𝑡) · -(log‘𝑦)))
199164recnd 10662 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℂ)
200166recnd 10662 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈ ℂ)
201199, 200mulneg2d 11087 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · -(log‘𝑦)) = -((1 − 𝑡) · (log‘𝑦)))
202198, 201eqtrd 2836 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦)) = -((1 − 𝑡) · (log‘𝑦)))
203192, 202oveq12d 7157 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦))) = (-(𝑡 · (log‘𝑥)) + -((1 − 𝑡) · (log‘𝑦))))
204161recnd 10662 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℂ)
205167recnd 10662 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈ ℂ)
206204, 205negdid 11003 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) = (-(𝑡 · (log‘𝑥)) + -((1 − 𝑡) · (log‘𝑦))))
207203, 206eqtr4d 2839 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦))) = -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))))
208176, 182, 2073brtr4d 5065 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦))))
209119, 123, 130, 208scvxcvx 25574 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ ℝ+𝑣 ∈ ℝ+𝑠 ∈ (0[,]1))) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((𝑠 · 𝑢) + ((1 − 𝑠) · 𝑣))) ≤ ((𝑠 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑢)) + ((1 − 𝑠) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑣))))
210119, 123, 130, 5, 137, 10, 153, 209jensen 25577 . . . . . . 7 (𝜑 → (((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f · 𝐹)) / (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))}))) ∈ ℝ+ ∧ ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f · 𝐹)) / (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))})))) ≤ ((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))})))))
211210simprd 499 . . . . . 6 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f · 𝐹)) / (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))})))) ≤ ((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))}))))
212131adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → (1 / (♯‘𝐴)) ∈ ℝ)
213139a1i 11 . . . . . . . . . . . . 13 (𝜑 → (𝐴 × {(1 / (♯‘𝐴))}) = (𝑘𝐴 ↦ (1 / (♯‘𝐴))))
2145, 212, 11, 213, 36offval2 7410 . . . . . . . . . . . 12 (𝜑 → ((𝐴 × {(1 / (♯‘𝐴))}) ∘f · 𝐹) = (𝑘𝐴 ↦ ((1 / (♯‘𝐴)) · (𝐹𝑘))))
215214oveq2d 7155 . . . . . . . . . . 11 (𝜑 → (ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f · 𝐹)) = (ℂfld Σg (𝑘𝐴 ↦ ((1 / (♯‘𝐴)) · (𝐹𝑘)))))
216 cnfldadd 20099 . . . . . . . . . . . 12 + = (+g‘ℂfld)
217 cnfldmul 20100 . . . . . . . . . . . 12 · = (.r‘ℂfld)
2182a1i 11 . . . . . . . . . . . 12 (𝜑 → ℂfld ∈ Ring)
219109fmpttd 6860 . . . . . . . . . . . . 13 (𝜑 → (𝑘𝐴 ↦ (𝐹𝑘)):𝐴⟶ℂ)
220219, 5, 16fdmfifsupp 8831 . . . . . . . . . . . 12 (𝜑 → (𝑘𝐴 ↦ (𝐹𝑘)) finSupp 0)
22153, 1, 216, 217, 218, 5, 143, 109, 220gsummulc2 19356 . . . . . . . . . . 11 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ ((1 / (♯‘𝐴)) · (𝐹𝑘)))) = ((1 / (♯‘𝐴)) · (ℂfld Σg (𝑘𝐴 ↦ (𝐹𝑘)))))
222 fss 6505 . . . . . . . . . . . . . . . 16 ((𝐹:𝐴⟶ℝ+ ∧ ℝ+ ⊆ ℝ) → 𝐹:𝐴⟶ℝ)
22310, 118, 222sylancl 589 . . . . . . . . . . . . . . 15 (𝜑𝐹:𝐴⟶ℝ)
22410, 5, 16fdmfifsupp 8831 . . . . . . . . . . . . . . 15 (𝜑𝐹 finSupp 0)
2251, 4, 5, 9, 223, 224gsumsubgcl 19036 . . . . . . . . . . . . . 14 (𝜑 → (ℂfld Σg 𝐹) ∈ ℝ)
226225recnd 10662 . . . . . . . . . . . . 13 (𝜑 → (ℂfld Σg 𝐹) ∈ ℂ)
227226, 24, 25divrec2d 11413 . . . . . . . . . . . 12 (𝜑 → ((ℂfld Σg 𝐹) / (♯‘𝐴)) = ((1 / (♯‘𝐴)) · (ℂfld Σg 𝐹)))
228108oveq2d 7155 . . . . . . . . . . . 12 (𝜑 → ((1 / (♯‘𝐴)) · (ℂfld Σg 𝐹)) = ((1 / (♯‘𝐴)) · (ℂfld Σg (𝑘𝐴 ↦ (𝐹𝑘)))))
229227, 228eqtr2d 2837 . . . . . . . . . . 11 (𝜑 → ((1 / (♯‘𝐴)) · (ℂfld Σg (𝑘𝐴 ↦ (𝐹𝑘)))) = ((ℂfld Σg 𝐹) / (♯‘𝐴)))
230215, 221, 2293eqtrd 2840 . . . . . . . . . 10 (𝜑 → (ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f · 𝐹)) = ((ℂfld Σg 𝐹) / (♯‘𝐴)))
231230, 152oveq12d 7157 . . . . . . . . 9 (𝜑 → ((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f · 𝐹)) / (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))}))) = (((ℂfld Σg 𝐹) / (♯‘𝐴)) / 1))
232225, 23nndivred 11683 . . . . . . . . . . 11 (𝜑 → ((ℂfld Σg 𝐹) / (♯‘𝐴)) ∈ ℝ)
233232recnd 10662 . . . . . . . . . 10 (𝜑 → ((ℂfld Σg 𝐹) / (♯‘𝐴)) ∈ ℂ)
234233div1d 11401 . . . . . . . . 9 (𝜑 → (((ℂfld Σg 𝐹) / (♯‘𝐴)) / 1) = ((ℂfld Σg 𝐹) / (♯‘𝐴)))
235231, 234eqtrd 2836 . . . . . . . 8 (𝜑 → ((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f · 𝐹)) / (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))}))) = ((ℂfld Σg 𝐹) / (♯‘𝐴)))
236235fveq2d 6653 . . . . . . 7 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f · 𝐹)) / (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))})))) = ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg 𝐹) / (♯‘𝐴))))
237 fveq2 6649 . . . . . . . . . 10 (𝑤 = ((ℂfld Σg 𝐹) / (♯‘𝐴)) → (log‘𝑤) = (log‘((ℂfld Σg 𝐹) / (♯‘𝐴))))
238237negeqd 10873 . . . . . . . . 9 (𝑤 = ((ℂfld Σg 𝐹) / (♯‘𝐴)) → -(log‘𝑤) = -(log‘((ℂfld Σg 𝐹) / (♯‘𝐴))))
239 negex 10877 . . . . . . . . 9 -(log‘((ℂfld Σg 𝐹) / (♯‘𝐴))) ∈ V
240238, 179, 239fvmpt 6749 . . . . . . . 8 (((ℂfld Σg 𝐹) / (♯‘𝐴)) ∈ ℝ+ → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg 𝐹) / (♯‘𝐴))) = -(log‘((ℂfld Σg 𝐹) / (♯‘𝐴))))
241115, 240syl 17 . . . . . . 7 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg 𝐹) / (♯‘𝐴))) = -(log‘((ℂfld Σg 𝐹) / (♯‘𝐴))))
242236, 241eqtrd 2836 . . . . . 6 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f · 𝐹)) / (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))})))) = -(log‘((ℂfld Σg 𝐹) / (♯‘𝐴))))
24353, 1, 216, 217, 218, 5, 143, 31, 17gsummulc2 19356 . . . . . . . . 9 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ ((1 / (♯‘𝐴)) · -(log‘(𝐹𝑘))))) = ((1 / (♯‘𝐴)) · (ℂfld Σg (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))))
244 negex 10877 . . . . . . . . . . . 12 -(log‘(𝐹𝑘)) ∈ V
245244a1i 11 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → -(log‘(𝐹𝑘)) ∈ V)
246 eqidd 2802 . . . . . . . . . . . 12 (𝜑 → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)))
247 fveq2 6649 . . . . . . . . . . . . 13 (𝑤 = (𝐹𝑘) → (log‘𝑤) = (log‘(𝐹𝑘)))
248247negeqd 10873 . . . . . . . . . . . 12 (𝑤 = (𝐹𝑘) → -(log‘𝑤) = -(log‘(𝐹𝑘)))
24911, 36, 246, 248fmptco 6872 . . . . . . . . . . 11 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹) = (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))
2505, 212, 245, 213, 249offval2 7410 . . . . . . . . . 10 (𝜑 → ((𝐴 × {(1 / (♯‘𝐴))}) ∘f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹)) = (𝑘𝐴 ↦ ((1 / (♯‘𝐴)) · -(log‘(𝐹𝑘)))))
251250oveq2d 7155 . . . . . . . . 9 (𝜑 → (ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) = (ℂfld Σg (𝑘𝐴 ↦ ((1 / (♯‘𝐴)) · -(log‘(𝐹𝑘))))))
25219, 24, 25divrec2d 11413 . . . . . . . . 9 (𝜑 → ((ℂfld Σg (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) / (♯‘𝐴)) = ((1 / (♯‘𝐴)) · (ℂfld Σg (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))))
253243, 251, 2523eqtr4d 2846 . . . . . . . 8 (𝜑 → (ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) = ((ℂfld Σg (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) / (♯‘𝐴)))
254253, 152oveq12d 7157 . . . . . . 7 (𝜑 → ((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))}))) = (((ℂfld Σg (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) / (♯‘𝐴)) / 1))
255117recnd 10662 . . . . . . . 8 (𝜑 → ((ℂfld Σg (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) / (♯‘𝐴)) ∈ ℂ)
256255div1d 11401 . . . . . . 7 (𝜑 → (((ℂfld Σg (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) / (♯‘𝐴)) / 1) = ((ℂfld Σg (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) / (♯‘𝐴)))
257254, 256eqtrd 2836 . . . . . 6 (𝜑 → ((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))}))) = ((ℂfld Σg (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) / (♯‘𝐴)))
258211, 242, 2573brtr3d 5064 . . . . 5 (𝜑 → -(log‘((ℂfld Σg 𝐹) / (♯‘𝐴))) ≤ ((ℂfld Σg (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) / (♯‘𝐴)))
259116, 117, 258lenegcon1d 11215 . . . 4 (𝜑 → -((ℂfld Σg (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) / (♯‘𝐴)) ≤ (log‘((ℂfld Σg 𝐹) / (♯‘𝐴))))
260107, 259eqbrtrrd 5057 . . 3 (𝜑 → ((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹))) ≤ (log‘((ℂfld Σg 𝐹) / (♯‘𝐴))))
261131, 104remulcld 10664 . . . 4 (𝜑 → ((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹))) ∈ ℝ)
262 efle 15466 . . . 4 ((((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹))) ∈ ℝ ∧ (log‘((ℂfld Σg 𝐹) / (♯‘𝐴))) ∈ ℝ) → (((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹))) ≤ (log‘((ℂfld Σg 𝐹) / (♯‘𝐴))) ↔ (exp‘((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹)))) ≤ (exp‘(log‘((ℂfld Σg 𝐹) / (♯‘𝐴))))))
263261, 116, 262syl2anc 587 . . 3 (𝜑 → (((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹))) ≤ (log‘((ℂfld Σg 𝐹) / (♯‘𝐴))) ↔ (exp‘((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹)))) ≤ (exp‘(log‘((ℂfld Σg 𝐹) / (♯‘𝐴))))))
264260, 263mpbid 235 . 2 (𝜑 → (exp‘((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹)))) ≤ (exp‘(log‘((ℂfld Σg 𝐹) / (♯‘𝐴)))))
265100rpcnd 12425 . . 3 (𝜑 → (𝑀 Σg 𝐹) ∈ ℂ)
266100rpne0d 12428 . . 3 (𝜑 → (𝑀 Σg 𝐹) ≠ 0)
267265, 266, 143cxpefd 25306 . 2 (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 / (♯‘𝐴))) = (exp‘((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹)))))
268115reeflogd 25218 . . 3 (𝜑 → (exp‘(log‘((ℂfld Σg 𝐹) / (♯‘𝐴)))) = ((ℂfld Σg 𝐹) / (♯‘𝐴)))
269268eqcomd 2807 . 2 (𝜑 → ((ℂfld Σg 𝐹) / (♯‘𝐴)) = (exp‘(log‘((ℂfld Σg 𝐹) / (♯‘𝐴)))))
270264, 267, 2693brtr4d 5065 1 (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 / (♯‘𝐴))) ≤ ((ℂfld Σg 𝐹) / (♯‘𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2112  wne 2990  Vcvv 3444  cdif 3881  wss 3884  c0 4246  {csn 4528   class class class wbr 5033  cmpt 5113   × cxp 5521  cres 5525  ccom 5527  wf 6324  1-1-ontowf1o 6327  cfv 6328  (class class class)co 7139  f cof 7391  Fincfn 8496  cc 10528  cr 10529  0cc0 10530  1c1 10531   + caddc 10533   · cmul 10535  +∞cpnf 10665   < clt 10668  cle 10669  cmin 10863  -cneg 10864   / cdiv 11290  cn 11629  cz 11973  +crp 12381  (,)cioo 12730  [,)cico 12732  [,]cicc 12733  chash 13690  Σcsu 15037  expce 15410  Basecbs 16478  s cress 16479  0gc0g 16708   Σg cgsu 16709  Mndcmnd 17906   MndHom cmhm 17949  SubMndcsubmnd 17950  .gcmg 18219  SubGrpcsubg 18268   GrpHom cghm 18350   GrpIso cgim 18392  CMndccmn 18901  Abelcabl 18902  mulGrpcmgp 19235  Ringcrg 19293  CRingccrg 19294  DivRingcdr 19498  SubRingcsubrg 19527  fldccnfld 20094  fldcrefld 20296  logclog 25149  𝑐ccxp 25150
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-inf2 9092  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-pre-sup 10608  ax-addf 10609  ax-mulf 10610
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-of 7393  df-om 7565  df-1st 7675  df-2nd 7676  df-supp 7818  df-tpos 7879  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-map 8395  df-pm 8396  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-card 9356  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-nn 11630  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-ioo 12734  df-ioc 12735  df-ico 12736  df-icc 12737  df-fz 12890  df-fzo 13033  df-fl 13161  df-mod 13237  df-seq 13369  df-exp 13430  df-fac 13634  df-bc 13663  df-hash 13691  df-shft 14421  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-limsup 14823  df-clim 14840  df-rlim 14841  df-sum 15038  df-ef 15416  df-sin 15418  df-cos 15419  df-pi 15421  df-struct 16480  df-ndx 16481  df-slot 16482  df-base 16484  df-sets 16485  df-ress 16486  df-plusg 16573  df-mulr 16574  df-starv 16575  df-sca 16576  df-vsca 16577  df-ip 16578  df-tset 16579  df-ple 16580  df-ds 16582  df-unif 16583  df-hom 16584  df-cco 16585  df-rest 16691  df-topn 16692  df-0g 16710  df-gsum 16711  df-topgen 16712  df-pt 16713  df-prds 16716  df-xrs 16770  df-qtop 16775  df-imas 16776  df-xps 16778  df-mre 16852  df-mrc 16853  df-acs 16855  df-mgm 17847  df-sgrp 17896  df-mnd 17907  df-mhm 17951  df-submnd 17952  df-grp 18101  df-minusg 18102  df-mulg 18220  df-subg 18271  df-ghm 18351  df-gim 18394  df-cntz 18442  df-cmn 18903  df-abl 18904  df-mgp 19236  df-ur 19248  df-ring 19295  df-cring 19296  df-oppr 19372  df-dvdsr 19390  df-unit 19391  df-invr 19421  df-dvr 19432  df-drng 19500  df-subrg 19529  df-psmet 20086  df-xmet 20087  df-met 20088  df-bl 20089  df-mopn 20090  df-fbas 20091  df-fg 20092  df-cnfld 20095  df-refld 20297  df-top 21502  df-topon 21519  df-topsp 21541  df-bases 21554  df-cld 21627  df-ntr 21628  df-cls 21629  df-nei 21706  df-lp 21744  df-perf 21745  df-cn 21835  df-cnp 21836  df-haus 21923  df-cmp 21995  df-tx 22170  df-hmeo 22363  df-fil 22454  df-fm 22546  df-flim 22547  df-flf 22548  df-xms 22930  df-ms 22931  df-tms 22932  df-cncf 23486  df-limc 24472  df-dv 24473  df-log 25151  df-cxp 25152
This theorem is referenced by:  amgm  25579  amgm2d  40891  amgm3d  40892  amgm4d  40893
  Copyright terms: Public domain W3C validator