Theorem divcncf

Description: The quotient of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	divcncf.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ ℂ ) )
	divcncf.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝑋 –cn→ ( ℂ ∖ { 0 } ) ) )
Assertion	divcncf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐵 ) ) ∈ ( 𝑋 –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		divcncf.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ ℂ ) )
2		divcncf.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝑋 –cn→ ( ℂ ∖ { 0 } ) ) )
3		cncff	⊢ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ ℂ ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ )
4	1 3	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ )
5	4	fvmptelrn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
6		cncff	⊢ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝑋 –cn→ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ( ℂ ∖ { 0 } ) )
7	2 6	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ( ℂ ∖ { 0 } ) )
8	7	fvmptelrn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ( ℂ ∖ { 0 } ) )
9	8	eldifad	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ℂ )
10		eldifsni	⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 } ) → 𝐵 ≠ 0 )
11	8 10	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ≠ 0 )
12	5 9 11	divrecd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 / 𝐵 ) = ( 𝐴 · ( 1 / 𝐵 ) ) )
13	12	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐵 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · ( 1 / 𝐵 ) ) ) )
14	8	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐵 ∈ ( ℂ ∖ { 0 } ) )
15		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
16		eqidd	⊢ ( 𝜑 → ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) )
17	14 15 16	fmptcos	⊢ ( 𝜑 → ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝐵 / 𝑦 ⦌ ( 1 / 𝑦 ) ) )
18		csbov2g	⊢ ( 𝐵 ∈ ℂ → ⦋ 𝐵 / 𝑦 ⦌ ( 1 / 𝑦 ) = ( 1 / ⦋ 𝐵 / 𝑦 ⦌ 𝑦 ) )
19	9 18	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ⦋ 𝐵 / 𝑦 ⦌ ( 1 / 𝑦 ) = ( 1 / ⦋ 𝐵 / 𝑦 ⦌ 𝑦 ) )
20		csbvarg	⊢ ( 𝐵 ∈ ℂ → ⦋ 𝐵 / 𝑦 ⦌ 𝑦 = 𝐵 )
21	9 20	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ⦋ 𝐵 / 𝑦 ⦌ 𝑦 = 𝐵 )
22	21	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 1 / ⦋ 𝐵 / 𝑦 ⦌ 𝑦 ) = ( 1 / 𝐵 ) )
23	19 22	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ⦋ 𝐵 / 𝑦 ⦌ ( 1 / 𝑦 ) = ( 1 / 𝐵 ) )
24	23	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ⦋ 𝐵 / 𝑦 ⦌ ( 1 / 𝑦 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 1 / 𝐵 ) ) )
25	17 24	eqtr2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 1 / 𝐵 ) ) = ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ) )
26		ax-1cn	⊢ 1 ∈ ℂ
27		eqid	⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) )
28	27	cdivcncf	⊢ ( 1 ∈ ℂ → ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ∈ ( ( ℂ ∖ { 0 } ) –cn→ ℂ ) )
29	26 28	mp1i	⊢ ( 𝜑 → ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ∈ ( ( ℂ ∖ { 0 } ) –cn→ ℂ ) )
30	2 29	cncfco	⊢ ( 𝜑 → ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ) ∈ ( 𝑋 –cn→ ℂ ) )
31	25 30	eqeltrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 1 / 𝐵 ) ) ∈ ( 𝑋 –cn→ ℂ ) )
32	1 31	mulcncf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · ( 1 / 𝐵 ) ) ) ∈ ( 𝑋 –cn→ ℂ ) )
33	13 32	eqeltrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐵 ) ) ∈ ( 𝑋 –cn→ ℂ ) )