Step | Hyp | Ref
| Expression |
1 | | simpl1 1057 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐴 ∈
ℝ+) |
2 | 1 | rpred 11748 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐴 ∈
ℝ) |
3 | | simpl2 1058 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐵 ∈
ℝ+) |
4 | 3 | rpred 11748 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐵 ∈
ℝ) |
5 | | simpl3 1059 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐴 < 𝐵) |
6 | 1 | rpgt0d 11751 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 0 <
𝐴) |
7 | | ltpnf 11830 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ℝ → 𝐵 < +∞) |
8 | 4, 7 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐵 < +∞) |
9 | | 0xr 9965 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ* |
10 | | pnfxr 9971 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
11 | | iccssioo 12113 |
. . . . . . . . . . . 12
⊢ (((0
∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (0
< 𝐴 ∧ 𝐵 < +∞)) → (𝐴[,]𝐵) ⊆ (0(,)+∞)) |
12 | 9, 10, 11 | mpanl12 714 |
. . . . . . . . . . 11
⊢ ((0 <
𝐴 ∧ 𝐵 < +∞) → (𝐴[,]𝐵) ⊆ (0(,)+∞)) |
13 | 6, 8, 12 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝐴[,]𝐵) ⊆ (0(,)+∞)) |
14 | | ioorp 12122 |
. . . . . . . . . 10
⊢
(0(,)+∞) = ℝ+ |
15 | 13, 14 | syl6sseq 3614 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝐴[,]𝐵) ⊆
ℝ+) |
16 | 15 | sselda 3568 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ+) |
17 | 16 | relogcld 24173 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (log‘𝑥) ∈ ℝ) |
18 | 17 | renegcld 10336 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → -(log‘𝑥) ∈ ℝ) |
19 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) |
20 | 18, 19 | fmptd 6292 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)):(𝐴[,]𝐵)⟶ℝ) |
21 | | ax-resscn 9872 |
. . . . . 6
⊢ ℝ
⊆ ℂ |
22 | 15 | resabs1d 5348 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((log
↾ ℝ+) ↾ (𝐴[,]𝐵)) = (log ↾ (𝐴[,]𝐵))) |
23 | | ssid 3587 |
. . . . . . . . . . 11
⊢ ℂ
⊆ ℂ |
24 | | cncfss 22510 |
. . . . . . . . . . 11
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) →
(ℝ+–cn→ℝ) ⊆
(ℝ+–cn→ℂ)) |
25 | 21, 23, 24 | mp2an 704 |
. . . . . . . . . 10
⊢
(ℝ+–cn→ℝ) ⊆
(ℝ+–cn→ℂ) |
26 | | relogcn 24184 |
. . . . . . . . . 10
⊢ (log
↾ ℝ+) ∈ (ℝ+–cn→ℝ) |
27 | 25, 26 | sselii 3565 |
. . . . . . . . 9
⊢ (log
↾ ℝ+) ∈ (ℝ+–cn→ℂ) |
28 | | rescncf 22508 |
. . . . . . . . 9
⊢ ((𝐴[,]𝐵) ⊆ ℝ+ → ((log
↾ ℝ+) ∈ (ℝ+–cn→ℂ) → ((log ↾
ℝ+) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ))) |
29 | 15, 27, 28 | mpisyl 21 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((log
↾ ℝ+) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
30 | 22, 29 | eqeltrrd 2689 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (log
↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
31 | | fvres 6117 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((log ↾ (𝐴[,]𝐵))‘𝑥) = (log‘𝑥)) |
32 | 31 | negeqd 10154 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴[,]𝐵) → -((log ↾ (𝐴[,]𝐵))‘𝑥) = -(log‘𝑥)) |
33 | 32 | mpteq2ia 4668 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ -((log ↾ (𝐴[,]𝐵))‘𝑥)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) |
34 | 33 | eqcomi 2619 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ -((log ↾ (𝐴[,]𝐵))‘𝑥)) |
35 | 34 | negfcncf 22530 |
. . . . . . 7
⊢ ((log
↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
36 | 30, 35 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
37 | | cncffvrn 22509 |
. . . . . 6
⊢ ((ℝ
⊆ ℂ ∧ (𝑥
∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℝ) ↔ (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)):(𝐴[,]𝐵)⟶ℝ)) |
38 | 21, 36, 37 | sylancr 694 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℝ) ↔ (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)):(𝐴[,]𝐵)⟶ℝ)) |
39 | 20, 38 | mpbird 246 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
40 | | ioossre 12106 |
. . . . . . . 8
⊢ (𝐴(,)𝐵) ⊆ ℝ |
41 | | ltso 9997 |
. . . . . . . 8
⊢ < Or
ℝ |
42 | | soss 4977 |
. . . . . . . 8
⊢ ((𝐴(,)𝐵) ⊆ ℝ → ( < Or ℝ
→ < Or (𝐴(,)𝐵))) |
43 | 40, 41, 42 | mp2 9 |
. . . . . . 7
⊢ < Or
(𝐴(,)𝐵) |
44 | 43 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → < Or
(𝐴(,)𝐵)) |
45 | | ioossicc 12130 |
. . . . . . . . . . . . . 14
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
46 | 45, 15 | syl5ss 3579 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝐴(,)𝐵) ⊆
ℝ+) |
47 | 46 | sselda 3568 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℝ+) |
48 | 47 | rprecred 11759 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (1 / 𝑥) ∈ ℝ) |
49 | 48 | renegcld 10336 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ (𝐴(,)𝐵)) → -(1 / 𝑥) ∈ ℝ) |
50 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) |
51 | 49, 50 | fmptd 6292 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)):(𝐴(,)𝐵)⟶ℝ) |
52 | | frn 5966 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)):(𝐴(,)𝐵)⟶ℝ → ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) ⊆ ℝ) |
53 | 51, 52 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ran
(𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) ⊆ ℝ) |
54 | | soss 4977 |
. . . . . . . 8
⊢ (ran
(𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) ⊆ ℝ → ( < Or ℝ
→ < Or ran (𝑥
∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)))) |
55 | 53, 41, 54 | mpisyl 21 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → < Or
ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) |
56 | | sopo 4976 |
. . . . . . 7
⊢ ( < Or
ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) → < Po ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) |
57 | 55, 56 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → < Po
ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) |
58 | | negex 10158 |
. . . . . . . . 9
⊢ -(1 /
𝑥) ∈
V |
59 | 58, 50 | fnmpti 5935 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) Fn (𝐴(,)𝐵) |
60 | | dffn4 6034 |
. . . . . . . 8
⊢ ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) Fn (𝐴(,)𝐵) ↔ (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)):(𝐴(,)𝐵)–onto→ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) |
61 | 59, 60 | mpbi 219 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)):(𝐴(,)𝐵)–onto→ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) |
62 | 61 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)):(𝐴(,)𝐵)–onto→ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) |
63 | 46 | sselda 3568 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑧 ∈ ℝ+) |
64 | 63 | adantrl 748 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → 𝑧 ∈ ℝ+) |
65 | 64 | rprecred 11759 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → (1 / 𝑧) ∈ ℝ) |
66 | 46 | sselda 3568 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ℝ+) |
67 | 66 | adantrr 749 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → 𝑦 ∈ ℝ+) |
68 | 67 | rprecred 11759 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → (1 / 𝑦) ∈ ℝ) |
69 | 65, 68 | ltnegd 10484 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → ((1 / 𝑧) < (1 / 𝑦) ↔ -(1 / 𝑦) < -(1 / 𝑧))) |
70 | 67, 64 | ltrecd 11766 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → (𝑦 < 𝑧 ↔ (1 / 𝑧) < (1 / 𝑦))) |
71 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (1 / 𝑥) = (1 / 𝑦)) |
72 | 71 | negeqd 10154 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → -(1 / 𝑥) = -(1 / 𝑦)) |
73 | | negex 10158 |
. . . . . . . . . . . 12
⊢ -(1 /
𝑦) ∈
V |
74 | 72, 50, 73 | fvmpt 6191 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝐴(,)𝐵) → ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑦) = -(1 / 𝑦)) |
75 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (1 / 𝑥) = (1 / 𝑧)) |
76 | 75 | negeqd 10154 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → -(1 / 𝑥) = -(1 / 𝑧)) |
77 | | negex 10158 |
. . . . . . . . . . . 12
⊢ -(1 /
𝑧) ∈
V |
78 | 76, 50, 77 | fvmpt 6191 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝐴(,)𝐵) → ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑧) = -(1 / 𝑧)) |
79 | 74, 78 | breqan12d 4599 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑦) < ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑧) ↔ -(1 / 𝑦) < -(1 / 𝑧))) |
80 | 79 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → (((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑦) < ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑧) ↔ -(1 / 𝑦) < -(1 / 𝑧))) |
81 | 69, 70, 80 | 3bitr4d 299 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → (𝑦 < 𝑧 ↔ ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑦) < ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑧))) |
82 | 81 | biimpd 218 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵))) → (𝑦 < 𝑧 → ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑦) < ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑧))) |
83 | 82 | ralrimivva 2954 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
∀𝑦 ∈ (𝐴(,)𝐵)∀𝑧 ∈ (𝐴(,)𝐵)(𝑦 < 𝑧 → ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑦) < ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑧))) |
84 | | soisoi 6478 |
. . . . . 6
⊢ ((( <
Or (𝐴(,)𝐵) ∧ < Po ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) ∧ ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)):(𝐴(,)𝐵)–onto→ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) ∧ ∀𝑦 ∈ (𝐴(,)𝐵)∀𝑧 ∈ (𝐴(,)𝐵)(𝑦 < 𝑧 → ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑦) < ((𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))‘𝑧)))) → (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) Isom < , < ((𝐴(,)𝐵), ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)))) |
85 | 44, 57, 62, 83, 84 | syl22anc 1319 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) Isom < , < ((𝐴(,)𝐵), ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)))) |
86 | | reelprrecn 9907 |
. . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} |
87 | 86 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ℝ
∈ {ℝ, ℂ}) |
88 | | relogcl 24126 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
89 | 88 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ ℝ+)
→ (log‘𝑥) ∈
ℝ) |
90 | 89 | recnd 9947 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ ℝ+)
→ (log‘𝑥) ∈
ℂ) |
91 | 90 | negcld 10258 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ ℝ+)
→ -(log‘𝑥)
∈ ℂ) |
92 | 58 | a1i 11 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ ℝ+)
→ -(1 / 𝑥) ∈
V) |
93 | | ovex 6577 |
. . . . . . . . 9
⊢ (1 /
𝑥) ∈
V |
94 | 93 | a1i 11 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) ∧ 𝑥 ∈ ℝ+)
→ (1 / 𝑥) ∈
V) |
95 | | dvrelog 24183 |
. . . . . . . . 9
⊢ (ℝ
D (log ↾ ℝ+)) = (𝑥 ∈ ℝ+ ↦ (1 /
𝑥)) |
96 | | relogf1o 24117 |
. . . . . . . . . . . . 13
⊢ (log
↾ ℝ+):ℝ+–1-1-onto→ℝ |
97 | | f1of 6050 |
. . . . . . . . . . . . 13
⊢ ((log
↾ ℝ+):ℝ+–1-1-onto→ℝ → (log ↾
ℝ+):ℝ+⟶ℝ) |
98 | 96, 97 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (log
↾
ℝ+):ℝ+⟶ℝ) |
99 | 98 | feqmptd 6159 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (log
↾ ℝ+) = (𝑥 ∈ ℝ+ ↦ ((log
↾ ℝ+)‘𝑥))) |
100 | | fvres 6117 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ ((log ↾ ℝ+)‘𝑥) = (log‘𝑥)) |
101 | 100 | mpteq2ia 4668 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
↦ ((log ↾ ℝ+)‘𝑥)) = (𝑥 ∈ ℝ+ ↦
(log‘𝑥)) |
102 | 99, 101 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (log
↾ ℝ+) = (𝑥 ∈ ℝ+ ↦
(log‘𝑥))) |
103 | 102 | oveq2d 6565 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (ℝ
D (log ↾ ℝ+)) = (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘𝑥)))) |
104 | 95, 103 | syl5reqr 2659 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (ℝ
D (𝑥 ∈
ℝ+ ↦ (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (1 /
𝑥))) |
105 | 87, 90, 94, 104 | dvmptneg 23535 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (ℝ
D (𝑥 ∈
ℝ+ ↦ -(log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ -(1 /
𝑥))) |
106 | | eqid 2610 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
107 | 106 | tgioo2 22414 |
. . . . . . 7
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
108 | | iccntr 22432 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
109 | 2, 4, 108 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
110 | 87, 91, 92, 105, 15, 107, 106, 109 | dvmptres2 23531 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (ℝ
D (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) |
111 | | isoeq1 6467 |
. . . . . 6
⊢ ((ℝ
D (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) → ((ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))) Isom < , < ((𝐴(,)𝐵), ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) ↔ (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) Isom < , < ((𝐴(,)𝐵), ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))))) |
112 | 110, 111 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
((ℝ D (𝑥 ∈
(𝐴[,]𝐵) ↦ -(log‘𝑥))) Isom < , < ((𝐴(,)𝐵), ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))) ↔ (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)) Isom < , < ((𝐴(,)𝐵), ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥))))) |
113 | 85, 112 | mpbird 246 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (ℝ
D (𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))) Isom < , < ((𝐴(,)𝐵), ran (𝑥 ∈ (𝐴(,)𝐵) ↦ -(1 / 𝑥)))) |
114 | | simpr 476 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝑇 ∈
(0(,)1)) |
115 | | eqid 2610 |
. . . 4
⊢ ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) = ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) |
116 | 2, 4, 5, 39, 113, 114, 115 | dvcvx 23587 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < ((𝑇 · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐴)) + ((1 − 𝑇) · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐵)))) |
117 | | ax-1cn 9873 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
118 | | elioore 12076 |
. . . . . . . . . 10
⊢ (𝑇 ∈ (0(,)1) → 𝑇 ∈
ℝ) |
119 | 118 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝑇 ∈
ℝ) |
120 | 119 | recnd 9947 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝑇 ∈
ℂ) |
121 | | nncan 10189 |
. . . . . . . 8
⊢ ((1
∈ ℂ ∧ 𝑇
∈ ℂ) → (1 − (1 − 𝑇)) = 𝑇) |
122 | 117, 120,
121 | sylancr 694 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (1
− (1 − 𝑇)) =
𝑇) |
123 | 122 | oveq1d 6564 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((1
− (1 − 𝑇))
· 𝐴) = (𝑇 · 𝐴)) |
124 | 123 | oveq1d 6564 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (((1
− (1 − 𝑇))
· 𝐴) + ((1 −
𝑇) · 𝐵)) = ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) |
125 | | ioossicc 12130 |
. . . . . . . 8
⊢ (0(,)1)
⊆ (0[,]1) |
126 | 125, 114 | sseldi 3566 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝑇 ∈
(0[,]1)) |
127 | | iirev 22536 |
. . . . . . 7
⊢ (𝑇 ∈ (0[,]1) → (1
− 𝑇) ∈
(0[,]1)) |
128 | 126, 127 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (1
− 𝑇) ∈
(0[,]1)) |
129 | | lincmb01cmp 12186 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ (1 − 𝑇) ∈ (0[,]1)) → (((1 − (1
− 𝑇)) · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝐴[,]𝐵)) |
130 | 2, 4, 5, 128, 129 | syl31anc 1321 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (((1
− (1 − 𝑇))
· 𝐴) + ((1 −
𝑇) · 𝐵)) ∈ (𝐴[,]𝐵)) |
131 | 124, 130 | eqeltrrd 2689 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝐴[,]𝐵)) |
132 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) → (log‘𝑥) = (log‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))) |
133 | 132 | negeqd 10154 |
. . . . 5
⊢ (𝑥 = ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) → -(log‘𝑥) = -(log‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))) |
134 | | negex 10158 |
. . . . 5
⊢
-(log‘((𝑇
· 𝐴) + ((1 −
𝑇) · 𝐵))) ∈ V |
135 | 133, 19, 134 | fvmpt 6191 |
. . . 4
⊢ (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = -(log‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))) |
136 | 131, 135 | syl 17 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = -(log‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))) |
137 | 1 | rpxrd 11749 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐴 ∈
ℝ*) |
138 | 3 | rpxrd 11749 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐵 ∈
ℝ*) |
139 | 2, 4, 5 | ltled 10064 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐴 ≤ 𝐵) |
140 | | lbicc2 12159 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) |
141 | 137, 138,
139, 140 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐴 ∈ (𝐴[,]𝐵)) |
142 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (log‘𝑥) = (log‘𝐴)) |
143 | 142 | negeqd 10154 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → -(log‘𝑥) = -(log‘𝐴)) |
144 | | negex 10158 |
. . . . . . . . 9
⊢
-(log‘𝐴)
∈ V |
145 | 143, 19, 144 | fvmpt 6191 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐴) = -(log‘𝐴)) |
146 | 141, 145 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐴) = -(log‘𝐴)) |
147 | 146 | oveq2d 6565 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑇 · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐴)) = (𝑇 · -(log‘𝐴))) |
148 | 1 | relogcld 24173 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
(log‘𝐴) ∈
ℝ) |
149 | 148 | recnd 9947 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
(log‘𝐴) ∈
ℂ) |
150 | 120, 149 | mulneg2d 10363 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑇 · -(log‘𝐴)) = -(𝑇 · (log‘𝐴))) |
151 | 147, 150 | eqtrd 2644 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑇 · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐴)) = -(𝑇 · (log‘𝐴))) |
152 | | ubicc2 12160 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) |
153 | 137, 138,
139, 152 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → 𝐵 ∈ (𝐴[,]𝐵)) |
154 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → (log‘𝑥) = (log‘𝐵)) |
155 | 154 | negeqd 10154 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → -(log‘𝑥) = -(log‘𝐵)) |
156 | | negex 10158 |
. . . . . . . . 9
⊢
-(log‘𝐵)
∈ V |
157 | 155, 19, 156 | fvmpt 6191 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐵) = -(log‘𝐵)) |
158 | 153, 157 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐵) = -(log‘𝐵)) |
159 | 158 | oveq2d 6565 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((1
− 𝑇) · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐵)) = ((1 − 𝑇) · -(log‘𝐵))) |
160 | | 1re 9918 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
161 | | resubcl 10224 |
. . . . . . . . 9
⊢ ((1
∈ ℝ ∧ 𝑇
∈ ℝ) → (1 − 𝑇) ∈ ℝ) |
162 | 160, 119,
161 | sylancr 694 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (1
− 𝑇) ∈
ℝ) |
163 | 162 | recnd 9947 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (1
− 𝑇) ∈
ℂ) |
164 | 3 | relogcld 24173 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
(log‘𝐵) ∈
ℝ) |
165 | 164 | recnd 9947 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
(log‘𝐵) ∈
ℂ) |
166 | 163, 165 | mulneg2d 10363 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((1
− 𝑇) ·
-(log‘𝐵)) = -((1
− 𝑇) ·
(log‘𝐵))) |
167 | 159, 166 | eqtrd 2644 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((1
− 𝑇) · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐵)) = -((1 − 𝑇) · (log‘𝐵))) |
168 | 151, 167 | oveq12d 6567 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑇 · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐴)) + ((1 − 𝑇) · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐵))) = (-(𝑇 · (log‘𝐴)) + -((1 − 𝑇) · (log‘𝐵)))) |
169 | 119, 148 | remulcld 9949 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑇 · (log‘𝐴)) ∈
ℝ) |
170 | 169 | recnd 9947 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (𝑇 · (log‘𝐴)) ∈
ℂ) |
171 | 162, 164 | remulcld 9949 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((1
− 𝑇) ·
(log‘𝐵)) ∈
ℝ) |
172 | 171 | recnd 9947 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((1
− 𝑇) ·
(log‘𝐵)) ∈
ℂ) |
173 | 170, 172 | negdid 10284 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → -((𝑇 · (log‘𝐴)) + ((1 − 𝑇) · (log‘𝐵))) = (-(𝑇 · (log‘𝐴)) + -((1 − 𝑇) · (log‘𝐵)))) |
174 | 168, 173 | eqtr4d 2647 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑇 · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐴)) + ((1 − 𝑇) · ((𝑥 ∈ (𝐴[,]𝐵) ↦ -(log‘𝑥))‘𝐵))) = -((𝑇 · (log‘𝐴)) + ((1 − 𝑇) · (log‘𝐵)))) |
175 | 116, 136,
174 | 3brtr3d 4614 |
. 2
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
-(log‘((𝑇 ·
𝐴) + ((1 − 𝑇) · 𝐵))) < -((𝑇 · (log‘𝐴)) + ((1 − 𝑇) · (log‘𝐵)))) |
176 | 169, 171 | readdcld 9948 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑇 · (log‘𝐴)) + ((1 − 𝑇) · (log‘𝐵))) ∈
ℝ) |
177 | 15, 131 | sseldd 3569 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈
ℝ+) |
178 | 177 | relogcld 24173 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) →
(log‘((𝑇 ·
𝐴) + ((1 − 𝑇) · 𝐵))) ∈ ℝ) |
179 | 176, 178 | ltnegd 10484 |
. 2
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (((𝑇 · (log‘𝐴)) + ((1 − 𝑇) · (log‘𝐵))) < (log‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) ↔ -(log‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < -((𝑇 · (log‘𝐴)) + ((1 − 𝑇) · (log‘𝐵))))) |
180 | 175, 179 | mpbird 246 |
1
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+ ∧ 𝐴
< 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑇 · (log‘𝐴)) + ((1 − 𝑇) · (log‘𝐵))) < (log‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))) |