| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | amgmwlem.1 | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ Fin) | 
| 2 |  | amgmwlem.3 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝐴⟶ℝ+) | 
| 3 | 2 | ffvelcdmda 7103 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈
ℝ+) | 
| 4 |  | amgmwlem.4 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑊:𝐴⟶ℝ+) | 
| 5 | 4 | ffvelcdmda 7103 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈
ℝ+) | 
| 6 | 5 | rpred 13078 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ) | 
| 7 | 3, 6 | rpcxpcld 26776 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘)↑𝑐(𝑊‘𝑘)) ∈
ℝ+) | 
| 8 | 7 | relogcld 26666 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) ∈ ℝ) | 
| 9 | 8 | recnd 11290 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) ∈ ℂ) | 
| 10 | 1, 9 | gsumfsum 21453 | . . . . . . 7
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))))) = Σ𝑘 ∈ 𝐴 (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘)))) | 
| 11 | 9 | negnegd 11612 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → --(log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) = (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘)))) | 
| 12 | 11 | sumeq2dv 15739 | . . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 --(log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) = Σ𝑘 ∈ 𝐴 (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘)))) | 
| 13 | 8 | renegcld 11691 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) ∈ ℝ) | 
| 14 | 13 | recnd 11290 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) ∈ ℂ) | 
| 15 | 1, 14 | fsumneg 15824 | . . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 --(log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) = -Σ𝑘 ∈ 𝐴 -(log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘)))) | 
| 16 | 3, 6 | logcxpd 26777 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) = ((𝑊‘𝑘) · (log‘(𝐹‘𝑘)))) | 
| 17 | 16 | negeqd 11503 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) = -((𝑊‘𝑘) · (log‘(𝐹‘𝑘)))) | 
| 18 | 17 | sumeq2dv 15739 | . . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 -(log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) = Σ𝑘 ∈ 𝐴 -((𝑊‘𝑘) · (log‘(𝐹‘𝑘)))) | 
| 19 | 18 | negeqd 11503 | . . . . . . . 8
⊢ (𝜑 → -Σ𝑘 ∈ 𝐴 -(log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) = -Σ𝑘 ∈ 𝐴 -((𝑊‘𝑘) · (log‘(𝐹‘𝑘)))) | 
| 20 | 5 | rpcnd 13080 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℂ) | 
| 21 | 3 | relogcld 26666 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘(𝐹‘𝑘)) ∈ ℝ) | 
| 22 | 21 | recnd 11290 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘(𝐹‘𝑘)) ∈ ℂ) | 
| 23 | 20, 22 | mulneg2d 11718 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))) = -((𝑊‘𝑘) · (log‘(𝐹‘𝑘)))) | 
| 24 | 23 | eqcomd 2742 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -((𝑊‘𝑘) · (log‘(𝐹‘𝑘))) = ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘)))) | 
| 25 | 24 | sumeq2dv 15739 | . . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 -((𝑊‘𝑘) · (log‘(𝐹‘𝑘))) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘)))) | 
| 26 | 25 | negeqd 11503 | . . . . . . . 8
⊢ (𝜑 → -Σ𝑘 ∈ 𝐴 -((𝑊‘𝑘) · (log‘(𝐹‘𝑘))) = -Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘)))) | 
| 27 | 15, 19, 26 | 3eqtrd 2780 | . . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 --(log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) = -Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘)))) | 
| 28 | 10, 12, 27 | 3eqtr2rd 2783 | . . . . . 6
⊢ (𝜑 → -Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))) = (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘)))))) | 
| 29 |  | negex 11507 | . . . . . . . . . . 11
⊢
-(log‘(𝐹‘𝑘)) ∈ V | 
| 30 | 29 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘(𝐹‘𝑘)) ∈ V) | 
| 31 | 4 | feqmptd 6976 | . . . . . . . . . 10
⊢ (𝜑 → 𝑊 = (𝑘 ∈ 𝐴 ↦ (𝑊‘𝑘))) | 
| 32 |  | eqidd 2737 | . . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))) = (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) | 
| 33 | 1, 5, 30, 31, 32 | offval2 7718 | . . . . . . . . 9
⊢ (𝜑 → (𝑊 ∘f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) = (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))))) | 
| 34 | 33 | oveq2d 7448 | . . . . . . . 8
⊢ (𝜑 → (ℂfld
Σg (𝑊 ∘f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))) = (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘)))))) | 
| 35 | 22 | negcld 11608 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘(𝐹‘𝑘)) ∈ ℂ) | 
| 36 | 20, 35 | mulcld 11282 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))) ∈ ℂ) | 
| 37 | 1, 36 | gsumfsum 21453 | . . . . . . . 8
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))))) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘)))) | 
| 38 | 34, 37 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → (ℂfld
Σg (𝑊 ∘f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘)))) | 
| 39 | 38 | negeqd 11503 | . . . . . 6
⊢ (𝜑 → -(ℂfld
Σg (𝑊 ∘f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))) = -Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘)))) | 
| 40 |  | relogf1o 26609 | . . . . . . . . . 10
⊢ (log
↾ ℝ+):ℝ+–1-1-onto→ℝ | 
| 41 |  | f1of 6847 | . . . . . . . . . 10
⊢ ((log
↾ ℝ+):ℝ+–1-1-onto→ℝ → (log ↾
ℝ+):ℝ+⟶ℝ) | 
| 42 | 40, 41 | ax-mp 5 | . . . . . . . . 9
⊢ (log
↾
ℝ+):ℝ+⟶ℝ | 
| 43 |  | rpre 13044 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) | 
| 44 | 43 | anim2i 617 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑦 ∈
ℝ+) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈
ℝ)) | 
| 45 | 44 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (𝑥 ∈
ℝ+ ∧ 𝑦
∈ ℝ)) | 
| 46 |  | rpcxpcl 26719 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑦 ∈ ℝ)
→ (𝑥↑𝑐𝑦) ∈
ℝ+) | 
| 47 | 45, 46 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (𝑥↑𝑐𝑦) ∈
ℝ+) | 
| 48 |  | inidm 4226 | . . . . . . . . . 10
⊢ (𝐴 ∩ 𝐴) = 𝐴 | 
| 49 | 47, 2, 4, 1, 1, 48 | off 7716 | . . . . . . . . 9
⊢ (𝜑 → (𝐹 ∘f
↑𝑐𝑊):𝐴⟶ℝ+) | 
| 50 |  | fcompt 7152 | . . . . . . . . 9
⊢ (((log
↾ ℝ+):ℝ+⟶ℝ ∧ (𝐹 ∘f
↑𝑐𝑊):𝐴⟶ℝ+) → ((log
↾ ℝ+) ∘ (𝐹 ∘f
↑𝑐𝑊)) = (𝑘 ∈ 𝐴 ↦ ((log ↾
ℝ+)‘((𝐹 ∘f
↑𝑐𝑊)‘𝑘)))) | 
| 51 | 42, 49, 50 | sylancr 587 | . . . . . . . 8
⊢ (𝜑 → ((log ↾
ℝ+) ∘ (𝐹 ∘f
↑𝑐𝑊)) = (𝑘 ∈ 𝐴 ↦ ((log ↾
ℝ+)‘((𝐹 ∘f
↑𝑐𝑊)‘𝑘)))) | 
| 52 | 49 | ffvelcdmda 7103 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹 ∘f
↑𝑐𝑊)‘𝑘) ∈
ℝ+) | 
| 53 |  | fvres 6924 | . . . . . . . . . . 11
⊢ (((𝐹 ∘f
↑𝑐𝑊)‘𝑘) ∈ ℝ+ → ((log
↾ ℝ+)‘((𝐹 ∘f
↑𝑐𝑊)‘𝑘)) = (log‘((𝐹 ∘f
↑𝑐𝑊)‘𝑘))) | 
| 54 | 52, 53 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((log ↾
ℝ+)‘((𝐹 ∘f
↑𝑐𝑊)‘𝑘)) = (log‘((𝐹 ∘f
↑𝑐𝑊)‘𝑘))) | 
| 55 | 2 | ffnd 6736 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 Fn 𝐴) | 
| 56 | 4 | ffnd 6736 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 Fn 𝐴) | 
| 57 |  | eqidd 2737 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) = (𝐹‘𝑘)) | 
| 58 |  | eqidd 2737 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) = (𝑊‘𝑘)) | 
| 59 | 55, 56, 1, 1, 48, 57, 58 | ofval 7709 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹 ∘f
↑𝑐𝑊)‘𝑘) = ((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) | 
| 60 | 59 | fveq2d 6909 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘((𝐹 ∘f
↑𝑐𝑊)‘𝑘)) = (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘)))) | 
| 61 | 54, 60 | eqtrd 2776 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((log ↾
ℝ+)‘((𝐹 ∘f
↑𝑐𝑊)‘𝑘)) = (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘)))) | 
| 62 | 61 | mpteq2dva 5241 | . . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ ((log ↾
ℝ+)‘((𝐹 ∘f
↑𝑐𝑊)‘𝑘))) = (𝑘 ∈ 𝐴 ↦ (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))))) | 
| 63 | 51, 62 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → ((log ↾
ℝ+) ∘ (𝐹 ∘f
↑𝑐𝑊)) = (𝑘 ∈ 𝐴 ↦ (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))))) | 
| 64 | 63 | oveq2d 7448 | . . . . . 6
⊢ (𝜑 → (ℂfld
Σg ((log ↾ ℝ+) ∘ (𝐹 ∘f
↑𝑐𝑊))) = (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘)))))) | 
| 65 | 28, 39, 64 | 3eqtr4d 2786 | . . . . 5
⊢ (𝜑 → -(ℂfld
Σg (𝑊 ∘f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))) = (ℂfld
Σg ((log ↾ ℝ+) ∘ (𝐹 ∘f
↑𝑐𝑊)))) | 
| 66 |  | amgmwlem.0 | . . . . . . . . . . . . 13
⊢ 𝑀 =
(mulGrp‘ℂfld) | 
| 67 | 66 | oveq1i 7442 | . . . . . . . . . . . 12
⊢ (𝑀 ↾s (ℂ
∖ {0})) = ((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0})) | 
| 68 | 67 | rpmsubg 21450 | . . . . . . . . . . 11
⊢
ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖
{0}))) | 
| 69 |  | subgsubm 19167 | . . . . . . . . . . 11
⊢
(ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0})))
→ ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖
{0})))) | 
| 70 | 68, 69 | ax-mp 5 | . . . . . . . . . 10
⊢
ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖
{0}))) | 
| 71 |  | cnring 21404 | . . . . . . . . . . 11
⊢
ℂfld ∈ Ring | 
| 72 |  | cnfldbas 21369 | . . . . . . . . . . . . 13
⊢ ℂ =
(Base‘ℂfld) | 
| 73 |  | cnfld0 21406 | . . . . . . . . . . . . 13
⊢ 0 =
(0g‘ℂfld) | 
| 74 |  | cndrng 21412 | . . . . . . . . . . . . 13
⊢
ℂfld ∈ DivRing | 
| 75 | 72, 73, 74 | drngui 20736 | . . . . . . . . . . . 12
⊢ (ℂ
∖ {0}) = (Unit‘ℂfld) | 
| 76 | 75, 66 | unitsubm 20387 | . . . . . . . . . . 11
⊢
(ℂfld ∈ Ring → (ℂ ∖ {0}) ∈
(SubMnd‘𝑀)) | 
| 77 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ (𝑀 ↾s (ℂ
∖ {0})) = (𝑀
↾s (ℂ ∖ {0})) | 
| 78 | 77 | subsubm 18830 | . . . . . . . . . . 11
⊢ ((ℂ
∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈
(SubMnd‘(𝑀
↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈
(SubMnd‘𝑀) ∧
ℝ+ ⊆ (ℂ ∖ {0})))) | 
| 79 | 71, 76, 78 | mp2b 10 | . . . . . . . . . 10
⊢
(ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0})))
↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ
∖ {0}))) | 
| 80 | 70, 79 | mpbi 230 | . . . . . . . . 9
⊢
(ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ
∖ {0})) | 
| 81 | 80 | simpli 483 | . . . . . . . 8
⊢
ℝ+ ∈ (SubMnd‘𝑀) | 
| 82 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑀 ↾s
ℝ+) = (𝑀
↾s ℝ+) | 
| 83 | 82 | submbas 18828 | . . . . . . . 8
⊢
(ℝ+ ∈ (SubMnd‘𝑀) → ℝ+ =
(Base‘(𝑀
↾s ℝ+))) | 
| 84 | 81, 83 | ax-mp 5 | . . . . . . 7
⊢
ℝ+ = (Base‘(𝑀 ↾s
ℝ+)) | 
| 85 |  | cnfld1 21407 | . . . . . . . . 9
⊢ 1 =
(1r‘ℂfld) | 
| 86 | 66, 85 | ringidval 20181 | . . . . . . . 8
⊢ 1 =
(0g‘𝑀) | 
| 87 |  | eqid 2736 | . . . . . . . . . 10
⊢
(0g‘𝑀) = (0g‘𝑀) | 
| 88 | 82, 87 | subm0 18829 | . . . . . . . . 9
⊢
(ℝ+ ∈ (SubMnd‘𝑀) → (0g‘𝑀) = (0g‘(𝑀 ↾s
ℝ+))) | 
| 89 | 81, 88 | ax-mp 5 | . . . . . . . 8
⊢
(0g‘𝑀) = (0g‘(𝑀 ↾s
ℝ+)) | 
| 90 | 86, 89 | eqtri 2764 | . . . . . . 7
⊢ 1 =
(0g‘(𝑀
↾s ℝ+)) | 
| 91 |  | cncrng 21402 | . . . . . . . . 9
⊢
ℂfld ∈ CRing | 
| 92 | 66 | crngmgp 20239 | . . . . . . . . 9
⊢
(ℂfld ∈ CRing → 𝑀 ∈ CMnd) | 
| 93 | 91, 92 | mp1i 13 | . . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ CMnd) | 
| 94 | 82 | submmnd 18827 | . . . . . . . . 9
⊢
(ℝ+ ∈ (SubMnd‘𝑀) → (𝑀 ↾s ℝ+)
∈ Mnd) | 
| 95 | 81, 94 | mp1i 13 | . . . . . . . 8
⊢ (𝜑 → (𝑀 ↾s ℝ+)
∈ Mnd) | 
| 96 | 82 | subcmn 19856 | . . . . . . . 8
⊢ ((𝑀 ∈ CMnd ∧ (𝑀 ↾s
ℝ+) ∈ Mnd) → (𝑀 ↾s ℝ+)
∈ CMnd) | 
| 97 | 93, 95, 96 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (𝑀 ↾s ℝ+)
∈ CMnd) | 
| 98 |  | resubdrg 21627 | . . . . . . . . . 10
⊢ (ℝ
∈ (SubRing‘ℂfld) ∧ ℝfld ∈
DivRing) | 
| 99 | 98 | simpli 483 | . . . . . . . . 9
⊢ ℝ
∈ (SubRing‘ℂfld) | 
| 100 |  | df-refld 21624 | . . . . . . . . . 10
⊢
ℝfld = (ℂfld ↾s
ℝ) | 
| 101 | 100 | subrgring 20575 | . . . . . . . . 9
⊢ (ℝ
∈ (SubRing‘ℂfld) → ℝfld
∈ Ring) | 
| 102 | 99, 101 | ax-mp 5 | . . . . . . . 8
⊢
ℝfld ∈ Ring | 
| 103 |  | ringmnd 20241 | . . . . . . . 8
⊢
(ℝfld ∈ Ring → ℝfld ∈
Mnd) | 
| 104 | 102, 103 | mp1i 13 | . . . . . . 7
⊢ (𝜑 → ℝfld
∈ Mnd) | 
| 105 | 66 | oveq1i 7442 | . . . . . . . . . 10
⊢ (𝑀 ↾s
ℝ+) = ((mulGrp‘ℂfld)
↾s ℝ+) | 
| 106 | 105 | reloggim 26642 | . . . . . . . . 9
⊢ (log
↾ ℝ+) ∈ ((𝑀 ↾s ℝ+)
GrpIso ℝfld) | 
| 107 |  | gimghm 19283 | . . . . . . . . 9
⊢ ((log
↾ ℝ+) ∈ ((𝑀 ↾s ℝ+)
GrpIso ℝfld) → (log ↾ ℝ+) ∈
((𝑀 ↾s
ℝ+) GrpHom ℝfld)) | 
| 108 | 106, 107 | ax-mp 5 | . . . . . . . 8
⊢ (log
↾ ℝ+) ∈ ((𝑀 ↾s ℝ+)
GrpHom ℝfld) | 
| 109 |  | ghmmhm 19245 | . . . . . . . 8
⊢ ((log
↾ ℝ+) ∈ ((𝑀 ↾s ℝ+)
GrpHom ℝfld) → (log ↾ ℝ+) ∈
((𝑀 ↾s
ℝ+) MndHom ℝfld)) | 
| 110 | 108, 109 | mp1i 13 | . . . . . . 7
⊢ (𝜑 → (log ↾
ℝ+) ∈ ((𝑀 ↾s ℝ+)
MndHom ℝfld)) | 
| 111 |  | 1red 11263 | . . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ) | 
| 112 | 49, 1, 111 | fdmfifsupp 9416 | . . . . . . 7
⊢ (𝜑 → (𝐹 ∘f
↑𝑐𝑊) finSupp 1) | 
| 113 | 84, 90, 97, 104, 1, 110, 49, 112 | gsummhm 19957 | . . . . . 6
⊢ (𝜑 → (ℝfld
Σg ((log ↾ ℝ+) ∘ (𝐹 ∘f
↑𝑐𝑊))) = ((log ↾
ℝ+)‘((𝑀 ↾s ℝ+)
Σg (𝐹 ∘f
↑𝑐𝑊)))) | 
| 114 |  | subrgsubg 20578 | . . . . . . . . . 10
⊢ (ℝ
∈ (SubRing‘ℂfld) → ℝ ∈
(SubGrp‘ℂfld)) | 
| 115 | 99, 114 | ax-mp 5 | . . . . . . . . 9
⊢ ℝ
∈ (SubGrp‘ℂfld) | 
| 116 |  | subgsubm 19167 | . . . . . . . . 9
⊢ (ℝ
∈ (SubGrp‘ℂfld) → ℝ ∈
(SubMnd‘ℂfld)) | 
| 117 | 115, 116 | ax-mp 5 | . . . . . . . 8
⊢ ℝ
∈ (SubMnd‘ℂfld) | 
| 118 | 117 | a1i 11 | . . . . . . 7
⊢ (𝜑 → ℝ ∈
(SubMnd‘ℂfld)) | 
| 119 | 40, 41 | mp1i 13 | . . . . . . . 8
⊢ (𝜑 → (log ↾
ℝ+):ℝ+⟶ℝ) | 
| 120 |  | fco 6759 | . . . . . . . 8
⊢ (((log
↾ ℝ+):ℝ+⟶ℝ ∧ (𝐹 ∘f
↑𝑐𝑊):𝐴⟶ℝ+) → ((log
↾ ℝ+) ∘ (𝐹 ∘f
↑𝑐𝑊)):𝐴⟶ℝ) | 
| 121 | 119, 49, 120 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → ((log ↾
ℝ+) ∘ (𝐹 ∘f
↑𝑐𝑊)):𝐴⟶ℝ) | 
| 122 | 1, 118, 121, 100 | gsumsubm 18849 | . . . . . 6
⊢ (𝜑 → (ℂfld
Σg ((log ↾ ℝ+) ∘ (𝐹 ∘f
↑𝑐𝑊))) = (ℝfld
Σg ((log ↾ ℝ+) ∘ (𝐹 ∘f
↑𝑐𝑊)))) | 
| 123 | 81 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → ℝ+ ∈
(SubMnd‘𝑀)) | 
| 124 | 1, 123, 49, 82 | gsumsubm 18849 | . . . . . . 7
⊢ (𝜑 → (𝑀 Σg (𝐹 ∘f
↑𝑐𝑊)) = ((𝑀 ↾s ℝ+)
Σg (𝐹 ∘f
↑𝑐𝑊))) | 
| 125 | 124 | fveq2d 6909 | . . . . . 6
⊢ (𝜑 → ((log ↾
ℝ+)‘(𝑀 Σg (𝐹 ∘f
↑𝑐𝑊))) = ((log ↾
ℝ+)‘((𝑀 ↾s ℝ+)
Σg (𝐹 ∘f
↑𝑐𝑊)))) | 
| 126 | 113, 122,
125 | 3eqtr4d 2786 | . . . . 5
⊢ (𝜑 → (ℂfld
Σg ((log ↾ ℝ+) ∘ (𝐹 ∘f
↑𝑐𝑊))) = ((log ↾
ℝ+)‘(𝑀 Σg (𝐹 ∘f
↑𝑐𝑊)))) | 
| 127 | 86, 93, 1, 123, 49, 112 | gsumsubmcl 19938 | . . . . . 6
⊢ (𝜑 → (𝑀 Σg (𝐹 ∘f
↑𝑐𝑊)) ∈
ℝ+) | 
| 128 |  | fvres 6924 | . . . . . 6
⊢ ((𝑀 Σg
(𝐹 ∘f
↑𝑐𝑊)) ∈ ℝ+ → ((log
↾ ℝ+)‘(𝑀 Σg (𝐹 ∘f
↑𝑐𝑊))) = (log‘(𝑀 Σg (𝐹 ∘f
↑𝑐𝑊)))) | 
| 129 | 127, 128 | syl 17 | . . . . 5
⊢ (𝜑 → ((log ↾
ℝ+)‘(𝑀 Σg (𝐹 ∘f
↑𝑐𝑊))) = (log‘(𝑀 Σg (𝐹 ∘f
↑𝑐𝑊)))) | 
| 130 | 65, 126, 129 | 3eqtrd 2780 | . . . 4
⊢ (𝜑 → -(ℂfld
Σg (𝑊 ∘f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))) = (log‘(𝑀 Σg (𝐹 ∘f
↑𝑐𝑊)))) | 
| 131 |  | simprl 770 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ 𝑥 ∈
ℝ+) | 
| 132 | 131 | rpcnd 13080 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ 𝑥 ∈
ℂ) | 
| 133 |  | simprr 772 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ 𝑦 ∈
ℝ+) | 
| 134 | 133 | rpcnd 13080 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ 𝑦 ∈
ℂ) | 
| 135 | 132, 134 | mulcomd 11283 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (𝑥 · 𝑦) = (𝑦 · 𝑥)) | 
| 136 | 1, 4, 2, 135 | caofcom 7735 | . . . . . . . 8
⊢ (𝜑 → (𝑊 ∘f · 𝐹) = (𝐹 ∘f · 𝑊)) | 
| 137 | 136 | oveq2d 7448 | . . . . . . 7
⊢ (𝜑 → (ℂfld
Σg (𝑊 ∘f · 𝐹)) = (ℂfld
Σg (𝐹 ∘f · 𝑊))) | 
| 138 | 2 | feqmptd 6976 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) | 
| 139 | 1, 5, 3, 31, 138 | offval2 7718 | . . . . . . . . . 10
⊢ (𝜑 → (𝑊 ∘f · 𝐹) = (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · (𝐹‘𝑘)))) | 
| 140 | 139 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝜑 → (ℂfld
Σg (𝑊 ∘f · 𝐹)) = (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · (𝐹‘𝑘))))) | 
| 141 | 5, 3 | rpmulcld 13094 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈
ℝ+) | 
| 142 | 141 | rpcnd 13080 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℂ) | 
| 143 | 1, 142 | gsumfsum 21453 | . . . . . . . . 9
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · (𝐹‘𝑘)))) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · (𝐹‘𝑘))) | 
| 144 | 140, 143 | eqtrd 2776 | . . . . . . . 8
⊢ (𝜑 → (ℂfld
Σg (𝑊 ∘f · 𝐹)) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · (𝐹‘𝑘))) | 
| 145 |  | amgmwlem.2 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ≠ ∅) | 
| 146 | 1, 145, 141 | fsumrpcl 15774 | . . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈
ℝ+) | 
| 147 | 144, 146 | eqeltrd 2840 | . . . . . . 7
⊢ (𝜑 → (ℂfld
Σg (𝑊 ∘f · 𝐹)) ∈
ℝ+) | 
| 148 | 137, 147 | eqeltrrd 2841 | . . . . . 6
⊢ (𝜑 → (ℂfld
Σg (𝐹 ∘f · 𝑊)) ∈
ℝ+) | 
| 149 | 148 | relogcld 26666 | . . . . 5
⊢ (𝜑 →
(log‘(ℂfld Σg (𝐹 ∘f · 𝑊))) ∈
ℝ) | 
| 150 |  | ringcmn 20280 | . . . . . . 7
⊢
(ℂfld ∈ Ring → ℂfld ∈
CMnd) | 
| 151 | 71, 150 | mp1i 13 | . . . . . 6
⊢ (𝜑 → ℂfld
∈ CMnd) | 
| 152 |  | remulcl 11241 | . . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ) | 
| 153 | 152 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ) | 
| 154 |  | rpssre 13043 | . . . . . . . 8
⊢
ℝ+ ⊆ ℝ | 
| 155 |  | fss 6751 | . . . . . . . 8
⊢ ((𝑊:𝐴⟶ℝ+ ∧
ℝ+ ⊆ ℝ) → 𝑊:𝐴⟶ℝ) | 
| 156 | 4, 154, 155 | sylancl 586 | . . . . . . 7
⊢ (𝜑 → 𝑊:𝐴⟶ℝ) | 
| 157 | 21 | renegcld 11691 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘(𝐹‘𝑘)) ∈ ℝ) | 
| 158 | 157 | fmpttd 7134 | . . . . . . 7
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))):𝐴⟶ℝ) | 
| 159 | 153, 156,
158, 1, 1, 48 | off 7716 | . . . . . 6
⊢ (𝜑 → (𝑊 ∘f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))):𝐴⟶ℝ) | 
| 160 |  | 0red 11265 | . . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ) | 
| 161 | 159, 1, 160 | fdmfifsupp 9416 | . . . . . 6
⊢ (𝜑 → (𝑊 ∘f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) finSupp 0) | 
| 162 | 73, 151, 1, 118, 159, 161 | gsumsubmcl 19938 | . . . . 5
⊢ (𝜑 → (ℂfld
Σg (𝑊 ∘f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))) ∈ ℝ) | 
| 163 | 154 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → ℝ+
⊆ ℝ) | 
| 164 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈
ℝ+) | 
| 165 | 164 | relogcld 26666 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
(log‘𝑤) ∈
ℝ) | 
| 166 | 165 | renegcld 11691 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
-(log‘𝑤) ∈
ℝ) | 
| 167 | 166 | fmpttd 7134 | . . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ ℝ+ ↦
-(log‘𝑤)):ℝ+⟶ℝ) | 
| 168 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) → 𝑎 ∈ ℝ+) | 
| 169 |  | ioorp 13466 | . . . . . . . . . . . 12
⊢
(0(,)+∞) = ℝ+ | 
| 170 | 168, 169 | eleqtrrdi 2851 | . . . . . . . . . . 11
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) → 𝑎 ∈ (0(,)+∞)) | 
| 171 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) → 𝑏 ∈ ℝ+) | 
| 172 | 171, 169 | eleqtrrdi 2851 | . . . . . . . . . . 11
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) → 𝑏 ∈ (0(,)+∞)) | 
| 173 |  | iccssioo2 13461 | . . . . . . . . . . 11
⊢ ((𝑎 ∈ (0(,)+∞) ∧
𝑏 ∈ (0(,)+∞))
→ (𝑎[,]𝑏) ⊆
(0(,)+∞)) | 
| 174 | 170, 172,
173 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) → (𝑎[,]𝑏) ⊆ (0(,)+∞)) | 
| 175 | 174, 169 | sseqtrdi 4023 | . . . . . . . . 9
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) → (𝑎[,]𝑏) ⊆
ℝ+) | 
| 176 | 175 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
→ (𝑎[,]𝑏) ⊆
ℝ+) | 
| 177 |  | ioossico 13479 | . . . . . . . . . 10
⊢
(0(,)+∞) ⊆ (0[,)+∞) | 
| 178 | 169, 177 | eqsstrri 4030 | . . . . . . . . 9
⊢
ℝ+ ⊆ (0[,)+∞) | 
| 179 |  | fss 6751 | . . . . . . . . 9
⊢ ((𝑊:𝐴⟶ℝ+ ∧
ℝ+ ⊆ (0[,)+∞)) → 𝑊:𝐴⟶(0[,)+∞)) | 
| 180 | 4, 178, 179 | sylancl 586 | . . . . . . . 8
⊢ (𝜑 → 𝑊:𝐴⟶(0[,)+∞)) | 
| 181 |  | 0lt1 11786 | . . . . . . . . 9
⊢ 0 <
1 | 
| 182 |  | amgmwlem.5 | . . . . . . . . 9
⊢ (𝜑 → (ℂfld
Σg 𝑊) = 1) | 
| 183 | 181, 182 | breqtrrid 5180 | . . . . . . . 8
⊢ (𝜑 → 0 <
(ℂfld Σg 𝑊)) | 
| 184 |  | logccv 26706 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ 𝑦 ∈
ℝ+ ∧ 𝑥
< 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))) | 
| 185 | 184 | 3adant1 1130 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))) | 
| 186 |  | elioore 13418 | . . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈
ℝ) | 
| 187 | 186 | 3ad2ant3 1135 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ) | 
| 188 |  | simp21 1206 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑥 ∈ ℝ+) | 
| 189 | 188 | relogcld 26666 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈
ℝ) | 
| 190 | 187, 189 | remulcld 11292 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℝ) | 
| 191 |  | 1red 11263 | . . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ (0(,)1) → 1 ∈
ℝ) | 
| 192 | 191, 186 | resubcld 11692 | . . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ (0(,)1) → (1
− 𝑡) ∈
ℝ) | 
| 193 | 192 | 3ad2ant3 1135 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈
ℝ) | 
| 194 |  | simp22 1207 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑦 ∈ ℝ+) | 
| 195 | 194 | relogcld 26666 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈
ℝ) | 
| 196 | 193, 195 | remulcld 11292 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈
ℝ) | 
| 197 | 190, 196 | readdcld 11291 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) ∈ ℝ) | 
| 198 |  | eliooord 13447 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ (0(,)1) → (0 <
𝑡 ∧ 𝑡 < 1)) | 
| 199 | 198 | simpld 494 | . . . . . . . . . . . . . . . . 17
⊢ (𝑡 ∈ (0(,)1) → 0 <
𝑡) | 
| 200 | 186, 199 | elrpd 13075 | . . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈
ℝ+) | 
| 201 | 200 | 3ad2ant3 1135 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ+) | 
| 202 | 201, 188 | rpmulcld 13094 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · 𝑥) ∈
ℝ+) | 
| 203 |  | 0red 11265 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ (0(,)1) → 0 ∈
ℝ) | 
| 204 | 198 | simprd 495 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 ∈ (0(,)1) → 𝑡 < 1) | 
| 205 |  | 1m0e1 12388 | . . . . . . . . . . . . . . . . . . 19
⊢ (1
− 0) = 1 | 
| 206 | 204, 205 | breqtrrdi 5184 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ (0(,)1) → 𝑡 < (1 −
0)) | 
| 207 | 186, 191,
203, 206 | ltsub13d 11870 | . . . . . . . . . . . . . . . . 17
⊢ (𝑡 ∈ (0(,)1) → 0 < (1
− 𝑡)) | 
| 208 | 192, 207 | elrpd 13075 | . . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ (0(,)1) → (1
− 𝑡) ∈
ℝ+) | 
| 209 | 208 | 3ad2ant3 1135 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈
ℝ+) | 
| 210 | 209, 194 | rpmulcld 13094 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · 𝑦) ∈
ℝ+) | 
| 211 |  | rpaddcl 13058 | . . . . . . . . . . . . . 14
⊢ (((𝑡 · 𝑥) ∈ ℝ+ ∧ ((1
− 𝑡) · 𝑦) ∈ ℝ+)
→ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈
ℝ+) | 
| 212 | 202, 210,
211 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈
ℝ+) | 
| 213 | 212 | relogcld 26666 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ ℝ) | 
| 214 | 197, 213 | ltnegd 11842 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ↔ -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))))) | 
| 215 | 185, 214 | mpbid 232 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦)))) | 
| 216 |  | eqidd 2737 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑤 ∈ ℝ+ ↦
-(log‘𝑤)) = (𝑤 ∈ ℝ+
↦ -(log‘𝑤))) | 
| 217 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) → (log‘𝑤) = (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))) | 
| 218 | 217 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) ∧ 𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) → (log‘𝑤) = (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))) | 
| 219 | 218 | negeqd 11503 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) ∧ 𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) → -(log‘𝑤) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))) | 
| 220 |  | negex 11507 | . . . . . . . . . . . 12
⊢
-(log‘((𝑡
· 𝑥) + ((1 −
𝑡) · 𝑦))) ∈ V | 
| 221 | 220 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ V) | 
| 222 | 216, 219,
212, 221 | fvmptd 7022 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)))) | 
| 223 |  | fveq2 6905 | . . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑥 → (log‘𝑤) = (log‘𝑥)) | 
| 224 | 223 | negeqd 11503 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑥 → -(log‘𝑤) = -(log‘𝑥)) | 
| 225 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ℝ+
↦ -(log‘𝑤)) =
(𝑤 ∈
ℝ+ ↦ -(log‘𝑤)) | 
| 226 |  | negex 11507 | . . . . . . . . . . . . . . . 16
⊢
-(log‘𝑤)
∈ V | 
| 227 | 224, 225,
226 | fvmpt3i 7020 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ ((𝑤 ∈
ℝ+ ↦ -(log‘𝑤))‘𝑥) = -(log‘𝑥)) | 
| 228 | 188, 227 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑥) = -(log‘𝑥)) | 
| 229 | 228 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑥)) = (𝑡 · -(log‘𝑥))) | 
| 230 | 187 | recnd 11290 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℂ) | 
| 231 | 189 | recnd 11290 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈
ℂ) | 
| 232 | 230, 231 | mulneg2d 11718 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · -(log‘𝑥)) = -(𝑡 · (log‘𝑥))) | 
| 233 | 229, 232 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑥)) = -(𝑡 · (log‘𝑥))) | 
| 234 |  | fveq2 6905 | . . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑦 → (log‘𝑤) = (log‘𝑦)) | 
| 235 | 234 | negeqd 11503 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑦 → -(log‘𝑤) = -(log‘𝑦)) | 
| 236 | 235, 225,
226 | fvmpt3i 7020 | . . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ+
→ ((𝑤 ∈
ℝ+ ↦ -(log‘𝑤))‘𝑦) = -(log‘𝑦)) | 
| 237 | 194, 236 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑦) = -(log‘𝑦)) | 
| 238 | 237 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑦)) = ((1 − 𝑡) · -(log‘𝑦))) | 
| 239 | 209 | rpcnd 13080 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈
ℂ) | 
| 240 | 195 | recnd 11290 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈
ℂ) | 
| 241 | 239, 240 | mulneg2d 11718 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · -(log‘𝑦)) = -((1 − 𝑡) · (log‘𝑦))) | 
| 242 | 238, 241 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑦)) = -((1 − 𝑡) · (log‘𝑦))) | 
| 243 | 233, 242 | oveq12d 7450 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑦))) = (-(𝑡 · (log‘𝑥)) + -((1 − 𝑡) · (log‘𝑦)))) | 
| 244 | 190 | recnd 11290 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℂ) | 
| 245 | 196 | recnd 11290 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈
ℂ) | 
| 246 | 244, 245 | negdid 11634 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) = (-(𝑡 · (log‘𝑥)) + -((1 − 𝑡) · (log‘𝑦)))) | 
| 247 | 243, 246 | eqtr4d 2779 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑦))) = -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦)))) | 
| 248 | 215, 222,
247 | 3brtr4d 5174 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+
∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑦)))) | 
| 249 | 163, 167,
176, 248 | scvxcvx 27030 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+
∧ 𝑠 ∈ (0[,]1)))
→ ((𝑤 ∈
ℝ+ ↦ -(log‘𝑤))‘((𝑠 · 𝑢) + ((1 − 𝑠) · 𝑣))) ≤ ((𝑠 · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑢)) + ((1 − 𝑠) · ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘𝑣)))) | 
| 250 | 163, 167,
176, 1, 180, 2, 183, 249 | jensen 27033 | . . . . . . 7
⊢ (𝜑 → (((ℂfld
Σg (𝑊 ∘f · 𝐹)) / (ℂfld
Σg 𝑊)) ∈ ℝ+ ∧ ((𝑤 ∈ ℝ+
↦ -(log‘𝑤))‘((ℂfld
Σg (𝑊 ∘f · 𝐹)) / (ℂfld
Σg 𝑊))) ≤ ((ℂfld
Σg (𝑊 ∘f · ((𝑤 ∈ ℝ+
↦ -(log‘𝑤))
∘ 𝐹))) /
(ℂfld Σg 𝑊)))) | 
| 251 | 250 | simprd 495 | . . . . . 6
⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘((ℂfld
Σg (𝑊 ∘f · 𝐹)) / (ℂfld
Σg 𝑊))) ≤ ((ℂfld
Σg (𝑊 ∘f · ((𝑤 ∈ ℝ+
↦ -(log‘𝑤))
∘ 𝐹))) /
(ℂfld Σg 𝑊))) | 
| 252 | 182 | oveq2d 7448 | . . . . . . . 8
⊢ (𝜑 → ((ℂfld
Σg (𝑊 ∘f · 𝐹)) / (ℂfld
Σg 𝑊)) = ((ℂfld
Σg (𝑊 ∘f · 𝐹)) / 1)) | 
| 253 | 252 | fveq2d 6909 | . . . . . . 7
⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘((ℂfld
Σg (𝑊 ∘f · 𝐹)) / (ℂfld
Σg 𝑊))) = ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘((ℂfld
Σg (𝑊 ∘f · 𝐹)) / 1))) | 
| 254 | 147 | rpcnd 13080 | . . . . . . . . 9
⊢ (𝜑 → (ℂfld
Σg (𝑊 ∘f · 𝐹)) ∈
ℂ) | 
| 255 | 254 | div1d 12036 | . . . . . . . 8
⊢ (𝜑 → ((ℂfld
Σg (𝑊 ∘f · 𝐹)) / 1) = (ℂfld
Σg (𝑊 ∘f · 𝐹))) | 
| 256 | 255 | fveq2d 6909 | . . . . . . 7
⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘((ℂfld
Σg (𝑊 ∘f · 𝐹)) / 1)) = ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘(ℂfld
Σg (𝑊 ∘f · 𝐹)))) | 
| 257 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑤 = (ℂfld
Σg (𝑊 ∘f · 𝐹)) → (log‘𝑤) =
(log‘(ℂfld Σg (𝑊 ∘f · 𝐹)))) | 
| 258 | 257 | negeqd 11503 | . . . . . . . . . 10
⊢ (𝑤 = (ℂfld
Σg (𝑊 ∘f · 𝐹)) → -(log‘𝑤) =
-(log‘(ℂfld Σg (𝑊 ∘f ·
𝐹)))) | 
| 259 | 258, 225,
226 | fvmpt3i 7020 | . . . . . . . . 9
⊢
((ℂfld Σg (𝑊 ∘f · 𝐹)) ∈ ℝ+
→ ((𝑤 ∈
ℝ+ ↦ -(log‘𝑤))‘(ℂfld
Σg (𝑊 ∘f · 𝐹))) =
-(log‘(ℂfld Σg (𝑊 ∘f ·
𝐹)))) | 
| 260 | 147, 259 | syl 17 | . . . . . . . 8
⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘(ℂfld
Σg (𝑊 ∘f · 𝐹))) =
-(log‘(ℂfld Σg (𝑊 ∘f ·
𝐹)))) | 
| 261 | 137 | fveq2d 6909 | . . . . . . . . 9
⊢ (𝜑 →
(log‘(ℂfld Σg (𝑊 ∘f · 𝐹))) =
(log‘(ℂfld Σg (𝐹 ∘f · 𝑊)))) | 
| 262 | 261 | negeqd 11503 | . . . . . . . 8
⊢ (𝜑 →
-(log‘(ℂfld Σg (𝑊 ∘f ·
𝐹))) =
-(log‘(ℂfld Σg (𝐹 ∘f ·
𝑊)))) | 
| 263 | 260, 262 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘(ℂfld
Σg (𝑊 ∘f · 𝐹))) =
-(log‘(ℂfld Σg (𝐹 ∘f ·
𝑊)))) | 
| 264 | 253, 256,
263 | 3eqtrd 2780 | . . . . . 6
⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤))‘((ℂfld
Σg (𝑊 ∘f · 𝐹)) / (ℂfld
Σg 𝑊))) = -(log‘(ℂfld
Σg (𝐹 ∘f · 𝑊)))) | 
| 265 | 182 | oveq2d 7448 | . . . . . . 7
⊢ (𝜑 → ((ℂfld
Σg (𝑊 ∘f · ((𝑤 ∈ ℝ+
↦ -(log‘𝑤))
∘ 𝐹))) /
(ℂfld Σg 𝑊)) = ((ℂfld
Σg (𝑊 ∘f · ((𝑤 ∈ ℝ+
↦ -(log‘𝑤))
∘ 𝐹))) /
1)) | 
| 266 |  | ringmnd 20241 | . . . . . . . . . . 11
⊢
(ℂfld ∈ Ring → ℂfld ∈
Mnd) | 
| 267 | 71, 266 | ax-mp 5 | . . . . . . . . . 10
⊢
ℂfld ∈ Mnd | 
| 268 | 72 | submid 18824 | . . . . . . . . . 10
⊢
(ℂfld ∈ Mnd → ℂ ∈
(SubMnd‘ℂfld)) | 
| 269 | 267, 268 | mp1i 13 | . . . . . . . . 9
⊢ (𝜑 → ℂ ∈
(SubMnd‘ℂfld)) | 
| 270 |  | mulcl 11240 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) | 
| 271 | 270 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ) | 
| 272 |  | rpcn 13046 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) | 
| 273 | 272 | ssriv 3986 | . . . . . . . . . . . 12
⊢
ℝ+ ⊆ ℂ | 
| 274 | 273 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → ℝ+
⊆ ℂ) | 
| 275 | 4, 274 | fssd 6752 | . . . . . . . . . 10
⊢ (𝜑 → 𝑊:𝐴⟶ℂ) | 
| 276 | 165 | recnd 11290 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
(log‘𝑤) ∈
ℂ) | 
| 277 | 276 | negcld 11608 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
-(log‘𝑤) ∈
ℂ) | 
| 278 | 277 | fmpttd 7134 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑤 ∈ ℝ+ ↦
-(log‘𝑤)):ℝ+⟶ℂ) | 
| 279 |  | fco 6759 | . . . . . . . . . . 11
⊢ (((𝑤 ∈ ℝ+
↦ -(log‘𝑤)):ℝ+⟶ℂ ∧
𝐹:𝐴⟶ℝ+) → ((𝑤 ∈ ℝ+
↦ -(log‘𝑤))
∘ 𝐹):𝐴⟶ℂ) | 
| 280 | 278, 2, 279 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤)) ∘
𝐹):𝐴⟶ℂ) | 
| 281 | 271, 275,
280, 1, 1, 48 | off 7716 | . . . . . . . . 9
⊢ (𝜑 → (𝑊 ∘f · ((𝑤 ∈ ℝ+
↦ -(log‘𝑤))
∘ 𝐹)):𝐴⟶ℂ) | 
| 282 | 281, 1, 160 | fdmfifsupp 9416 | . . . . . . . . 9
⊢ (𝜑 → (𝑊 ∘f · ((𝑤 ∈ ℝ+
↦ -(log‘𝑤))
∘ 𝐹)) finSupp
0) | 
| 283 | 73, 151, 1, 269, 281, 282 | gsumsubmcl 19938 | . . . . . . . 8
⊢ (𝜑 → (ℂfld
Σg (𝑊 ∘f · ((𝑤 ∈ ℝ+
↦ -(log‘𝑤))
∘ 𝐹))) ∈
ℂ) | 
| 284 | 283 | div1d 12036 | . . . . . . 7
⊢ (𝜑 → ((ℂfld
Σg (𝑊 ∘f · ((𝑤 ∈ ℝ+
↦ -(log‘𝑤))
∘ 𝐹))) / 1) =
(ℂfld Σg (𝑊 ∘f · ((𝑤 ∈ ℝ+
↦ -(log‘𝑤))
∘ 𝐹)))) | 
| 285 |  | eqidd 2737 | . . . . . . . . . 10
⊢ (𝜑 → (𝑤 ∈ ℝ+ ↦
-(log‘𝑤)) = (𝑤 ∈ ℝ+
↦ -(log‘𝑤))) | 
| 286 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑤 = (𝐹‘𝑘) → (log‘𝑤) = (log‘(𝐹‘𝑘))) | 
| 287 | 286 | negeqd 11503 | . . . . . . . . . 10
⊢ (𝑤 = (𝐹‘𝑘) → -(log‘𝑤) = -(log‘(𝐹‘𝑘))) | 
| 288 | 3, 138, 285, 287 | fmptco 7148 | . . . . . . . . 9
⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦
-(log‘𝑤)) ∘
𝐹) = (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) | 
| 289 | 288 | oveq2d 7448 | . . . . . . . 8
⊢ (𝜑 → (𝑊 ∘f · ((𝑤 ∈ ℝ+
↦ -(log‘𝑤))
∘ 𝐹)) = (𝑊 ∘f ·
(𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))) | 
| 290 | 289 | oveq2d 7448 | . . . . . . 7
⊢ (𝜑 → (ℂfld
Σg (𝑊 ∘f · ((𝑤 ∈ ℝ+
↦ -(log‘𝑤))
∘ 𝐹))) =
(ℂfld Σg (𝑊 ∘f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))))) | 
| 291 | 265, 284,
290 | 3eqtrd 2780 | . . . . . 6
⊢ (𝜑 → ((ℂfld
Σg (𝑊 ∘f · ((𝑤 ∈ ℝ+
↦ -(log‘𝑤))
∘ 𝐹))) /
(ℂfld Σg 𝑊)) = (ℂfld
Σg (𝑊 ∘f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))))) | 
| 292 | 251, 264,
291 | 3brtr3d 5173 | . . . . 5
⊢ (𝜑 →
-(log‘(ℂfld Σg (𝐹 ∘f ·
𝑊))) ≤
(ℂfld Σg (𝑊 ∘f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))))) | 
| 293 | 149, 162,
292 | lenegcon1d 11846 | . . . 4
⊢ (𝜑 → -(ℂfld
Σg (𝑊 ∘f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))) ≤ (log‘(ℂfld
Σg (𝐹 ∘f · 𝑊)))) | 
| 294 | 130, 293 | eqbrtrrd 5166 | . . 3
⊢ (𝜑 → (log‘(𝑀 Σg
(𝐹 ∘f
↑𝑐𝑊))) ≤ (log‘(ℂfld
Σg (𝐹 ∘f · 𝑊)))) | 
| 295 | 127 | relogcld 26666 | . . . 4
⊢ (𝜑 → (log‘(𝑀 Σg
(𝐹 ∘f
↑𝑐𝑊))) ∈ ℝ) | 
| 296 |  | efle 16155 | . . . 4
⊢
(((log‘(𝑀
Σg (𝐹 ∘f
↑𝑐𝑊))) ∈ ℝ ∧
(log‘(ℂfld Σg (𝐹 ∘f · 𝑊))) ∈ ℝ) →
((log‘(𝑀
Σg (𝐹 ∘f
↑𝑐𝑊))) ≤ (log‘(ℂfld
Σg (𝐹 ∘f · 𝑊))) ↔
(exp‘(log‘(𝑀
Σg (𝐹 ∘f
↑𝑐𝑊)))) ≤
(exp‘(log‘(ℂfld Σg (𝐹 ∘f ·
𝑊)))))) | 
| 297 | 295, 149,
296 | syl2anc 584 | . . 3
⊢ (𝜑 → ((log‘(𝑀 Σg
(𝐹 ∘f
↑𝑐𝑊))) ≤ (log‘(ℂfld
Σg (𝐹 ∘f · 𝑊))) ↔
(exp‘(log‘(𝑀
Σg (𝐹 ∘f
↑𝑐𝑊)))) ≤
(exp‘(log‘(ℂfld Σg (𝐹 ∘f ·
𝑊)))))) | 
| 298 | 294, 297 | mpbid 232 | . 2
⊢ (𝜑 →
(exp‘(log‘(𝑀
Σg (𝐹 ∘f
↑𝑐𝑊)))) ≤
(exp‘(log‘(ℂfld Σg (𝐹 ∘f ·
𝑊))))) | 
| 299 | 127 | reeflogd 26667 | . . 3
⊢ (𝜑 →
(exp‘(log‘(𝑀
Σg (𝐹 ∘f
↑𝑐𝑊)))) = (𝑀 Σg (𝐹 ∘f
↑𝑐𝑊))) | 
| 300 | 299 | eqcomd 2742 | . 2
⊢ (𝜑 → (𝑀 Σg (𝐹 ∘f
↑𝑐𝑊)) = (exp‘(log‘(𝑀 Σg
(𝐹 ∘f
↑𝑐𝑊))))) | 
| 301 | 148 | reeflogd 26667 | . . 3
⊢ (𝜑 →
(exp‘(log‘(ℂfld Σg (𝐹 ∘f ·
𝑊)))) =
(ℂfld Σg (𝐹 ∘f · 𝑊))) | 
| 302 | 301 | eqcomd 2742 | . 2
⊢ (𝜑 → (ℂfld
Σg (𝐹 ∘f · 𝑊)) =
(exp‘(log‘(ℂfld Σg (𝐹 ∘f ·
𝑊))))) | 
| 303 | 298, 300,
302 | 3brtr4d 5174 | 1
⊢ (𝜑 → (𝑀 Σg (𝐹 ∘f
↑𝑐𝑊)) ≤ (ℂfld
Σg (𝐹 ∘f · 𝑊))) |