Step | Hyp | Ref
| Expression |
1 | | cnfld0 19589 |
. . . . . . . 8
⊢ 0 =
(0g‘ℂfld) |
2 | | cnring 19587 |
. . . . . . . . 9
⊢
ℂfld ∈ Ring |
3 | | ringabl 18403 |
. . . . . . . . 9
⊢
(ℂfld ∈ Ring → ℂfld ∈
Abel) |
4 | 2, 3 | mp1i 13 |
. . . . . . . 8
⊢ (𝜑 → ℂfld
∈ Abel) |
5 | | amgm.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ Fin) |
6 | | resubdrg 19773 |
. . . . . . . . . 10
⊢ (ℝ
∈ (SubRing‘ℂfld) ∧ ℝfld ∈
DivRing) |
7 | 6 | simpli 473 |
. . . . . . . . 9
⊢ ℝ
∈ (SubRing‘ℂfld) |
8 | | subrgsubg 18609 |
. . . . . . . . 9
⊢ (ℝ
∈ (SubRing‘ℂfld) → ℝ ∈
(SubGrp‘ℂfld)) |
9 | 7, 8 | mp1i 13 |
. . . . . . . 8
⊢ (𝜑 → ℝ ∈
(SubGrp‘ℂfld)) |
10 | | amgm.4 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝐴⟶ℝ+) |
11 | 10 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈
ℝ+) |
12 | 11 | relogcld 24173 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘(𝐹‘𝑘)) ∈ ℝ) |
13 | 12 | renegcld 10336 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘(𝐹‘𝑘)) ∈ ℝ) |
14 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))) = (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))) |
15 | 13, 14 | fmptd 6292 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))):𝐴⟶ℝ) |
16 | | c0ex 9913 |
. . . . . . . . . 10
⊢ 0 ∈
V |
17 | 16 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
V) |
18 | 15, 5, 17 | fdmfifsupp 8168 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))) finSupp 0) |
19 | 1, 4, 5, 9, 15, 18 | gsumsubgcl 18143 |
. . . . . . 7
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) ∈ ℝ) |
20 | 19 | recnd 9947 |
. . . . . 6
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) ∈ ℂ) |
21 | | amgm.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ≠ ∅) |
22 | | hashnncl 13018 |
. . . . . . . . 9
⊢ (𝐴 ∈ Fin →
((#‘𝐴) ∈ ℕ
↔ 𝐴 ≠
∅)) |
23 | 5, 22 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) |
24 | 21, 23 | mpbird 246 |
. . . . . . 7
⊢ (𝜑 → (#‘𝐴) ∈ ℕ) |
25 | 24 | nncnd 10913 |
. . . . . 6
⊢ (𝜑 → (#‘𝐴) ∈ ℂ) |
26 | 24 | nnne0d 10942 |
. . . . . 6
⊢ (𝜑 → (#‘𝐴) ≠ 0) |
27 | 20, 25, 26 | divnegd 10693 |
. . . . 5
⊢ (𝜑 → -((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (#‘𝐴)) = (-(ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (#‘𝐴))) |
28 | 12 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘(𝐹‘𝑘)) ∈ ℂ) |
29 | 5, 28 | gsumfsum 19632 |
. . . . . . . . 9
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (log‘(𝐹‘𝑘)))) = Σ𝑘 ∈ 𝐴 (log‘(𝐹‘𝑘))) |
30 | 28 | negnegd 10262 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → --(log‘(𝐹‘𝑘)) = (log‘(𝐹‘𝑘))) |
31 | 30 | sumeq2dv 14281 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 --(log‘(𝐹‘𝑘)) = Σ𝑘 ∈ 𝐴 (log‘(𝐹‘𝑘))) |
32 | 13 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘(𝐹‘𝑘)) ∈ ℂ) |
33 | 5, 32 | fsumneg 14361 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 --(log‘(𝐹‘𝑘)) = -Σ𝑘 ∈ 𝐴 -(log‘(𝐹‘𝑘))) |
34 | 29, 31, 33 | 3eqtr2rd 2651 |
. . . . . . . 8
⊢ (𝜑 → -Σ𝑘 ∈ 𝐴 -(log‘(𝐹‘𝑘)) = (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (log‘(𝐹‘𝑘))))) |
35 | 5, 32 | gsumfsum 19632 |
. . . . . . . . 9
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) = Σ𝑘 ∈ 𝐴 -(log‘(𝐹‘𝑘))) |
36 | 35 | negeqd 10154 |
. . . . . . . 8
⊢ (𝜑 → -(ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) = -Σ𝑘 ∈ 𝐴 -(log‘(𝐹‘𝑘))) |
37 | 10 | feqmptd 6159 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) |
38 | | relogf1o 24117 |
. . . . . . . . . . . . 13
⊢ (log
↾ ℝ+):ℝ+–1-1-onto→ℝ |
39 | | f1of 6050 |
. . . . . . . . . . . . 13
⊢ ((log
↾ ℝ+):ℝ+–1-1-onto→ℝ → (log ↾
ℝ+):ℝ+⟶ℝ) |
40 | 38, 39 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (𝜑 → (log ↾
ℝ+):ℝ+⟶ℝ) |
41 | 40 | feqmptd 6159 |
. . . . . . . . . . 11
⊢ (𝜑 → (log ↾
ℝ+) = (𝑥
∈ ℝ+ ↦ ((log ↾
ℝ+)‘𝑥))) |
42 | | fvres 6117 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ ((log ↾ ℝ+)‘𝑥) = (log‘𝑥)) |
43 | 42 | mpteq2ia 4668 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
↦ ((log ↾ ℝ+)‘𝑥)) = (𝑥 ∈ ℝ+ ↦
(log‘𝑥)) |
44 | 41, 43 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (𝜑 → (log ↾
ℝ+) = (𝑥
∈ ℝ+ ↦ (log‘𝑥))) |
45 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐹‘𝑘) → (log‘𝑥) = (log‘(𝐹‘𝑘))) |
46 | 11, 37, 44, 45 | fmptco 6303 |
. . . . . . . . 9
⊢ (𝜑 → ((log ↾
ℝ+) ∘ 𝐹) = (𝑘 ∈ 𝐴 ↦ (log‘(𝐹‘𝑘)))) |
47 | 46 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝜑 → (ℂfld
Σg ((log ↾ ℝ+) ∘ 𝐹)) = (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (log‘(𝐹‘𝑘))))) |
48 | 34, 36, 47 | 3eqtr4d 2654 |
. . . . . . 7
⊢ (𝜑 → -(ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) = (ℂfld
Σg ((log ↾ ℝ+) ∘ 𝐹))) |
49 | | amgm.1 |
. . . . . . . . . . . . . . 15
⊢ 𝑀 =
(mulGrp‘ℂfld) |
50 | 49 | oveq1i 6559 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ↾s (ℂ
∖ {0})) = ((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0})) |
51 | 50 | rpmsubg 19629 |
. . . . . . . . . . . . 13
⊢
ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖
{0}))) |
52 | | subgsubm 17439 |
. . . . . . . . . . . . 13
⊢
(ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0})))
→ ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖
{0})))) |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖
{0}))) |
54 | | cnfldbas 19571 |
. . . . . . . . . . . . . . 15
⊢ ℂ =
(Base‘ℂfld) |
55 | | cndrng 19594 |
. . . . . . . . . . . . . . 15
⊢
ℂfld ∈ DivRing |
56 | 54, 1, 55 | drngui 18576 |
. . . . . . . . . . . . . 14
⊢ (ℂ
∖ {0}) = (Unit‘ℂfld) |
57 | 56, 49 | unitsubm 18493 |
. . . . . . . . . . . . 13
⊢
(ℂfld ∈ Ring → (ℂ ∖ {0}) ∈
(SubMnd‘𝑀)) |
58 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ↾s (ℂ
∖ {0})) = (𝑀
↾s (ℂ ∖ {0})) |
59 | 58 | subsubm 17180 |
. . . . . . . . . . . . 13
⊢ ((ℂ
∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈
(SubMnd‘(𝑀
↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈
(SubMnd‘𝑀) ∧
ℝ+ ⊆ (ℂ ∖ {0})))) |
60 | 2, 57, 59 | mp2b 10 |
. . . . . . . . . . . 12
⊢
(ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0})))
↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ
∖ {0}))) |
61 | 53, 60 | mpbi 219 |
. . . . . . . . . . 11
⊢
(ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ
∖ {0})) |
62 | 61 | simpli 473 |
. . . . . . . . . 10
⊢
ℝ+ ∈ (SubMnd‘𝑀) |
63 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑀 ↾s
ℝ+) = (𝑀
↾s ℝ+) |
64 | 63 | submbas 17178 |
. . . . . . . . . 10
⊢
(ℝ+ ∈ (SubMnd‘𝑀) → ℝ+ =
(Base‘(𝑀
↾s ℝ+))) |
65 | 62, 64 | ax-mp 5 |
. . . . . . . . 9
⊢
ℝ+ = (Base‘(𝑀 ↾s
ℝ+)) |
66 | | cnfld1 19590 |
. . . . . . . . . . . 12
⊢ 1 =
(1r‘ℂfld) |
67 | 49, 66 | ringidval 18326 |
. . . . . . . . . . 11
⊢ 1 =
(0g‘𝑀) |
68 | 63, 67 | subm0 17179 |
. . . . . . . . . 10
⊢
(ℝ+ ∈ (SubMnd‘𝑀) → 1 = (0g‘(𝑀 ↾s
ℝ+))) |
69 | 62, 68 | ax-mp 5 |
. . . . . . . . 9
⊢ 1 =
(0g‘(𝑀
↾s ℝ+)) |
70 | | cncrng 19586 |
. . . . . . . . . . 11
⊢
ℂfld ∈ CRing |
71 | 49 | crngmgp 18378 |
. . . . . . . . . . 11
⊢
(ℂfld ∈ CRing → 𝑀 ∈ CMnd) |
72 | 70, 71 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ CMnd) |
73 | 63 | submmnd 17177 |
. . . . . . . . . . 11
⊢
(ℝ+ ∈ (SubMnd‘𝑀) → (𝑀 ↾s ℝ+)
∈ Mnd) |
74 | 62, 73 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 ↾s ℝ+)
∈ Mnd) |
75 | 63 | subcmn 18065 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ CMnd ∧ (𝑀 ↾s
ℝ+) ∈ Mnd) → (𝑀 ↾s ℝ+)
∈ CMnd) |
76 | 72, 74, 75 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 ↾s ℝ+)
∈ CMnd) |
77 | | df-refld 19770 |
. . . . . . . . . . . 12
⊢
ℝfld = (ℂfld ↾s
ℝ) |
78 | 77 | subrgring 18606 |
. . . . . . . . . . 11
⊢ (ℝ
∈ (SubRing‘ℂfld) → ℝfld
∈ Ring) |
79 | 7, 78 | ax-mp 5 |
. . . . . . . . . 10
⊢
ℝfld ∈ Ring |
80 | | ringmnd 18379 |
. . . . . . . . . 10
⊢
(ℝfld ∈ Ring → ℝfld ∈
Mnd) |
81 | 79, 80 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → ℝfld
∈ Mnd) |
82 | 49 | oveq1i 6559 |
. . . . . . . . . . . 12
⊢ (𝑀 ↾s
ℝ+) = ((mulGrp‘ℂfld)
↾s ℝ+) |
83 | 82 | reloggim 24149 |
. . . . . . . . . . 11
⊢ (log
↾ ℝ+) ∈ ((𝑀 ↾s ℝ+)
GrpIso ℝfld) |
84 | | gimghm 17529 |
. . . . . . . . . . 11
⊢ ((log
↾ ℝ+) ∈ ((𝑀 ↾s ℝ+)
GrpIso ℝfld) → (log ↾ ℝ+) ∈
((𝑀 ↾s
ℝ+) GrpHom ℝfld)) |
85 | 83, 84 | ax-mp 5 |
. . . . . . . . . 10
⊢ (log
↾ ℝ+) ∈ ((𝑀 ↾s ℝ+)
GrpHom ℝfld) |
86 | | ghmmhm 17493 |
. . . . . . . . . 10
⊢ ((log
↾ ℝ+) ∈ ((𝑀 ↾s ℝ+)
GrpHom ℝfld) → (log ↾ ℝ+) ∈
((𝑀 ↾s
ℝ+) MndHom ℝfld)) |
87 | 85, 86 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → (log ↾
ℝ+) ∈ ((𝑀 ↾s ℝ+)
MndHom ℝfld)) |
88 | | 1ex 9914 |
. . . . . . . . . . 11
⊢ 1 ∈
V |
89 | 88 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
V) |
90 | 10, 5, 89 | fdmfifsupp 8168 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 finSupp 1) |
91 | 65, 69, 76, 81, 5, 87, 10, 90 | gsummhm 18161 |
. . . . . . . 8
⊢ (𝜑 → (ℝfld
Σg ((log ↾ ℝ+) ∘ 𝐹)) = ((log ↾
ℝ+)‘((𝑀 ↾s ℝ+)
Σg 𝐹))) |
92 | | subgsubm 17439 |
. . . . . . . . . 10
⊢ (ℝ
∈ (SubGrp‘ℂfld) → ℝ ∈
(SubMnd‘ℂfld)) |
93 | 9, 92 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ℝ ∈
(SubMnd‘ℂfld)) |
94 | | fco 5971 |
. . . . . . . . . 10
⊢ (((log
↾ ℝ+):ℝ+⟶ℝ ∧ 𝐹:𝐴⟶ℝ+) → ((log
↾ ℝ+) ∘ 𝐹):𝐴⟶ℝ) |
95 | 40, 10, 94 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → ((log ↾
ℝ+) ∘ 𝐹):𝐴⟶ℝ) |
96 | 5, 93, 95, 77 | gsumsubm 17196 |
. . . . . . . 8
⊢ (𝜑 → (ℂfld
Σg ((log ↾ ℝ+) ∘ 𝐹)) = (ℝfld
Σg ((log ↾ ℝ+) ∘ 𝐹))) |
97 | 62 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ+ ∈
(SubMnd‘𝑀)) |
98 | 5, 97, 10, 63 | gsumsubm 17196 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 Σg 𝐹) = ((𝑀 ↾s ℝ+)
Σg 𝐹)) |
99 | 98 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝜑 → ((log ↾
ℝ+)‘(𝑀 Σg 𝐹)) = ((log ↾
ℝ+)‘((𝑀 ↾s ℝ+)
Σg 𝐹))) |
100 | 91, 96, 99 | 3eqtr4d 2654 |
. . . . . . 7
⊢ (𝜑 → (ℂfld
Σg ((log ↾ ℝ+) ∘ 𝐹)) = ((log ↾
ℝ+)‘(𝑀 Σg 𝐹))) |
101 | 67, 72, 5, 97, 10, 90 | gsumsubmcl 18142 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 Σg 𝐹) ∈
ℝ+) |
102 | | fvres 6117 |
. . . . . . . 8
⊢ ((𝑀 Σg
𝐹) ∈
ℝ+ → ((log ↾ ℝ+)‘(𝑀 Σg
𝐹)) = (log‘(𝑀 Σg
𝐹))) |
103 | 101, 102 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((log ↾
ℝ+)‘(𝑀 Σg 𝐹)) = (log‘(𝑀 Σg
𝐹))) |
104 | 48, 100, 103 | 3eqtrd 2648 |
. . . . . 6
⊢ (𝜑 → -(ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) = (log‘(𝑀 Σg 𝐹))) |
105 | 104 | oveq1d 6564 |
. . . . 5
⊢ (𝜑 → (-(ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (#‘𝐴)) = ((log‘(𝑀 Σg 𝐹)) / (#‘𝐴))) |
106 | 101 | relogcld 24173 |
. . . . . . 7
⊢ (𝜑 → (log‘(𝑀 Σg
𝐹)) ∈
ℝ) |
107 | 106 | recnd 9947 |
. . . . . 6
⊢ (𝜑 → (log‘(𝑀 Σg
𝐹)) ∈
ℂ) |
108 | 107, 25, 26 | divrec2d 10684 |
. . . . 5
⊢ (𝜑 → ((log‘(𝑀 Σg
𝐹)) / (#‘𝐴)) = ((1 / (#‘𝐴)) · (log‘(𝑀 Σg
𝐹)))) |
109 | 27, 105, 108 | 3eqtrd 2648 |
. . . 4
⊢ (𝜑 → -((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (#‘𝐴)) = ((1 / (#‘𝐴)) · (log‘(𝑀 Σg 𝐹)))) |
110 | 37 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝜑 → (ℂfld
Σg 𝐹) = (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))) |
111 | 11 | rpcnd 11750 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℂ) |
112 | 5, 111 | gsumfsum 19632 |
. . . . . . . . 9
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) = Σ𝑘 ∈ 𝐴 (𝐹‘𝑘)) |
113 | 110, 112 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝜑 → (ℂfld
Σg 𝐹) = Σ𝑘 ∈ 𝐴 (𝐹‘𝑘)) |
114 | 5, 21, 11 | fsumrpcl 14315 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (𝐹‘𝑘) ∈
ℝ+) |
115 | 113, 114 | eqeltrd 2688 |
. . . . . . 7
⊢ (𝜑 → (ℂfld
Σg 𝐹) ∈
ℝ+) |
116 | 24 | nnrpd 11746 |
. . . . . . 7
⊢ (𝜑 → (#‘𝐴) ∈
ℝ+) |
117 | 115, 116 | rpdivcld 11765 |
. . . . . 6
⊢ (𝜑 → ((ℂfld
Σg 𝐹) / (#‘𝐴)) ∈
ℝ+) |
118 | 117 | relogcld 24173 |
. . . . 5
⊢ (𝜑 →
(log‘((ℂfld Σg 𝐹) / (#‘𝐴))) ∈ ℝ) |
119 | 19, 24 | nndivred 10946 |
. . . . 5
⊢ (𝜑 → ((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (#‘𝐴)) ∈ ℝ) |
120 | | rpssre 11719 |
. . . . . . . . 9
⊢
ℝ+ ⊆ ℝ |
121 | 120 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ+
⊆ ℝ) |
122 | | relogcl 24126 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ℝ+
→ (log‘𝑤) ∈
ℝ) |
123 | 122 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
(log‘𝑤) ∈
ℝ) |
124 | 123 | renegcld 10336 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
-(log‘𝑤) ∈
ℝ) |
125 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑤 ∈ ℝ+
↦ -(log‘𝑤)) =
(𝑤 ∈
ℝ+ ↦ -(log‘𝑤)) |
126 | 124, 125 | fmptd 6292 |
. . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ ℝ+ ↦
-(log‘𝑤)):ℝ+⟶ℝ) |
127 | | ioorp 12122 |
. . . . . . . . . . . 12
⊢
(0(,)+∞) = ℝ+ |
128 | 127 | eleq2i 2680 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (0(,)+∞) ↔
𝑎 ∈
ℝ+) |
129 | 127 | eleq2i 2680 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ (0(,)+∞) ↔
𝑏 ∈
ℝ+) |
130 | | iccssioo2 12117 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ (0(,)+∞) ∧
𝑏 ∈ (0(,)+∞))
→ (𝑎[,]𝑏) ⊆
(0(,)+∞)) |
131 | 128, 129,
130 | syl2anbr 496 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) → (𝑎[,]𝑏) ⊆ (0(,)+∞)) |
132 | 131, 127 | syl6sseq 3614 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) → (𝑎[,]𝑏) ⊆
ℝ+) |
133 | 132 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
→ (𝑎[,]𝑏) ⊆
ℝ+) |
134 | 24 | nnrecred 10943 |
. . . . . . . . . 10
⊢ (𝜑 → (1 / (#‘𝐴)) ∈
ℝ) |
135 | 116 | rpreccld 11758 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 / (#‘𝐴)) ∈
ℝ+) |
136 | 135 | rpge0d 11752 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ (1 / (#‘𝐴))) |
137 | | elrege0 12149 |
. . . . . . . . . 10
⊢ ((1 /
(#‘𝐴)) ∈
(0[,)+∞) ↔ ((1 / (#‘𝐴)) ∈ ℝ ∧ 0 ≤ (1 /
(#‘𝐴)))) |
138 | 134, 136,
137 | sylanbrc 695 |
. . . . . . . . 9
⊢ (𝜑 → (1 / (#‘𝐴)) ∈
(0[,)+∞)) |
139 | | fconst6g 6007 |
. . . . . . . . 9
⊢ ((1 /
(#‘𝐴)) ∈
(0[,)+∞) → (𝐴
× {(1 / (#‘𝐴))}):𝐴⟶(0[,)+∞)) |
140 | 138, 139 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 × {(1 / (#‘𝐴))}):𝐴⟶(0[,)+∞)) |
141 | | 0lt1 10429 |
. . . . . . . . 9
⊢ 0 <
1 |
142 | | fconstmpt 5085 |
. . . . . . . . . . 11
⊢ (𝐴 × {(1 / (#‘𝐴))}) = (𝑘 ∈ 𝐴 ↦ (1 / (#‘𝐴))) |
143 | 142 | oveq2i 6560 |
. . . . . . . . . 10
⊢
(ℂfld Σg (𝐴 × {(1 / (#‘𝐴))})) = (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (1 / (#‘𝐴)))) |
144 | | ringmnd 18379 |
. . . . . . . . . . . . 13
⊢
(ℂfld ∈ Ring → ℂfld ∈
Mnd) |
145 | 2, 144 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℂfld
∈ Mnd) |
146 | 134 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 / (#‘𝐴)) ∈
ℂ) |
147 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(.g‘ℂfld) =
(.g‘ℂfld) |
148 | 54, 147 | gsumconst 18157 |
. . . . . . . . . . . 12
⊢
((ℂfld ∈ Mnd ∧ 𝐴 ∈ Fin ∧ (1 / (#‘𝐴)) ∈ ℂ) →
(ℂfld Σg (𝑘 ∈ 𝐴 ↦ (1 / (#‘𝐴)))) = ((#‘𝐴)(.g‘ℂfld)(1
/ (#‘𝐴)))) |
149 | 145, 5, 146, 148 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (1 / (#‘𝐴)))) = ((#‘𝐴)(.g‘ℂfld)(1
/ (#‘𝐴)))) |
150 | 24 | nnzd 11357 |
. . . . . . . . . . . 12
⊢ (𝜑 → (#‘𝐴) ∈ ℤ) |
151 | | cnfldmulg 19597 |
. . . . . . . . . . . 12
⊢
(((#‘𝐴) ∈
ℤ ∧ (1 / (#‘𝐴)) ∈ ℂ) → ((#‘𝐴)(.g‘ℂfld)(1
/ (#‘𝐴))) =
((#‘𝐴) · (1 /
(#‘𝐴)))) |
152 | 150, 146,
151 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → ((#‘𝐴)(.g‘ℂfld)(1
/ (#‘𝐴))) =
((#‘𝐴) · (1 /
(#‘𝐴)))) |
153 | 25, 26 | recidd 10675 |
. . . . . . . . . . 11
⊢ (𝜑 → ((#‘𝐴) · (1 / (#‘𝐴))) = 1) |
154 | 149, 152,
153 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (1 / (#‘𝐴)))) = 1) |
155 | 143, 154 | syl5eq 2656 |
. . . . . . . . 9
⊢ (𝜑 → (ℂfld
Σg (𝐴 × {(1 / (#‘𝐴))})) = 1) |
156 | 141, 155 | syl5breqr 4621 |
. . . . . . . 8
⊢ (𝜑 → 0 <
(ℂfld Σg (𝐴 × {(1 / (#‘𝐴))}))) |
157 | | logccv 24209 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ 𝑦 ∈
ℝ+ ∧ 𝑥
< 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))) |
158 | 157 | 3adant1 1072 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))) |
159 | | ioossre 12106 |
. . . . . . . . . . . . . . 15
⊢ (0(,)1)
⊆ ℝ |
160 | | simp3 1056 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ (0(,)1)) |
161 | 159, 160 | sseldi 3566 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ) |
162 | | simp21 1087 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑥 ∈ ℝ+) |
163 | 162 | relogcld 24173 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈
ℝ) |
164 | 161, 163 | remulcld 9949 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℝ) |
165 | | 1re 9918 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
166 | | resubcl 10224 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ ∧ 𝑡
∈ ℝ) → (1 − 𝑡) ∈ ℝ) |
167 | 165, 161,
166 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈
ℝ) |
168 | | simp22 1088 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑦 ∈ ℝ+) |
169 | 168 | relogcld 24173 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈
ℝ) |
170 | 167, 169 | remulcld 9949 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈
ℝ) |
171 | 164, 170 | readdcld 9948 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) ∈ ℝ) |
172 | | simp1 1054 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝜑) |
173 | | ioossicc 12130 |
. . . . . . . . . . . . . . 15
⊢ (0(,)1)
⊆ (0[,]1) |
174 | 173, 160 | sseldi 3566 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ (0[,]1)) |
175 | 121, 133 | cvxcl 24511 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑡 ∈ (0[,]1)))
→ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈
ℝ+) |
176 | 172, 162,
168, 174, 175 | syl13anc 1320 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈
ℝ+) |
177 | 176 | relogcld 24173 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ ℝ) |
178 | 171, 177 | ltnegd 10484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ↔ -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))))) |
179 | 158, 178 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦)))) |
180 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) → (log‘𝑤) = (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))) |
181 | 180 | negeqd 10154 |
. . . . . . . . . . . 12
⊢ (𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) → -(log‘𝑤) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))) |
182 | | negex 10158 |
. . . . . . . . . . . 12
⊢
-(log‘((𝑡
· 𝑥) + ((1 −
𝑡) · 𝑦))) ∈ V |
183 | 181, 125,
182 | fvmpt 6191 |
. . . . . . . . . . 11
⊢ (((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ+ → ((𝑤 ∈ ℝ+
↦ -(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))) |
184 | 176, 183 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))) |
185 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑥 → (log‘𝑤) = (log‘𝑥)) |
186 | 185 | negeqd 10154 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑥 → -(log‘𝑤) = -(log‘𝑥)) |
187 | | negex 10158 |
. . . . . . . . . . . . . . . 16
⊢
-(log‘𝑥)
∈ V |
188 | 186, 125,
187 | fvmpt 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ ((𝑤 ∈
ℝ+ ↦ -(log‘𝑤))‘𝑥) = -(log‘𝑥)) |
189 | 162, 188 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑥) = -(log‘𝑥)) |
190 | 189 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑥)) = (𝑡 · -(log‘𝑥))) |
191 | 161 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℂ) |
192 | 163 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈
ℂ) |
193 | 191, 192 | mulneg2d 10363 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · -(log‘𝑥)) = -(𝑡 · (log‘𝑥))) |
194 | 190, 193 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑥)) = -(𝑡 · (log‘𝑥))) |
195 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑦 → (log‘𝑤) = (log‘𝑦)) |
196 | 195 | negeqd 10154 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑦 → -(log‘𝑤) = -(log‘𝑦)) |
197 | | negex 10158 |
. . . . . . . . . . . . . . . 16
⊢
-(log‘𝑦)
∈ V |
198 | 196, 125,
197 | fvmpt 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ+
→ ((𝑤 ∈
ℝ+ ↦ -(log‘𝑤))‘𝑦) = -(log‘𝑦)) |
199 | 168, 198 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑦) = -(log‘𝑦)) |
200 | 199 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑦)) = ((1 − 𝑡) · -(log‘𝑦))) |
201 | 167 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈
ℂ) |
202 | 169 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈
ℂ) |
203 | 201, 202 | mulneg2d 10363 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · -(log‘𝑦)) = -((1 − 𝑡) · (log‘𝑦))) |
204 | 200, 203 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑦)) = -((1 − 𝑡) · (log‘𝑦))) |
205 | 194, 204 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑦))) = (-(𝑡 · (log‘𝑥)) + -((1 − 𝑡) · (log‘𝑦)))) |
206 | 164 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℂ) |
207 | 170 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈
ℂ) |
208 | 206, 207 | negdid 10284 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) = (-(𝑡 · (log‘𝑥)) + -((1 − 𝑡) · (log‘𝑦)))) |
209 | 205, 208 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑦))) = -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦)))) |
210 | 179, 184,
209 | 3brtr4d 4615 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑦)))) |
211 | 121, 126,
133, 210 | scvxcvx 24512 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+
∧ 𝑠 ∈ (0[,]1)))
→ ((𝑤 ∈
ℝ+ ↦ -(log‘𝑤))‘((𝑠 · 𝑢) + ((1 − 𝑠) · 𝑣))) ≤ ((𝑠 · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑢)) + ((1 − 𝑠) · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑣)))) |
212 | 121, 126,
133, 5, 140, 10, 156, 211 | jensen 24515 |
. . . . . . 7
⊢ (𝜑 → (((ℂfld
Σg ((𝐴 × {(1 / (#‘𝐴))}) ∘𝑓 ·
𝐹)) /
(ℂfld Σg (𝐴 × {(1 / (#‘𝐴))}))) ∈ ℝ+ ∧
((𝑤 ∈
ℝ+ ↦ -(log‘𝑤))‘((ℂfld
Σg ((𝐴 × {(1 / (#‘𝐴))}) ∘𝑓 ·
𝐹)) /
(ℂfld Σg (𝐴 × {(1 / (#‘𝐴))})))) ≤ ((ℂfld
Σg ((𝐴 × {(1 / (#‘𝐴))}) ∘𝑓 ·
((𝑤 ∈
ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld
Σg (𝐴 × {(1 / (#‘𝐴))}))))) |
213 | 212 | simprd 478 |
. . . . . 6
⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘((ℂfld
Σg ((𝐴 × {(1 / (#‘𝐴))}) ∘𝑓 ·
𝐹)) /
(ℂfld Σg (𝐴 × {(1 / (#‘𝐴))})))) ≤ ((ℂfld
Σg ((𝐴 × {(1 / (#‘𝐴))}) ∘𝑓 ·
((𝑤 ∈
ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld
Σg (𝐴 × {(1 / (#‘𝐴))})))) |
214 | 134 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (1 / (#‘𝐴)) ∈ ℝ) |
215 | 142 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 × {(1 / (#‘𝐴))}) = (𝑘 ∈ 𝐴 ↦ (1 / (#‘𝐴)))) |
216 | 5, 214, 11, 215, 37 | offval2 6812 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴 × {(1 / (#‘𝐴))}) ∘𝑓 ·
𝐹) = (𝑘 ∈ 𝐴 ↦ ((1 / (#‘𝐴)) · (𝐹‘𝑘)))) |
217 | 216 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℂfld
Σg ((𝐴 × {(1 / (#‘𝐴))}) ∘𝑓 ·
𝐹)) =
(ℂfld Σg (𝑘 ∈ 𝐴 ↦ ((1 / (#‘𝐴)) · (𝐹‘𝑘))))) |
218 | | cnfldadd 19572 |
. . . . . . . . . . . 12
⊢ + =
(+g‘ℂfld) |
219 | | cnfldmul 19573 |
. . . . . . . . . . . 12
⊢ ·
= (.r‘ℂfld) |
220 | 2 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℂfld
∈ Ring) |
221 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) |
222 | 111, 221 | fmptd 6292 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)):𝐴⟶ℂ) |
223 | 222, 5, 17 | fdmfifsupp 8168 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) finSupp 0) |
224 | 54, 1, 218, 219, 220, 5, 146, 111, 223 | gsummulc2 18430 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ ((1 / (#‘𝐴)) · (𝐹‘𝑘)))) = ((1 / (#‘𝐴)) · (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))))) |
225 | | fss 5969 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝐴⟶ℝ+ ∧
ℝ+ ⊆ ℝ) → 𝐹:𝐴⟶ℝ) |
226 | 10, 120, 225 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) |
227 | 10, 5, 17 | fdmfifsupp 8168 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 finSupp 0) |
228 | 1, 4, 5, 9, 226, 227 | gsumsubgcl 18143 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℂfld
Σg 𝐹) ∈ ℝ) |
229 | 228 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℂfld
Σg 𝐹) ∈ ℂ) |
230 | 229, 25, 26 | divrec2d 10684 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((ℂfld
Σg 𝐹) / (#‘𝐴)) = ((1 / (#‘𝐴)) · (ℂfld
Σg 𝐹))) |
231 | 110 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((1 / (#‘𝐴)) ·
(ℂfld Σg 𝐹)) = ((1 / (#‘𝐴)) · (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))))) |
232 | 230, 231 | eqtr2d 2645 |
. . . . . . . . . . 11
⊢ (𝜑 → ((1 / (#‘𝐴)) ·
(ℂfld Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))) = ((ℂfld
Σg 𝐹) / (#‘𝐴))) |
233 | 217, 224,
232 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ (𝜑 → (ℂfld
Σg ((𝐴 × {(1 / (#‘𝐴))}) ∘𝑓 ·
𝐹)) =
((ℂfld Σg 𝐹) / (#‘𝐴))) |
234 | 233, 155 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝜑 → ((ℂfld
Σg ((𝐴 × {(1 / (#‘𝐴))}) ∘𝑓 ·
𝐹)) /
(ℂfld Σg (𝐴 × {(1 / (#‘𝐴))}))) = (((ℂfld
Σg 𝐹) / (#‘𝐴)) / 1)) |
235 | 228, 24 | nndivred 10946 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℂfld
Σg 𝐹) / (#‘𝐴)) ∈ ℝ) |
236 | 235 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℂfld
Σg 𝐹) / (#‘𝐴)) ∈ ℂ) |
237 | 236 | div1d 10672 |
. . . . . . . . 9
⊢ (𝜑 → (((ℂfld
Σg 𝐹) / (#‘𝐴)) / 1) = ((ℂfld
Σg 𝐹) / (#‘𝐴))) |
238 | 234, 237 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝜑 → ((ℂfld
Σg ((𝐴 × {(1 / (#‘𝐴))}) ∘𝑓 ·
𝐹)) /
(ℂfld Σg (𝐴 × {(1 / (#‘𝐴))}))) = ((ℂfld
Σg 𝐹) / (#‘𝐴))) |
239 | 238 | fveq2d 6107 |
. . . . . . 7
⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘((ℂfld
Σg ((𝐴 × {(1 / (#‘𝐴))}) ∘𝑓 ·
𝐹)) /
(ℂfld Σg (𝐴 × {(1 / (#‘𝐴))})))) = ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘((ℂfld
Σg 𝐹) / (#‘𝐴)))) |
240 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑤 = ((ℂfld
Σg 𝐹) / (#‘𝐴)) → (log‘𝑤) = (log‘((ℂfld
Σg 𝐹) / (#‘𝐴)))) |
241 | 240 | negeqd 10154 |
. . . . . . . . 9
⊢ (𝑤 = ((ℂfld
Σg 𝐹) / (#‘𝐴)) → -(log‘𝑤) = -(log‘((ℂfld
Σg 𝐹) / (#‘𝐴)))) |
242 | | negex 10158 |
. . . . . . . . 9
⊢
-(log‘((ℂfld Σg 𝐹) / (#‘𝐴))) ∈ V |
243 | 241, 125,
242 | fvmpt 6191 |
. . . . . . . 8
⊢
(((ℂfld Σg 𝐹) / (#‘𝐴)) ∈ ℝ+ → ((𝑤 ∈ ℝ+
↦ -(log‘𝑤))‘((ℂfld
Σg 𝐹) / (#‘𝐴))) = -(log‘((ℂfld
Σg 𝐹) / (#‘𝐴)))) |
244 | 117, 243 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘((ℂfld
Σg 𝐹) / (#‘𝐴))) = -(log‘((ℂfld
Σg 𝐹) / (#‘𝐴)))) |
245 | 239, 244 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘((ℂfld
Σg ((𝐴 × {(1 / (#‘𝐴))}) ∘𝑓 ·
𝐹)) /
(ℂfld Σg (𝐴 × {(1 / (#‘𝐴))})))) =
-(log‘((ℂfld Σg 𝐹) / (#‘𝐴)))) |
246 | 54, 1, 218, 219, 220, 5, 146, 32, 18 | gsummulc2 18430 |
. . . . . . . . 9
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ ((1 / (#‘𝐴)) · -(log‘(𝐹‘𝑘))))) = ((1 / (#‘𝐴)) · (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))))) |
247 | | negex 10158 |
. . . . . . . . . . . 12
⊢
-(log‘(𝐹‘𝑘)) ∈ V |
248 | 247 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘(𝐹‘𝑘)) ∈ V) |
249 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑤 ∈ ℝ+ ↦
-(log‘𝑤)) = (𝑤 ∈ ℝ+
↦ -(log‘𝑤))) |
250 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝐹‘𝑘) → (log‘𝑤) = (log‘(𝐹‘𝑘))) |
251 | 250 | negeqd 10154 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝐹‘𝑘) → -(log‘𝑤) = -(log‘(𝐹‘𝑘))) |
252 | 11, 37, 249, 251 | fmptco 6303 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤)) ∘
𝐹) = (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) |
253 | 5, 214, 248, 215, 252 | offval2 6812 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 × {(1 / (#‘𝐴))}) ∘𝑓 ·
((𝑤 ∈
ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹)) = (𝑘 ∈ 𝐴 ↦ ((1 / (#‘𝐴)) · -(log‘(𝐹‘𝑘))))) |
254 | 253 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝜑 → (ℂfld
Σg ((𝐴 × {(1 / (#‘𝐴))}) ∘𝑓 ·
((𝑤 ∈
ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) = (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ ((1 / (#‘𝐴)) · -(log‘(𝐹‘𝑘)))))) |
255 | 20, 25, 26 | divrec2d 10684 |
. . . . . . . . 9
⊢ (𝜑 → ((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (#‘𝐴)) = ((1 / (#‘𝐴)) · (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))))) |
256 | 246, 254,
255 | 3eqtr4d 2654 |
. . . . . . . 8
⊢ (𝜑 → (ℂfld
Σg ((𝐴 × {(1 / (#‘𝐴))}) ∘𝑓 ·
((𝑤 ∈
ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) = ((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (#‘𝐴))) |
257 | 256, 155 | oveq12d 6567 |
. . . . . . 7
⊢ (𝜑 → ((ℂfld
Σg ((𝐴 × {(1 / (#‘𝐴))}) ∘𝑓 ·
((𝑤 ∈
ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld
Σg (𝐴 × {(1 / (#‘𝐴))}))) = (((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (#‘𝐴)) / 1)) |
258 | 119 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → ((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (#‘𝐴)) ∈ ℂ) |
259 | 258 | div1d 10672 |
. . . . . . 7
⊢ (𝜑 → (((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (#‘𝐴)) / 1) = ((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (#‘𝐴))) |
260 | 257, 259 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → ((ℂfld
Σg ((𝐴 × {(1 / (#‘𝐴))}) ∘𝑓 ·
((𝑤 ∈
ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld
Σg (𝐴 × {(1 / (#‘𝐴))}))) = ((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (#‘𝐴))) |
261 | 213, 245,
260 | 3brtr3d 4614 |
. . . . 5
⊢ (𝜑 →
-(log‘((ℂfld Σg 𝐹) / (#‘𝐴))) ≤ ((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (#‘𝐴))) |
262 | 118, 119,
261 | lenegcon1d 10488 |
. . . 4
⊢ (𝜑 → -((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (#‘𝐴)) ≤ (log‘((ℂfld
Σg 𝐹) / (#‘𝐴)))) |
263 | 109, 262 | eqbrtrrd 4607 |
. . 3
⊢ (𝜑 → ((1 / (#‘𝐴)) · (log‘(𝑀 Σg
𝐹))) ≤
(log‘((ℂfld Σg 𝐹) / (#‘𝐴)))) |
264 | 134, 106 | remulcld 9949 |
. . . 4
⊢ (𝜑 → ((1 / (#‘𝐴)) · (log‘(𝑀 Σg
𝐹))) ∈
ℝ) |
265 | | efle 14687 |
. . . 4
⊢ ((((1 /
(#‘𝐴)) ·
(log‘(𝑀
Σg 𝐹))) ∈ ℝ ∧
(log‘((ℂfld Σg 𝐹) / (#‘𝐴))) ∈ ℝ) → (((1 /
(#‘𝐴)) ·
(log‘(𝑀
Σg 𝐹))) ≤ (log‘((ℂfld
Σg 𝐹) / (#‘𝐴))) ↔ (exp‘((1 / (#‘𝐴)) · (log‘(𝑀 Σg
𝐹)))) ≤
(exp‘(log‘((ℂfld Σg 𝐹) / (#‘𝐴)))))) |
266 | 264, 118,
265 | syl2anc 691 |
. . 3
⊢ (𝜑 → (((1 / (#‘𝐴)) · (log‘(𝑀 Σg
𝐹))) ≤
(log‘((ℂfld Σg 𝐹) / (#‘𝐴))) ↔ (exp‘((1 / (#‘𝐴)) · (log‘(𝑀 Σg
𝐹)))) ≤
(exp‘(log‘((ℂfld Σg 𝐹) / (#‘𝐴)))))) |
267 | 263, 266 | mpbid 221 |
. 2
⊢ (𝜑 → (exp‘((1 /
(#‘𝐴)) ·
(log‘(𝑀
Σg 𝐹)))) ≤
(exp‘(log‘((ℂfld Σg 𝐹) / (#‘𝐴))))) |
268 | 101 | rpcnd 11750 |
. . 3
⊢ (𝜑 → (𝑀 Σg 𝐹) ∈
ℂ) |
269 | 101 | rpne0d 11753 |
. . 3
⊢ (𝜑 → (𝑀 Σg 𝐹) ≠ 0) |
270 | 268, 269,
146 | cxpefd 24258 |
. 2
⊢ (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 /
(#‘𝐴))) =
(exp‘((1 / (#‘𝐴)) · (log‘(𝑀 Σg 𝐹))))) |
271 | 117 | reeflogd 24174 |
. . 3
⊢ (𝜑 →
(exp‘(log‘((ℂfld Σg 𝐹) / (#‘𝐴)))) = ((ℂfld
Σg 𝐹) / (#‘𝐴))) |
272 | 271 | eqcomd 2616 |
. 2
⊢ (𝜑 → ((ℂfld
Σg 𝐹) / (#‘𝐴)) =
(exp‘(log‘((ℂfld Σg 𝐹) / (#‘𝐴))))) |
273 | 267, 270,
272 | 3brtr4d 4615 |
1
⊢ (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 /
(#‘𝐴))) ≤
((ℂfld Σg 𝐹) / (#‘𝐴))) |