Step |
Hyp |
Ref |
Expression |
1 |
|
relogf1o |
⊢ ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ |
2 |
|
f1of |
⊢ ( ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ → ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ ) |
3 |
1 2
|
ax-mp |
⊢ ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ |
4 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
5 |
|
fss |
⊢ ( ( ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → ( log ↾ ℝ+ ) : ℝ+ ⟶ ℂ ) |
6 |
3 4 5
|
mp2an |
⊢ ( log ↾ ℝ+ ) : ℝ+ ⟶ ℂ |
7 |
|
rpssre |
⊢ ℝ+ ⊆ ℝ |
8 |
|
ovex |
⊢ ( 1 / 𝑥 ) ∈ V |
9 |
|
dvrelog |
⊢ ( ℝ D ( log ↾ ℝ+ ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) |
10 |
8 9
|
dmmpti |
⊢ dom ( ℝ D ( log ↾ ℝ+ ) ) = ℝ+ |
11 |
|
dvcn |
⊢ ( ( ( ℝ ⊆ ℂ ∧ ( log ↾ ℝ+ ) : ℝ+ ⟶ ℂ ∧ ℝ+ ⊆ ℝ ) ∧ dom ( ℝ D ( log ↾ ℝ+ ) ) = ℝ+ ) → ( log ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℂ ) ) |
12 |
10 11
|
mpan2 |
⊢ ( ( ℝ ⊆ ℂ ∧ ( log ↾ ℝ+ ) : ℝ+ ⟶ ℂ ∧ ℝ+ ⊆ ℝ ) → ( log ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℂ ) ) |
13 |
4 6 7 12
|
mp3an |
⊢ ( log ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℂ ) |
14 |
|
cncffvrn |
⊢ ( ( ℝ ⊆ ℂ ∧ ( log ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℂ ) ) → ( ( log ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℝ ) ↔ ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ ) ) |
15 |
4 13 14
|
mp2an |
⊢ ( ( log ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℝ ) ↔ ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ ) |
16 |
3 15
|
mpbir |
⊢ ( log ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℝ ) |