Step | Hyp | Ref
| Expression |
1 | | cnfld0 20671 |
. . . . . . . 8
β’ 0 =
(0gββfld) |
2 | | cnring 20669 |
. . . . . . . . 9
β’
βfld β Ring |
3 | | ringabl 19868 |
. . . . . . . . 9
β’
(βfld β Ring β βfld β
Abel) |
4 | 2, 3 | mp1i 13 |
. . . . . . . 8
β’ (π β βfld
β Abel) |
5 | | amgm.2 |
. . . . . . . 8
β’ (π β π΄ β Fin) |
6 | | resubdrg 20862 |
. . . . . . . . . 10
β’ (β
β (SubRingββfld) β§ βfld β
DivRing) |
7 | 6 | simpli 485 |
. . . . . . . . 9
β’ β
β (SubRingββfld) |
8 | | subrgsubg 20079 |
. . . . . . . . 9
β’ (β
β (SubRingββfld) β β β
(SubGrpββfld)) |
9 | 7, 8 | mp1i 13 |
. . . . . . . 8
β’ (π β β β
(SubGrpββfld)) |
10 | | amgm.4 |
. . . . . . . . . . . 12
β’ (π β πΉ:π΄βΆβ+) |
11 | 10 | ffvelcdmda 6993 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β (πΉβπ) β
β+) |
12 | 11 | relogcld 25827 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β (logβ(πΉβπ)) β β) |
13 | 12 | renegcld 11452 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β -(logβ(πΉβπ)) β β) |
14 | 13 | fmpttd 7021 |
. . . . . . . 8
β’ (π β (π β π΄ β¦ -(logβ(πΉβπ))):π΄βΆβ) |
15 | | c0ex 11019 |
. . . . . . . . . 10
β’ 0 β
V |
16 | 15 | a1i 11 |
. . . . . . . . 9
β’ (π β 0 β
V) |
17 | 14, 5, 16 | fdmfifsupp 9186 |
. . . . . . . 8
β’ (π β (π β π΄ β¦ -(logβ(πΉβπ))) finSupp 0) |
18 | 1, 4, 5, 9, 14, 17 | gsumsubgcl 19570 |
. . . . . . 7
β’ (π β (βfld
Ξ£g (π β π΄ β¦ -(logβ(πΉβπ)))) β β) |
19 | 18 | recnd 11053 |
. . . . . 6
β’ (π β (βfld
Ξ£g (π β π΄ β¦ -(logβ(πΉβπ)))) β β) |
20 | | amgm.3 |
. . . . . . . 8
β’ (π β π΄ β β
) |
21 | | hashnncl 14130 |
. . . . . . . . 9
β’ (π΄ β Fin β
((β―βπ΄) β
β β π΄ β
β
)) |
22 | 5, 21 | syl 17 |
. . . . . . . 8
β’ (π β ((β―βπ΄) β β β π΄ β β
)) |
23 | 20, 22 | mpbird 257 |
. . . . . . 7
β’ (π β (β―βπ΄) β
β) |
24 | 23 | nncnd 12039 |
. . . . . 6
β’ (π β (β―βπ΄) β
β) |
25 | 23 | nnne0d 12073 |
. . . . . 6
β’ (π β (β―βπ΄) β 0) |
26 | 19, 24, 25 | divnegd 11814 |
. . . . 5
β’ (π β -((βfld
Ξ£g (π β π΄ β¦ -(logβ(πΉβπ)))) / (β―βπ΄)) = (-(βfld
Ξ£g (π β π΄ β¦ -(logβ(πΉβπ)))) / (β―βπ΄))) |
27 | 12 | recnd 11053 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β (logβ(πΉβπ)) β β) |
28 | 5, 27 | gsumfsum 20714 |
. . . . . . . . 9
β’ (π β (βfld
Ξ£g (π β π΄ β¦ (logβ(πΉβπ)))) = Ξ£π β π΄ (logβ(πΉβπ))) |
29 | 27 | negnegd 11373 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β --(logβ(πΉβπ)) = (logβ(πΉβπ))) |
30 | 29 | sumeq2dv 15464 |
. . . . . . . . 9
β’ (π β Ξ£π β π΄ --(logβ(πΉβπ)) = Ξ£π β π΄ (logβ(πΉβπ))) |
31 | 13 | recnd 11053 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β -(logβ(πΉβπ)) β β) |
32 | 5, 31 | fsumneg 15548 |
. . . . . . . . 9
β’ (π β Ξ£π β π΄ --(logβ(πΉβπ)) = -Ξ£π β π΄ -(logβ(πΉβπ))) |
33 | 28, 30, 32 | 3eqtr2rd 2783 |
. . . . . . . 8
β’ (π β -Ξ£π β π΄ -(logβ(πΉβπ)) = (βfld
Ξ£g (π β π΄ β¦ (logβ(πΉβπ))))) |
34 | 5, 31 | gsumfsum 20714 |
. . . . . . . . 9
β’ (π β (βfld
Ξ£g (π β π΄ β¦ -(logβ(πΉβπ)))) = Ξ£π β π΄ -(logβ(πΉβπ))) |
35 | 34 | negeqd 11265 |
. . . . . . . 8
β’ (π β -(βfld
Ξ£g (π β π΄ β¦ -(logβ(πΉβπ)))) = -Ξ£π β π΄ -(logβ(πΉβπ))) |
36 | 10 | feqmptd 6869 |
. . . . . . . . . 10
β’ (π β πΉ = (π β π΄ β¦ (πΉβπ))) |
37 | | relogf1o 25771 |
. . . . . . . . . . . . 13
β’ (log
βΎ β+):β+β1-1-ontoββ |
38 | | f1of 6746 |
. . . . . . . . . . . . 13
β’ ((log
βΎ β+):β+β1-1-ontoββ β (log βΎ
β+):β+βΆβ) |
39 | 37, 38 | mp1i 13 |
. . . . . . . . . . . 12
β’ (π β (log βΎ
β+):β+βΆβ) |
40 | 39 | feqmptd 6869 |
. . . . . . . . . . 11
β’ (π β (log βΎ
β+) = (π₯
β β+ β¦ ((log βΎ
β+)βπ₯))) |
41 | | fvres 6823 |
. . . . . . . . . . . 12
β’ (π₯ β β+
β ((log βΎ β+)βπ₯) = (logβπ₯)) |
42 | 41 | mpteq2ia 5184 |
. . . . . . . . . . 11
β’ (π₯ β β+
β¦ ((log βΎ β+)βπ₯)) = (π₯ β β+ β¦
(logβπ₯)) |
43 | 40, 42 | eqtrdi 2792 |
. . . . . . . . . 10
β’ (π β (log βΎ
β+) = (π₯
β β+ β¦ (logβπ₯))) |
44 | | fveq2 6804 |
. . . . . . . . . 10
β’ (π₯ = (πΉβπ) β (logβπ₯) = (logβ(πΉβπ))) |
45 | 11, 36, 43, 44 | fmptco 7033 |
. . . . . . . . 9
β’ (π β ((log βΎ
β+) β πΉ) = (π β π΄ β¦ (logβ(πΉβπ)))) |
46 | 45 | oveq2d 7323 |
. . . . . . . 8
β’ (π β (βfld
Ξ£g ((log βΎ β+) β πΉ)) = (βfld
Ξ£g (π β π΄ β¦ (logβ(πΉβπ))))) |
47 | 33, 35, 46 | 3eqtr4d 2786 |
. . . . . . 7
β’ (π β -(βfld
Ξ£g (π β π΄ β¦ -(logβ(πΉβπ)))) = (βfld
Ξ£g ((log βΎ β+) β πΉ))) |
48 | | amgm.1 |
. . . . . . . . . . . . . . 15
β’ π =
(mulGrpββfld) |
49 | 48 | oveq1i 7317 |
. . . . . . . . . . . . . 14
β’ (π βΎs (β
β {0})) = ((mulGrpββfld) βΎs
(β β {0})) |
50 | 49 | rpmsubg 20711 |
. . . . . . . . . . . . 13
β’
β+ β (SubGrpβ(π βΎs (β β
{0}))) |
51 | | subgsubm 18826 |
. . . . . . . . . . . . 13
β’
(β+ β (SubGrpβ(π βΎs (β β {0})))
β β+ β (SubMndβ(π βΎs (β β
{0})))) |
52 | 50, 51 | ax-mp 5 |
. . . . . . . . . . . 12
β’
β+ β (SubMndβ(π βΎs (β β
{0}))) |
53 | | cnfldbas 20650 |
. . . . . . . . . . . . . . 15
β’ β =
(Baseββfld) |
54 | | cndrng 20676 |
. . . . . . . . . . . . . . 15
β’
βfld β DivRing |
55 | 53, 1, 54 | drngui 20046 |
. . . . . . . . . . . . . 14
β’ (β
β {0}) = (Unitββfld) |
56 | 55, 48 | unitsubm 19961 |
. . . . . . . . . . . . 13
β’
(βfld β Ring β (β β {0}) β
(SubMndβπ)) |
57 | | eqid 2736 |
. . . . . . . . . . . . . 14
β’ (π βΎs (β
β {0})) = (π
βΎs (β β {0})) |
58 | 57 | subsubm 18504 |
. . . . . . . . . . . . 13
β’ ((β
β {0}) β (SubMndβπ) β (β+ β
(SubMndβ(π
βΎs (β β {0}))) β (β+ β
(SubMndβπ) β§
β+ β (β β {0})))) |
59 | 2, 56, 58 | mp2b 10 |
. . . . . . . . . . . 12
β’
(β+ β (SubMndβ(π βΎs (β β {0})))
β (β+ β (SubMndβπ) β§ β+ β (β
β {0}))) |
60 | 52, 59 | mpbi 229 |
. . . . . . . . . . 11
β’
(β+ β (SubMndβπ) β§ β+ β (β
β {0})) |
61 | 60 | simpli 485 |
. . . . . . . . . 10
β’
β+ β (SubMndβπ) |
62 | | eqid 2736 |
. . . . . . . . . . 11
β’ (π βΎs
β+) = (π
βΎs β+) |
63 | 62 | submbas 18502 |
. . . . . . . . . 10
β’
(β+ β (SubMndβπ) β β+ =
(Baseβ(π
βΎs β+))) |
64 | 61, 63 | ax-mp 5 |
. . . . . . . . 9
β’
β+ = (Baseβ(π βΎs
β+)) |
65 | | cnfld1 20672 |
. . . . . . . . . . . 12
β’ 1 =
(1rββfld) |
66 | 48, 65 | ringidval 19788 |
. . . . . . . . . . 11
β’ 1 =
(0gβπ) |
67 | 62, 66 | subm0 18503 |
. . . . . . . . . 10
β’
(β+ β (SubMndβπ) β 1 = (0gβ(π βΎs
β+))) |
68 | 61, 67 | ax-mp 5 |
. . . . . . . . 9
β’ 1 =
(0gβ(π
βΎs β+)) |
69 | | cncrng 20668 |
. . . . . . . . . . 11
β’
βfld β CRing |
70 | 48 | crngmgp 19840 |
. . . . . . . . . . 11
β’
(βfld β CRing β π β CMnd) |
71 | 69, 70 | mp1i 13 |
. . . . . . . . . 10
β’ (π β π β CMnd) |
72 | 62 | submmnd 18501 |
. . . . . . . . . . 11
β’
(β+ β (SubMndβπ) β (π βΎs β+)
β Mnd) |
73 | 61, 72 | mp1i 13 |
. . . . . . . . . 10
β’ (π β (π βΎs β+)
β Mnd) |
74 | 62 | subcmn 19487 |
. . . . . . . . . 10
β’ ((π β CMnd β§ (π βΎs
β+) β Mnd) β (π βΎs β+)
β CMnd) |
75 | 71, 73, 74 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π βΎs β+)
β CMnd) |
76 | | df-refld 20859 |
. . . . . . . . . . . 12
β’
βfld = (βfld βΎs
β) |
77 | 76 | subrgring 20076 |
. . . . . . . . . . 11
β’ (β
β (SubRingββfld) β βfld
β Ring) |
78 | 7, 77 | ax-mp 5 |
. . . . . . . . . 10
β’
βfld β Ring |
79 | | ringmnd 19842 |
. . . . . . . . . 10
β’
(βfld β Ring β βfld β
Mnd) |
80 | 78, 79 | mp1i 13 |
. . . . . . . . 9
β’ (π β βfld
β Mnd) |
81 | 48 | oveq1i 7317 |
. . . . . . . . . . . 12
β’ (π βΎs
β+) = ((mulGrpββfld)
βΎs β+) |
82 | 81 | reloggim 25803 |
. . . . . . . . . . 11
β’ (log
βΎ β+) β ((π βΎs β+)
GrpIso βfld) |
83 | | gimghm 18929 |
. . . . . . . . . . 11
β’ ((log
βΎ β+) β ((π βΎs β+)
GrpIso βfld) β (log βΎ β+) β
((π βΎs
β+) GrpHom βfld)) |
84 | 82, 83 | ax-mp 5 |
. . . . . . . . . 10
β’ (log
βΎ β+) β ((π βΎs β+)
GrpHom βfld) |
85 | | ghmmhm 18893 |
. . . . . . . . . 10
β’ ((log
βΎ β+) β ((π βΎs β+)
GrpHom βfld) β (log βΎ β+) β
((π βΎs
β+) MndHom βfld)) |
86 | 84, 85 | mp1i 13 |
. . . . . . . . 9
β’ (π β (log βΎ
β+) β ((π βΎs β+)
MndHom βfld)) |
87 | | 1ex 11021 |
. . . . . . . . . . 11
β’ 1 β
V |
88 | 87 | a1i 11 |
. . . . . . . . . 10
β’ (π β 1 β
V) |
89 | 10, 5, 88 | fdmfifsupp 9186 |
. . . . . . . . 9
β’ (π β πΉ finSupp 1) |
90 | 64, 68, 75, 80, 5, 86, 10, 89 | gsummhm 19588 |
. . . . . . . 8
β’ (π β (βfld
Ξ£g ((log βΎ β+) β πΉ)) = ((log βΎ
β+)β((π βΎs β+)
Ξ£g πΉ))) |
91 | | subgsubm 18826 |
. . . . . . . . . 10
β’ (β
β (SubGrpββfld) β β β
(SubMndββfld)) |
92 | 9, 91 | syl 17 |
. . . . . . . . 9
β’ (π β β β
(SubMndββfld)) |
93 | | fco 6654 |
. . . . . . . . . 10
β’ (((log
βΎ β+):β+βΆβ β§ πΉ:π΄βΆβ+) β ((log
βΎ β+) β πΉ):π΄βΆβ) |
94 | 39, 10, 93 | syl2anc 585 |
. . . . . . . . 9
β’ (π β ((log βΎ
β+) β πΉ):π΄βΆβ) |
95 | 5, 92, 94, 76 | gsumsubm 18522 |
. . . . . . . 8
β’ (π β (βfld
Ξ£g ((log βΎ β+) β πΉ)) = (βfld
Ξ£g ((log βΎ β+) β πΉ))) |
96 | 61 | a1i 11 |
. . . . . . . . . 10
β’ (π β β+ β
(SubMndβπ)) |
97 | 5, 96, 10, 62 | gsumsubm 18522 |
. . . . . . . . 9
β’ (π β (π Ξ£g πΉ) = ((π βΎs β+)
Ξ£g πΉ)) |
98 | 97 | fveq2d 6808 |
. . . . . . . 8
β’ (π β ((log βΎ
β+)β(π Ξ£g πΉ)) = ((log βΎ
β+)β((π βΎs β+)
Ξ£g πΉ))) |
99 | 90, 95, 98 | 3eqtr4d 2786 |
. . . . . . 7
β’ (π β (βfld
Ξ£g ((log βΎ β+) β πΉ)) = ((log βΎ
β+)β(π Ξ£g πΉ))) |
100 | 66, 71, 5, 96, 10, 89 | gsumsubmcl 19569 |
. . . . . . . 8
β’ (π β (π Ξ£g πΉ) β
β+) |
101 | 100 | fvresd 6824 |
. . . . . . 7
β’ (π β ((log βΎ
β+)β(π Ξ£g πΉ)) = (logβ(π Ξ£g
πΉ))) |
102 | 47, 99, 101 | 3eqtrd 2780 |
. . . . . 6
β’ (π β -(βfld
Ξ£g (π β π΄ β¦ -(logβ(πΉβπ)))) = (logβ(π Ξ£g πΉ))) |
103 | 102 | oveq1d 7322 |
. . . . 5
β’ (π β (-(βfld
Ξ£g (π β π΄ β¦ -(logβ(πΉβπ)))) / (β―βπ΄)) = ((logβ(π Ξ£g πΉ)) / (β―βπ΄))) |
104 | 100 | relogcld 25827 |
. . . . . . 7
β’ (π β (logβ(π Ξ£g
πΉ)) β
β) |
105 | 104 | recnd 11053 |
. . . . . 6
β’ (π β (logβ(π Ξ£g
πΉ)) β
β) |
106 | 105, 24, 25 | divrec2d 11805 |
. . . . 5
β’ (π β ((logβ(π Ξ£g
πΉ)) / (β―βπ΄)) = ((1 / (β―βπ΄)) Β· (logβ(π Ξ£g
πΉ)))) |
107 | 26, 103, 106 | 3eqtrd 2780 |
. . . 4
β’ (π β -((βfld
Ξ£g (π β π΄ β¦ -(logβ(πΉβπ)))) / (β―βπ΄)) = ((1 / (β―βπ΄)) Β· (logβ(π Ξ£g πΉ)))) |
108 | 36 | oveq2d 7323 |
. . . . . . . . 9
β’ (π β (βfld
Ξ£g πΉ) = (βfld
Ξ£g (π β π΄ β¦ (πΉβπ)))) |
109 | 11 | rpcnd 12824 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β (πΉβπ) β β) |
110 | 5, 109 | gsumfsum 20714 |
. . . . . . . . 9
β’ (π β (βfld
Ξ£g (π β π΄ β¦ (πΉβπ))) = Ξ£π β π΄ (πΉβπ)) |
111 | 108, 110 | eqtrd 2776 |
. . . . . . . 8
β’ (π β (βfld
Ξ£g πΉ) = Ξ£π β π΄ (πΉβπ)) |
112 | 5, 20, 11 | fsumrpcl 15498 |
. . . . . . . 8
β’ (π β Ξ£π β π΄ (πΉβπ) β
β+) |
113 | 111, 112 | eqeltrd 2837 |
. . . . . . 7
β’ (π β (βfld
Ξ£g πΉ) β
β+) |
114 | 23 | nnrpd 12820 |
. . . . . . 7
β’ (π β (β―βπ΄) β
β+) |
115 | 113, 114 | rpdivcld 12839 |
. . . . . 6
β’ (π β ((βfld
Ξ£g πΉ) / (β―βπ΄)) β
β+) |
116 | 115 | relogcld 25827 |
. . . . 5
β’ (π β
(logβ((βfld Ξ£g πΉ) / (β―βπ΄))) β β) |
117 | 18, 23 | nndivred 12077 |
. . . . 5
β’ (π β ((βfld
Ξ£g (π β π΄ β¦ -(logβ(πΉβπ)))) / (β―βπ΄)) β β) |
118 | | rpssre 12787 |
. . . . . . . . 9
β’
β+ β β |
119 | 118 | a1i 11 |
. . . . . . . 8
β’ (π β β+
β β) |
120 | | relogcl 25780 |
. . . . . . . . . . 11
β’ (π€ β β+
β (logβπ€) β
β) |
121 | 120 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π€ β β+) β
(logβπ€) β
β) |
122 | 121 | renegcld 11452 |
. . . . . . . . 9
β’ ((π β§ π€ β β+) β
-(logβπ€) β
β) |
123 | 122 | fmpttd 7021 |
. . . . . . . 8
β’ (π β (π€ β β+ β¦
-(logβπ€)):β+βΆβ) |
124 | | ioorp 13207 |
. . . . . . . . . . . 12
β’
(0(,)+β) = β+ |
125 | 124 | eleq2i 2828 |
. . . . . . . . . . 11
β’ (π β (0(,)+β) β
π β
β+) |
126 | 124 | eleq2i 2828 |
. . . . . . . . . . 11
β’ (π β (0(,)+β) β
π β
β+) |
127 | | iccssioo2 13202 |
. . . . . . . . . . 11
β’ ((π β (0(,)+β) β§
π β (0(,)+β))
β (π[,]π) β
(0(,)+β)) |
128 | 125, 126,
127 | syl2anbr 600 |
. . . . . . . . . 10
β’ ((π β β+
β§ π β
β+) β (π[,]π) β (0(,)+β)) |
129 | 128, 124 | sseqtrdi 3976 |
. . . . . . . . 9
β’ ((π β β+
β§ π β
β+) β (π[,]π) β
β+) |
130 | 129 | adantl 483 |
. . . . . . . 8
β’ ((π β§ (π β β+ β§ π β β+))
β (π[,]π) β
β+) |
131 | 23 | nnrecred 12074 |
. . . . . . . . . 10
β’ (π β (1 / (β―βπ΄)) β
β) |
132 | 114 | rpreccld 12832 |
. . . . . . . . . . 11
β’ (π β (1 / (β―βπ΄)) β
β+) |
133 | 132 | rpge0d 12826 |
. . . . . . . . . 10
β’ (π β 0 β€ (1 /
(β―βπ΄))) |
134 | | elrege0 13236 |
. . . . . . . . . 10
β’ ((1 /
(β―βπ΄)) β
(0[,)+β) β ((1 / (β―βπ΄)) β β β§ 0 β€ (1 /
(β―βπ΄)))) |
135 | 131, 133,
134 | sylanbrc 584 |
. . . . . . . . 9
β’ (π β (1 / (β―βπ΄)) β
(0[,)+β)) |
136 | | fconst6g 6693 |
. . . . . . . . 9
β’ ((1 /
(β―βπ΄)) β
(0[,)+β) β (π΄
Γ {(1 / (β―βπ΄))}):π΄βΆ(0[,)+β)) |
137 | 135, 136 | syl 17 |
. . . . . . . 8
β’ (π β (π΄ Γ {(1 / (β―βπ΄))}):π΄βΆ(0[,)+β)) |
138 | | 0lt1 11547 |
. . . . . . . . 9
β’ 0 <
1 |
139 | | fconstmpt 5660 |
. . . . . . . . . . 11
β’ (π΄ Γ {(1 /
(β―βπ΄))}) =
(π β π΄ β¦ (1 / (β―βπ΄))) |
140 | 139 | oveq2i 7318 |
. . . . . . . . . 10
β’
(βfld Ξ£g (π΄ Γ {(1 / (β―βπ΄))})) = (βfld
Ξ£g (π β π΄ β¦ (1 / (β―βπ΄)))) |
141 | | ringmnd 19842 |
. . . . . . . . . . . . 13
β’
(βfld β Ring β βfld β
Mnd) |
142 | 2, 141 | mp1i 13 |
. . . . . . . . . . . 12
β’ (π β βfld
β Mnd) |
143 | 131 | recnd 11053 |
. . . . . . . . . . . 12
β’ (π β (1 / (β―βπ΄)) β
β) |
144 | | eqid 2736 |
. . . . . . . . . . . . 13
β’
(.gββfld) =
(.gββfld) |
145 | 53, 144 | gsumconst 19584 |
. . . . . . . . . . . 12
β’
((βfld β Mnd β§ π΄ β Fin β§ (1 / (β―βπ΄)) β β) β
(βfld Ξ£g (π β π΄ β¦ (1 / (β―βπ΄)))) = ((β―βπ΄)(.gββfld)(1
/ (β―βπ΄)))) |
146 | 142, 5, 143, 145 | syl3anc 1371 |
. . . . . . . . . . 11
β’ (π β (βfld
Ξ£g (π β π΄ β¦ (1 / (β―βπ΄)))) = ((β―βπ΄)(.gββfld)(1
/ (β―βπ΄)))) |
147 | 23 | nnzd 12475 |
. . . . . . . . . . . 12
β’ (π β (β―βπ΄) β
β€) |
148 | | cnfldmulg 20679 |
. . . . . . . . . . . 12
β’
(((β―βπ΄)
β β€ β§ (1 / (β―βπ΄)) β β) β
((β―βπ΄)(.gββfld)(1
/ (β―βπ΄))) =
((β―βπ΄) Β·
(1 / (β―βπ΄)))) |
149 | 147, 143,
148 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β ((β―βπ΄)(.gββfld)(1
/ (β―βπ΄))) =
((β―βπ΄) Β·
(1 / (β―βπ΄)))) |
150 | 24, 25 | recidd 11796 |
. . . . . . . . . . 11
β’ (π β ((β―βπ΄) Β· (1 /
(β―βπ΄))) =
1) |
151 | 146, 149,
150 | 3eqtrd 2780 |
. . . . . . . . . 10
β’ (π β (βfld
Ξ£g (π β π΄ β¦ (1 / (β―βπ΄)))) = 1) |
152 | 140, 151 | eqtrid 2788 |
. . . . . . . . 9
β’ (π β (βfld
Ξ£g (π΄ Γ {(1 / (β―βπ΄))})) = 1) |
153 | 138, 152 | breqtrrid 5119 |
. . . . . . . 8
β’ (π β 0 <
(βfld Ξ£g (π΄ Γ {(1 / (β―βπ΄))}))) |
154 | | logccv 25867 |
. . . . . . . . . . . 12
β’ (((π₯ β β+
β§ π¦ β
β+ β§ π₯
< π¦) β§ π‘ β (0(,)1)) β ((π‘ Β· (logβπ₯)) + ((1 β π‘) Β· (logβπ¦))) < (logβ((π‘ Β· π₯) + ((1 β π‘) Β· π¦)))) |
155 | 154 | 3adant1 1130 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β ((π‘ Β· (logβπ₯)) + ((1 β π‘) Β· (logβπ¦))) < (logβ((π‘ Β· π₯) + ((1 β π‘) Β· π¦)))) |
156 | | ioossre 13190 |
. . . . . . . . . . . . . . 15
β’ (0(,)1)
β β |
157 | | simp3 1138 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β π‘ β (0(,)1)) |
158 | 156, 157 | sselid 3924 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β π‘ β β) |
159 | | simp21 1206 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β π₯ β β+) |
160 | 159 | relogcld 25827 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β (logβπ₯) β
β) |
161 | 158, 160 | remulcld 11055 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β (π‘ Β· (logβπ₯)) β β) |
162 | | 1re 11025 |
. . . . . . . . . . . . . . 15
β’ 1 β
β |
163 | | resubcl 11335 |
. . . . . . . . . . . . . . 15
β’ ((1
β β β§ π‘
β β) β (1 β π‘) β β) |
164 | 162, 158,
163 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β (1 β π‘) β
β) |
165 | | simp22 1207 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β π¦ β β+) |
166 | 165 | relogcld 25827 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β (logβπ¦) β
β) |
167 | 164, 166 | remulcld 11055 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β ((1 β π‘) Β· (logβπ¦)) β
β) |
168 | 161, 167 | readdcld 11054 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β ((π‘ Β· (logβπ₯)) + ((1 β π‘) Β· (logβπ¦))) β β) |
169 | | simp1 1136 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β π) |
170 | | ioossicc 13215 |
. . . . . . . . . . . . . . 15
β’ (0(,)1)
β (0[,]1) |
171 | 170, 157 | sselid 3924 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β π‘ β (0[,]1)) |
172 | 119, 130 | cvxcl 26183 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π‘ β (0[,]1)))
β ((π‘ Β· π₯) + ((1 β π‘) Β· π¦)) β
β+) |
173 | 169, 159,
165, 171, 172 | syl13anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β ((π‘ Β· π₯) + ((1 β π‘) Β· π¦)) β
β+) |
174 | 173 | relogcld 25827 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β (logβ((π‘ Β· π₯) + ((1 β π‘) Β· π¦))) β β) |
175 | 168, 174 | ltnegd 11603 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β (((π‘ Β· (logβπ₯)) + ((1 β π‘) Β· (logβπ¦))) < (logβ((π‘ Β· π₯) + ((1 β π‘) Β· π¦))) β -(logβ((π‘ Β· π₯) + ((1 β π‘) Β· π¦))) < -((π‘ Β· (logβπ₯)) + ((1 β π‘) Β· (logβπ¦))))) |
176 | 155, 175 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β -(logβ((π‘ Β· π₯) + ((1 β π‘) Β· π¦))) < -((π‘ Β· (logβπ₯)) + ((1 β π‘) Β· (logβπ¦)))) |
177 | | fveq2 6804 |
. . . . . . . . . . . . 13
β’ (π€ = ((π‘ Β· π₯) + ((1 β π‘) Β· π¦)) β (logβπ€) = (logβ((π‘ Β· π₯) + ((1 β π‘) Β· π¦)))) |
178 | 177 | negeqd 11265 |
. . . . . . . . . . . 12
β’ (π€ = ((π‘ Β· π₯) + ((1 β π‘) Β· π¦)) β -(logβπ€) = -(logβ((π‘ Β· π₯) + ((1 β π‘) Β· π¦)))) |
179 | | eqid 2736 |
. . . . . . . . . . . 12
β’ (π€ β β+
β¦ -(logβπ€)) =
(π€ β
β+ β¦ -(logβπ€)) |
180 | | negex 11269 |
. . . . . . . . . . . 12
β’
-(logβ((π‘
Β· π₯) + ((1 β
π‘) Β· π¦))) β V |
181 | 178, 179,
180 | fvmpt 6907 |
. . . . . . . . . . 11
β’ (((π‘ Β· π₯) + ((1 β π‘) Β· π¦)) β β+ β ((π€ β β+
β¦ -(logβπ€))β((π‘ Β· π₯) + ((1 β π‘) Β· π¦))) = -(logβ((π‘ Β· π₯) + ((1 β π‘) Β· π¦)))) |
182 | 173, 181 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β ((π€ β β+ β¦
-(logβπ€))β((π‘ Β· π₯) + ((1 β π‘) Β· π¦))) = -(logβ((π‘ Β· π₯) + ((1 β π‘) Β· π¦)))) |
183 | | fveq2 6804 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = π₯ β (logβπ€) = (logβπ₯)) |
184 | 183 | negeqd 11265 |
. . . . . . . . . . . . . . . 16
β’ (π€ = π₯ β -(logβπ€) = -(logβπ₯)) |
185 | | negex 11269 |
. . . . . . . . . . . . . . . 16
β’
-(logβπ₯)
β V |
186 | 184, 179,
185 | fvmpt 6907 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β+
β ((π€ β
β+ β¦ -(logβπ€))βπ₯) = -(logβπ₯)) |
187 | 159, 186 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β ((π€ β β+ β¦
-(logβπ€))βπ₯) = -(logβπ₯)) |
188 | 187 | oveq2d 7323 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β (π‘ Β· ((π€ β β+ β¦
-(logβπ€))βπ₯)) = (π‘ Β· -(logβπ₯))) |
189 | 158 | recnd 11053 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β π‘ β β) |
190 | 160 | recnd 11053 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β (logβπ₯) β
β) |
191 | 189, 190 | mulneg2d 11479 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β (π‘ Β· -(logβπ₯)) = -(π‘ Β· (logβπ₯))) |
192 | 188, 191 | eqtrd 2776 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β (π‘ Β· ((π€ β β+ β¦
-(logβπ€))βπ₯)) = -(π‘ Β· (logβπ₯))) |
193 | | fveq2 6804 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = π¦ β (logβπ€) = (logβπ¦)) |
194 | 193 | negeqd 11265 |
. . . . . . . . . . . . . . . 16
β’ (π€ = π¦ β -(logβπ€) = -(logβπ¦)) |
195 | | negex 11269 |
. . . . . . . . . . . . . . . 16
β’
-(logβπ¦)
β V |
196 | 194, 179,
195 | fvmpt 6907 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β+
β ((π€ β
β+ β¦ -(logβπ€))βπ¦) = -(logβπ¦)) |
197 | 165, 196 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β ((π€ β β+ β¦
-(logβπ€))βπ¦) = -(logβπ¦)) |
198 | 197 | oveq2d 7323 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β ((1 β π‘) Β· ((π€ β β+ β¦
-(logβπ€))βπ¦)) = ((1 β π‘) Β· -(logβπ¦))) |
199 | 164 | recnd 11053 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β (1 β π‘) β
β) |
200 | 166 | recnd 11053 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β (logβπ¦) β
β) |
201 | 199, 200 | mulneg2d 11479 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β ((1 β π‘) Β· -(logβπ¦)) = -((1 β π‘) Β· (logβπ¦))) |
202 | 198, 201 | eqtrd 2776 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β ((1 β π‘) Β· ((π€ β β+ β¦
-(logβπ€))βπ¦)) = -((1 β π‘) Β· (logβπ¦))) |
203 | 192, 202 | oveq12d 7325 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β ((π‘ Β· ((π€ β β+ β¦
-(logβπ€))βπ₯)) + ((1 β π‘) Β· ((π€ β β+ β¦
-(logβπ€))βπ¦))) = (-(π‘ Β· (logβπ₯)) + -((1 β π‘) Β· (logβπ¦)))) |
204 | 161 | recnd 11053 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β (π‘ Β· (logβπ₯)) β β) |
205 | 167 | recnd 11053 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β ((1 β π‘) Β· (logβπ¦)) β
β) |
206 | 204, 205 | negdid 11395 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β -((π‘ Β· (logβπ₯)) + ((1 β π‘) Β· (logβπ¦))) = (-(π‘ Β· (logβπ₯)) + -((1 β π‘) Β· (logβπ¦)))) |
207 | 203, 206 | eqtr4d 2779 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β ((π‘ Β· ((π€ β β+ β¦
-(logβπ€))βπ₯)) + ((1 β π‘) Β· ((π€ β β+ β¦
-(logβπ€))βπ¦))) = -((π‘ Β· (logβπ₯)) + ((1 β π‘) Β· (logβπ¦)))) |
208 | 176, 182,
207 | 3brtr4d 5113 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β+ β§ π¦ β β+
β§ π₯ < π¦) β§ π‘ β (0(,)1)) β ((π€ β β+ β¦
-(logβπ€))β((π‘ Β· π₯) + ((1 β π‘) Β· π¦))) < ((π‘ Β· ((π€ β β+ β¦
-(logβπ€))βπ₯)) + ((1 β π‘) Β· ((π€ β β+ β¦
-(logβπ€))βπ¦)))) |
209 | 119, 123,
130, 208 | scvxcvx 26184 |
. . . . . . . 8
β’ ((π β§ (π’ β β+ β§ π£ β β+
β§ π β (0[,]1)))
β ((π€ β
β+ β¦ -(logβπ€))β((π Β· π’) + ((1 β π ) Β· π£))) β€ ((π Β· ((π€ β β+ β¦
-(logβπ€))βπ’)) + ((1 β π ) Β· ((π€ β β+ β¦
-(logβπ€))βπ£)))) |
210 | 119, 123,
130, 5, 137, 10, 153, 209 | jensen 26187 |
. . . . . . 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 497 |
. . . . . 6
β’ (π β ((π€ β β+ β¦
-(logβπ€))β((βfld
Ξ£g ((π΄ Γ {(1 / (β―βπ΄))}) βf
Β· πΉ)) /
(βfld Ξ£g (π΄ Γ {(1 / (β―βπ΄))})))) β€
((βfld Ξ£g ((π΄ Γ {(1 / (β―βπ΄))}) βf
Β· ((π€ β
β+ β¦ -(logβπ€)) β πΉ))) / (βfld
Ξ£g (π΄ Γ {(1 / (β―βπ΄))})))) |
212 | 131 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΄) β (1 / (β―βπ΄)) β
β) |
213 | 139 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β (π΄ Γ {(1 / (β―βπ΄))}) = (π β π΄ β¦ (1 / (β―βπ΄)))) |
214 | 5, 212, 11, 213, 36 | offval2 7585 |
. . . . . . . . . . . 12
β’ (π β ((π΄ Γ {(1 / (β―βπ΄))}) βf
Β· πΉ) = (π β π΄ β¦ ((1 / (β―βπ΄)) Β· (πΉβπ)))) |
215 | 214 | oveq2d 7323 |
. . . . . . . . . . 11
β’ (π β (βfld
Ξ£g ((π΄ Γ {(1 / (β―βπ΄))}) βf
Β· πΉ)) =
(βfld Ξ£g (π β π΄ β¦ ((1 / (β―βπ΄)) Β· (πΉβπ))))) |
216 | | cnfldadd 20651 |
. . . . . . . . . . . 12
β’ + =
(+gββfld) |
217 | | cnfldmul 20652 |
. . . . . . . . . . . 12
β’ Β·
= (.rββfld) |
218 | 2 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β βfld
β Ring) |
219 | 109 | fmpttd 7021 |
. . . . . . . . . . . . 13
β’ (π β (π β π΄ β¦ (πΉβπ)):π΄βΆβ) |
220 | 219, 5, 16 | fdmfifsupp 9186 |
. . . . . . . . . . . 12
β’ (π β (π β π΄ β¦ (πΉβπ)) finSupp 0) |
221 | 53, 1, 216, 217, 218, 5, 143, 109, 220 | gsummulc2 19895 |
. . . . . . . . . . 11
β’ (π β (βfld
Ξ£g (π β π΄ β¦ ((1 / (β―βπ΄)) Β· (πΉβπ)))) = ((1 / (β―βπ΄)) Β· (βfld
Ξ£g (π β π΄ β¦ (πΉβπ))))) |
222 | | fss 6647 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ:π΄βΆβ+ β§
β+ β β) β πΉ:π΄βΆβ) |
223 | 10, 118, 222 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ:π΄βΆβ) |
224 | 10, 5, 16 | fdmfifsupp 9186 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ finSupp 0) |
225 | 1, 4, 5, 9, 223, 224 | gsumsubgcl 19570 |
. . . . . . . . . . . . . 14
β’ (π β (βfld
Ξ£g πΉ) β β) |
226 | 225 | recnd 11053 |
. . . . . . . . . . . . 13
β’ (π β (βfld
Ξ£g πΉ) β β) |
227 | 226, 24, 25 | divrec2d 11805 |
. . . . . . . . . . . 12
β’ (π β ((βfld
Ξ£g πΉ) / (β―βπ΄)) = ((1 / (β―βπ΄)) Β· (βfld
Ξ£g πΉ))) |
228 | 108 | oveq2d 7323 |
. . . . . . . . . . . 12
β’ (π β ((1 / (β―βπ΄)) Β·
(βfld Ξ£g πΉ)) = ((1 / (β―βπ΄)) Β· (βfld
Ξ£g (π β π΄ β¦ (πΉβπ))))) |
229 | 227, 228 | eqtr2d 2777 |
. . . . . . . . . . 11
β’ (π β ((1 / (β―βπ΄)) Β·
(βfld Ξ£g (π β π΄ β¦ (πΉβπ)))) = ((βfld
Ξ£g πΉ) / (β―βπ΄))) |
230 | 215, 221,
229 | 3eqtrd 2780 |
. . . . . . . . . 10
β’ (π β (βfld
Ξ£g ((π΄ Γ {(1 / (β―βπ΄))}) βf
Β· πΉ)) =
((βfld Ξ£g πΉ) / (β―βπ΄))) |
231 | 230, 152 | oveq12d 7325 |
. . . . . . . . 9
β’ (π β ((βfld
Ξ£g ((π΄ Γ {(1 / (β―βπ΄))}) βf
Β· πΉ)) /
(βfld Ξ£g (π΄ Γ {(1 / (β―βπ΄))}))) =
(((βfld Ξ£g πΉ) / (β―βπ΄)) / 1)) |
232 | 225, 23 | nndivred 12077 |
. . . . . . . . . . 11
β’ (π β ((βfld
Ξ£g πΉ) / (β―βπ΄)) β β) |
233 | 232 | recnd 11053 |
. . . . . . . . . 10
β’ (π β ((βfld
Ξ£g πΉ) / (β―βπ΄)) β β) |
234 | 233 | div1d 11793 |
. . . . . . . . 9
β’ (π β (((βfld
Ξ£g πΉ) / (β―βπ΄)) / 1) = ((βfld
Ξ£g πΉ) / (β―βπ΄))) |
235 | 231, 234 | eqtrd 2776 |
. . . . . . . 8
β’ (π β ((βfld
Ξ£g ((π΄ Γ {(1 / (β―βπ΄))}) βf
Β· πΉ)) /
(βfld Ξ£g (π΄ Γ {(1 / (β―βπ΄))}))) = ((βfld
Ξ£g πΉ) / (β―βπ΄))) |
236 | 235 | fveq2d 6808 |
. . . . . . 7
β’ (π β ((π€ β β+ β¦
-(logβπ€))β((βfld
Ξ£g ((π΄ Γ {(1 / (β―βπ΄))}) βf
Β· πΉ)) /
(βfld Ξ£g (π΄ Γ {(1 / (β―βπ΄))})))) = ((π€ β β+ β¦
-(logβπ€))β((βfld
Ξ£g πΉ) / (β―βπ΄)))) |
237 | | fveq2 6804 |
. . . . . . . . . 10
β’ (π€ = ((βfld
Ξ£g πΉ) / (β―βπ΄)) β (logβπ€) = (logβ((βfld
Ξ£g πΉ) / (β―βπ΄)))) |
238 | 237 | negeqd 11265 |
. . . . . . . . 9
β’ (π€ = ((βfld
Ξ£g πΉ) / (β―βπ΄)) β -(logβπ€) = -(logβ((βfld
Ξ£g πΉ) / (β―βπ΄)))) |
239 | | negex 11269 |
. . . . . . . . 9
β’
-(logβ((βfld Ξ£g πΉ) / (β―βπ΄))) β V |
240 | 238, 179,
239 | fvmpt 6907 |
. . . . . . . 8
β’
(((βfld Ξ£g πΉ) / (β―βπ΄)) β β+ β ((π€ β β+
β¦ -(logβπ€))β((βfld
Ξ£g πΉ) / (β―βπ΄))) = -(logβ((βfld
Ξ£g πΉ) / (β―βπ΄)))) |
241 | 115, 240 | syl 17 |
. . . . . . 7
β’ (π β ((π€ β β+ β¦
-(logβπ€))β((βfld
Ξ£g πΉ) / (β―βπ΄))) = -(logβ((βfld
Ξ£g πΉ) / (β―βπ΄)))) |
242 | 236, 241 | eqtrd 2776 |
. . . . . 6
β’ (π β ((π€ β β+ β¦
-(logβπ€))β((βfld
Ξ£g ((π΄ Γ {(1 / (β―βπ΄))}) βf
Β· πΉ)) /
(βfld Ξ£g (π΄ Γ {(1 / (β―βπ΄))})))) =
-(logβ((βfld Ξ£g πΉ) / (β―βπ΄)))) |
243 | 53, 1, 216, 217, 218, 5, 143, 31, 17 | gsummulc2 19895 |
. . . . . . . . 9
β’ (π β (βfld
Ξ£g (π β π΄ β¦ ((1 / (β―βπ΄)) Β· -(logβ(πΉβπ))))) = ((1 / (β―βπ΄)) Β·
(βfld Ξ£g (π β π΄ β¦ -(logβ(πΉβπ)))))) |
244 | | negex 11269 |
. . . . . . . . . . . 12
β’
-(logβ(πΉβπ)) β V |
245 | 244 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β -(logβ(πΉβπ)) β V) |
246 | | eqidd 2737 |
. . . . . . . . . . . 12
β’ (π β (π€ β β+ β¦
-(logβπ€)) = (π€ β β+
β¦ -(logβπ€))) |
247 | | fveq2 6804 |
. . . . . . . . . . . . 13
β’ (π€ = (πΉβπ) β (logβπ€) = (logβ(πΉβπ))) |
248 | 247 | negeqd 11265 |
. . . . . . . . . . . 12
β’ (π€ = (πΉβπ) β -(logβπ€) = -(logβ(πΉβπ))) |
249 | 11, 36, 246, 248 | fmptco 7033 |
. . . . . . . . . . 11
β’ (π β ((π€ β β+ β¦
-(logβπ€)) β
πΉ) = (π β π΄ β¦ -(logβ(πΉβπ)))) |
250 | 5, 212, 245, 213, 249 | offval2 7585 |
. . . . . . . . . 10
β’ (π β ((π΄ Γ {(1 / (β―βπ΄))}) βf
Β· ((π€ β
β+ β¦ -(logβπ€)) β πΉ)) = (π β π΄ β¦ ((1 / (β―βπ΄)) Β· -(logβ(πΉβπ))))) |
251 | 250 | oveq2d 7323 |
. . . . . . . . 9
β’ (π β (βfld
Ξ£g ((π΄ Γ {(1 / (β―βπ΄))}) βf
Β· ((π€ β
β+ β¦ -(logβπ€)) β πΉ))) = (βfld
Ξ£g (π β π΄ β¦ ((1 / (β―βπ΄)) Β· -(logβ(πΉβπ)))))) |
252 | 19, 24, 25 | divrec2d 11805 |
. . . . . . . . 9
β’ (π β ((βfld
Ξ£g (π β π΄ β¦ -(logβ(πΉβπ)))) / (β―βπ΄)) = ((1 / (β―βπ΄)) Β· (βfld
Ξ£g (π β π΄ β¦ -(logβ(πΉβπ)))))) |
253 | 243, 251,
252 | 3eqtr4d 2786 |
. . . . . . . 8
β’ (π β (βfld
Ξ£g ((π΄ Γ {(1 / (β―βπ΄))}) βf
Β· ((π€ β
β+ β¦ -(logβπ€)) β πΉ))) = ((βfld
Ξ£g (π β π΄ β¦ -(logβ(πΉβπ)))) / (β―βπ΄))) |
254 | 253, 152 | oveq12d 7325 |
. . . . . . 7
β’ (π β ((βfld
Ξ£g ((π΄ Γ {(1 / (β―βπ΄))}) βf
Β· ((π€ β
β+ β¦ -(logβπ€)) β πΉ))) / (βfld
Ξ£g (π΄ Γ {(1 / (β―βπ΄))}))) =
(((βfld Ξ£g (π β π΄ β¦ -(logβ(πΉβπ)))) / (β―βπ΄)) / 1)) |
255 | 117 | recnd 11053 |
. . . . . . . 8
β’ (π β ((βfld
Ξ£g (π β π΄ β¦ -(logβ(πΉβπ)))) / (β―βπ΄)) β β) |
256 | 255 | div1d 11793 |
. . . . . . 7
β’ (π β (((βfld
Ξ£g (π β π΄ β¦ -(logβ(πΉβπ)))) / (β―βπ΄)) / 1) = ((βfld
Ξ£g (π β π΄ β¦ -(logβ(πΉβπ)))) / (β―βπ΄))) |
257 | 254, 256 | eqtrd 2776 |
. . . . . 6
β’ (π β ((βfld
Ξ£g ((π΄ Γ {(1 / (β―βπ΄))}) βf
Β· ((π€ β
β+ β¦ -(logβπ€)) β πΉ))) / (βfld
Ξ£g (π΄ Γ {(1 / (β―βπ΄))}))) = ((βfld
Ξ£g (π β π΄ β¦ -(logβ(πΉβπ)))) / (β―βπ΄))) |
258 | 211, 242,
257 | 3brtr3d 5112 |
. . . . 5
β’ (π β
-(logβ((βfld Ξ£g πΉ) / (β―βπ΄))) β€ ((βfld
Ξ£g (π β π΄ β¦ -(logβ(πΉβπ)))) / (β―βπ΄))) |
259 | 116, 117,
258 | lenegcon1d 11607 |
. . . 4
β’ (π β -((βfld
Ξ£g (π β π΄ β¦ -(logβ(πΉβπ)))) / (β―βπ΄)) β€ (logβ((βfld
Ξ£g πΉ) / (β―βπ΄)))) |
260 | 107, 259 | eqbrtrrd 5105 |
. . 3
β’ (π β ((1 / (β―βπ΄)) Β· (logβ(π Ξ£g
πΉ))) β€
(logβ((βfld Ξ£g πΉ) / (β―βπ΄)))) |
261 | 131, 104 | remulcld 11055 |
. . . 4
β’ (π β ((1 / (β―βπ΄)) Β· (logβ(π Ξ£g
πΉ))) β
β) |
262 | | efle 15876 |
. . . 4
β’ ((((1 /
(β―βπ΄)) Β·
(logβ(π
Ξ£g πΉ))) β β β§
(logβ((βfld Ξ£g πΉ) / (β―βπ΄))) β β) β (((1 /
(β―βπ΄)) Β·
(logβ(π
Ξ£g πΉ))) β€ (logβ((βfld
Ξ£g πΉ) / (β―βπ΄))) β (expβ((1 /
(β―βπ΄)) Β·
(logβ(π
Ξ£g πΉ)))) β€
(expβ(logβ((βfld Ξ£g πΉ) / (β―βπ΄)))))) |
263 | 261, 116,
262 | syl2anc 585 |
. . 3
β’ (π β (((1 /
(β―βπ΄)) Β·
(logβ(π
Ξ£g πΉ))) β€ (logβ((βfld
Ξ£g πΉ) / (β―βπ΄))) β (expβ((1 /
(β―βπ΄)) Β·
(logβ(π
Ξ£g πΉ)))) β€
(expβ(logβ((βfld Ξ£g πΉ) / (β―βπ΄)))))) |
264 | 260, 263 | mpbid 231 |
. 2
β’ (π β (expβ((1 /
(β―βπ΄)) Β·
(logβ(π
Ξ£g πΉ)))) β€
(expβ(logβ((βfld Ξ£g πΉ) / (β―βπ΄))))) |
265 | 100 | rpcnd 12824 |
. . 3
β’ (π β (π Ξ£g πΉ) β
β) |
266 | 100 | rpne0d 12827 |
. . 3
β’ (π β (π Ξ£g πΉ) β 0) |
267 | 265, 266,
143 | cxpefd 25916 |
. 2
β’ (π β ((π Ξ£g πΉ)βπ(1 /
(β―βπ΄))) =
(expβ((1 / (β―βπ΄)) Β· (logβ(π Ξ£g πΉ))))) |
268 | 115 | reeflogd 25828 |
. . 3
β’ (π β
(expβ(logβ((βfld Ξ£g πΉ) / (β―βπ΄)))) = ((βfld
Ξ£g πΉ) / (β―βπ΄))) |
269 | 268 | eqcomd 2742 |
. 2
β’ (π β ((βfld
Ξ£g πΉ) / (β―βπ΄)) =
(expβ(logβ((βfld Ξ£g πΉ) / (β―βπ΄))))) |
270 | 264, 267,
269 | 3brtr4d 5113 |
1
β’ (π β ((π Ξ£g πΉ)βπ(1 /
(β―βπ΄))) β€
((βfld Ξ£g πΉ) / (β―βπ΄))) |