Step |
Hyp |
Ref |
Expression |
1 |
|
dvrelog3.1 |
⊢ ( 𝜑 → 𝐴 ∈ ℝ* ) |
2 |
|
dvrelog3.2 |
⊢ ( 𝜑 → 𝐵 ∈ ℝ* ) |
3 |
|
dvrelog3.3 |
⊢ ( 𝜑 → 0 ≤ 𝐴 ) |
4 |
|
dvrelog3.4 |
⊢ ( 𝜑 → 𝐴 ≤ 𝐵 ) |
5 |
|
dvrelog3.5 |
⊢ 𝐹 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( log ‘ 𝑥 ) ) |
6 |
|
dvrelog3.6 |
⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) ) |
7 |
5
|
a1i |
⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( log ‘ 𝑥 ) ) ) |
8 |
7
|
oveq2d |
⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( log ‘ 𝑥 ) ) ) ) |
9 |
|
reelprrecn |
⊢ ℝ ∈ { ℝ , ℂ } |
10 |
9
|
a1i |
⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } ) |
11 |
|
rpcn |
⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ ) |
12 |
11
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ ) |
13 |
|
rpne0 |
⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ≠ 0 ) |
14 |
13
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ≠ 0 ) |
15 |
12 14
|
logcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℂ ) |
16 |
|
1red |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 1 ∈ ℝ ) |
17 |
|
rpre |
⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ ) |
18 |
17
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ ) |
19 |
16 18 14
|
redivcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 / 𝑥 ) ∈ ℝ ) |
20 |
|
logf1o |
⊢ log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log |
21 |
|
f1of |
⊢ ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → log : ( ℂ ∖ { 0 } ) ⟶ ran log ) |
22 |
20 21
|
ax-mp |
⊢ log : ( ℂ ∖ { 0 } ) ⟶ ran log |
23 |
22
|
a1i |
⊢ ( 𝜑 → log : ( ℂ ∖ { 0 } ) ⟶ ran log ) |
24 |
|
0nrp |
⊢ ¬ 0 ∈ ℝ+ |
25 |
|
disjsn |
⊢ ( ( ℝ+ ∩ { 0 } ) = ∅ ↔ ¬ 0 ∈ ℝ+ ) |
26 |
24 25
|
mpbir |
⊢ ( ℝ+ ∩ { 0 } ) = ∅ |
27 |
|
disjdif2 |
⊢ ( ( ℝ+ ∩ { 0 } ) = ∅ → ( ℝ+ ∖ { 0 } ) = ℝ+ ) |
28 |
26 27
|
ax-mp |
⊢ ( ℝ+ ∖ { 0 } ) = ℝ+ |
29 |
|
rpssre |
⊢ ℝ+ ⊆ ℝ |
30 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
31 |
29 30
|
sstri |
⊢ ℝ+ ⊆ ℂ |
32 |
|
ssdif |
⊢ ( ℝ+ ⊆ ℂ → ( ℝ+ ∖ { 0 } ) ⊆ ( ℂ ∖ { 0 } ) ) |
33 |
31 32
|
ax-mp |
⊢ ( ℝ+ ∖ { 0 } ) ⊆ ( ℂ ∖ { 0 } ) |
34 |
28 33
|
eqsstrri |
⊢ ℝ+ ⊆ ( ℂ ∖ { 0 } ) |
35 |
34
|
a1i |
⊢ ( 𝜑 → ℝ+ ⊆ ( ℂ ∖ { 0 } ) ) |
36 |
23 35
|
feqresmpt |
⊢ ( 𝜑 → ( log ↾ ℝ+ ) = ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ) |
37 |
36
|
eqcomd |
⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) = ( log ↾ ℝ+ ) ) |
38 |
37
|
oveq2d |
⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ) = ( ℝ D ( log ↾ ℝ+ ) ) ) |
39 |
|
dvrelog |
⊢ ( ℝ D ( log ↾ ℝ+ ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) |
40 |
39
|
a1i |
⊢ ( 𝜑 → ( ℝ D ( log ↾ ℝ+ ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ) |
41 |
38 40
|
eqtrd |
⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ) |
42 |
|
elioo2 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴 < 𝑦 ∧ 𝑦 < 𝐵 ) ) ) |
43 |
1 2 42
|
syl2anc |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴 < 𝑦 ∧ 𝑦 < 𝐵 ) ) ) |
44 |
43
|
biimpa |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑦 ∈ ℝ ∧ 𝐴 < 𝑦 ∧ 𝑦 < 𝐵 ) ) |
45 |
44
|
simp1d |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ℝ ) |
46 |
|
0red |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ∈ ℝ ) |
47 |
46
|
rexrd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ∈ ℝ* ) |
48 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ* ) |
49 |
45
|
rexrd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ℝ* ) |
50 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ≤ 𝐴 ) |
51 |
44
|
simp2d |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < 𝑦 ) |
52 |
47 48 49 50 51
|
xrlelttrd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 < 𝑦 ) |
53 |
45 52
|
jca |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑦 ∈ ℝ ∧ 0 < 𝑦 ) ) |
54 |
|
elrp |
⊢ ( 𝑦 ∈ ℝ+ ↔ ( 𝑦 ∈ ℝ ∧ 0 < 𝑦 ) ) |
55 |
53 54
|
sylibr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ℝ+ ) |
56 |
55
|
ex |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) → 𝑦 ∈ ℝ+ ) ) |
57 |
56
|
ssrdv |
⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ+ ) |
58 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
59 |
58
|
tgioo2 |
⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) |
60 |
|
retop |
⊢ ( topGen ‘ ran (,) ) ∈ Top |
61 |
60
|
a1i |
⊢ ( 𝜑 → ( topGen ‘ ran (,) ) ∈ Top ) |
62 |
|
iooretop |
⊢ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) |
63 |
62
|
a1i |
⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) ) |
64 |
|
isopn3i |
⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) ) |
65 |
61 63 64
|
syl2anc |
⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) ) |
66 |
10 15 19 41 57 59 58 65
|
dvmptres2 |
⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( log ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) ) ) |
67 |
8 66
|
eqtrd |
⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) ) ) |
68 |
6
|
a1i |
⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) ) ) |
69 |
68
|
eqcomd |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) ) = 𝐺 ) |
70 |
67 69
|
eqtrd |
⊢ ( 𝜑 → ( ℝ D 𝐹 ) = 𝐺 ) |