This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 cncfcdm ⊢ ( ( ℝ ⊆ ℂ ∧ ( log ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℂ ) ) → ( ( log ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℝ ) ↔ ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ ) )
15 4 13 14 mp2an ⊢ ( ( log ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℝ ) ↔ ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ )
16 3 15 mpbir ⊢ ( log ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℝ )