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	syl5eq	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 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→ ℂ ) )