Step | Hyp | Ref
| Expression |
1 | | simpl1 1084 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐴 ∈
ℝ+) |
2 | 1 | rpred 11910 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐴 ∈
ℝ) |
3 | | simpl2 1085 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐵 ∈
ℝ+) |
4 | 3 | rpred 11910 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐵 ∈
ℝ) |
5 | | simpl3 1086 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐴 < 𝐵) |
6 | 1 | rpgt0d 11913 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 0 <
𝐴) |
7 | | ltpnf 11992 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ℝ → 𝐵 < +∞) |
8 | 4, 7 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐵 < +∞) |
9 | | 0xr 10124 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ* |
10 | | pnfxr 10130 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
11 | | iccssioo 12280 |
. . . . . . . . . . . 12
⊢ (((0
∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (0
< 𝐴 ∧ 𝐵 < +∞)) → (𝐴[,]𝐵) ⊆ (0(,)+∞)) |
12 | 9, 10, 11 | mpanl12 718 |
. . . . . . . . . . 11
⊢ ((0 <
𝐴 ∧ 𝐵 < +∞) → (𝐴[,]𝐵) ⊆ (0(,)+∞)) |
13 | 6, 8, 12 | syl2anc 694 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝐴[,]𝐵) ⊆ (0(,)+∞)) |
14 | | ioorp 12289 |
. . . . . . . . . 10
⊢
(0(,)+∞) = ℝ+ |
15 | 13, 14 | syl6sseq 3684 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝐴[,]𝐵) ⊆
ℝ+) |
16 | 15 | sselda 3636 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ+) |
17 | 16 | relogcld 24414 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (log‘𝑥) ∈ ℝ) |
18 | 17 | renegcld 10495 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → -(log‘𝑥) ∈ ℝ) |
19 | | eqid 2651 |
. . . . . 6
⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) |
20 | 18, 19 | fmptd 6425 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)):(𝐴[,]𝐵)⟶ℝ) |
21 | | ax-resscn 10031 |
. . . . . 6
⊢ ℝ
⊆ ℂ |
22 | 15 | resabs1d 5463 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((log
↾ ℝ+) ↾ (𝐴[,]𝐵)) = (log ↾ (𝐴[,]𝐵))) |
23 | | ssid 3657 |
. . . . . . . . . . 11
⊢ ℂ
⊆ ℂ |
24 | | cncfss 22749 |
. . . . . . . . . . 11
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) →
(ℝ+–cn→ℝ) ⊆
(ℝ+–cn→ℂ)) |
25 | 21, 23, 24 | mp2an 708 |
. . . . . . . . . 10
⊢
(ℝ+–cn→ℝ) ⊆
(ℝ+–cn→ℂ) |
26 | | relogcn 24429 |
. . . . . . . . . 10
⊢ (log
↾ ℝ+) ∈ (ℝ+–cn→ℝ) |
27 | 25, 26 | sselii 3633 |
. . . . . . . . 9
⊢ (log
↾ ℝ+) ∈ (ℝ+–cn→ℂ) |
28 | | rescncf 22747 |
. . . . . . . . 9
⊢ ((𝐴[,]𝐵) ⊆ ℝ+ → ((log
↾ ℝ+) ∈ (ℝ+–cn→ℂ) → ((log ↾
ℝ+) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ))) |
29 | 15, 27, 28 | mpisyl 21 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((log
↾ ℝ+) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
30 | 22, 29 | eqeltrrd 2731 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (log
↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
31 | | fvres 6245 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((log ↾ (𝐴[,]𝐵))‘𝑥) = (log‘𝑥)) |
32 | 31 | negeqd 10313 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴[,]𝐵) → -((log ↾ (𝐴[,]𝐵))‘𝑥) = -(log‘𝑥)) |
33 | 32 | mpteq2ia 4773 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ -((log ↾ (𝐴[,]𝐵))‘𝑥)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) |
34 | 33 | eqcomi 2660 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ -((log ↾ (𝐴[,]𝐵))‘𝑥)) |
35 | 34 | negfcncf 22769 |
. . . . . . 7
⊢ ((log
↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
36 | 30, 35 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
37 | | cncffvrn 22748 |
. . . . . 6
⊢ ((ℝ
⊆ ℂ ∧ (𝑥
∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℝ) ↔ (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)):(𝐴[,]𝐵)⟶ℝ)) |
38 | 21, 36, 37 | sylancr 696 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℝ) ↔ (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)):(𝐴[,]𝐵)⟶ℝ)) |
39 | 20, 38 | mpbird 247 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
40 | | ioossre 12273 |
. . . . . . . 8
⊢ (𝐴(,)𝐵) ⊆ ℝ |
41 | | ltso 10156 |
. . . . . . . 8
⊢ < Or
ℝ |
42 | | soss 5082 |
. . . . . . . 8
⊢ ((𝐴(,)𝐵) ⊆ ℝ → ( < Or ℝ
→ < Or (𝐴(,)𝐵))) |
43 | 40, 41, 42 | mp2 9 |
. . . . . . 7
⊢ < Or
(𝐴(,)𝐵) |
44 | 43 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → < Or
(𝐴(,)𝐵)) |
45 | | ioossicc 12297 |
. . . . . . . . . . . . . 14
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
46 | 45, 15 | syl5ss 3647 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝐴(,)𝐵) ⊆
ℝ+) |
47 | 46 | sselda 3636 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℝ+) |
48 | 47 | rprecred 11921 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (1 / 𝑥) ∈ ℝ) |
49 | 48 | renegcld 10495 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ (𝐴(,)𝐵)) → -(1 / 𝑥) ∈ ℝ) |
50 | | eqid 2651 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) |
51 | 49, 50 | fmptd 6425 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)):(𝐴(,)𝐵)⟶ℝ) |
52 | | frn 6091 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)):(𝐴(,)𝐵)⟶ℝ → ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) ⊆ ℝ) |
53 | 51, 52 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ran
(𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) ⊆ ℝ) |
54 | | soss 5082 |
. . . . . . . 8
⊢ (ran
(𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) ⊆ ℝ → ( < Or ℝ
→ < Or ran (𝑥
∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)))) |
55 | 53, 41, 54 | mpisyl 21 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → < Or
ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) |
56 | | sopo 5081 |
. . . . . . 7
⊢ ( < Or
ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) → < Po ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) |
57 | 55, 56 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → < Po
ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) |
58 | | negex 10317 |
. . . . . . . . 9
⊢ -(1 /
𝑥) ∈
V |
59 | 58, 50 | fnmpti 6060 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) Fn (𝐴(,)𝐵) |
60 | | dffn4 6159 |
. . . . . . . 8
⊢ ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) Fn (𝐴(,)𝐵) ↔ (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)):(𝐴(,)𝐵)–onto→ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) |
61 | 59, 60 | mpbi 220 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)):(𝐴(,)𝐵)–onto→ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) |
62 | 61 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)):(𝐴(,)𝐵)–onto→ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) |
63 | 46 | sselda 3636 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑧 ∈ ℝ+) |
64 | 63 | adantrl 752 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → 𝑧 ∈ ℝ+) |
65 | 64 | rprecred 11921 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → (1 / 𝑧) ∈ ℝ) |
66 | 46 | sselda 3636 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ℝ+) |
67 | 66 | adantrr 753 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → 𝑦 ∈ ℝ+) |
68 | 67 | rprecred 11921 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → (1 / 𝑦) ∈ ℝ) |
69 | 65, 68 | ltnegd 10643 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → ((1 / 𝑧) < (1 / 𝑦) ↔ -(1 / 𝑦) < -(1 / 𝑧))) |
70 | 67, 64 | ltrecd 11928 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → (𝑦 < 𝑧 ↔ (1 / 𝑧) < (1 / 𝑦))) |
71 | | oveq2 6698 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (1 / 𝑥) = (1 / 𝑦)) |
72 | 71 | negeqd 10313 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → -(1 / 𝑥) = -(1 / 𝑦)) |
73 | | negex 10317 |
. . . . . . . . . . . 12
⊢ -(1 /
𝑦) ∈
V |
74 | 72, 50, 73 | fvmpt 6321 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝐴(,)𝐵) → ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑦) = -(1 / 𝑦)) |
75 | | oveq2 6698 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (1 / 𝑥) = (1 / 𝑧)) |
76 | 75 | negeqd 10313 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → -(1 / 𝑥) = -(1 / 𝑧)) |
77 | | negex 10317 |
. . . . . . . . . . . 12
⊢ -(1 /
𝑧) ∈
V |
78 | 76, 50, 77 | fvmpt 6321 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝐴(,)𝐵) → ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑧) = -(1 / 𝑧)) |
79 | 74, 78 | breqan12d 4701 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑦) < ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑧) ↔ -(1 / 𝑦) < -(1 / 𝑧))) |
80 | 79 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → (((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑦) < ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑧) ↔ -(1 / 𝑦) < -(1 / 𝑧))) |
81 | 69, 70, 80 | 3bitr4d 300 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → (𝑦 < 𝑧 ↔ ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑦) < ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑧))) |
82 | 81 | biimpd 219 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → (𝑦 < 𝑧 → ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑦) < ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑧))) |
83 | 82 | ralrimivva 3000 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
∀𝑦 ∈ (𝐴(,)𝐵)∀𝑧 ∈ (𝐴(,)𝐵)(𝑦 < 𝑧 → ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑦) < ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑧))) |
84 | | soisoi 6618 |
. . . . . 6
⊢ ((( <
Or (𝐴(,)𝐵) ∧ < Po ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) ∧ ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)):(𝐴(,)𝐵)–onto→ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) ∧ ∀𝑦 ∈ (𝐴(,)𝐵)∀𝑧 ∈ (𝐴(,)𝐵)(𝑦 < 𝑧 → ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑦) < ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑧)))) → (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) Isom < , < ((𝐴(,)𝐵), ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)))) |
85 | 44, 57, 62, 83, 84 | syl22anc 1367 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) Isom < , < ((𝐴(,)𝐵), ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)))) |
86 | | reelprrecn 10066 |
. . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} |
87 | 86 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ℝ
∈ {ℝ, ℂ}) |
88 | | relogcl 24367 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
89 | 88 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ ℝ+)
→ (log‘𝑥) ∈
ℝ) |
90 | 89 | recnd 10106 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ ℝ+)
→ (log‘𝑥) ∈
ℂ) |
91 | 90 | negcld 10417 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ ℝ+)
→ -(log‘𝑥)
∈ ℂ) |
92 | 58 | a1i 11 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ ℝ+)
→ -(1 / 𝑥) ∈
V) |
93 | | ovexd 6720 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ ℝ+)
→ (1 / 𝑥) ∈
V) |
94 | | dvrelog 24428 |
. . . . . . . . 9
⊢ (ℝ
D (log ↾ ℝ+)) = (𝑥 ∈ ℝ+ ↦ (1 /
𝑥)) |
95 | | relogf1o 24358 |
. . . . . . . . . . . . 13
⊢ (log
↾ ℝ+):ℝ+–1-1-onto→ℝ |
96 | | f1of 6175 |
. . . . . . . . . . . . 13
⊢ ((log
↾ ℝ+):ℝ+–1-1-onto→ℝ → (log ↾
ℝ+):ℝ+⟶ℝ) |
97 | 95, 96 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (log
↾
ℝ+):ℝ+⟶ℝ) |
98 | 97 | feqmptd 6288 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (log
↾ ℝ+) = (𝑥 ∈ ℝ+ ↦ ((log
↾ ℝ+)‘𝑥))) |
99 | | fvres 6245 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ ((log ↾ ℝ+)‘𝑥) = (log‘𝑥)) |
100 | 99 | mpteq2ia 4773 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
↦ ((log ↾ ℝ+)‘𝑥)) = (𝑥 ∈ ℝ+ ↦
(log‘𝑥)) |
101 | 98, 100 | syl6eq 2701 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (log
↾ ℝ+) = (𝑥 ∈ ℝ+ ↦
(log‘𝑥))) |
102 | 101 | oveq2d 6706 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (ℝ
D (log ↾ ℝ+)) = (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘𝑥)))) |
103 | 94, 102 | syl5reqr 2700 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (ℝ
D (𝑥 ∈
ℝ+ ↦ (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (1 /
𝑥))) |
104 | 87, 90, 93, 103 | dvmptneg 23774 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (ℝ
D (𝑥 ∈
ℝ+ ↦ -(log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ -(1 /
𝑥))) |
105 | | eqid 2651 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
106 | 105 | tgioo2 22653 |
. . . . . . 7
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
107 | | iccntr 22671 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
108 | 2, 4, 107 | syl2anc 694 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
109 | 87, 91, 92, 104, 15, 106, 105, 108 | dvmptres2 23770 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (ℝ
D (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) |
110 | | isoeq1 6607 |
. . . . . 6
⊢ ((ℝ
D (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) → ((ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))) Isom < , < ((𝐴(,)𝐵), ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) ↔ (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) Isom < , < ((𝐴(,)𝐵), ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))))) |
111 | 109, 110 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
((ℝ D (𝑥 ∈
(𝐴[,]𝐵) ↦ -(log‘𝑥))) Isom < , < ((𝐴(,)𝐵), ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) ↔ (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) Isom < , < ((𝐴(,)𝐵), ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))))) |
112 | 85, 111 | mpbird 247 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (ℝ
D (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))) Isom < , < ((𝐴(,)𝐵), ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)))) |
113 | | simpr 476 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝑇 ∈
(0(,)1)) |
114 | | eqid 2651 |
. . . 4
⊢ ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) = ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) |
115 | 2, 4, 5, 39, 112, 113, 114 | dvcvx 23828 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < ((𝑇 · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐴)) + ((1 − 𝑇) · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐵)))) |
116 | | ax-1cn 10032 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
117 | | elioore 12243 |
. . . . . . . . . 10
⊢ (𝑇 ∈ (0(,)1) → 𝑇 ∈
ℝ) |
118 | 117 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝑇 ∈
ℝ) |
119 | 118 | recnd 10106 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝑇 ∈
ℂ) |
120 | | nncan 10348 |
. . . . . . . 8
⊢ ((1
∈ ℂ ∧ 𝑇
∈ ℂ) → (1 − (1 − 𝑇)) = 𝑇) |
121 | 116, 119,
120 | sylancr 696 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (1
− (1 − 𝑇)) =
𝑇) |
122 | 121 | oveq1d 6705 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((1
− (1 − 𝑇))
· 𝐴) = (𝑇 · 𝐴)) |
123 | 122 | oveq1d 6705 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (((1
− (1 − 𝑇))
· 𝐴) + ((1 −
𝑇) · 𝐵)) = ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) |
124 | | ioossicc 12297 |
. . . . . . . 8
⊢ (0(,)1)
⊆ (0[,]1) |
125 | 124, 113 | sseldi 3634 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝑇 ∈
(0[,]1)) |
126 | | iirev 22775 |
. . . . . . 7
⊢ (𝑇 ∈ (0[,]1) → (1
− 𝑇) ∈
(0[,]1)) |
127 | 125, 126 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (1
− 𝑇) ∈
(0[,]1)) |
128 | | lincmb01cmp 12353 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (1 − 𝑇) ∈ (0[,]1)) → (((1 − (1
− 𝑇)) · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝐴[,]𝐵)) |
129 | 2, 4, 5, 127, 128 | syl31anc 1369 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (((1
− (1 − 𝑇))
· 𝐴) + ((1 −
𝑇) · 𝐵)) ∈ (𝐴[,]𝐵)) |
130 | 123, 129 | eqeltrrd 2731 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝐴[,]𝐵)) |
131 | | fveq2 6229 |
. . . . . 6
⊢ (𝑥 = ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) → (log‘𝑥) = (log‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))) |
132 | 131 | negeqd 10313 |
. . . . 5
⊢ (𝑥 = ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) → -(log‘𝑥) = -(log‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))) |
133 | | negex 10317 |
. . . . 5
⊢
-(log‘((𝑇
· 𝐴) + ((1 −
𝑇) · 𝐵))) ∈ V |
134 | 132, 19, 133 | fvmpt 6321 |
. . . 4
⊢ (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = -(log‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))) |
135 | 130, 134 | syl 17 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = -(log‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))) |
136 | 1 | rpxrd 11911 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐴 ∈
ℝ*) |
137 | 3 | rpxrd 11911 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐵 ∈
ℝ*) |
138 | 2, 4, 5 | ltled 10223 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐴 ≤ 𝐵) |
139 | | lbicc2 12326 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) |
140 | 136, 137,
138, 139 | syl3anc 1366 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐴 ∈ (𝐴[,]𝐵)) |
141 | | fveq2 6229 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (log‘𝑥) = (log‘𝐴)) |
142 | 141 | negeqd 10313 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → -(log‘𝑥) = -(log‘𝐴)) |
143 | | negex 10317 |
. . . . . . . . 9
⊢
-(log‘𝐴)
∈ V |
144 | 142, 19, 143 | fvmpt 6321 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐴) = -(log‘𝐴)) |
145 | 140, 144 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐴) = -(log‘𝐴)) |
146 | 145 | oveq2d 6706 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑇 · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐴)) = (𝑇 · -(log‘𝐴))) |
147 | 1 | relogcld 24414 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
(log‘𝐴) ∈
ℝ) |
148 | 147 | recnd 10106 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
(log‘𝐴) ∈
ℂ) |
149 | 119, 148 | mulneg2d 10522 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑇 · -(log‘𝐴)) = -(𝑇 · (log‘𝐴))) |
150 | 146, 149 | eqtrd 2685 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑇 · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐴)) = -(𝑇 · (log‘𝐴))) |
151 | | ubicc2 12327 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) |
152 | 136, 137,
138, 151 | syl3anc 1366 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐵 ∈ (𝐴[,]𝐵)) |
153 | | fveq2 6229 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → (log‘𝑥) = (log‘𝐵)) |
154 | 153 | negeqd 10313 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → -(log‘𝑥) = -(log‘𝐵)) |
155 | | negex 10317 |
. . . . . . . . 9
⊢
-(log‘𝐵)
∈ V |
156 | 154, 19, 155 | fvmpt 6321 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐵) = -(log‘𝐵)) |
157 | 152, 156 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐵) = -(log‘𝐵)) |
158 | 157 | oveq2d 6706 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((1
− 𝑇) · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐵)) = ((1 − 𝑇) · -(log‘𝐵))) |
159 | | 1re 10077 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
160 | | resubcl 10383 |
. . . . . . . . 9
⊢ ((1
∈ ℝ ∧ 𝑇
∈ ℝ) → (1 − 𝑇) ∈ ℝ) |
161 | 159, 118,
160 | sylancr 696 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (1
− 𝑇) ∈
ℝ) |
162 | 161 | recnd 10106 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (1
− 𝑇) ∈
ℂ) |
163 | 3 | relogcld 24414 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
(log‘𝐵) ∈
ℝ) |
164 | 163 | recnd 10106 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
(log‘𝐵) ∈
ℂ) |
165 | 162, 164 | mulneg2d 10522 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((1
− 𝑇) ·
-(log‘𝐵)) = -((1
− 𝑇) ·
(log‘𝐵))) |
166 | 158, 165 | eqtrd 2685 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((1
− 𝑇) · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐵)) = -((1 − 𝑇) · (log‘𝐵))) |
167 | 150, 166 | oveq12d 6708 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑇 · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐴)) + ((1 − 𝑇) · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐵))) = (-(𝑇 · (log‘𝐴)) + -((1 − 𝑇) · (log‘𝐵)))) |
168 | 118, 147 | remulcld 10108 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑇 · (log‘𝐴)) ∈
ℝ) |
169 | 168 | recnd 10106 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑇 · (log‘𝐴)) ∈
ℂ) |
170 | 161, 163 | remulcld 10108 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((1
− 𝑇) ·
(log‘𝐵)) ∈
ℝ) |
171 | 170 | recnd 10106 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((1
− 𝑇) ·
(log‘𝐵)) ∈
ℂ) |
172 | 169, 171 | negdid 10443 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → -((𝑇 · (log‘𝐴)) + ((1 − 𝑇) · (log‘𝐵))) = (-(𝑇 · (log‘𝐴)) + -((1 − 𝑇) · (log‘𝐵)))) |
173 | 167, 172 | eqtr4d 2688 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑇 · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐴)) + ((1 − 𝑇) · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐵))) = -((𝑇 · (log‘𝐴)) + ((1 − 𝑇) · (log‘𝐵)))) |
174 | 115, 135,
173 | 3brtr3d 4716 |
. 2
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
-(log‘((𝑇 ·
𝐴) + ((1 − 𝑇) · 𝐵))) < -((𝑇 · (log‘𝐴)) + ((1 − 𝑇) · (log‘𝐵)))) |
175 | 168, 170 | readdcld 10107 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑇 · (log‘𝐴)) + ((1 − 𝑇) · (log‘𝐵))) ∈
ℝ) |
176 | 15, 130 | sseldd 3637 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈
ℝ+) |
177 | 176 | relogcld 24414 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
(log‘((𝑇 ·
𝐴) + ((1 − 𝑇) · 𝐵))) ∈ ℝ) |
178 | 175, 177 | ltnegd 10643 |
. 2
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (((𝑇 · (log‘𝐴)) + ((1 − 𝑇) · (log‘𝐵))) < (log‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) ↔ -(log‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < -((𝑇 · (log‘𝐴)) + ((1 − 𝑇) · (log‘𝐵))))) |
179 | 174, 178 | mpbird 247 |
1
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑇 · (log‘𝐴)) + ((1 − 𝑇) · (log‘𝐵))) < (log‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))) |