Step |
Hyp |
Ref |
Expression |
1 |
|
amgmwlem.0 |
⊢ 𝑀 = ( mulGrp ‘ ℂfld ) |
2 |
|
amgmwlem.1 |
⊢ ( 𝜑 → 𝐴 ∈ Fin ) |
3 |
|
amgmwlem.2 |
⊢ ( 𝜑 → 𝐴 ≠ ∅ ) |
4 |
|
amgmwlem.3 |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ+ ) |
5 |
|
amgmwlem.4 |
⊢ ( 𝜑 → 𝑊 : 𝐴 ⟶ ℝ+ ) |
6 |
|
amgmwlem.5 |
⊢ ( 𝜑 → ( ℂfld Σg 𝑊 ) = 1 ) |
7 |
4
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ+ ) |
8 |
5
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑊 ‘ 𝑘 ) ∈ ℝ+ ) |
9 |
8
|
rpred |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑊 ‘ 𝑘 ) ∈ ℝ ) |
10 |
7 9
|
rpcxpcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ∈ ℝ+ ) |
11 |
10
|
relogcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) ∈ ℝ ) |
12 |
11
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) ∈ ℂ ) |
13 |
2 12
|
gsumfsum |
⊢ ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) ) ) = Σ 𝑘 ∈ 𝐴 ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) ) |
14 |
12
|
negnegd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → - - ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) = ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) ) |
15 |
14
|
sumeq2dv |
⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 - - ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) = Σ 𝑘 ∈ 𝐴 ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) ) |
16 |
11
|
renegcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → - ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) ∈ ℝ ) |
17 |
16
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → - ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) ∈ ℂ ) |
18 |
2 17
|
fsumneg |
⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 - - ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) = - Σ 𝑘 ∈ 𝐴 - ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) ) |
19 |
7 9
|
logcxpd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) = ( ( 𝑊 ‘ 𝑘 ) · ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) |
20 |
19
|
negeqd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → - ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) = - ( ( 𝑊 ‘ 𝑘 ) · ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) |
21 |
20
|
sumeq2dv |
⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 - ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) = Σ 𝑘 ∈ 𝐴 - ( ( 𝑊 ‘ 𝑘 ) · ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) |
22 |
21
|
negeqd |
⊢ ( 𝜑 → - Σ 𝑘 ∈ 𝐴 - ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) = - Σ 𝑘 ∈ 𝐴 - ( ( 𝑊 ‘ 𝑘 ) · ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) |
23 |
8
|
rpcnd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑊 ‘ 𝑘 ) ∈ ℂ ) |
24 |
7
|
relogcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) |
25 |
24
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℂ ) |
26 |
23 25
|
mulneg2d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑊 ‘ 𝑘 ) · - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) = - ( ( 𝑊 ‘ 𝑘 ) · ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) |
27 |
26
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → - ( ( 𝑊 ‘ 𝑘 ) · ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( ( 𝑊 ‘ 𝑘 ) · - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) |
28 |
27
|
sumeq2dv |
⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 - ( ( 𝑊 ‘ 𝑘 ) · ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) = Σ 𝑘 ∈ 𝐴 ( ( 𝑊 ‘ 𝑘 ) · - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) |
29 |
28
|
negeqd |
⊢ ( 𝜑 → - Σ 𝑘 ∈ 𝐴 - ( ( 𝑊 ‘ 𝑘 ) · ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) = - Σ 𝑘 ∈ 𝐴 ( ( 𝑊 ‘ 𝑘 ) · - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) |
30 |
18 22 29
|
3eqtrd |
⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 - - ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) = - Σ 𝑘 ∈ 𝐴 ( ( 𝑊 ‘ 𝑘 ) · - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) |
31 |
13 15 30
|
3eqtr2rd |
⊢ ( 𝜑 → - Σ 𝑘 ∈ 𝐴 ( ( 𝑊 ‘ 𝑘 ) · - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) ) ) ) |
32 |
|
negex |
⊢ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ V |
33 |
32
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ V ) |
34 |
5
|
feqmptd |
⊢ ( 𝜑 → 𝑊 = ( 𝑘 ∈ 𝐴 ↦ ( 𝑊 ‘ 𝑘 ) ) ) |
35 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) |
36 |
2 8 33 34 35
|
offval2 |
⊢ ( 𝜑 → ( 𝑊 ∘f · ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝑘 ∈ 𝐴 ↦ ( ( 𝑊 ‘ 𝑘 ) · - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) |
37 |
36
|
oveq2d |
⊢ ( 𝜑 → ( ℂfld Σg ( 𝑊 ∘f · ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) = ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( ( 𝑊 ‘ 𝑘 ) · - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) |
38 |
25
|
negcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℂ ) |
39 |
23 38
|
mulcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑊 ‘ 𝑘 ) · - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℂ ) |
40 |
2 39
|
gsumfsum |
⊢ ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( ( 𝑊 ‘ 𝑘 ) · - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) = Σ 𝑘 ∈ 𝐴 ( ( 𝑊 ‘ 𝑘 ) · - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) |
41 |
37 40
|
eqtrd |
⊢ ( 𝜑 → ( ℂfld Σg ( 𝑊 ∘f · ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) = Σ 𝑘 ∈ 𝐴 ( ( 𝑊 ‘ 𝑘 ) · - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) |
42 |
41
|
negeqd |
⊢ ( 𝜑 → - ( ℂfld Σg ( 𝑊 ∘f · ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) = - Σ 𝑘 ∈ 𝐴 ( ( 𝑊 ‘ 𝑘 ) · - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) |
43 |
|
relogf1o |
⊢ ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ |
44 |
|
f1of |
⊢ ( ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ → ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ ) |
45 |
43 44
|
ax-mp |
⊢ ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ |
46 |
|
rpre |
⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ ) |
47 |
46
|
anim2i |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ ) ) |
48 |
47
|
adantl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) → ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ ) ) |
49 |
|
rpcxpcl |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ↑𝑐 𝑦 ) ∈ ℝ+ ) |
50 |
48 49
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) → ( 𝑥 ↑𝑐 𝑦 ) ∈ ℝ+ ) |
51 |
|
inidm |
⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴 |
52 |
50 4 5 2 2 51
|
off |
⊢ ( 𝜑 → ( 𝐹 ∘f ↑𝑐 𝑊 ) : 𝐴 ⟶ ℝ+ ) |
53 |
|
fcompt |
⊢ ( ( ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ ∧ ( 𝐹 ∘f ↑𝑐 𝑊 ) : 𝐴 ⟶ ℝ+ ) → ( ( log ↾ ℝ+ ) ∘ ( 𝐹 ∘f ↑𝑐 𝑊 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( ( log ↾ ℝ+ ) ‘ ( ( 𝐹 ∘f ↑𝑐 𝑊 ) ‘ 𝑘 ) ) ) ) |
54 |
45 52 53
|
sylancr |
⊢ ( 𝜑 → ( ( log ↾ ℝ+ ) ∘ ( 𝐹 ∘f ↑𝑐 𝑊 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( ( log ↾ ℝ+ ) ‘ ( ( 𝐹 ∘f ↑𝑐 𝑊 ) ‘ 𝑘 ) ) ) ) |
55 |
52
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐹 ∘f ↑𝑐 𝑊 ) ‘ 𝑘 ) ∈ ℝ+ ) |
56 |
|
fvres |
⊢ ( ( ( 𝐹 ∘f ↑𝑐 𝑊 ) ‘ 𝑘 ) ∈ ℝ+ → ( ( log ↾ ℝ+ ) ‘ ( ( 𝐹 ∘f ↑𝑐 𝑊 ) ‘ 𝑘 ) ) = ( log ‘ ( ( 𝐹 ∘f ↑𝑐 𝑊 ) ‘ 𝑘 ) ) ) |
57 |
55 56
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( log ↾ ℝ+ ) ‘ ( ( 𝐹 ∘f ↑𝑐 𝑊 ) ‘ 𝑘 ) ) = ( log ‘ ( ( 𝐹 ∘f ↑𝑐 𝑊 ) ‘ 𝑘 ) ) ) |
58 |
4
|
ffnd |
⊢ ( 𝜑 → 𝐹 Fn 𝐴 ) |
59 |
5
|
ffnd |
⊢ ( 𝜑 → 𝑊 Fn 𝐴 ) |
60 |
|
eqidd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) ) |
61 |
|
eqidd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑊 ‘ 𝑘 ) = ( 𝑊 ‘ 𝑘 ) ) |
62 |
58 59 2 2 51 60 61
|
ofval |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐹 ∘f ↑𝑐 𝑊 ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) |
63 |
62
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( log ‘ ( ( 𝐹 ∘f ↑𝑐 𝑊 ) ‘ 𝑘 ) ) = ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) ) |
64 |
57 63
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( log ↾ ℝ+ ) ‘ ( ( 𝐹 ∘f ↑𝑐 𝑊 ) ‘ 𝑘 ) ) = ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) ) |
65 |
64
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ ( ( log ↾ ℝ+ ) ‘ ( ( 𝐹 ∘f ↑𝑐 𝑊 ) ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝐴 ↦ ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) ) ) |
66 |
54 65
|
eqtrd |
⊢ ( 𝜑 → ( ( log ↾ ℝ+ ) ∘ ( 𝐹 ∘f ↑𝑐 𝑊 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) ) ) |
67 |
66
|
oveq2d |
⊢ ( 𝜑 → ( ℂfld Σg ( ( log ↾ ℝ+ ) ∘ ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) = ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( log ‘ ( ( 𝐹 ‘ 𝑘 ) ↑𝑐 ( 𝑊 ‘ 𝑘 ) ) ) ) ) ) |
68 |
31 42 67
|
3eqtr4d |
⊢ ( 𝜑 → - ( ℂfld Σg ( 𝑊 ∘f · ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) = ( ℂfld Σg ( ( log ↾ ℝ+ ) ∘ ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) ) |
69 |
1
|
oveq1i |
⊢ ( 𝑀 ↾s ( ℂ ∖ { 0 } ) ) = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) |
70 |
69
|
rpmsubg |
⊢ ℝ+ ∈ ( SubGrp ‘ ( 𝑀 ↾s ( ℂ ∖ { 0 } ) ) ) |
71 |
|
subgsubm |
⊢ ( ℝ+ ∈ ( SubGrp ‘ ( 𝑀 ↾s ( ℂ ∖ { 0 } ) ) ) → ℝ+ ∈ ( SubMnd ‘ ( 𝑀 ↾s ( ℂ ∖ { 0 } ) ) ) ) |
72 |
70 71
|
ax-mp |
⊢ ℝ+ ∈ ( SubMnd ‘ ( 𝑀 ↾s ( ℂ ∖ { 0 } ) ) ) |
73 |
|
cnring |
⊢ ℂfld ∈ Ring |
74 |
|
cnfldbas |
⊢ ℂ = ( Base ‘ ℂfld ) |
75 |
|
cnfld0 |
⊢ 0 = ( 0g ‘ ℂfld ) |
76 |
|
cndrng |
⊢ ℂfld ∈ DivRing |
77 |
74 75 76
|
drngui |
⊢ ( ℂ ∖ { 0 } ) = ( Unit ‘ ℂfld ) |
78 |
77 1
|
unitsubm |
⊢ ( ℂfld ∈ Ring → ( ℂ ∖ { 0 } ) ∈ ( SubMnd ‘ 𝑀 ) ) |
79 |
|
eqid |
⊢ ( 𝑀 ↾s ( ℂ ∖ { 0 } ) ) = ( 𝑀 ↾s ( ℂ ∖ { 0 } ) ) |
80 |
79
|
subsubm |
⊢ ( ( ℂ ∖ { 0 } ) ∈ ( SubMnd ‘ 𝑀 ) → ( ℝ+ ∈ ( SubMnd ‘ ( 𝑀 ↾s ( ℂ ∖ { 0 } ) ) ) ↔ ( ℝ+ ∈ ( SubMnd ‘ 𝑀 ) ∧ ℝ+ ⊆ ( ℂ ∖ { 0 } ) ) ) ) |
81 |
73 78 80
|
mp2b |
⊢ ( ℝ+ ∈ ( SubMnd ‘ ( 𝑀 ↾s ( ℂ ∖ { 0 } ) ) ) ↔ ( ℝ+ ∈ ( SubMnd ‘ 𝑀 ) ∧ ℝ+ ⊆ ( ℂ ∖ { 0 } ) ) ) |
82 |
72 81
|
mpbi |
⊢ ( ℝ+ ∈ ( SubMnd ‘ 𝑀 ) ∧ ℝ+ ⊆ ( ℂ ∖ { 0 } ) ) |
83 |
82
|
simpli |
⊢ ℝ+ ∈ ( SubMnd ‘ 𝑀 ) |
84 |
|
eqid |
⊢ ( 𝑀 ↾s ℝ+ ) = ( 𝑀 ↾s ℝ+ ) |
85 |
84
|
submbas |
⊢ ( ℝ+ ∈ ( SubMnd ‘ 𝑀 ) → ℝ+ = ( Base ‘ ( 𝑀 ↾s ℝ+ ) ) ) |
86 |
83 85
|
ax-mp |
⊢ ℝ+ = ( Base ‘ ( 𝑀 ↾s ℝ+ ) ) |
87 |
|
cnfld1 |
⊢ 1 = ( 1r ‘ ℂfld ) |
88 |
1 87
|
ringidval |
⊢ 1 = ( 0g ‘ 𝑀 ) |
89 |
|
eqid |
⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 ) |
90 |
84 89
|
subm0 |
⊢ ( ℝ+ ∈ ( SubMnd ‘ 𝑀 ) → ( 0g ‘ 𝑀 ) = ( 0g ‘ ( 𝑀 ↾s ℝ+ ) ) ) |
91 |
83 90
|
ax-mp |
⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ ( 𝑀 ↾s ℝ+ ) ) |
92 |
88 91
|
eqtri |
⊢ 1 = ( 0g ‘ ( 𝑀 ↾s ℝ+ ) ) |
93 |
|
cncrng |
⊢ ℂfld ∈ CRing |
94 |
1
|
crngmgp |
⊢ ( ℂfld ∈ CRing → 𝑀 ∈ CMnd ) |
95 |
93 94
|
mp1i |
⊢ ( 𝜑 → 𝑀 ∈ CMnd ) |
96 |
84
|
submmnd |
⊢ ( ℝ+ ∈ ( SubMnd ‘ 𝑀 ) → ( 𝑀 ↾s ℝ+ ) ∈ Mnd ) |
97 |
83 96
|
mp1i |
⊢ ( 𝜑 → ( 𝑀 ↾s ℝ+ ) ∈ Mnd ) |
98 |
84
|
subcmn |
⊢ ( ( 𝑀 ∈ CMnd ∧ ( 𝑀 ↾s ℝ+ ) ∈ Mnd ) → ( 𝑀 ↾s ℝ+ ) ∈ CMnd ) |
99 |
95 97 98
|
syl2anc |
⊢ ( 𝜑 → ( 𝑀 ↾s ℝ+ ) ∈ CMnd ) |
100 |
|
resubdrg |
⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) ∧ ℝfld ∈ DivRing ) |
101 |
100
|
simpli |
⊢ ℝ ∈ ( SubRing ‘ ℂfld ) |
102 |
|
df-refld |
⊢ ℝfld = ( ℂfld ↾s ℝ ) |
103 |
102
|
subrgring |
⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) → ℝfld ∈ Ring ) |
104 |
101 103
|
ax-mp |
⊢ ℝfld ∈ Ring |
105 |
|
ringmnd |
⊢ ( ℝfld ∈ Ring → ℝfld ∈ Mnd ) |
106 |
104 105
|
mp1i |
⊢ ( 𝜑 → ℝfld ∈ Mnd ) |
107 |
1
|
oveq1i |
⊢ ( 𝑀 ↾s ℝ+ ) = ( ( mulGrp ‘ ℂfld ) ↾s ℝ+ ) |
108 |
107
|
reloggim |
⊢ ( log ↾ ℝ+ ) ∈ ( ( 𝑀 ↾s ℝ+ ) GrpIso ℝfld ) |
109 |
|
gimghm |
⊢ ( ( log ↾ ℝ+ ) ∈ ( ( 𝑀 ↾s ℝ+ ) GrpIso ℝfld ) → ( log ↾ ℝ+ ) ∈ ( ( 𝑀 ↾s ℝ+ ) GrpHom ℝfld ) ) |
110 |
108 109
|
ax-mp |
⊢ ( log ↾ ℝ+ ) ∈ ( ( 𝑀 ↾s ℝ+ ) GrpHom ℝfld ) |
111 |
|
ghmmhm |
⊢ ( ( log ↾ ℝ+ ) ∈ ( ( 𝑀 ↾s ℝ+ ) GrpHom ℝfld ) → ( log ↾ ℝ+ ) ∈ ( ( 𝑀 ↾s ℝ+ ) MndHom ℝfld ) ) |
112 |
110 111
|
mp1i |
⊢ ( 𝜑 → ( log ↾ ℝ+ ) ∈ ( ( 𝑀 ↾s ℝ+ ) MndHom ℝfld ) ) |
113 |
|
1red |
⊢ ( 𝜑 → 1 ∈ ℝ ) |
114 |
52 2 113
|
fdmfifsupp |
⊢ ( 𝜑 → ( 𝐹 ∘f ↑𝑐 𝑊 ) finSupp 1 ) |
115 |
86 92 99 106 2 112 52 114
|
gsummhm |
⊢ ( 𝜑 → ( ℝfld Σg ( ( log ↾ ℝ+ ) ∘ ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) = ( ( log ↾ ℝ+ ) ‘ ( ( 𝑀 ↾s ℝ+ ) Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) ) |
116 |
|
subrgsubg |
⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) → ℝ ∈ ( SubGrp ‘ ℂfld ) ) |
117 |
101 116
|
ax-mp |
⊢ ℝ ∈ ( SubGrp ‘ ℂfld ) |
118 |
|
subgsubm |
⊢ ( ℝ ∈ ( SubGrp ‘ ℂfld ) → ℝ ∈ ( SubMnd ‘ ℂfld ) ) |
119 |
117 118
|
ax-mp |
⊢ ℝ ∈ ( SubMnd ‘ ℂfld ) |
120 |
119
|
a1i |
⊢ ( 𝜑 → ℝ ∈ ( SubMnd ‘ ℂfld ) ) |
121 |
43 44
|
mp1i |
⊢ ( 𝜑 → ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ ) |
122 |
|
fco |
⊢ ( ( ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ ∧ ( 𝐹 ∘f ↑𝑐 𝑊 ) : 𝐴 ⟶ ℝ+ ) → ( ( log ↾ ℝ+ ) ∘ ( 𝐹 ∘f ↑𝑐 𝑊 ) ) : 𝐴 ⟶ ℝ ) |
123 |
121 52 122
|
syl2anc |
⊢ ( 𝜑 → ( ( log ↾ ℝ+ ) ∘ ( 𝐹 ∘f ↑𝑐 𝑊 ) ) : 𝐴 ⟶ ℝ ) |
124 |
2 120 123 102
|
gsumsubm |
⊢ ( 𝜑 → ( ℂfld Σg ( ( log ↾ ℝ+ ) ∘ ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) = ( ℝfld Σg ( ( log ↾ ℝ+ ) ∘ ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) ) |
125 |
83
|
a1i |
⊢ ( 𝜑 → ℝ+ ∈ ( SubMnd ‘ 𝑀 ) ) |
126 |
2 125 52 84
|
gsumsubm |
⊢ ( 𝜑 → ( 𝑀 Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) = ( ( 𝑀 ↾s ℝ+ ) Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) |
127 |
126
|
fveq2d |
⊢ ( 𝜑 → ( ( log ↾ ℝ+ ) ‘ ( 𝑀 Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) = ( ( log ↾ ℝ+ ) ‘ ( ( 𝑀 ↾s ℝ+ ) Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) ) |
128 |
115 124 127
|
3eqtr4d |
⊢ ( 𝜑 → ( ℂfld Σg ( ( log ↾ ℝ+ ) ∘ ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) = ( ( log ↾ ℝ+ ) ‘ ( 𝑀 Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) ) |
129 |
88 95 2 125 52 114
|
gsumsubmcl |
⊢ ( 𝜑 → ( 𝑀 Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ∈ ℝ+ ) |
130 |
|
fvres |
⊢ ( ( 𝑀 Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ∈ ℝ+ → ( ( log ↾ ℝ+ ) ‘ ( 𝑀 Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) = ( log ‘ ( 𝑀 Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) ) |
131 |
129 130
|
syl |
⊢ ( 𝜑 → ( ( log ↾ ℝ+ ) ‘ ( 𝑀 Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) = ( log ‘ ( 𝑀 Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) ) |
132 |
68 128 131
|
3eqtrd |
⊢ ( 𝜑 → - ( ℂfld Σg ( 𝑊 ∘f · ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) = ( log ‘ ( 𝑀 Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) ) |
133 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) → 𝑥 ∈ ℝ+ ) |
134 |
133
|
rpcnd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) → 𝑥 ∈ ℂ ) |
135 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) → 𝑦 ∈ ℝ+ ) |
136 |
135
|
rpcnd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) → 𝑦 ∈ ℂ ) |
137 |
134 136
|
mulcomd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) ) |
138 |
2 5 4 137
|
caofcom |
⊢ ( 𝜑 → ( 𝑊 ∘f · 𝐹 ) = ( 𝐹 ∘f · 𝑊 ) ) |
139 |
138
|
oveq2d |
⊢ ( 𝜑 → ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) = ( ℂfld Σg ( 𝐹 ∘f · 𝑊 ) ) ) |
140 |
4
|
feqmptd |
⊢ ( 𝜑 → 𝐹 = ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ) |
141 |
2 8 7 34 140
|
offval2 |
⊢ ( 𝜑 → ( 𝑊 ∘f · 𝐹 ) = ( 𝑘 ∈ 𝐴 ↦ ( ( 𝑊 ‘ 𝑘 ) · ( 𝐹 ‘ 𝑘 ) ) ) ) |
142 |
141
|
oveq2d |
⊢ ( 𝜑 → ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) = ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( ( 𝑊 ‘ 𝑘 ) · ( 𝐹 ‘ 𝑘 ) ) ) ) ) |
143 |
8 7
|
rpmulcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑊 ‘ 𝑘 ) · ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ+ ) |
144 |
143
|
rpcnd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑊 ‘ 𝑘 ) · ( 𝐹 ‘ 𝑘 ) ) ∈ ℂ ) |
145 |
2 144
|
gsumfsum |
⊢ ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ ( ( 𝑊 ‘ 𝑘 ) · ( 𝐹 ‘ 𝑘 ) ) ) ) = Σ 𝑘 ∈ 𝐴 ( ( 𝑊 ‘ 𝑘 ) · ( 𝐹 ‘ 𝑘 ) ) ) |
146 |
142 145
|
eqtrd |
⊢ ( 𝜑 → ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) = Σ 𝑘 ∈ 𝐴 ( ( 𝑊 ‘ 𝑘 ) · ( 𝐹 ‘ 𝑘 ) ) ) |
147 |
2 3 143
|
fsumrpcl |
⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( ( 𝑊 ‘ 𝑘 ) · ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ+ ) |
148 |
146 147
|
eqeltrd |
⊢ ( 𝜑 → ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) ∈ ℝ+ ) |
149 |
139 148
|
eqeltrrd |
⊢ ( 𝜑 → ( ℂfld Σg ( 𝐹 ∘f · 𝑊 ) ) ∈ ℝ+ ) |
150 |
149
|
relogcld |
⊢ ( 𝜑 → ( log ‘ ( ℂfld Σg ( 𝐹 ∘f · 𝑊 ) ) ) ∈ ℝ ) |
151 |
|
ringcmn |
⊢ ( ℂfld ∈ Ring → ℂfld ∈ CMnd ) |
152 |
73 151
|
mp1i |
⊢ ( 𝜑 → ℂfld ∈ CMnd ) |
153 |
|
remulcl |
⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 · 𝑦 ) ∈ ℝ ) |
154 |
153
|
adantl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑥 · 𝑦 ) ∈ ℝ ) |
155 |
|
rpssre |
⊢ ℝ+ ⊆ ℝ |
156 |
|
fss |
⊢ ( ( 𝑊 : 𝐴 ⟶ ℝ+ ∧ ℝ+ ⊆ ℝ ) → 𝑊 : 𝐴 ⟶ ℝ ) |
157 |
5 155 156
|
sylancl |
⊢ ( 𝜑 → 𝑊 : 𝐴 ⟶ ℝ ) |
158 |
24
|
renegcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) |
159 |
158
|
fmpttd |
⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) : 𝐴 ⟶ ℝ ) |
160 |
154 157 159 2 2 51
|
off |
⊢ ( 𝜑 → ( 𝑊 ∘f · ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) : 𝐴 ⟶ ℝ ) |
161 |
|
0red |
⊢ ( 𝜑 → 0 ∈ ℝ ) |
162 |
160 2 161
|
fdmfifsupp |
⊢ ( 𝜑 → ( 𝑊 ∘f · ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) finSupp 0 ) |
163 |
75 152 2 120 160 162
|
gsumsubmcl |
⊢ ( 𝜑 → ( ℂfld Σg ( 𝑊 ∘f · ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ∈ ℝ ) |
164 |
155
|
a1i |
⊢ ( 𝜑 → ℝ+ ⊆ ℝ ) |
165 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → 𝑤 ∈ ℝ+ ) |
166 |
165
|
relogcld |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ( log ‘ 𝑤 ) ∈ ℝ ) |
167 |
166
|
renegcld |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → - ( log ‘ 𝑤 ) ∈ ℝ ) |
168 |
167
|
fmpttd |
⊢ ( 𝜑 → ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) : ℝ+ ⟶ ℝ ) |
169 |
|
simpl |
⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → 𝑎 ∈ ℝ+ ) |
170 |
|
ioorp |
⊢ ( 0 (,) +∞ ) = ℝ+ |
171 |
169 170
|
eleqtrrdi |
⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → 𝑎 ∈ ( 0 (,) +∞ ) ) |
172 |
|
simpr |
⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → 𝑏 ∈ ℝ+ ) |
173 |
172 170
|
eleqtrrdi |
⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → 𝑏 ∈ ( 0 (,) +∞ ) ) |
174 |
|
iccssioo2 |
⊢ ( ( 𝑎 ∈ ( 0 (,) +∞ ) ∧ 𝑏 ∈ ( 0 (,) +∞ ) ) → ( 𝑎 [,] 𝑏 ) ⊆ ( 0 (,) +∞ ) ) |
175 |
171 173 174
|
syl2anc |
⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → ( 𝑎 [,] 𝑏 ) ⊆ ( 0 (,) +∞ ) ) |
176 |
175 170
|
sseqtrdi |
⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → ( 𝑎 [,] 𝑏 ) ⊆ ℝ+ ) |
177 |
176
|
adantl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) → ( 𝑎 [,] 𝑏 ) ⊆ ℝ+ ) |
178 |
|
ioossico |
⊢ ( 0 (,) +∞ ) ⊆ ( 0 [,) +∞ ) |
179 |
170 178
|
eqsstrri |
⊢ ℝ+ ⊆ ( 0 [,) +∞ ) |
180 |
|
fss |
⊢ ( ( 𝑊 : 𝐴 ⟶ ℝ+ ∧ ℝ+ ⊆ ( 0 [,) +∞ ) ) → 𝑊 : 𝐴 ⟶ ( 0 [,) +∞ ) ) |
181 |
5 179 180
|
sylancl |
⊢ ( 𝜑 → 𝑊 : 𝐴 ⟶ ( 0 [,) +∞ ) ) |
182 |
|
0lt1 |
⊢ 0 < 1 |
183 |
182 6
|
breqtrrid |
⊢ ( 𝜑 → 0 < ( ℂfld Σg 𝑊 ) ) |
184 |
|
logccv |
⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) < ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ) |
185 |
184
|
3adant1 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) < ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ) |
186 |
|
elioore |
⊢ ( 𝑡 ∈ ( 0 (,) 1 ) → 𝑡 ∈ ℝ ) |
187 |
186
|
3ad2ant3 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑡 ∈ ℝ ) |
188 |
|
simp21 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑥 ∈ ℝ+ ) |
189 |
188
|
relogcld |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( log ‘ 𝑥 ) ∈ ℝ ) |
190 |
187 189
|
remulcld |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑡 · ( log ‘ 𝑥 ) ) ∈ ℝ ) |
191 |
|
1red |
⊢ ( 𝑡 ∈ ( 0 (,) 1 ) → 1 ∈ ℝ ) |
192 |
191 186
|
resubcld |
⊢ ( 𝑡 ∈ ( 0 (,) 1 ) → ( 1 − 𝑡 ) ∈ ℝ ) |
193 |
192
|
3ad2ant3 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 − 𝑡 ) ∈ ℝ ) |
194 |
|
simp22 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑦 ∈ ℝ+ ) |
195 |
194
|
relogcld |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( log ‘ 𝑦 ) ∈ ℝ ) |
196 |
193 195
|
remulcld |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ∈ ℝ ) |
197 |
190 196
|
readdcld |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) ∈ ℝ ) |
198 |
|
eliooord |
⊢ ( 𝑡 ∈ ( 0 (,) 1 ) → ( 0 < 𝑡 ∧ 𝑡 < 1 ) ) |
199 |
198
|
simpld |
⊢ ( 𝑡 ∈ ( 0 (,) 1 ) → 0 < 𝑡 ) |
200 |
186 199
|
elrpd |
⊢ ( 𝑡 ∈ ( 0 (,) 1 ) → 𝑡 ∈ ℝ+ ) |
201 |
200
|
3ad2ant3 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑡 ∈ ℝ+ ) |
202 |
201 188
|
rpmulcld |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑡 · 𝑥 ) ∈ ℝ+ ) |
203 |
|
0red |
⊢ ( 𝑡 ∈ ( 0 (,) 1 ) → 0 ∈ ℝ ) |
204 |
198
|
simprd |
⊢ ( 𝑡 ∈ ( 0 (,) 1 ) → 𝑡 < 1 ) |
205 |
|
1m0e1 |
⊢ ( 1 − 0 ) = 1 |
206 |
204 205
|
breqtrrdi |
⊢ ( 𝑡 ∈ ( 0 (,) 1 ) → 𝑡 < ( 1 − 0 ) ) |
207 |
186 191 203 206
|
ltsub13d |
⊢ ( 𝑡 ∈ ( 0 (,) 1 ) → 0 < ( 1 − 𝑡 ) ) |
208 |
192 207
|
elrpd |
⊢ ( 𝑡 ∈ ( 0 (,) 1 ) → ( 1 − 𝑡 ) ∈ ℝ+ ) |
209 |
208
|
3ad2ant3 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 − 𝑡 ) ∈ ℝ+ ) |
210 |
209 194
|
rpmulcld |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 1 − 𝑡 ) · 𝑦 ) ∈ ℝ+ ) |
211 |
|
rpaddcl |
⊢ ( ( ( 𝑡 · 𝑥 ) ∈ ℝ+ ∧ ( ( 1 − 𝑡 ) · 𝑦 ) ∈ ℝ+ ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ ℝ+ ) |
212 |
202 210 211
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ ℝ+ ) |
213 |
212
|
relogcld |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ ℝ ) |
214 |
197 213
|
ltnegd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) < ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ↔ - ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < - ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) ) ) |
215 |
185 214
|
mpbid |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → - ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < - ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) ) |
216 |
|
eqidd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) = ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ) |
217 |
|
fveq2 |
⊢ ( 𝑤 = ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) → ( log ‘ 𝑤 ) = ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ) |
218 |
217
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) ∧ 𝑤 = ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) → ( log ‘ 𝑤 ) = ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ) |
219 |
218
|
negeqd |
⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) ∧ 𝑤 = ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) → - ( log ‘ 𝑤 ) = - ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ) |
220 |
|
negex |
⊢ - ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ V |
221 |
220
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → - ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ V ) |
222 |
216 219 212 221
|
fvmptd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) = - ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ) |
223 |
|
fveq2 |
⊢ ( 𝑤 = 𝑥 → ( log ‘ 𝑤 ) = ( log ‘ 𝑥 ) ) |
224 |
223
|
negeqd |
⊢ ( 𝑤 = 𝑥 → - ( log ‘ 𝑤 ) = - ( log ‘ 𝑥 ) ) |
225 |
|
eqid |
⊢ ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) = ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) |
226 |
|
negex |
⊢ - ( log ‘ 𝑤 ) ∈ V |
227 |
224 225 226
|
fvmpt3i |
⊢ ( 𝑥 ∈ ℝ+ → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑥 ) = - ( log ‘ 𝑥 ) ) |
228 |
188 227
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑥 ) = - ( log ‘ 𝑥 ) ) |
229 |
228
|
oveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑡 · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑥 ) ) = ( 𝑡 · - ( log ‘ 𝑥 ) ) ) |
230 |
187
|
recnd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑡 ∈ ℂ ) |
231 |
189
|
recnd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( log ‘ 𝑥 ) ∈ ℂ ) |
232 |
230 231
|
mulneg2d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑡 · - ( log ‘ 𝑥 ) ) = - ( 𝑡 · ( log ‘ 𝑥 ) ) ) |
233 |
229 232
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑡 · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑥 ) ) = - ( 𝑡 · ( log ‘ 𝑥 ) ) ) |
234 |
|
fveq2 |
⊢ ( 𝑤 = 𝑦 → ( log ‘ 𝑤 ) = ( log ‘ 𝑦 ) ) |
235 |
234
|
negeqd |
⊢ ( 𝑤 = 𝑦 → - ( log ‘ 𝑤 ) = - ( log ‘ 𝑦 ) ) |
236 |
235 225 226
|
fvmpt3i |
⊢ ( 𝑦 ∈ ℝ+ → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑦 ) = - ( log ‘ 𝑦 ) ) |
237 |
194 236
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑦 ) = - ( log ‘ 𝑦 ) ) |
238 |
237
|
oveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 1 − 𝑡 ) · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑦 ) ) = ( ( 1 − 𝑡 ) · - ( log ‘ 𝑦 ) ) ) |
239 |
209
|
rpcnd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 − 𝑡 ) ∈ ℂ ) |
240 |
195
|
recnd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( log ‘ 𝑦 ) ∈ ℂ ) |
241 |
239 240
|
mulneg2d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 1 − 𝑡 ) · - ( log ‘ 𝑦 ) ) = - ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) |
242 |
238 241
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 1 − 𝑡 ) · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑦 ) ) = - ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) |
243 |
233 242
|
oveq12d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑡 · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑦 ) ) ) = ( - ( 𝑡 · ( log ‘ 𝑥 ) ) + - ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) ) |
244 |
190
|
recnd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑡 · ( log ‘ 𝑥 ) ) ∈ ℂ ) |
245 |
196
|
recnd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ∈ ℂ ) |
246 |
244 245
|
negdid |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → - ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) = ( - ( 𝑡 · ( log ‘ 𝑥 ) ) + - ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) ) |
247 |
243 246
|
eqtr4d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑡 · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑦 ) ) ) = - ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) ) |
248 |
215 222 247
|
3brtr4d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑦 ) ) ) ) |
249 |
164 168 177 248
|
scvxcvx |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( 𝑠 · 𝑢 ) + ( ( 1 − 𝑠 ) · 𝑣 ) ) ) ≤ ( ( 𝑠 · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑢 ) ) + ( ( 1 − 𝑠 ) · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑣 ) ) ) ) |
250 |
164 168 177 2 181 4 183 249
|
jensen |
⊢ ( 𝜑 → ( ( ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) / ( ℂfld Σg 𝑊 ) ) ∈ ℝ+ ∧ ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) / ( ℂfld Σg 𝑊 ) ) ) ≤ ( ( ℂfld Σg ( 𝑊 ∘f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) / ( ℂfld Σg 𝑊 ) ) ) ) |
251 |
250
|
simprd |
⊢ ( 𝜑 → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) / ( ℂfld Σg 𝑊 ) ) ) ≤ ( ( ℂfld Σg ( 𝑊 ∘f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) / ( ℂfld Σg 𝑊 ) ) ) |
252 |
6
|
oveq2d |
⊢ ( 𝜑 → ( ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) / ( ℂfld Σg 𝑊 ) ) = ( ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) / 1 ) ) |
253 |
252
|
fveq2d |
⊢ ( 𝜑 → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) / ( ℂfld Σg 𝑊 ) ) ) = ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) / 1 ) ) ) |
254 |
148
|
rpcnd |
⊢ ( 𝜑 → ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) ∈ ℂ ) |
255 |
254
|
div1d |
⊢ ( 𝜑 → ( ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) / 1 ) = ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) ) |
256 |
255
|
fveq2d |
⊢ ( 𝜑 → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) / 1 ) ) = ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) ) ) |
257 |
|
fveq2 |
⊢ ( 𝑤 = ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) → ( log ‘ 𝑤 ) = ( log ‘ ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) ) ) |
258 |
257
|
negeqd |
⊢ ( 𝑤 = ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) → - ( log ‘ 𝑤 ) = - ( log ‘ ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) ) ) |
259 |
258 225 226
|
fvmpt3i |
⊢ ( ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) ∈ ℝ+ → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) ) = - ( log ‘ ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) ) ) |
260 |
148 259
|
syl |
⊢ ( 𝜑 → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) ) = - ( log ‘ ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) ) ) |
261 |
139
|
fveq2d |
⊢ ( 𝜑 → ( log ‘ ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) ) = ( log ‘ ( ℂfld Σg ( 𝐹 ∘f · 𝑊 ) ) ) ) |
262 |
261
|
negeqd |
⊢ ( 𝜑 → - ( log ‘ ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) ) = - ( log ‘ ( ℂfld Σg ( 𝐹 ∘f · 𝑊 ) ) ) ) |
263 |
260 262
|
eqtrd |
⊢ ( 𝜑 → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) ) = - ( log ‘ ( ℂfld Σg ( 𝐹 ∘f · 𝑊 ) ) ) ) |
264 |
253 256 263
|
3eqtrd |
⊢ ( 𝜑 → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( ℂfld Σg ( 𝑊 ∘f · 𝐹 ) ) / ( ℂfld Σg 𝑊 ) ) ) = - ( log ‘ ( ℂfld Σg ( 𝐹 ∘f · 𝑊 ) ) ) ) |
265 |
6
|
oveq2d |
⊢ ( 𝜑 → ( ( ℂfld Σg ( 𝑊 ∘f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) / ( ℂfld Σg 𝑊 ) ) = ( ( ℂfld Σg ( 𝑊 ∘f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) / 1 ) ) |
266 |
|
ringmnd |
⊢ ( ℂfld ∈ Ring → ℂfld ∈ Mnd ) |
267 |
73 266
|
ax-mp |
⊢ ℂfld ∈ Mnd |
268 |
74
|
submid |
⊢ ( ℂfld ∈ Mnd → ℂ ∈ ( SubMnd ‘ ℂfld ) ) |
269 |
267 268
|
mp1i |
⊢ ( 𝜑 → ℂ ∈ ( SubMnd ‘ ℂfld ) ) |
270 |
|
mulcl |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ ) |
271 |
270
|
adantl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 · 𝑦 ) ∈ ℂ ) |
272 |
|
rpcn |
⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ ) |
273 |
272
|
ssriv |
⊢ ℝ+ ⊆ ℂ |
274 |
273
|
a1i |
⊢ ( 𝜑 → ℝ+ ⊆ ℂ ) |
275 |
5 274
|
fssd |
⊢ ( 𝜑 → 𝑊 : 𝐴 ⟶ ℂ ) |
276 |
166
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ( log ‘ 𝑤 ) ∈ ℂ ) |
277 |
276
|
negcld |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → - ( log ‘ 𝑤 ) ∈ ℂ ) |
278 |
277
|
fmpttd |
⊢ ( 𝜑 → ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) : ℝ+ ⟶ ℂ ) |
279 |
|
fco |
⊢ ( ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) : ℝ+ ⟶ ℂ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) : 𝐴 ⟶ ℂ ) |
280 |
278 4 279
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) : 𝐴 ⟶ ℂ ) |
281 |
271 275 280 2 2 51
|
off |
⊢ ( 𝜑 → ( 𝑊 ∘f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) : 𝐴 ⟶ ℂ ) |
282 |
281 2 161
|
fdmfifsupp |
⊢ ( 𝜑 → ( 𝑊 ∘f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) finSupp 0 ) |
283 |
75 152 2 269 281 282
|
gsumsubmcl |
⊢ ( 𝜑 → ( ℂfld Σg ( 𝑊 ∘f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) ∈ ℂ ) |
284 |
283
|
div1d |
⊢ ( 𝜑 → ( ( ℂfld Σg ( 𝑊 ∘f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) / 1 ) = ( ℂfld Σg ( 𝑊 ∘f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) ) |
285 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) = ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ) |
286 |
|
fveq2 |
⊢ ( 𝑤 = ( 𝐹 ‘ 𝑘 ) → ( log ‘ 𝑤 ) = ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) |
287 |
286
|
negeqd |
⊢ ( 𝑤 = ( 𝐹 ‘ 𝑘 ) → - ( log ‘ 𝑤 ) = - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) |
288 |
7 140 285 287
|
fmptco |
⊢ ( 𝜑 → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) = ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) |
289 |
288
|
oveq2d |
⊢ ( 𝜑 → ( 𝑊 ∘f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) = ( 𝑊 ∘f · ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) |
290 |
289
|
oveq2d |
⊢ ( 𝜑 → ( ℂfld Σg ( 𝑊 ∘f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) = ( ℂfld Σg ( 𝑊 ∘f · ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) |
291 |
265 284 290
|
3eqtrd |
⊢ ( 𝜑 → ( ( ℂfld Σg ( 𝑊 ∘f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) / ( ℂfld Σg 𝑊 ) ) = ( ℂfld Σg ( 𝑊 ∘f · ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) |
292 |
251 264 291
|
3brtr3d |
⊢ ( 𝜑 → - ( log ‘ ( ℂfld Σg ( 𝐹 ∘f · 𝑊 ) ) ) ≤ ( ℂfld Σg ( 𝑊 ∘f · ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) |
293 |
150 163 292
|
lenegcon1d |
⊢ ( 𝜑 → - ( ℂfld Σg ( 𝑊 ∘f · ( 𝑘 ∈ 𝐴 ↦ - ( log ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ≤ ( log ‘ ( ℂfld Σg ( 𝐹 ∘f · 𝑊 ) ) ) ) |
294 |
132 293
|
eqbrtrrd |
⊢ ( 𝜑 → ( log ‘ ( 𝑀 Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) ≤ ( log ‘ ( ℂfld Σg ( 𝐹 ∘f · 𝑊 ) ) ) ) |
295 |
129
|
relogcld |
⊢ ( 𝜑 → ( log ‘ ( 𝑀 Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) ∈ ℝ ) |
296 |
|
efle |
⊢ ( ( ( 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 150 296
|
syl2anc |
⊢ ( 𝜑 → ( ( log ‘ ( 𝑀 Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) ≤ ( log ‘ ( ℂfld Σg ( 𝐹 ∘f · 𝑊 ) ) ) ↔ ( exp ‘ ( log ‘ ( 𝑀 Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) ) ≤ ( exp ‘ ( log ‘ ( ℂfld Σg ( 𝐹 ∘f · 𝑊 ) ) ) ) ) ) |
298 |
294 297
|
mpbid |
⊢ ( 𝜑 → ( exp ‘ ( log ‘ ( 𝑀 Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) ) ≤ ( exp ‘ ( log ‘ ( ℂfld Σg ( 𝐹 ∘f · 𝑊 ) ) ) ) ) |
299 |
129
|
reeflogd |
⊢ ( 𝜑 → ( exp ‘ ( log ‘ ( 𝑀 Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) ) = ( 𝑀 Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) |
300 |
299
|
eqcomd |
⊢ ( 𝜑 → ( 𝑀 Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) = ( exp ‘ ( log ‘ ( 𝑀 Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ) ) ) |
301 |
149
|
reeflogd |
⊢ ( 𝜑 → ( exp ‘ ( log ‘ ( ℂfld Σg ( 𝐹 ∘f · 𝑊 ) ) ) ) = ( ℂfld Σg ( 𝐹 ∘f · 𝑊 ) ) ) |
302 |
301
|
eqcomd |
⊢ ( 𝜑 → ( ℂfld Σg ( 𝐹 ∘f · 𝑊 ) ) = ( exp ‘ ( log ‘ ( ℂfld Σg ( 𝐹 ∘f · 𝑊 ) ) ) ) ) |
303 |
298 300 302
|
3brtr4d |
⊢ ( 𝜑 → ( 𝑀 Σg ( 𝐹 ∘f ↑𝑐 𝑊 ) ) ≤ ( ℂfld Σg ( 𝐹 ∘f · 𝑊 ) ) ) |