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

Metamath Proof Explorer

Theorem divccncf

Description: Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007)

Ref Expression
Hypothesis divccncf.1 ⊢ 𝐹 = ( 𝑥 ∈ ℂ ↦ ( 𝑥 / 𝐴 ) )
Assertion divccncf ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐹 ∈ ( ℂ –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 divccncf.1 ⊢ 𝐹 = ( 𝑥 ∈ ℂ ↦ ( 𝑥 / 𝐴 ) )
2 divrec2 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 / 𝐴 ) = ( ( 1 / 𝐴 ) · 𝑥 ) )
3 2 3expb ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) → ( 𝑥 / 𝐴 ) = ( ( 1 / 𝐴 ) · 𝑥 ) )
4 3 ancoms ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℂ ) → ( 𝑥 / 𝐴 ) = ( ( 1 / 𝐴 ) · 𝑥 ) )
5 4 mpteq2dva ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 / 𝐴 ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 1 / 𝐴 ) · 𝑥 ) ) )
6 1 5 eqtrid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐹 = ( 𝑥 ∈ ℂ ↦ ( ( 1 / 𝐴 ) · 𝑥 ) ) )
7 reccl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ∈ ℂ )
8 eqid ⊢ ( 𝑥 ∈ ℂ ↦ ( ( 1 / 𝐴 ) · 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 1 / 𝐴 ) · 𝑥 ) )
9 8 mulc1cncf ⊢ ( ( 1 / 𝐴 ) ∈ ℂ → ( 𝑥 ∈ ℂ ↦ ( ( 1 / 𝐴 ) · 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) )
10 7 9 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ ( ( 1 / 𝐴 ) · 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) )
11 6 10 eqeltrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐹 ∈ ( ℂ –cn→ ℂ ) )