| Step | Hyp | Ref
| Expression |
| 1 | | cnfld0 21405 |
. . . . . . . 8
⊢ 0 =
(0g‘ℂfld) |
| 2 | | cnring 21403 |
. . . . . . . . 9
⊢
ℂfld ∈ Ring |
| 3 | | ringabl 20278 |
. . . . . . . . 9
⊢
(ℂfld ∈ Ring → ℂfld ∈
Abel) |
| 4 | 2, 3 | mp1i 13 |
. . . . . . . 8
⊢ (𝜑 → ℂfld
∈ Abel) |
| 5 | | amgm.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ Fin) |
| 6 | | resubdrg 21626 |
. . . . . . . . . 10
⊢ (ℝ
∈ (SubRing‘ℂfld) ∧ ℝfld ∈
DivRing) |
| 7 | 6 | simpli 483 |
. . . . . . . . 9
⊢ ℝ
∈ (SubRing‘ℂfld) |
| 8 | | subrgsubg 20577 |
. . . . . . . . 9
⊢ (ℝ
∈ (SubRing‘ℂfld) → ℝ ∈
(SubGrp‘ℂfld)) |
| 9 | 7, 8 | mp1i 13 |
. . . . . . . 8
⊢ (𝜑 → ℝ ∈
(SubGrp‘ℂfld)) |
| 10 | | amgm.4 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝐴⟶ℝ+) |
| 11 | 10 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈
ℝ+) |
| 12 | 11 | relogcld 26665 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘(𝐹‘𝑘)) ∈ ℝ) |
| 13 | 12 | renegcld 11690 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘(𝐹‘𝑘)) ∈ ℝ) |
| 14 | 13 | fmpttd 7135 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))):𝐴⟶ℝ) |
| 15 | | c0ex 11255 |
. . . . . . . . . 10
⊢ 0 ∈
V |
| 16 | 15 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
V) |
| 17 | 14, 5, 16 | fdmfifsupp 9415 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))) finSupp 0) |
| 18 | 1, 4, 5, 9, 14, 17 | gsumsubgcl 19938 |
. . . . . . 7
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) ∈ ℝ) |
| 19 | 18 | recnd 11289 |
. . . . . 6
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) ∈ ℂ) |
| 20 | | amgm.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ≠ ∅) |
| 21 | | hashnncl 14405 |
. . . . . . . . 9
⊢ (𝐴 ∈ Fin →
((♯‘𝐴) ∈
ℕ ↔ 𝐴 ≠
∅)) |
| 22 | 5, 21 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) |
| 23 | 20, 22 | mpbird 257 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝐴) ∈
ℕ) |
| 24 | 23 | nncnd 12282 |
. . . . . 6
⊢ (𝜑 → (♯‘𝐴) ∈
ℂ) |
| 25 | 23 | nnne0d 12316 |
. . . . . 6
⊢ (𝜑 → (♯‘𝐴) ≠ 0) |
| 26 | 19, 24, 25 | divnegd 12056 |
. . . . 5
⊢ (𝜑 → -((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) = (-(ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴))) |
| 27 | 12 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘(𝐹‘𝑘)) ∈ ℂ) |
| 28 | 5, 27 | gsumfsum 21452 |
. . . . . . . . 9
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (log‘(𝐹‘𝑘)))) = Σ𝑘 ∈ 𝐴 (log‘(𝐹‘𝑘))) |
| 29 | 27 | negnegd 11611 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → --(log‘(𝐹‘𝑘)) = (log‘(𝐹‘𝑘))) |
| 30 | 29 | sumeq2dv 15738 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 --(log‘(𝐹‘𝑘)) = Σ𝑘 ∈ 𝐴 (log‘(𝐹‘𝑘))) |
| 31 | 13 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘(𝐹‘𝑘)) ∈ ℂ) |
| 32 | 5, 31 | fsumneg 15823 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 --(log‘(𝐹‘𝑘)) = -Σ𝑘 ∈ 𝐴 -(log‘(𝐹‘𝑘))) |
| 33 | 28, 30, 32 | 3eqtr2rd 2784 |
. . . . . . . 8
⊢ (𝜑 → -Σ𝑘 ∈ 𝐴 -(log‘(𝐹‘𝑘)) = (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (log‘(𝐹‘𝑘))))) |
| 34 | 5, 31 | gsumfsum 21452 |
. . . . . . . . 9
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) = Σ𝑘 ∈ 𝐴 -(log‘(𝐹‘𝑘))) |
| 35 | 34 | negeqd 11502 |
. . . . . . . 8
⊢ (𝜑 → -(ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) = -Σ𝑘 ∈ 𝐴 -(log‘(𝐹‘𝑘))) |
| 36 | 10 | feqmptd 6977 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) |
| 37 | | relogf1o 26608 |
. . . . . . . . . . . . 13
⊢ (log
↾ ℝ+):ℝ+–1-1-onto→ℝ |
| 38 | | f1of 6848 |
. . . . . . . . . . . . 13
⊢ ((log
↾ ℝ+):ℝ+–1-1-onto→ℝ → (log ↾
ℝ+):ℝ+⟶ℝ) |
| 39 | 37, 38 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (𝜑 → (log ↾
ℝ+):ℝ+⟶ℝ) |
| 40 | 39 | feqmptd 6977 |
. . . . . . . . . . 11
⊢ (𝜑 → (log ↾
ℝ+) = (𝑥
∈ ℝ+ ↦ ((log ↾
ℝ+)‘𝑥))) |
| 41 | | fvres 6925 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ ((log ↾ ℝ+)‘𝑥) = (log‘𝑥)) |
| 42 | 41 | mpteq2ia 5245 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
↦ ((log ↾ ℝ+)‘𝑥)) = (𝑥 ∈ ℝ+ ↦
(log‘𝑥)) |
| 43 | 40, 42 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝜑 → (log ↾
ℝ+) = (𝑥
∈ ℝ+ ↦ (log‘𝑥))) |
| 44 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐹‘𝑘) → (log‘𝑥) = (log‘(𝐹‘𝑘))) |
| 45 | 11, 36, 43, 44 | fmptco 7149 |
. . . . . . . . 9
⊢ (𝜑 → ((log ↾
ℝ+) ∘ 𝐹) = (𝑘 ∈ 𝐴 ↦ (log‘(𝐹‘𝑘)))) |
| 46 | 45 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝜑 → (ℂfld
Σg ((log ↾ ℝ+) ∘ 𝐹)) = (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (log‘(𝐹‘𝑘))))) |
| 47 | 33, 35, 46 | 3eqtr4d 2787 |
. . . . . . 7
⊢ (𝜑 → -(ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) = (ℂfld
Σg ((log ↾ ℝ+) ∘ 𝐹))) |
| 48 | | amgm.1 |
. . . . . . . . . . . . . . 15
⊢ 𝑀 =
(mulGrp‘ℂfld) |
| 49 | 48 | oveq1i 7441 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ↾s (ℂ
∖ {0})) = ((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0})) |
| 50 | 49 | rpmsubg 21449 |
. . . . . . . . . . . . 13
⊢
ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖
{0}))) |
| 51 | | subgsubm 19166 |
. . . . . . . . . . . . 13
⊢
(ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0})))
→ ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖
{0})))) |
| 52 | 50, 51 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖
{0}))) |
| 53 | | cnfldbas 21368 |
. . . . . . . . . . . . . . 15
⊢ ℂ =
(Base‘ℂfld) |
| 54 | | cndrng 21411 |
. . . . . . . . . . . . . . 15
⊢
ℂfld ∈ DivRing |
| 55 | 53, 1, 54 | drngui 20735 |
. . . . . . . . . . . . . 14
⊢ (ℂ
∖ {0}) = (Unit‘ℂfld) |
| 56 | 55, 48 | unitsubm 20386 |
. . . . . . . . . . . . 13
⊢
(ℂfld ∈ Ring → (ℂ ∖ {0}) ∈
(SubMnd‘𝑀)) |
| 57 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ↾s (ℂ
∖ {0})) = (𝑀
↾s (ℂ ∖ {0})) |
| 58 | 57 | subsubm 18829 |
. . . . . . . . . . . . 13
⊢ ((ℂ
∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈
(SubMnd‘(𝑀
↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈
(SubMnd‘𝑀) ∧
ℝ+ ⊆ (ℂ ∖ {0})))) |
| 59 | 2, 56, 58 | mp2b 10 |
. . . . . . . . . . . 12
⊢
(ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0})))
↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ
∖ {0}))) |
| 60 | 52, 59 | mpbi 230 |
. . . . . . . . . . 11
⊢
(ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ
∖ {0})) |
| 61 | 60 | simpli 483 |
. . . . . . . . . 10
⊢
ℝ+ ∈ (SubMnd‘𝑀) |
| 62 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑀 ↾s
ℝ+) = (𝑀
↾s ℝ+) |
| 63 | 62 | submbas 18827 |
. . . . . . . . . 10
⊢
(ℝ+ ∈ (SubMnd‘𝑀) → ℝ+ =
(Base‘(𝑀
↾s ℝ+))) |
| 64 | 61, 63 | ax-mp 5 |
. . . . . . . . 9
⊢
ℝ+ = (Base‘(𝑀 ↾s
ℝ+)) |
| 65 | | cnfld1 21406 |
. . . . . . . . . . . 12
⊢ 1 =
(1r‘ℂfld) |
| 66 | 48, 65 | ringidval 20180 |
. . . . . . . . . . 11
⊢ 1 =
(0g‘𝑀) |
| 67 | 62, 66 | subm0 18828 |
. . . . . . . . . 10
⊢
(ℝ+ ∈ (SubMnd‘𝑀) → 1 = (0g‘(𝑀 ↾s
ℝ+))) |
| 68 | 61, 67 | ax-mp 5 |
. . . . . . . . 9
⊢ 1 =
(0g‘(𝑀
↾s ℝ+)) |
| 69 | | cncrng 21401 |
. . . . . . . . . . 11
⊢
ℂfld ∈ CRing |
| 70 | 48 | crngmgp 20238 |
. . . . . . . . . . 11
⊢
(ℂfld ∈ CRing → 𝑀 ∈ CMnd) |
| 71 | 69, 70 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ CMnd) |
| 72 | 62 | submmnd 18826 |
. . . . . . . . . . 11
⊢
(ℝ+ ∈ (SubMnd‘𝑀) → (𝑀 ↾s ℝ+)
∈ Mnd) |
| 73 | 61, 72 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 ↾s ℝ+)
∈ Mnd) |
| 74 | 62 | subcmn 19855 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ CMnd ∧ (𝑀 ↾s
ℝ+) ∈ Mnd) → (𝑀 ↾s ℝ+)
∈ CMnd) |
| 75 | 71, 73, 74 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 ↾s ℝ+)
∈ CMnd) |
| 76 | | df-refld 21623 |
. . . . . . . . . . . 12
⊢
ℝfld = (ℂfld ↾s
ℝ) |
| 77 | 76 | subrgring 20574 |
. . . . . . . . . . 11
⊢ (ℝ
∈ (SubRing‘ℂfld) → ℝfld
∈ Ring) |
| 78 | 7, 77 | ax-mp 5 |
. . . . . . . . . 10
⊢
ℝfld ∈ Ring |
| 79 | | ringmnd 20240 |
. . . . . . . . . 10
⊢
(ℝfld ∈ Ring → ℝfld ∈
Mnd) |
| 80 | 78, 79 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → ℝfld
∈ Mnd) |
| 81 | 48 | oveq1i 7441 |
. . . . . . . . . . . 12
⊢ (𝑀 ↾s
ℝ+) = ((mulGrp‘ℂfld)
↾s ℝ+) |
| 82 | 81 | reloggim 26641 |
. . . . . . . . . . 11
⊢ (log
↾ ℝ+) ∈ ((𝑀 ↾s ℝ+)
GrpIso ℝfld) |
| 83 | | gimghm 19282 |
. . . . . . . . . . 11
⊢ ((log
↾ ℝ+) ∈ ((𝑀 ↾s ℝ+)
GrpIso ℝfld) → (log ↾ ℝ+) ∈
((𝑀 ↾s
ℝ+) GrpHom ℝfld)) |
| 84 | 82, 83 | ax-mp 5 |
. . . . . . . . . 10
⊢ (log
↾ ℝ+) ∈ ((𝑀 ↾s ℝ+)
GrpHom ℝfld) |
| 85 | | ghmmhm 19244 |
. . . . . . . . . 10
⊢ ((log
↾ ℝ+) ∈ ((𝑀 ↾s ℝ+)
GrpHom ℝfld) → (log ↾ ℝ+) ∈
((𝑀 ↾s
ℝ+) MndHom ℝfld)) |
| 86 | 84, 85 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → (log ↾
ℝ+) ∈ ((𝑀 ↾s ℝ+)
MndHom ℝfld)) |
| 87 | | 1ex 11257 |
. . . . . . . . . . 11
⊢ 1 ∈
V |
| 88 | 87 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
V) |
| 89 | 10, 5, 88 | fdmfifsupp 9415 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 finSupp 1) |
| 90 | 64, 68, 75, 80, 5, 86, 10, 89 | gsummhm 19956 |
. . . . . . . 8
⊢ (𝜑 → (ℝfld
Σg ((log ↾ ℝ+) ∘ 𝐹)) = ((log ↾
ℝ+)‘((𝑀 ↾s ℝ+)
Σg 𝐹))) |
| 91 | | subgsubm 19166 |
. . . . . . . . . 10
⊢ (ℝ
∈ (SubGrp‘ℂfld) → ℝ ∈
(SubMnd‘ℂfld)) |
| 92 | 9, 91 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ℝ ∈
(SubMnd‘ℂfld)) |
| 93 | | fco 6760 |
. . . . . . . . . 10
⊢ (((log
↾ ℝ+):ℝ+⟶ℝ ∧ 𝐹:𝐴⟶ℝ+) → ((log
↾ ℝ+) ∘ 𝐹):𝐴⟶ℝ) |
| 94 | 39, 10, 93 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ((log ↾
ℝ+) ∘ 𝐹):𝐴⟶ℝ) |
| 95 | 5, 92, 94, 76 | gsumsubm 18848 |
. . . . . . . 8
⊢ (𝜑 → (ℂfld
Σg ((log ↾ ℝ+) ∘ 𝐹)) = (ℝfld
Σg ((log ↾ ℝ+) ∘ 𝐹))) |
| 96 | 61 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ+ ∈
(SubMnd‘𝑀)) |
| 97 | 5, 96, 10, 62 | gsumsubm 18848 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 Σg 𝐹) = ((𝑀 ↾s ℝ+)
Σg 𝐹)) |
| 98 | 97 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝜑 → ((log ↾
ℝ+)‘(𝑀 Σg 𝐹)) = ((log ↾
ℝ+)‘((𝑀 ↾s ℝ+)
Σg 𝐹))) |
| 99 | 90, 95, 98 | 3eqtr4d 2787 |
. . . . . . 7
⊢ (𝜑 → (ℂfld
Σg ((log ↾ ℝ+) ∘ 𝐹)) = ((log ↾
ℝ+)‘(𝑀 Σg 𝐹))) |
| 100 | 66, 71, 5, 96, 10, 89 | gsumsubmcl 19937 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 Σg 𝐹) ∈
ℝ+) |
| 101 | 100 | fvresd 6926 |
. . . . . . 7
⊢ (𝜑 → ((log ↾
ℝ+)‘(𝑀 Σg 𝐹)) = (log‘(𝑀 Σg
𝐹))) |
| 102 | 47, 99, 101 | 3eqtrd 2781 |
. . . . . 6
⊢ (𝜑 → -(ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) = (log‘(𝑀 Σg 𝐹))) |
| 103 | 102 | oveq1d 7446 |
. . . . 5
⊢ (𝜑 → (-(ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) = ((log‘(𝑀 Σg 𝐹)) / (♯‘𝐴))) |
| 104 | 100 | relogcld 26665 |
. . . . . . 7
⊢ (𝜑 → (log‘(𝑀 Σg
𝐹)) ∈
ℝ) |
| 105 | 104 | recnd 11289 |
. . . . . 6
⊢ (𝜑 → (log‘(𝑀 Σg
𝐹)) ∈
ℂ) |
| 106 | 105, 24, 25 | divrec2d 12047 |
. . . . 5
⊢ (𝜑 → ((log‘(𝑀 Σg
𝐹)) / (♯‘𝐴)) = ((1 / (♯‘𝐴)) · (log‘(𝑀 Σg
𝐹)))) |
| 107 | 26, 103, 106 | 3eqtrd 2781 |
. . . 4
⊢ (𝜑 → -((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) = ((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹)))) |
| 108 | 36 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → (ℂfld
Σg 𝐹) = (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))) |
| 109 | 11 | rpcnd 13079 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℂ) |
| 110 | 5, 109 | gsumfsum 21452 |
. . . . . . . . 9
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) = Σ𝑘 ∈ 𝐴 (𝐹‘𝑘)) |
| 111 | 108, 110 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → (ℂfld
Σg 𝐹) = Σ𝑘 ∈ 𝐴 (𝐹‘𝑘)) |
| 112 | 5, 20, 11 | fsumrpcl 15773 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (𝐹‘𝑘) ∈
ℝ+) |
| 113 | 111, 112 | eqeltrd 2841 |
. . . . . . 7
⊢ (𝜑 → (ℂfld
Σg 𝐹) ∈
ℝ+) |
| 114 | 23 | nnrpd 13075 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝐴) ∈
ℝ+) |
| 115 | 113, 114 | rpdivcld 13094 |
. . . . . 6
⊢ (𝜑 → ((ℂfld
Σg 𝐹) / (♯‘𝐴)) ∈
ℝ+) |
| 116 | 115 | relogcld 26665 |
. . . . 5
⊢ (𝜑 →
(log‘((ℂfld Σg 𝐹) / (♯‘𝐴))) ∈ ℝ) |
| 117 | 18, 23 | nndivred 12320 |
. . . . 5
⊢ (𝜑 → ((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) ∈ ℝ) |
| 118 | | rpssre 13042 |
. . . . . . . . 9
⊢
ℝ+ ⊆ ℝ |
| 119 | 118 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ+
⊆ ℝ) |
| 120 | | relogcl 26617 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ℝ+
→ (log‘𝑤) ∈
ℝ) |
| 121 | 120 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
(log‘𝑤) ∈
ℝ) |
| 122 | 121 | renegcld 11690 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
-(log‘𝑤) ∈
ℝ) |
| 123 | 122 | fmpttd 7135 |
. . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ ℝ+ ↦
-(log‘𝑤)):ℝ+⟶ℝ) |
| 124 | | ioorp 13465 |
. . . . . . . . . . . 12
⊢
(0(,)+∞) = ℝ+ |
| 125 | 124 | eleq2i 2833 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (0(,)+∞) ↔
𝑎 ∈
ℝ+) |
| 126 | 124 | eleq2i 2833 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ (0(,)+∞) ↔
𝑏 ∈
ℝ+) |
| 127 | | iccssioo2 13460 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ (0(,)+∞) ∧
𝑏 ∈ (0(,)+∞))
→ (𝑎[,]𝑏) ⊆
(0(,)+∞)) |
| 128 | 125, 126,
127 | syl2anbr 599 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) → (𝑎[,]𝑏) ⊆ (0(,)+∞)) |
| 129 | 128, 124 | sseqtrdi 4024 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) → (𝑎[,]𝑏) ⊆
ℝ+) |
| 130 | 129 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
→ (𝑎[,]𝑏) ⊆
ℝ+) |
| 131 | 23 | nnrecred 12317 |
. . . . . . . . . 10
⊢ (𝜑 → (1 / (♯‘𝐴)) ∈
ℝ) |
| 132 | 114 | rpreccld 13087 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 / (♯‘𝐴)) ∈
ℝ+) |
| 133 | 132 | rpge0d 13081 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ (1 /
(♯‘𝐴))) |
| 134 | | elrege0 13494 |
. . . . . . . . . 10
⊢ ((1 /
(♯‘𝐴)) ∈
(0[,)+∞) ↔ ((1 / (♯‘𝐴)) ∈ ℝ ∧ 0 ≤ (1 /
(♯‘𝐴)))) |
| 135 | 131, 133,
134 | sylanbrc 583 |
. . . . . . . . 9
⊢ (𝜑 → (1 / (♯‘𝐴)) ∈
(0[,)+∞)) |
| 136 | | fconst6g 6797 |
. . . . . . . . 9
⊢ ((1 /
(♯‘𝐴)) ∈
(0[,)+∞) → (𝐴
× {(1 / (♯‘𝐴))}):𝐴⟶(0[,)+∞)) |
| 137 | 135, 136 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 × {(1 / (♯‘𝐴))}):𝐴⟶(0[,)+∞)) |
| 138 | | 0lt1 11785 |
. . . . . . . . 9
⊢ 0 <
1 |
| 139 | | fconstmpt 5747 |
. . . . . . . . . . 11
⊢ (𝐴 × {(1 /
(♯‘𝐴))}) =
(𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴))) |
| 140 | 139 | oveq2i 7442 |
. . . . . . . . . 10
⊢
(ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))})) = (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴)))) |
| 141 | | ringmnd 20240 |
. . . . . . . . . . . . 13
⊢
(ℂfld ∈ Ring → ℂfld ∈
Mnd) |
| 142 | 2, 141 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℂfld
∈ Mnd) |
| 143 | 131 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 / (♯‘𝐴)) ∈
ℂ) |
| 144 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(.g‘ℂfld) =
(.g‘ℂfld) |
| 145 | 53, 144 | gsumconst 19952 |
. . . . . . . . . . . 12
⊢
((ℂfld ∈ Mnd ∧ 𝐴 ∈ Fin ∧ (1 / (♯‘𝐴)) ∈ ℂ) →
(ℂfld Σg (𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴)))) = ((♯‘𝐴)(.g‘ℂfld)(1
/ (♯‘𝐴)))) |
| 146 | 142, 5, 143, 145 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴)))) = ((♯‘𝐴)(.g‘ℂfld)(1
/ (♯‘𝐴)))) |
| 147 | 23 | nnzd 12640 |
. . . . . . . . . . . 12
⊢ (𝜑 → (♯‘𝐴) ∈
ℤ) |
| 148 | | cnfldmulg 21416 |
. . . . . . . . . . . 12
⊢
(((♯‘𝐴)
∈ ℤ ∧ (1 / (♯‘𝐴)) ∈ ℂ) →
((♯‘𝐴)(.g‘ℂfld)(1
/ (♯‘𝐴))) =
((♯‘𝐴) ·
(1 / (♯‘𝐴)))) |
| 149 | 147, 143,
148 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → ((♯‘𝐴)(.g‘ℂfld)(1
/ (♯‘𝐴))) =
((♯‘𝐴) ·
(1 / (♯‘𝐴)))) |
| 150 | 24, 25 | recidd 12038 |
. . . . . . . . . . 11
⊢ (𝜑 → ((♯‘𝐴) · (1 /
(♯‘𝐴))) =
1) |
| 151 | 146, 149,
150 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴)))) = 1) |
| 152 | 140, 151 | eqtrid 2789 |
. . . . . . . . 9
⊢ (𝜑 → (ℂfld
Σg (𝐴 × {(1 / (♯‘𝐴))})) = 1) |
| 153 | 138, 152 | breqtrrid 5181 |
. . . . . . . 8
⊢ (𝜑 → 0 <
(ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))}))) |
| 154 | | logccv 26705 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ 𝑦 ∈
ℝ+ ∧ 𝑥
< 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))) |
| 155 | 154 | 3adant1 1131 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))) |
| 156 | | ioossre 13448 |
. . . . . . . . . . . . . . 15
⊢ (0(,)1)
⊆ ℝ |
| 157 | | simp3 1139 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ (0(,)1)) |
| 158 | 156, 157 | sselid 3981 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ) |
| 159 | | simp21 1207 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑥 ∈ ℝ+) |
| 160 | 159 | relogcld 26665 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈
ℝ) |
| 161 | 158, 160 | remulcld 11291 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℝ) |
| 162 | | 1re 11261 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
| 163 | | resubcl 11573 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ ∧ 𝑡
∈ ℝ) → (1 − 𝑡) ∈ ℝ) |
| 164 | 162, 158,
163 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈
ℝ) |
| 165 | | simp22 1208 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑦 ∈ ℝ+) |
| 166 | 165 | relogcld 26665 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈
ℝ) |
| 167 | 164, 166 | remulcld 11291 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈
ℝ) |
| 168 | 161, 167 | readdcld 11290 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) ∈ ℝ) |
| 169 | | simp1 1137 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝜑) |
| 170 | | ioossicc 13473 |
. . . . . . . . . . . . . . 15
⊢ (0(,)1)
⊆ (0[,]1) |
| 171 | 170, 157 | sselid 3981 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ (0[,]1)) |
| 172 | 119, 130 | cvxcl 27028 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑡 ∈ (0[,]1)))
→ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈
ℝ+) |
| 173 | 169, 159,
165, 171, 172 | syl13anc 1374 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈
ℝ+) |
| 174 | 173 | relogcld 26665 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ ℝ) |
| 175 | 168, 174 | ltnegd 11841 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ↔ -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))))) |
| 176 | 155, 175 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦)))) |
| 177 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) → (log‘𝑤) = (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))) |
| 178 | 177 | negeqd 11502 |
. . . . . . . . . . . 12
⊢ (𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) → -(log‘𝑤) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))) |
| 179 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ ℝ+
↦ -(log‘𝑤)) =
(𝑤 ∈
ℝ+ ↦ -(log‘𝑤)) |
| 180 | | negex 11506 |
. . . . . . . . . . . 12
⊢
-(log‘((𝑡
· 𝑥) + ((1 −
𝑡) · 𝑦))) ∈ V |
| 181 | 178, 179,
180 | fvmpt 7016 |
. . . . . . . . . . 11
⊢ (((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ+ → ((𝑤 ∈ ℝ+
↦ -(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))) |
| 182 | 173, 181 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))) |
| 183 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑥 → (log‘𝑤) = (log‘𝑥)) |
| 184 | 183 | negeqd 11502 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑥 → -(log‘𝑤) = -(log‘𝑥)) |
| 185 | | negex 11506 |
. . . . . . . . . . . . . . . 16
⊢
-(log‘𝑥)
∈ V |
| 186 | 184, 179,
185 | fvmpt 7016 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ ((𝑤 ∈
ℝ+ ↦ -(log‘𝑤))‘𝑥) = -(log‘𝑥)) |
| 187 | 159, 186 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑥) = -(log‘𝑥)) |
| 188 | 187 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑥)) = (𝑡 · -(log‘𝑥))) |
| 189 | 158 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℂ) |
| 190 | 160 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈
ℂ) |
| 191 | 189, 190 | mulneg2d 11717 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · -(log‘𝑥)) = -(𝑡 · (log‘𝑥))) |
| 192 | 188, 191 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑥)) = -(𝑡 · (log‘𝑥))) |
| 193 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑦 → (log‘𝑤) = (log‘𝑦)) |
| 194 | 193 | negeqd 11502 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑦 → -(log‘𝑤) = -(log‘𝑦)) |
| 195 | | negex 11506 |
. . . . . . . . . . . . . . . 16
⊢
-(log‘𝑦)
∈ V |
| 196 | 194, 179,
195 | fvmpt 7016 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ+
→ ((𝑤 ∈
ℝ+ ↦ -(log‘𝑤))‘𝑦) = -(log‘𝑦)) |
| 197 | 165, 196 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑦) = -(log‘𝑦)) |
| 198 | 197 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑦)) = ((1 − 𝑡) · -(log‘𝑦))) |
| 199 | 164 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈
ℂ) |
| 200 | 166 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈
ℂ) |
| 201 | 199, 200 | mulneg2d 11717 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · -(log‘𝑦)) = -((1 − 𝑡) · (log‘𝑦))) |
| 202 | 198, 201 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑦)) = -((1 − 𝑡) · (log‘𝑦))) |
| 203 | 192, 202 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑦))) = (-(𝑡 · (log‘𝑥)) + -((1 − 𝑡) · (log‘𝑦)))) |
| 204 | 161 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℂ) |
| 205 | 167 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈
ℂ) |
| 206 | 204, 205 | negdid 11633 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) = (-(𝑡 · (log‘𝑥)) + -((1 − 𝑡) · (log‘𝑦)))) |
| 207 | 203, 206 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑦))) = -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦)))) |
| 208 | 176, 182,
207 | 3brtr4d 5175 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑦)))) |
| 209 | 119, 123,
130, 208 | scvxcvx 27029 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+
∧ 𝑠 ∈ (0[,]1)))
→ ((𝑤 ∈
ℝ+ ↦ -(log‘𝑤))‘((𝑠 · 𝑢) + ((1 − 𝑠) · 𝑣))) ≤ ((𝑠 · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑢)) + ((1 − 𝑠) · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑣)))) |
| 210 | 119, 123,
130, 5, 137, 10, 153, 209 | jensen 27032 |
. . . . . . 7
⊢ (𝜑 → (((ℂ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 495 |
. . . . . 6
⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘((ℂfld
Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f
· 𝐹)) /
(ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))})))) ≤
((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f
· ((𝑤 ∈
ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld
Σg (𝐴 × {(1 / (♯‘𝐴))})))) |
| 212 | 131 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (1 / (♯‘𝐴)) ∈
ℝ) |
| 213 | 139 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 × {(1 / (♯‘𝐴))}) = (𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴)))) |
| 214 | 5, 212, 11, 213, 36 | offval2 7717 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴 × {(1 / (♯‘𝐴))}) ∘f
· 𝐹) = (𝑘 ∈ 𝐴 ↦ ((1 / (♯‘𝐴)) · (𝐹‘𝑘)))) |
| 215 | 214 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℂfld
Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f
· 𝐹)) =
(ℂfld Σg (𝑘 ∈ 𝐴 ↦ ((1 / (♯‘𝐴)) · (𝐹‘𝑘))))) |
| 216 | | cnfldmul 21372 |
. . . . . . . . . . . 12
⊢ ·
= (.r‘ℂfld) |
| 217 | 2 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℂfld
∈ Ring) |
| 218 | 109 | fmpttd 7135 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)):𝐴⟶ℂ) |
| 219 | 218, 5, 16 | fdmfifsupp 9415 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) finSupp 0) |
| 220 | 53, 1, 216, 217, 5, 143, 109, 219 | gsummulc2 20314 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ ((1 / (♯‘𝐴)) · (𝐹‘𝑘)))) = ((1 / (♯‘𝐴)) · (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))))) |
| 221 | | fss 6752 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝐴⟶ℝ+ ∧
ℝ+ ⊆ ℝ) → 𝐹:𝐴⟶ℝ) |
| 222 | 10, 118, 221 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) |
| 223 | 10, 5, 16 | fdmfifsupp 9415 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 finSupp 0) |
| 224 | 1, 4, 5, 9, 222, 223 | gsumsubgcl 19938 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℂfld
Σg 𝐹) ∈ ℝ) |
| 225 | 224 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℂfld
Σg 𝐹) ∈ ℂ) |
| 226 | 225, 24, 25 | divrec2d 12047 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((ℂfld
Σg 𝐹) / (♯‘𝐴)) = ((1 / (♯‘𝐴)) · (ℂfld
Σg 𝐹))) |
| 227 | 108 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((1 / (♯‘𝐴)) ·
(ℂfld Σg 𝐹)) = ((1 / (♯‘𝐴)) · (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))))) |
| 228 | 226, 227 | eqtr2d 2778 |
. . . . . . . . . . 11
⊢ (𝜑 → ((1 / (♯‘𝐴)) ·
(ℂfld Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))) = ((ℂfld
Σg 𝐹) / (♯‘𝐴))) |
| 229 | 215, 220,
228 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ (𝜑 → (ℂfld
Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f
· 𝐹)) =
((ℂfld Σg 𝐹) / (♯‘𝐴))) |
| 230 | 229, 152 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝜑 → ((ℂfld
Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f
· 𝐹)) /
(ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))}))) =
(((ℂfld Σg 𝐹) / (♯‘𝐴)) / 1)) |
| 231 | 224, 23 | nndivred 12320 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℂfld
Σg 𝐹) / (♯‘𝐴)) ∈ ℝ) |
| 232 | 231 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℂfld
Σg 𝐹) / (♯‘𝐴)) ∈ ℂ) |
| 233 | 232 | div1d 12035 |
. . . . . . . . 9
⊢ (𝜑 → (((ℂfld
Σg 𝐹) / (♯‘𝐴)) / 1) = ((ℂfld
Σg 𝐹) / (♯‘𝐴))) |
| 234 | 230, 233 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → ((ℂfld
Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f
· 𝐹)) /
(ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))}))) = ((ℂfld
Σg 𝐹) / (♯‘𝐴))) |
| 235 | 234 | fveq2d 6910 |
. . . . . . 7
⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘((ℂfld
Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f
· 𝐹)) /
(ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))})))) = ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘((ℂfld
Σg 𝐹) / (♯‘𝐴)))) |
| 236 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑤 = ((ℂfld
Σg 𝐹) / (♯‘𝐴)) → (log‘𝑤) = (log‘((ℂfld
Σg 𝐹) / (♯‘𝐴)))) |
| 237 | 236 | negeqd 11502 |
. . . . . . . . 9
⊢ (𝑤 = ((ℂfld
Σg 𝐹) / (♯‘𝐴)) → -(log‘𝑤) = -(log‘((ℂfld
Σg 𝐹) / (♯‘𝐴)))) |
| 238 | | negex 11506 |
. . . . . . . . 9
⊢
-(log‘((ℂfld Σg 𝐹) / (♯‘𝐴))) ∈ V |
| 239 | 237, 179,
238 | fvmpt 7016 |
. . . . . . . 8
⊢
(((ℂfld Σg 𝐹) / (♯‘𝐴)) ∈ ℝ+ → ((𝑤 ∈ ℝ+
↦ -(log‘𝑤))‘((ℂfld
Σg 𝐹) / (♯‘𝐴))) = -(log‘((ℂfld
Σg 𝐹) / (♯‘𝐴)))) |
| 240 | 115, 239 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘((ℂfld
Σg 𝐹) / (♯‘𝐴))) = -(log‘((ℂfld
Σg 𝐹) / (♯‘𝐴)))) |
| 241 | 235, 240 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘((ℂfld
Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f
· 𝐹)) /
(ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))})))) =
-(log‘((ℂfld Σg 𝐹) / (♯‘𝐴)))) |
| 242 | 53, 1, 216, 217, 5, 143, 31, 17 | gsummulc2 20314 |
. . . . . . . . 9
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ ((1 / (♯‘𝐴)) · -(log‘(𝐹‘𝑘))))) = ((1 / (♯‘𝐴)) ·
(ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))))) |
| 243 | | negex 11506 |
. . . . . . . . . . . 12
⊢
-(log‘(𝐹‘𝑘)) ∈ V |
| 244 | 243 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘(𝐹‘𝑘)) ∈ V) |
| 245 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑤 ∈ ℝ+ ↦
-(log‘𝑤)) = (𝑤 ∈ ℝ+
↦ -(log‘𝑤))) |
| 246 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝐹‘𝑘) → (log‘𝑤) = (log‘(𝐹‘𝑘))) |
| 247 | 246 | negeqd 11502 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝐹‘𝑘) → -(log‘𝑤) = -(log‘(𝐹‘𝑘))) |
| 248 | 11, 36, 245, 247 | fmptco 7149 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤)) ∘
𝐹) = (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) |
| 249 | 5, 212, 244, 213, 248 | offval2 7717 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 × {(1 / (♯‘𝐴))}) ∘f
· ((𝑤 ∈
ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹)) = (𝑘 ∈ 𝐴 ↦ ((1 / (♯‘𝐴)) · -(log‘(𝐹‘𝑘))))) |
| 250 | 249 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → (ℂfld
Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f
· ((𝑤 ∈
ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) = (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ ((1 / (♯‘𝐴)) · -(log‘(𝐹‘𝑘)))))) |
| 251 | 19, 24, 25 | divrec2d 12047 |
. . . . . . . . 9
⊢ (𝜑 → ((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) = ((1 / (♯‘𝐴)) · (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))))) |
| 252 | 242, 250,
251 | 3eqtr4d 2787 |
. . . . . . . 8
⊢ (𝜑 → (ℂfld
Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f
· ((𝑤 ∈
ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) = ((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴))) |
| 253 | 252, 152 | oveq12d 7449 |
. . . . . . 7
⊢ (𝜑 → ((ℂfld
Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f
· ((𝑤 ∈
ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld
Σg (𝐴 × {(1 / (♯‘𝐴))}))) =
(((ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) / 1)) |
| 254 | 117 | recnd 11289 |
. . . . . . . 8
⊢ (𝜑 → ((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) ∈ ℂ) |
| 255 | 254 | div1d 12035 |
. . . . . . 7
⊢ (𝜑 → (((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) / 1) = ((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴))) |
| 256 | 253, 255 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → ((ℂfld
Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘f
· ((𝑤 ∈
ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld
Σg (𝐴 × {(1 / (♯‘𝐴))}))) = ((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴))) |
| 257 | 211, 241,
256 | 3brtr3d 5174 |
. . . . 5
⊢ (𝜑 →
-(log‘((ℂfld Σg 𝐹) / (♯‘𝐴))) ≤ ((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴))) |
| 258 | 116, 117,
257 | lenegcon1d 11845 |
. . . 4
⊢ (𝜑 → -((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) ≤ (log‘((ℂfld
Σg 𝐹) / (♯‘𝐴)))) |
| 259 | 107, 258 | eqbrtrrd 5167 |
. . 3
⊢ (𝜑 → ((1 / (♯‘𝐴)) · (log‘(𝑀 Σg
𝐹))) ≤
(log‘((ℂfld Σg 𝐹) / (♯‘𝐴)))) |
| 260 | 131, 104 | remulcld 11291 |
. . . 4
⊢ (𝜑 → ((1 / (♯‘𝐴)) · (log‘(𝑀 Σg
𝐹))) ∈
ℝ) |
| 261 | | efle 16154 |
. . . 4
⊢ ((((1 /
(♯‘𝐴)) ·
(log‘(𝑀
Σg 𝐹))) ∈ ℝ ∧
(log‘((ℂfld Σg 𝐹) / (♯‘𝐴))) ∈ ℝ) → (((1 /
(♯‘𝐴)) ·
(log‘(𝑀
Σg 𝐹))) ≤ (log‘((ℂfld
Σg 𝐹) / (♯‘𝐴))) ↔ (exp‘((1 /
(♯‘𝐴)) ·
(log‘(𝑀
Σg 𝐹)))) ≤
(exp‘(log‘((ℂfld Σg 𝐹) / (♯‘𝐴)))))) |
| 262 | 260, 116,
261 | syl2anc 584 |
. . 3
⊢ (𝜑 → (((1 /
(♯‘𝐴)) ·
(log‘(𝑀
Σg 𝐹))) ≤ (log‘((ℂfld
Σg 𝐹) / (♯‘𝐴))) ↔ (exp‘((1 /
(♯‘𝐴)) ·
(log‘(𝑀
Σg 𝐹)))) ≤
(exp‘(log‘((ℂfld Σg 𝐹) / (♯‘𝐴)))))) |
| 263 | 259, 262 | mpbid 232 |
. 2
⊢ (𝜑 → (exp‘((1 /
(♯‘𝐴)) ·
(log‘(𝑀
Σg 𝐹)))) ≤
(exp‘(log‘((ℂfld Σg 𝐹) / (♯‘𝐴))))) |
| 264 | 100 | rpcnd 13079 |
. . 3
⊢ (𝜑 → (𝑀 Σg 𝐹) ∈
ℂ) |
| 265 | 100 | rpne0d 13082 |
. . 3
⊢ (𝜑 → (𝑀 Σg 𝐹) ≠ 0) |
| 266 | 264, 265,
143 | cxpefd 26754 |
. 2
⊢ (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 /
(♯‘𝐴))) =
(exp‘((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹))))) |
| 267 | 115 | reeflogd 26666 |
. . 3
⊢ (𝜑 →
(exp‘(log‘((ℂfld Σg 𝐹) / (♯‘𝐴)))) = ((ℂfld
Σg 𝐹) / (♯‘𝐴))) |
| 268 | 267 | eqcomd 2743 |
. 2
⊢ (𝜑 → ((ℂfld
Σg 𝐹) / (♯‘𝐴)) =
(exp‘(log‘((ℂfld Σg 𝐹) / (♯‘𝐴))))) |
| 269 | 263, 266,
268 | 3brtr4d 5175 |
1
⊢ (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 /
(♯‘𝐴))) ≤
((ℂfld Σg 𝐹) / (♯‘𝐴))) |