Step | Hyp | Ref
| Expression |
1 | | simpl1 1191 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐴 ∈
ℝ+) |
2 | 1 | rpred 12957 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐴 ∈
ℝ) |
3 | | simpl2 1192 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐵 ∈
ℝ+) |
4 | 3 | rpred 12957 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐵 ∈
ℝ) |
5 | | simpl3 1193 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐴 < 𝐵) |
6 | 1 | rpgt0d 12960 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 0 <
𝐴) |
7 | 4 | ltpnfd 13042 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐵 < +∞) |
8 | | 0xr 11202 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ* |
9 | | pnfxr 11209 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
10 | | iccssioo 13333 |
. . . . . . . . . . . 12
⊢ (((0
∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (0
< 𝐴 ∧ 𝐵 < +∞)) → (𝐴[,]𝐵) ⊆ (0(,)+∞)) |
11 | 8, 9, 10 | mpanl12 700 |
. . . . . . . . . . 11
⊢ ((0 <
𝐴 ∧ 𝐵 < +∞) → (𝐴[,]𝐵) ⊆ (0(,)+∞)) |
12 | 6, 7, 11 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝐴[,]𝐵) ⊆ (0(,)+∞)) |
13 | | ioorp 13342 |
. . . . . . . . . 10
⊢
(0(,)+∞) = ℝ+ |
14 | 12, 13 | sseqtrdi 3994 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝐴[,]𝐵) ⊆
ℝ+) |
15 | 14 | sselda 3944 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ+) |
16 | 15 | relogcld 25978 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (log‘𝑥) ∈ ℝ) |
17 | 16 | renegcld 11582 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → -(log‘𝑥) ∈ ℝ) |
18 | 17 | fmpttd 7063 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)):(𝐴[,]𝐵)⟶ℝ) |
19 | | ax-resscn 11108 |
. . . . . 6
⊢ ℝ
⊆ ℂ |
20 | 14 | resabs1d 5968 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((log
↾ ℝ+) ↾ (𝐴[,]𝐵)) = (log ↾ (𝐴[,]𝐵))) |
21 | | ssid 3966 |
. . . . . . . . . . 11
⊢ ℂ
⊆ ℂ |
22 | | cncfss 24262 |
. . . . . . . . . . 11
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) →
(ℝ+–cn→ℝ) ⊆
(ℝ+–cn→ℂ)) |
23 | 19, 21, 22 | mp2an 690 |
. . . . . . . . . 10
⊢
(ℝ+–cn→ℝ) ⊆
(ℝ+–cn→ℂ) |
24 | | relogcn 25993 |
. . . . . . . . . 10
⊢ (log
↾ ℝ+) ∈ (ℝ+–cn→ℝ) |
25 | 23, 24 | sselii 3941 |
. . . . . . . . 9
⊢ (log
↾ ℝ+) ∈ (ℝ+–cn→ℂ) |
26 | | rescncf 24260 |
. . . . . . . . 9
⊢ ((𝐴[,]𝐵) ⊆ ℝ+ → ((log
↾ ℝ+) ∈ (ℝ+–cn→ℂ) → ((log ↾
ℝ+) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ))) |
27 | 14, 25, 26 | mpisyl 21 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((log
↾ ℝ+) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
28 | 20, 27 | eqeltrrd 2839 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (log
↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
29 | | fvres 6861 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((log ↾ (𝐴[,]𝐵))‘𝑥) = (log‘𝑥)) |
30 | 29 | negeqd 11395 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴[,]𝐵) → -((log ↾ (𝐴[,]𝐵))‘𝑥) = -(log‘𝑥)) |
31 | 30 | mpteq2ia 5208 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ -((log ↾ (𝐴[,]𝐵))‘𝑥)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) |
32 | 31 | eqcomi 2745 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ -((log ↾ (𝐴[,]𝐵))‘𝑥)) |
33 | 32 | negfcncf 24286 |
. . . . . . 7
⊢ ((log
↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
34 | 28, 33 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
35 | | cncfcdm 24261 |
. . . . . 6
⊢ ((ℝ
⊆ ℂ ∧ (𝑥
∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℝ) ↔ (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)):(𝐴[,]𝐵)⟶ℝ)) |
36 | 19, 34, 35 | sylancr 587 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℝ) ↔ (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)):(𝐴[,]𝐵)⟶ℝ)) |
37 | 18, 36 | mpbird 256 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
38 | | ioossre 13325 |
. . . . . . . 8
⊢ (𝐴(,)𝐵) ⊆ ℝ |
39 | | ltso 11235 |
. . . . . . . 8
⊢ < Or
ℝ |
40 | | soss 5565 |
. . . . . . . 8
⊢ ((𝐴(,)𝐵) ⊆ ℝ → ( < Or ℝ
→ < Or (𝐴(,)𝐵))) |
41 | 38, 39, 40 | mp2 9 |
. . . . . . 7
⊢ < Or
(𝐴(,)𝐵) |
42 | 41 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → < Or
(𝐴(,)𝐵)) |
43 | | ioossicc 13350 |
. . . . . . . . . . . . . 14
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
44 | 43, 14 | sstrid 3955 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝐴(,)𝐵) ⊆
ℝ+) |
45 | 44 | sselda 3944 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℝ+) |
46 | 45 | rprecred 12968 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (1 / 𝑥) ∈ ℝ) |
47 | 46 | renegcld 11582 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ (𝐴(,)𝐵)) → -(1 / 𝑥) ∈ ℝ) |
48 | 47 | fmpttd 7063 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)):(𝐴(,)𝐵)⟶ℝ) |
49 | 48 | frnd 6676 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ran
(𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) ⊆ ℝ) |
50 | | soss 5565 |
. . . . . . . 8
⊢ (ran
(𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) ⊆ ℝ → ( < Or ℝ
→ < Or ran (𝑥
∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)))) |
51 | 49, 39, 50 | mpisyl 21 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → < Or
ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) |
52 | | sopo 5564 |
. . . . . . 7
⊢ ( < Or
ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) → < Po ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) |
53 | 51, 52 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → < Po
ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) |
54 | | negex 11399 |
. . . . . . . . 9
⊢ -(1 /
𝑥) ∈
V |
55 | | eqid 2736 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) |
56 | 54, 55 | fnmpti 6644 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) Fn (𝐴(,)𝐵) |
57 | | dffn4 6762 |
. . . . . . . 8
⊢ ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) Fn (𝐴(,)𝐵) ↔ (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)):(𝐴(,)𝐵)–onto→ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) |
58 | 56, 57 | mpbi 229 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)):(𝐴(,)𝐵)–onto→ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) |
59 | 58 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)):(𝐴(,)𝐵)–onto→ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) |
60 | 44 | sselda 3944 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑧 ∈ ℝ+) |
61 | 60 | adantrl 714 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → 𝑧 ∈ ℝ+) |
62 | 61 | rprecred 12968 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → (1 / 𝑧) ∈ ℝ) |
63 | 44 | sselda 3944 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ℝ+) |
64 | 63 | adantrr 715 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → 𝑦 ∈ ℝ+) |
65 | 64 | rprecred 12968 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → (1 / 𝑦) ∈ ℝ) |
66 | 62, 65 | ltnegd 11733 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → ((1 / 𝑧) < (1 / 𝑦) ↔ -(1 / 𝑦) < -(1 / 𝑧))) |
67 | 64, 61 | ltrecd 12975 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → (𝑦 < 𝑧 ↔ (1 / 𝑧) < (1 / 𝑦))) |
68 | | oveq2 7365 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (1 / 𝑥) = (1 / 𝑦)) |
69 | 68 | negeqd 11395 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → -(1 / 𝑥) = -(1 / 𝑦)) |
70 | | negex 11399 |
. . . . . . . . . . . 12
⊢ -(1 /
𝑦) ∈
V |
71 | 69, 55, 70 | fvmpt 6948 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝐴(,)𝐵) → ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑦) = -(1 / 𝑦)) |
72 | | oveq2 7365 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (1 / 𝑥) = (1 / 𝑧)) |
73 | 72 | negeqd 11395 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → -(1 / 𝑥) = -(1 / 𝑧)) |
74 | | negex 11399 |
. . . . . . . . . . . 12
⊢ -(1 /
𝑧) ∈
V |
75 | 73, 55, 74 | fvmpt 6948 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝐴(,)𝐵) → ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑧) = -(1 / 𝑧)) |
76 | 71, 75 | breqan12d 5121 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑦) < ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑧) ↔ -(1 / 𝑦) < -(1 / 𝑧))) |
77 | 76 | adantl 482 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → (((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑦) < ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑧) ↔ -(1 / 𝑦) < -(1 / 𝑧))) |
78 | 66, 67, 77 | 3bitr4d 310 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → (𝑦 < 𝑧 ↔ ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑦) < ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑧))) |
79 | 78 | biimpd 228 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → (𝑦 < 𝑧 → ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑦) < ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑧))) |
80 | 79 | ralrimivva 3197 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
∀𝑦 ∈ (𝐴(,)𝐵)∀𝑧 ∈ (𝐴(,)𝐵)(𝑦 < 𝑧 → ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑦) < ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑧))) |
81 | | soisoi 7273 |
. . . . . 6
⊢ ((( <
Or (𝐴(,)𝐵) ∧ < Po ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) ∧ ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)):(𝐴(,)𝐵)–onto→ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) ∧ ∀𝑦 ∈ (𝐴(,)𝐵)∀𝑧 ∈ (𝐴(,)𝐵)(𝑦 < 𝑧 → ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑦) < ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑧)))) → (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) Isom < , < ((𝐴(,)𝐵), ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)))) |
82 | 42, 53, 59, 80, 81 | syl22anc 837 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) Isom < , < ((𝐴(,)𝐵), ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)))) |
83 | | reelprrecn 11143 |
. . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} |
84 | 83 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ℝ
∈ {ℝ, ℂ}) |
85 | | relogcl 25931 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
86 | 85 | adantl 482 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ ℝ+)
→ (log‘𝑥) ∈
ℝ) |
87 | 86 | recnd 11183 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ ℝ+)
→ (log‘𝑥) ∈
ℂ) |
88 | 87 | negcld 11499 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ ℝ+)
→ -(log‘𝑥)
∈ ℂ) |
89 | 54 | a1i 11 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ ℝ+)
→ -(1 / 𝑥) ∈
V) |
90 | | ovexd 7392 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ ℝ+)
→ (1 / 𝑥) ∈
V) |
91 | | relogf1o 25922 |
. . . . . . . . . . . . 13
⊢ (log
↾ ℝ+):ℝ+–1-1-onto→ℝ |
92 | | f1of 6784 |
. . . . . . . . . . . . 13
⊢ ((log
↾ ℝ+):ℝ+–1-1-onto→ℝ → (log ↾
ℝ+):ℝ+⟶ℝ) |
93 | 91, 92 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (log
↾
ℝ+):ℝ+⟶ℝ) |
94 | 93 | feqmptd 6910 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (log
↾ ℝ+) = (𝑥 ∈ ℝ+ ↦ ((log
↾ ℝ+)‘𝑥))) |
95 | | fvres 6861 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ ((log ↾ ℝ+)‘𝑥) = (log‘𝑥)) |
96 | 95 | mpteq2ia 5208 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
↦ ((log ↾ ℝ+)‘𝑥)) = (𝑥 ∈ ℝ+ ↦
(log‘𝑥)) |
97 | 94, 96 | eqtrdi 2792 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (log
↾ ℝ+) = (𝑥 ∈ ℝ+ ↦
(log‘𝑥))) |
98 | 97 | oveq2d 7373 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (ℝ
D (log ↾ ℝ+)) = (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘𝑥)))) |
99 | | dvrelog 25992 |
. . . . . . . . 9
⊢ (ℝ
D (log ↾ ℝ+)) = (𝑥 ∈ ℝ+ ↦ (1 /
𝑥)) |
100 | 98, 99 | eqtr3di 2791 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (ℝ
D (𝑥 ∈
ℝ+ ↦ (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (1 /
𝑥))) |
101 | 84, 87, 90, 100 | dvmptneg 25330 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (ℝ
D (𝑥 ∈
ℝ+ ↦ -(log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ -(1 /
𝑥))) |
102 | | eqid 2736 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
103 | 102 | tgioo2 24166 |
. . . . . . 7
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
104 | | iccntr 24184 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
105 | 2, 4, 104 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
106 | 84, 88, 89, 101, 14, 103, 102, 105 | dvmptres2 25326 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (ℝ
D (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) |
107 | | isoeq1 7262 |
. . . . . 6
⊢ ((ℝ
D (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) → ((ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))) Isom < , < ((𝐴(,)𝐵), ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) ↔ (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) Isom < , < ((𝐴(,)𝐵), ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))))) |
108 | 106, 107 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
((ℝ D (𝑥 ∈
(𝐴[,]𝐵) ↦ -(log‘𝑥))) Isom < , < ((𝐴(,)𝐵), ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) ↔ (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) Isom < , < ((𝐴(,)𝐵), ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))))) |
109 | 82, 108 | mpbird 256 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (ℝ
D (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))) Isom < , < ((𝐴(,)𝐵), ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)))) |
110 | | simpr 485 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝑇 ∈
(0(,)1)) |
111 | | eqid 2736 |
. . . 4
⊢ ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) = ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) |
112 | 2, 4, 5, 37, 109, 110, 111 | dvcvx 25384 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < ((𝑇 · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐴)) + ((1 − 𝑇) · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐵)))) |
113 | | ax-1cn 11109 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
114 | | elioore 13294 |
. . . . . . . . . 10
⊢ (𝑇 ∈ (0(,)1) → 𝑇 ∈
ℝ) |
115 | 114 | adantl 482 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝑇 ∈
ℝ) |
116 | 115 | recnd 11183 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝑇 ∈
ℂ) |
117 | | nncan 11430 |
. . . . . . . 8
⊢ ((1
∈ ℂ ∧ 𝑇
∈ ℂ) → (1 − (1 − 𝑇)) = 𝑇) |
118 | 113, 116,
117 | sylancr 587 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (1
− (1 − 𝑇)) =
𝑇) |
119 | 118 | oveq1d 7372 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((1
− (1 − 𝑇))
· 𝐴) = (𝑇 · 𝐴)) |
120 | 119 | oveq1d 7372 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (((1
− (1 − 𝑇))
· 𝐴) + ((1 −
𝑇) · 𝐵)) = ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) |
121 | | ioossicc 13350 |
. . . . . . . 8
⊢ (0(,)1)
⊆ (0[,]1) |
122 | 121, 110 | sselid 3942 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝑇 ∈
(0[,]1)) |
123 | | iirev 24292 |
. . . . . . 7
⊢ (𝑇 ∈ (0[,]1) → (1
− 𝑇) ∈
(0[,]1)) |
124 | 122, 123 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (1
− 𝑇) ∈
(0[,]1)) |
125 | | lincmb01cmp 13412 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (1 − 𝑇) ∈ (0[,]1)) → (((1 − (1
− 𝑇)) · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝐴[,]𝐵)) |
126 | 2, 4, 5, 124, 125 | syl31anc 1373 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (((1
− (1 − 𝑇))
· 𝐴) + ((1 −
𝑇) · 𝐵)) ∈ (𝐴[,]𝐵)) |
127 | 120, 126 | eqeltrrd 2839 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝐴[,]𝐵)) |
128 | | fveq2 6842 |
. . . . . 6
⊢ (𝑥 = ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) → (log‘𝑥) = (log‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))) |
129 | 128 | negeqd 11395 |
. . . . 5
⊢ (𝑥 = ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) → -(log‘𝑥) = -(log‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))) |
130 | | eqid 2736 |
. . . . 5
⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) |
131 | | negex 11399 |
. . . . 5
⊢
-(log‘((𝑇
· 𝐴) + ((1 −
𝑇) · 𝐵))) ∈ V |
132 | 129, 130,
131 | fvmpt 6948 |
. . . 4
⊢ (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = -(log‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))) |
133 | 127, 132 | syl 17 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = -(log‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))) |
134 | 1 | rpxrd 12958 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐴 ∈
ℝ*) |
135 | 3 | rpxrd 12958 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐵 ∈
ℝ*) |
136 | 2, 4, 5 | ltled 11303 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐴 ≤ 𝐵) |
137 | | lbicc2 13381 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) |
138 | 134, 135,
136, 137 | syl3anc 1371 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐴 ∈ (𝐴[,]𝐵)) |
139 | | fveq2 6842 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (log‘𝑥) = (log‘𝐴)) |
140 | 139 | negeqd 11395 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → -(log‘𝑥) = -(log‘𝐴)) |
141 | | negex 11399 |
. . . . . . . . 9
⊢
-(log‘𝐴)
∈ V |
142 | 140, 130,
141 | fvmpt 6948 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐴) = -(log‘𝐴)) |
143 | 138, 142 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐴) = -(log‘𝐴)) |
144 | 143 | oveq2d 7373 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑇 · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐴)) = (𝑇 · -(log‘𝐴))) |
145 | 1 | relogcld 25978 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
(log‘𝐴) ∈
ℝ) |
146 | 145 | recnd 11183 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
(log‘𝐴) ∈
ℂ) |
147 | 116, 146 | mulneg2d 11609 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑇 · -(log‘𝐴)) = -(𝑇 · (log‘𝐴))) |
148 | 144, 147 | eqtrd 2776 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑇 · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐴)) = -(𝑇 · (log‘𝐴))) |
149 | | ubicc2 13382 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) |
150 | 134, 135,
136, 149 | syl3anc 1371 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐵 ∈ (𝐴[,]𝐵)) |
151 | | fveq2 6842 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → (log‘𝑥) = (log‘𝐵)) |
152 | 151 | negeqd 11395 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → -(log‘𝑥) = -(log‘𝐵)) |
153 | | negex 11399 |
. . . . . . . . 9
⊢
-(log‘𝐵)
∈ V |
154 | 152, 130,
153 | fvmpt 6948 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐵) = -(log‘𝐵)) |
155 | 150, 154 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐵) = -(log‘𝐵)) |
156 | 155 | oveq2d 7373 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((1
− 𝑇) · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐵)) = ((1 − 𝑇) · -(log‘𝐵))) |
157 | | 1re 11155 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
158 | | resubcl 11465 |
. . . . . . . . 9
⊢ ((1
∈ ℝ ∧ 𝑇
∈ ℝ) → (1 − 𝑇) ∈ ℝ) |
159 | 157, 115,
158 | sylancr 587 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (1
− 𝑇) ∈
ℝ) |
160 | 159 | recnd 11183 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (1
− 𝑇) ∈
ℂ) |
161 | 3 | relogcld 25978 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
(log‘𝐵) ∈
ℝ) |
162 | 161 | recnd 11183 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
(log‘𝐵) ∈
ℂ) |
163 | 160, 162 | mulneg2d 11609 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((1
− 𝑇) ·
-(log‘𝐵)) = -((1
− 𝑇) ·
(log‘𝐵))) |
164 | 156, 163 | eqtrd 2776 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((1
− 𝑇) · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐵)) = -((1 − 𝑇) · (log‘𝐵))) |
165 | 148, 164 | oveq12d 7375 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑇 · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐴)) + ((1 − 𝑇) · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐵))) = (-(𝑇 · (log‘𝐴)) + -((1 − 𝑇) · (log‘𝐵)))) |
166 | 115, 145 | remulcld 11185 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑇 · (log‘𝐴)) ∈
ℝ) |
167 | 166 | recnd 11183 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑇 · (log‘𝐴)) ∈
ℂ) |
168 | 159, 161 | remulcld 11185 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((1
− 𝑇) ·
(log‘𝐵)) ∈
ℝ) |
169 | 168 | recnd 11183 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((1
− 𝑇) ·
(log‘𝐵)) ∈
ℂ) |
170 | 167, 169 | negdid 11525 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → -((𝑇 · (log‘𝐴)) + ((1 − 𝑇) · (log‘𝐵))) = (-(𝑇 · (log‘𝐴)) + -((1 − 𝑇) · (log‘𝐵)))) |
171 | 165, 170 | eqtr4d 2779 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑇 · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐴)) + ((1 − 𝑇) · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐵))) = -((𝑇 · (log‘𝐴)) + ((1 − 𝑇) · (log‘𝐵)))) |
172 | 112, 133,
171 | 3brtr3d 5136 |
. 2
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
-(log‘((𝑇 ·
𝐴) + ((1 − 𝑇) · 𝐵))) < -((𝑇 · (log‘𝐴)) + ((1 − 𝑇) · (log‘𝐵)))) |
173 | 166, 168 | readdcld 11184 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑇 · (log‘𝐴)) + ((1 − 𝑇) · (log‘𝐵))) ∈
ℝ) |
174 | 14, 127 | sseldd 3945 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈
ℝ+) |
175 | 174 | relogcld 25978 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
(log‘((𝑇 ·
𝐴) + ((1 − 𝑇) · 𝐵))) ∈ ℝ) |
176 | 173, 175 | ltnegd 11733 |
. 2
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (((𝑇 · (log‘𝐴)) + ((1 − 𝑇) · (log‘𝐵))) < (log‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) ↔ -(log‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < -((𝑇 · (log‘𝐴)) + ((1 − 𝑇) · (log‘𝐵))))) |
177 | 172, 176 | mpbird 256 |
1
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑇 · (log‘𝐴)) + ((1 − 𝑇) · (log‘𝐵))) < (log‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))) |