Metamath Proof Explorer

Theorem amgmlem

Description: Lemma for amgm . (Contributed by Mario Carneiro, 21-Jun-2015)

Ref Expression
Hypotheses amgm.1 ⊢ 𝑀 = ( mulGrp ‘ ℂfld )
amgm.2 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
amgm.3 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
amgm.4 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ+ )
Assertion amgmlem ( 𝜑 → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) ≤ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 amgm.1 ⊢ 𝑀 = ( mulGrp ‘ ℂfld )
2 amgm.2 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
3 amgm.3 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
4 amgm.4 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ+ )
5 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
6 cnring ⊢ ℂfld ∈ Ring
7 ringabl ⊢ ( ℂfld ∈ Ring → ℂfld ∈ Abel )
8 6 7 mp1i ⊢ ( 𝜑 → ℂfld ∈ Abel )
9 resubdrg ⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) ∧ ℝfld ∈ DivRing )
10 9 simpli ⊢ ℝ ∈ ( SubRing ‘ ℂfld )
11 subrgsubg ⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) → ℝ ∈ ( SubGrp ‘ ℂfld ) )
12 10 11 mp1i ⊢ ( 𝜑 → ℝ ∈ ( SubGrp ‘ ℂfld ) )
13 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ+ )
14 13 relogcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
15 14 renegcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
16 15 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) : 𝐴 ⟶ ℝ )
17 c0ex ⊢ 0 ∈ V
18 17 a1i ⊢ ( 𝜑 → 0 ∈ V )
19 16 2 18 fdmfifsupp ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) finSupp 0 )
20 5 8 2 12 16 19 gsumsubgcl ⊢ ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ∈ ℝ )
21 20 recnd ⊢ ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ∈ ℂ )
22 hashnncl ⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ 𝐴 ≠ ∅ ) )
23 2 22 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ 𝐴 ≠ ∅ ) )
24 3 23 mpbird ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℕ )
25 24 nncnd ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℂ )
26 24 nnne0d ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ≠ 0 )
27 21 25 26 divnegd ⊢ ( 𝜑 → - ( ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) / ( ♯ ‘ 𝐴 ) ) = ( - ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) / ( ♯ ‘ 𝐴 ) ) )
28 14 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℂ )
29 2 28 gsumfsum ⊢ ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = Σ 𝑘 ∈ 𝐴 ( log ‘ ( 𝐹 ‘ 𝑘 ) ) )
30 28 negnegd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → - - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) = ( log ‘ ( 𝐹 ‘ 𝑘 ) ) )
31 30 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 - - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) = Σ 𝑘 ∈ 𝐴 ( log ‘ ( 𝐹 ‘ 𝑘 ) ) )
32 15 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℂ )
33 2 32 fsumneg ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 - - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) = - Σ 𝑘 ∈ 𝐴 - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) )
34 29 31 33 3eqtr2rd ⊢ ( 𝜑 → - Σ 𝑘 ∈ 𝐴 - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
35 2 32 gsumfsum ⊢ ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = Σ 𝑘 ∈ 𝐴 - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) )
36 35 negeqd ⊢ ( 𝜑 → - ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = - Σ 𝑘 ∈ 𝐴 - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) )
37 4 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) )
38 relogf1o ⊢ ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ
39 f1of ⊢ ( ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ → ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ )
40 38 39 mp1i ⊢ ( 𝜑 → ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ )
41 40 feqmptd ⊢ ( 𝜑 → ( log ↾ ℝ+ ) = ( 𝑥 ∈ ℝ+ ↦ ( ( log ↾ ℝ+ ) ‘ 𝑥 ) ) )
42 fvres ⊢ ( 𝑥 ∈ ℝ+ → ( ( log ↾ ℝ+ ) ‘ 𝑥 ) = ( log ‘ 𝑥 ) )
43 42 mpteq2ia ⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( log ↾ ℝ+ ) ‘ 𝑥 ) ) = ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) )
44 41 43 eqtrdi ⊢ ( 𝜑 → ( log ↾ ℝ+ ) = ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) )
45 fveq2 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑘 ) → ( log ‘ 𝑥 ) = ( log ‘ ( 𝐹 ‘ 𝑘 ) ) )
46 13 37 44 45 fmptco ⊢ ( 𝜑 → ( ( log ↾ ℝ+ ) ∘ 𝐹 ) = ( 𝑘 ∈ 𝐴 ↦ ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
47 46 oveq2d ⊢ ( 𝜑 → ( ℂfld Σg ( ( log ↾ ℝ+ ) ∘ 𝐹 ) ) = ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
48 34 36 47 3eqtr4d ⊢ ( 𝜑 → - ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( ℂfld Σg ( ( log ↾ ℝ+ ) ∘ 𝐹 ) ) )
49 1 oveq1i ⊢ ( 𝑀 ↾s ( ℂ ∖ { 0 } ) ) = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
50 49 rpmsubg ⊢ ℝ+ ∈ ( SubGrp ‘ ( 𝑀 ↾s ( ℂ ∖ { 0 } ) ) )
51 subgsubm ⊢ ( ℝ+ ∈ ( SubGrp ‘ ( 𝑀 ↾s ( ℂ ∖ { 0 } ) ) ) → ℝ+ ∈ ( SubMnd ‘ ( 𝑀 ↾s ( ℂ ∖ { 0 } ) ) ) )
52 50 51 ax-mp ⊢ ℝ+ ∈ ( SubMnd ‘ ( 𝑀 ↾s ( ℂ ∖ { 0 } ) ) )
53 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
54 cndrng ⊢ ℂfld ∈ DivRing
55 53 5 54 drngui ⊢ ( ℂ ∖ { 0 } ) = ( Unit ‘ ℂfld )
56 55 1 unitsubm ⊢ ( ℂfld ∈ Ring → ( ℂ ∖ { 0 } ) ∈ ( SubMnd ‘ 𝑀 ) )
57 eqid ⊢ ( 𝑀 ↾s ( ℂ ∖ { 0 } ) ) = ( 𝑀 ↾s ( ℂ ∖ { 0 } ) )
58 57 subsubm ⊢ ( ( ℂ ∖ { 0 } ) ∈ ( SubMnd ‘ 𝑀 ) → ( ℝ+ ∈ ( SubMnd ‘ ( 𝑀 ↾s ( ℂ ∖ { 0 } ) ) ) ↔ ( ℝ+ ∈ ( SubMnd ‘ 𝑀 ) ∧ ℝ+ ⊆ ( ℂ ∖ { 0 } ) ) ) )
59 6 56 58 mp2b ⊢ ( ℝ+ ∈ ( SubMnd ‘ ( 𝑀 ↾s ( ℂ ∖ { 0 } ) ) ) ↔ ( ℝ+ ∈ ( SubMnd ‘ 𝑀 ) ∧ ℝ+ ⊆ ( ℂ ∖ { 0 } ) ) )
60 52 59 mpbi ⊢ ( ℝ+ ∈ ( SubMnd ‘ 𝑀 ) ∧ ℝ+ ⊆ ( ℂ ∖ { 0 } ) )
61 60 simpli ⊢ ℝ+ ∈ ( SubMnd ‘ 𝑀 )
62 eqid ⊢ ( 𝑀 ↾s ℝ+ ) = ( 𝑀 ↾s ℝ+ )
63 62 submbas ⊢ ( ℝ+ ∈ ( SubMnd ‘ 𝑀 ) → ℝ+ = ( Base ‘ ( 𝑀 ↾s ℝ+ ) ) )
64 61 63 ax-mp ⊢ ℝ+ = ( Base ‘ ( 𝑀 ↾s ℝ+ ) )
65 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
66 1 65 ringidval ⊢ 1 = ( 0g ‘ 𝑀 )
67 62 66 subm0 ⊢ ( ℝ+ ∈ ( SubMnd ‘ 𝑀 ) → 1 = ( 0g ‘ ( 𝑀 ↾s ℝ+ ) ) )
68 61 67 ax-mp ⊢ 1 = ( 0g ‘ ( 𝑀 ↾s ℝ+ ) )
69 cncrng ⊢ ℂfld ∈ CRing
70 1 crngmgp ⊢ ( ℂfld ∈ CRing → 𝑀 ∈ CMnd )
71 69 70 mp1i ⊢ ( 𝜑 → 𝑀 ∈ CMnd )
72 62 submmnd ⊢ ( ℝ+ ∈ ( SubMnd ‘ 𝑀 ) → ( 𝑀 ↾s ℝ+ ) ∈ Mnd )
73 61 72 mp1i ⊢ ( 𝜑 → ( 𝑀 ↾s ℝ+ ) ∈ Mnd )
74 62 subcmn ⊢ ( ( 𝑀 ∈ CMnd ∧ ( 𝑀 ↾s ℝ+ ) ∈ Mnd ) → ( 𝑀 ↾s ℝ+ ) ∈ CMnd )
75 71 73 74 syl2anc ⊢ ( 𝜑 → ( 𝑀 ↾s ℝ+ ) ∈ CMnd )
76 df-refld ⊢ ℝfld = ( ℂfld ↾s ℝ )
77 76 subrgring ⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) → ℝfld ∈ Ring )
78 10 77 ax-mp ⊢ ℝfld ∈ Ring
79 ringmnd ⊢ ( ℝfld ∈ Ring → ℝfld ∈ Mnd )
80 78 79 mp1i ⊢ ( 𝜑 → ℝfld ∈ Mnd )
81 1 oveq1i ⊢ ( 𝑀 ↾s ℝ+ ) = ( ( mulGrp ‘ ℂfld ) ↾s ℝ+ )
82 81 reloggim ⊢ ( log ↾ ℝ+ ) ∈ ( ( 𝑀 ↾s ℝ+ ) GrpIso ℝfld )
83 gimghm ⊢ ( ( log ↾ ℝ+ ) ∈ ( ( 𝑀 ↾s ℝ+ ) GrpIso ℝfld ) → ( log ↾ ℝ+ ) ∈ ( ( 𝑀 ↾s ℝ+ ) GrpHom ℝfld ) )
84 82 83 ax-mp ⊢ ( log ↾ ℝ+ ) ∈ ( ( 𝑀 ↾s ℝ+ ) GrpHom ℝfld )
85 ghmmhm ⊢ ( ( log ↾ ℝ+ ) ∈ ( ( 𝑀 ↾s ℝ+ ) GrpHom ℝfld ) → ( log ↾ ℝ+ ) ∈ ( ( 𝑀 ↾s ℝ+ ) MndHom ℝfld ) )
86 84 85 mp1i ⊢ ( 𝜑 → ( log ↾ ℝ+ ) ∈ ( ( 𝑀 ↾s ℝ+ ) MndHom ℝfld ) )
87 1ex ⊢ 1 ∈ V
88 87 a1i ⊢ ( 𝜑 → 1 ∈ V )
89 4 2 88 fdmfifsupp ⊢ ( 𝜑 → 𝐹 finSupp 1 )
90 64 68 75 80 2 86 4 89 gsummhm ⊢ ( 𝜑 → ( ℝfld Σg ( ( log ↾ ℝ+ ) ∘ 𝐹 ) ) = ( ( log ↾ ℝ+ ) ‘ ( ( 𝑀 ↾s ℝ+ ) Σg 𝐹 ) ) )
91 subgsubm ⊢ ( ℝ ∈ ( SubGrp ‘ ℂfld ) → ℝ ∈ ( SubMnd ‘ ℂfld ) )
92 12 91 syl ⊢ ( 𝜑 → ℝ ∈ ( SubMnd ‘ ℂfld ) )
93 fco ⊢ ( ( ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) → ( ( log ↾ ℝ+ ) ∘ 𝐹 ) : 𝐴 ⟶ ℝ )
94 40 4 93 syl2anc ⊢ ( 𝜑 → ( ( log ↾ ℝ+ ) ∘ 𝐹 ) : 𝐴 ⟶ ℝ )
95 2 92 94 76 gsumsubm ⊢ ( 𝜑 → ( ℂfld Σg ( ( log ↾ ℝ+ ) ∘ 𝐹 ) ) = ( ℝfld Σg ( ( log ↾ ℝ+ ) ∘ 𝐹 ) ) )
96 61 a1i ⊢ ( 𝜑 → ℝ+ ∈ ( SubMnd ‘ 𝑀 ) )
97 2 96 4 62 gsumsubm ⊢ ( 𝜑 → ( 𝑀 Σg 𝐹 ) = ( ( 𝑀 ↾s ℝ+ ) Σg 𝐹 ) )
98 97 fveq2d ⊢ ( 𝜑 → ( ( log ↾ ℝ+ ) ‘ ( 𝑀 Σg 𝐹 ) ) = ( ( log ↾ ℝ+ ) ‘ ( ( 𝑀 ↾s ℝ+ ) Σg 𝐹 ) ) )
99 90 95 98 3eqtr4d ⊢ ( 𝜑 → ( ℂfld Σg ( ( log ↾ ℝ+ ) ∘ 𝐹 ) ) = ( ( log ↾ ℝ+ ) ‘ ( 𝑀 Σg 𝐹 ) ) )
100 66 71 2 96 4 89 gsumsubmcl ⊢ ( 𝜑 → ( 𝑀 Σg 𝐹 ) ∈ ℝ+ )
101 100 fvresd ⊢ ( 𝜑 → ( ( log ↾ ℝ+ ) ‘ ( 𝑀 Σg 𝐹 ) ) = ( log ‘ ( 𝑀 Σg 𝐹 ) ) )
102 48 99 101 3eqtrd ⊢ ( 𝜑 → - ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( log ‘ ( 𝑀 Σg 𝐹 ) ) )
103 102 oveq1d ⊢ ( 𝜑 → ( - ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) / ( ♯ ‘ 𝐴 ) ) = ( ( log ‘ ( 𝑀 Σg 𝐹 ) ) / ( ♯ ‘ 𝐴 ) ) )
104 100 relogcld ⊢ ( 𝜑 → ( log ‘ ( 𝑀 Σg 𝐹 ) ) ∈ ℝ )
105 104 recnd ⊢ ( 𝜑 → ( log ‘ ( 𝑀 Σg 𝐹 ) ) ∈ ℂ )
106 105 25 26 divrec2d ⊢ ( 𝜑 → ( ( log ‘ ( 𝑀 Σg 𝐹 ) ) / ( ♯ ‘ 𝐴 ) ) = ( ( 1 / ( ♯ ‘ 𝐴 ) ) · ( log ‘ ( 𝑀 Σg 𝐹 ) ) ) )
107 27 103 106 3eqtrd ⊢ ( 𝜑 → - ( ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) / ( ♯ ‘ 𝐴 ) ) = ( ( 1 / ( ♯ ‘ 𝐴 ) ) · ( log ‘ ( 𝑀 Σg 𝐹 ) ) ) )
108 37 oveq2d ⊢ ( 𝜑 → ( ℂfld Σg 𝐹 ) = ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
109 13 rpcnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
110 2 109 gsumfsum ⊢ ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) )
111 108 110 eqtrd ⊢ ( 𝜑 → ( ℂfld Σg 𝐹 ) = Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) )
112 2 3 13 fsumrpcl ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ∈ ℝ+ )
113 111 112 eqeltrd ⊢ ( 𝜑 → ( ℂfld Σg 𝐹 ) ∈ ℝ+ )
114 24 nnrpd ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℝ+ )
115 113 114 rpdivcld ⊢ ( 𝜑 → ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ∈ ℝ+ )
116 115 relogcld ⊢ ( 𝜑 → ( log ‘ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) ∈ ℝ )
117 20 24 nndivred ⊢ ( 𝜑 → ( ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) / ( ♯ ‘ 𝐴 ) ) ∈ ℝ )
118 rpssre ⊢ ℝ+ ⊆ ℝ
119 118 a1i ⊢ ( 𝜑 → ℝ+ ⊆ ℝ )
120 relogcl ⊢ ( 𝑤 ∈ ℝ+ → ( log ‘ 𝑤 ) ∈ ℝ )
121 120 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ( log ‘ 𝑤 ) ∈ ℝ )
122 121 renegcld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → - ( log ‘ 𝑤 ) ∈ ℝ )
123 122 fmpttd ⊢ ( 𝜑 → ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) : ℝ+ ⟶ ℝ )
124 ioorp ⊢ ( 0 (,) +∞ ) = ℝ+
125 124 eleq2i ⊢ ( 𝑎 ∈ ( 0 (,) +∞ ) ↔ 𝑎 ∈ ℝ+ )
126 124 eleq2i ⊢ ( 𝑏 ∈ ( 0 (,) +∞ ) ↔ 𝑏 ∈ ℝ+ )
127 iccssioo2 ⊢ ( ( 𝑎 ∈ ( 0 (,) +∞ ) ∧ 𝑏 ∈ ( 0 (,) +∞ ) ) → ( 𝑎 [,] 𝑏 ) ⊆ ( 0 (,) +∞ ) )
128 125 126 127 syl2anbr ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → ( 𝑎 [,] 𝑏 ) ⊆ ( 0 (,) +∞ ) )
129 128 124 sseqtrdi ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → ( 𝑎 [,] 𝑏 ) ⊆ ℝ+ )
130 129 adantl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) → ( 𝑎 [,] 𝑏 ) ⊆ ℝ+ )
131 24 nnrecred ⊢ ( 𝜑 → ( 1 / ( ♯ ‘ 𝐴 ) ) ∈ ℝ )
132 114 rpreccld ⊢ ( 𝜑 → ( 1 / ( ♯ ‘ 𝐴 ) ) ∈ ℝ+ )
133 132 rpge0d ⊢ ( 𝜑 → 0 ≤ ( 1 / ( ♯ ‘ 𝐴 ) ) )
134 elrege0 ⊢ ( ( 1 / ( ♯ ‘ 𝐴 ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( 1 / ( ♯ ‘ 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( 1 / ( ♯ ‘ 𝐴 ) ) ) )
135 131 133 134 sylanbrc ⊢ ( 𝜑 → ( 1 / ( ♯ ‘ 𝐴 ) ) ∈ ( 0 [,) +∞ ) )
136 fconst6g ⊢ ( ( 1 / ( ♯ ‘ 𝐴 ) ) ∈ ( 0 [,) +∞ ) → ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) : 𝐴 ⟶ ( 0 [,) +∞ ) )
137 135 136 syl ⊢ ( 𝜑 → ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) : 𝐴 ⟶ ( 0 [,) +∞ ) )
138 0lt1 ⊢ 0 < 1
139 fconstmpt ⊢ ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) = ( 𝑘 ∈ 𝐴 ↦ ( 1 / ( ♯ ‘ 𝐴 ) ) )
140 139 oveq2i ⊢ ( ℂfld Σg ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ) = ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( 1 / ( ♯ ‘ 𝐴 ) ) ) )
141 ringmnd ⊢ ( ℂfld ∈ Ring → ℂfld ∈ Mnd )
142 6 141 mp1i ⊢ ( 𝜑 → ℂfld ∈ Mnd )
143 131 recnd ⊢ ( 𝜑 → ( 1 / ( ♯ ‘ 𝐴 ) ) ∈ ℂ )
144 eqid ⊢ ( .g ‘ ℂfld ) = ( .g ‘ ℂfld )
145 53 144 gsumconst ⊢ ( ( ℂfld ∈ Mnd ∧ 𝐴 ∈ Fin ∧ ( 1 / ( ♯ ‘ 𝐴 ) ) ∈ ℂ ) → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( 1 / ( ♯ ‘ 𝐴 ) ) ) ) = ( ( ♯ ‘ 𝐴 ) ( .g ‘ ℂfld ) ( 1 / ( ♯ ‘ 𝐴 ) ) ) )
146 142 2 143 145 syl3anc ⊢ ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( 1 / ( ♯ ‘ 𝐴 ) ) ) ) = ( ( ♯ ‘ 𝐴 ) ( .g ‘ ℂfld ) ( 1 / ( ♯ ‘ 𝐴 ) ) ) )
147 24 nnzd ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℤ )
148 cnfldmulg ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ ( 1 / ( ♯ ‘ 𝐴 ) ) ∈ ℂ ) → ( ( ♯ ‘ 𝐴 ) ( .g ‘ ℂfld ) ( 1 / ( ♯ ‘ 𝐴 ) ) ) = ( ( ♯ ‘ 𝐴 ) · ( 1 / ( ♯ ‘ 𝐴 ) ) ) )
149 147 143 148 syl2anc ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) ( .g ‘ ℂfld ) ( 1 / ( ♯ ‘ 𝐴 ) ) ) = ( ( ♯ ‘ 𝐴 ) · ( 1 / ( ♯ ‘ 𝐴 ) ) ) )
150 25 26 recidd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) · ( 1 / ( ♯ ‘ 𝐴 ) ) ) = 1 )
151 146 149 150 3eqtrd ⊢ ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( 1 / ( ♯ ‘ 𝐴 ) ) ) ) = 1 )
152 140 151 eqtrid ⊢ ( 𝜑 → ( ℂfld Σg ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ) = 1 )
153 138 152 breqtrrid ⊢ ( 𝜑 → 0 < ( ℂfld Σg ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ) )
154 logccv ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) < ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) )
155 154 3adant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) < ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) )
156 ioossre ⊢ ( 0 (,) 1 ) ⊆ ℝ
157 simp3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑡 ∈ ( 0 (,) 1 ) )
158 156 157 sselid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑡 ∈ ℝ )
159 simp21 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑥 ∈ ℝ+ )
160 159 relogcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
161 158 160 remulcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑡 · ( log ‘ 𝑥 ) ) ∈ ℝ )
162 1re ⊢ 1 ∈ ℝ
163 resubcl ⊢ ( ( 1 ∈ ℝ ∧ 𝑡 ∈ ℝ ) → ( 1 − 𝑡 ) ∈ ℝ )
164 162 158 163 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 − 𝑡 ) ∈ ℝ )
165 simp22 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑦 ∈ ℝ+ )
166 165 relogcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( log ‘ 𝑦 ) ∈ ℝ )
167 164 166 remulcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ∈ ℝ )
168 161 167 readdcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) ∈ ℝ )
169 simp1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝜑 )
170 ioossicc ⊢ ( 0 (,) 1 ) ⊆ ( 0 [,] 1 )
171 170 157 sselid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑡 ∈ ( 0 [,] 1 ) )
172 119 130 cvxcl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ ℝ+ )
173 169 159 165 171 172 syl13anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ ℝ+ )
174 173 relogcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ ℝ )
175 168 174 ltnegd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) < ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ↔ - ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < - ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) ) )
176 155 175 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → - ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < - ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) )
177 fveq2 ⊢ ( 𝑤 = ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) → ( log ‘ 𝑤 ) = ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) )
178 177 negeqd ⊢ ( 𝑤 = ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) → - ( log ‘ 𝑤 ) = - ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) )
179 eqid ⊢ ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) = ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) )
180 negex ⊢ - ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ V
181 178 179 180 fvmpt ⊢ ( ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ ℝ+ → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) = - ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) )
182 173 181 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) = - ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) )
183 fveq2 ⊢ ( 𝑤 = 𝑥 → ( log ‘ 𝑤 ) = ( log ‘ 𝑥 ) )
184 183 negeqd ⊢ ( 𝑤 = 𝑥 → - ( log ‘ 𝑤 ) = - ( log ‘ 𝑥 ) )
185 negex ⊢ - ( log ‘ 𝑥 ) ∈ V
186 184 179 185 fvmpt ⊢ ( 𝑥 ∈ ℝ+ → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑥 ) = - ( log ‘ 𝑥 ) )
187 159 186 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑥 ) = - ( log ‘ 𝑥 ) )
188 187 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑡 · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑥 ) ) = ( 𝑡 · - ( log ‘ 𝑥 ) ) )
189 158 recnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑡 ∈ ℂ )
190 160 recnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
191 189 190 mulneg2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑡 · - ( log ‘ 𝑥 ) ) = - ( 𝑡 · ( log ‘ 𝑥 ) ) )
192 188 191 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑡 · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑥 ) ) = - ( 𝑡 · ( log ‘ 𝑥 ) ) )
193 fveq2 ⊢ ( 𝑤 = 𝑦 → ( log ‘ 𝑤 ) = ( log ‘ 𝑦 ) )
194 193 negeqd ⊢ ( 𝑤 = 𝑦 → - ( log ‘ 𝑤 ) = - ( log ‘ 𝑦 ) )
195 negex ⊢ - ( log ‘ 𝑦 ) ∈ V
196 194 179 195 fvmpt ⊢ ( 𝑦 ∈ ℝ+ → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑦 ) = - ( log ‘ 𝑦 ) )
197 165 196 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑦 ) = - ( log ‘ 𝑦 ) )
198 197 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 1 − 𝑡 ) · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑦 ) ) = ( ( 1 − 𝑡 ) · - ( log ‘ 𝑦 ) ) )
199 164 recnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 − 𝑡 ) ∈ ℂ )
200 166 recnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( log ‘ 𝑦 ) ∈ ℂ )
201 199 200 mulneg2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 1 − 𝑡 ) · - ( log ‘ 𝑦 ) ) = - ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) )
202 198 201 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 1 − 𝑡 ) · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑦 ) ) = - ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) )
203 192 202 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑡 · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑦 ) ) ) = ( - ( 𝑡 · ( log ‘ 𝑥 ) ) + - ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) )
204 161 recnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑡 · ( log ‘ 𝑥 ) ) ∈ ℂ )
205 167 recnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ∈ ℂ )
206 204 205 negdid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → - ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) = ( - ( 𝑡 · ( log ‘ 𝑥 ) ) + - ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) )
207 203 206 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑡 · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑦 ) ) ) = - ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) )
208 176 182 207 3brtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑦 ) ) ) )
209 119 123 130 208 scvxcvx ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( 𝑠 · 𝑢 ) + ( ( 1 − 𝑠 ) · 𝑣 ) ) ) ≤ ( ( 𝑠 · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑢 ) ) + ( ( 1 − 𝑠 ) · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑣 ) ) ) )
210 119 123 130 2 137 4 153 209 jensen ⊢ ( 𝜑 → ( ( ( ℂfld Σg ( ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ∘f · 𝐹 ) ) / ( ℂfld Σg ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ) ) ∈ ℝ+ ∧ ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( ℂfld Σg ( ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ∘f · 𝐹 ) ) / ( ℂfld Σg ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ) ) ) ≤ ( ( ℂfld Σg ( ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ∘f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) / ( ℂfld Σg ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ) ) ) )
211 210 simprd ⊢ ( 𝜑 → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( ℂfld Σg ( ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ∘f · 𝐹 ) ) / ( ℂfld Σg ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ) ) ) ≤ ( ( ℂfld Σg ( ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ∘f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) / ( ℂfld Σg ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ) ) )
212 131 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 1 / ( ♯ ‘ 𝐴 ) ) ∈ ℝ )
213 139 a1i ⊢ ( 𝜑 → ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) = ( 𝑘 ∈ 𝐴 ↦ ( 1 / ( ♯ ‘ 𝐴 ) ) ) )
214 2 212 13 213 37 offval2 ⊢ ( 𝜑 → ( ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ∘f · 𝐹 ) = ( 𝑘 ∈ 𝐴 ↦ ( ( 1 / ( ♯ ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑘 ) ) ) )
215 214 oveq2d ⊢ ( 𝜑 → ( ℂfld Σg ( ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ∘f · 𝐹 ) ) = ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( ( 1 / ( ♯ ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑘 ) ) ) ) )
216 cnfldadd ⊢ + = ( +g ‘ ℂfld )
217 cnfldmul ⊢ · = ( .r ‘ ℂfld )
218 6 a1i ⊢ ( 𝜑 → ℂfld ∈ Ring )
219 109 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) : 𝐴 ⟶ ℂ )
220 219 2 18 fdmfifsupp ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) finSupp 0 )
221 53 5 216 217 218 2 143 109 220 gsummulc2 ⊢ ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( ( 1 / ( ♯ ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑘 ) ) ) ) = ( ( 1 / ( ♯ ‘ 𝐴 ) ) · ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ) )
222 fss ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ+ ∧ ℝ+ ⊆ ℝ ) → 𝐹 : 𝐴 ⟶ ℝ )
223 4 118 222 sylancl ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
224 4 2 18 fdmfifsupp ⊢ ( 𝜑 → 𝐹 finSupp 0 )
225 5 8 2 12 223 224 gsumsubgcl ⊢ ( 𝜑 → ( ℂfld Σg 𝐹 ) ∈ ℝ )
226 225 recnd ⊢ ( 𝜑 → ( ℂfld Σg 𝐹 ) ∈ ℂ )
227 226 25 26 divrec2d ⊢ ( 𝜑 → ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) = ( ( 1 / ( ♯ ‘ 𝐴 ) ) · ( ℂfld Σg 𝐹 ) ) )
228 108 oveq2d ⊢ ( 𝜑 → ( ( 1 / ( ♯ ‘ 𝐴 ) ) · ( ℂfld Σg 𝐹 ) ) = ( ( 1 / ( ♯ ‘ 𝐴 ) ) · ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ) )
229 227 228 eqtr2d ⊢ ( 𝜑 → ( ( 1 / ( ♯ ‘ 𝐴 ) ) · ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) )
230 215 221 229 3eqtrd ⊢ ( 𝜑 → ( ℂfld Σg ( ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ∘f · 𝐹 ) ) = ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) )
231 230 152 oveq12d ⊢ ( 𝜑 → ( ( ℂfld Σg ( ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ∘f · 𝐹 ) ) / ( ℂfld Σg ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ) ) = ( ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) / 1 ) )
232 225 24 nndivred ⊢ ( 𝜑 → ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ∈ ℝ )
233 232 recnd ⊢ ( 𝜑 → ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ∈ ℂ )
234 233 div1d ⊢ ( 𝜑 → ( ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) / 1 ) = ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) )
235 231 234 eqtrd ⊢ ( 𝜑 → ( ( ℂfld Σg ( ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ∘f · 𝐹 ) ) / ( ℂfld Σg ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ) ) = ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) )
236 235 fveq2d ⊢ ( 𝜑 → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( ℂfld Σg ( ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ∘f · 𝐹 ) ) / ( ℂfld Σg ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ) ) ) = ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) )
237 fveq2 ⊢ ( 𝑤 = ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) → ( log ‘ 𝑤 ) = ( log ‘ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) )
238 237 negeqd ⊢ ( 𝑤 = ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) → - ( log ‘ 𝑤 ) = - ( log ‘ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) )
239 negex ⊢ - ( log ‘ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) ∈ V
240 238 179 239 fvmpt ⊢ ( ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ∈ ℝ+ → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) = - ( log ‘ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) )
241 115 240 syl ⊢ ( 𝜑 → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) = - ( log ‘ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) )
242 236 241 eqtrd ⊢ ( 𝜑 → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( ℂfld Σg ( ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ∘f · 𝐹 ) ) / ( ℂfld Σg ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ) ) ) = - ( log ‘ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) )
243 53 5 216 217 218 2 143 32 19 gsummulc2 ⊢ ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( ( 1 / ( ♯ ‘ 𝐴 ) ) · - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) = ( ( 1 / ( ♯ ‘ 𝐴 ) ) · ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
244 negex ⊢ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ V
245 244 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ V )
246 eqidd ⊢ ( 𝜑 → ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) = ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) )
247 fveq2 ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑘 ) → ( log ‘ 𝑤 ) = ( log ‘ ( 𝐹 ‘ 𝑘 ) ) )
248 247 negeqd ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑘 ) → - ( log ‘ 𝑤 ) = - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) )
249 13 37 246 248 fmptco ⊢ ( 𝜑 → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) = ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
250 2 212 245 213 249 offval2 ⊢ ( 𝜑 → ( ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ∘f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( ( 1 / ( ♯ ‘ 𝐴 ) ) · - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
251 250 oveq2d ⊢ ( 𝜑 → ( ℂfld Σg ( ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ∘f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) = ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( ( 1 / ( ♯ ‘ 𝐴 ) ) · - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
252 21 25 26 divrec2d ⊢ ( 𝜑 → ( ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) / ( ♯ ‘ 𝐴 ) ) = ( ( 1 / ( ♯ ‘ 𝐴 ) ) · ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
253 243 251 252 3eqtr4d ⊢ ( 𝜑 → ( ℂfld Σg ( ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ∘f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) = ( ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) / ( ♯ ‘ 𝐴 ) ) )
254 253 152 oveq12d ⊢ ( 𝜑 → ( ( ℂfld Σg ( ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ∘f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) / ( ℂfld Σg ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ) ) = ( ( ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) / ( ♯ ‘ 𝐴 ) ) / 1 ) )
255 117 recnd ⊢ ( 𝜑 → ( ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) / ( ♯ ‘ 𝐴 ) ) ∈ ℂ )
256 255 div1d ⊢ ( 𝜑 → ( ( ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) / ( ♯ ‘ 𝐴 ) ) / 1 ) = ( ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) / ( ♯ ‘ 𝐴 ) ) )
257 254 256 eqtrd ⊢ ( 𝜑 → ( ( ℂfld Σg ( ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ∘f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) / ( ℂfld Σg ( 𝐴 × { ( 1 / ( ♯ ‘ 𝐴 ) ) } ) ) ) = ( ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) / ( ♯ ‘ 𝐴 ) ) )
258 211 242 257 3brtr3d ⊢ ( 𝜑 → - ( log ‘ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) ≤ ( ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) / ( ♯ ‘ 𝐴 ) ) )
259 116 117 258 lenegcon1d ⊢ ( 𝜑 → - ( ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) / ( ♯ ‘ 𝐴 ) ) ≤ ( log ‘ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) )
260 107 259 eqbrtrrd ⊢ ( 𝜑 → ( ( 1 / ( ♯ ‘ 𝐴 ) ) · ( log ‘ ( 𝑀 Σg 𝐹 ) ) ) ≤ ( log ‘ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) )
261 131 104 remulcld ⊢ ( 𝜑 → ( ( 1 / ( ♯ ‘ 𝐴 ) ) · ( log ‘ ( 𝑀 Σg 𝐹 ) ) ) ∈ ℝ )
262 efle ⊢ ( ( ( ( 1 / ( ♯ ‘ 𝐴 ) ) · ( log ‘ ( 𝑀 Σg 𝐹 ) ) ) ∈ ℝ ∧ ( log ‘ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) ∈ ℝ ) → ( ( ( 1 / ( ♯ ‘ 𝐴 ) ) · ( log ‘ ( 𝑀 Σg 𝐹 ) ) ) ≤ ( log ‘ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) ↔ ( exp ‘ ( ( 1 / ( ♯ ‘ 𝐴 ) ) · ( log ‘ ( 𝑀 Σg 𝐹 ) ) ) ) ≤ ( exp ‘ ( log ‘ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) ) ) )
263 261 116 262 syl2anc ⊢ ( 𝜑 → ( ( ( 1 / ( ♯ ‘ 𝐴 ) ) · ( log ‘ ( 𝑀 Σg 𝐹 ) ) ) ≤ ( log ‘ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) ↔ ( exp ‘ ( ( 1 / ( ♯ ‘ 𝐴 ) ) · ( log ‘ ( 𝑀 Σg 𝐹 ) ) ) ) ≤ ( exp ‘ ( log ‘ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) ) ) )
264 260 263 mpbid ⊢ ( 𝜑 → ( exp ‘ ( ( 1 / ( ♯ ‘ 𝐴 ) ) · ( log ‘ ( 𝑀 Σg 𝐹 ) ) ) ) ≤ ( exp ‘ ( log ‘ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) ) )
265 100 rpcnd ⊢ ( 𝜑 → ( 𝑀 Σg 𝐹 ) ∈ ℂ )
266 100 rpne0d ⊢ ( 𝜑 → ( 𝑀 Σg 𝐹 ) ≠ 0 )
267 265 266 143 cxpefd ⊢ ( 𝜑 → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) = ( exp ‘ ( ( 1 / ( ♯ ‘ 𝐴 ) ) · ( log ‘ ( 𝑀 Σg 𝐹 ) ) ) ) )
268 115 reeflogd ⊢ ( 𝜑 → ( exp ‘ ( log ‘ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) ) = ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) )
269 268 eqcomd ⊢ ( 𝜑 → ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) = ( exp ‘ ( log ‘ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) ) )
270 264 267 269 3brtr4d ⊢ ( 𝜑 → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) ≤ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) )