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