Metamath Proof Explorer


Theorem relogcn

Description: The real logarithm function is continuous. (Contributed by Mario Carneiro, 17-Feb-2015)

Ref Expression
Assertion relogcn ( log ↾ ℝ+ ) ∈ ( ℝ+cn→ ℝ )

Proof

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→ ℝ )