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

Metamath Proof Explorer

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 fvmptelcdm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
6 cncff ⊢ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝑋 –cn→ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ( ℂ ∖ { 0 } ) )
7 2 6 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ( ℂ ∖ { 0 } ) )
8 7 fvmptelcdm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ( ℂ ∖ { 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→ ℂ ) )