Metamath Proof Explorer


Theorem divcncff

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

Ref Expression
Hypotheses divcncff.f ( 𝜑𝐹 ∈ ( 𝑋cn→ ℂ ) )
divcncff.g ( 𝜑𝐺 ∈ ( 𝑋cn→ ( ℂ ∖ { 0 } ) ) )
Assertion divcncff ( 𝜑 → ( 𝐹f / 𝐺 ) ∈ ( 𝑋cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 divcncff.f ( 𝜑𝐹 ∈ ( 𝑋cn→ ℂ ) )
2 divcncff.g ( 𝜑𝐺 ∈ ( 𝑋cn→ ( ℂ ∖ { 0 } ) ) )
3 cncfrss ( 𝐹 ∈ ( 𝑋cn→ ℂ ) → 𝑋 ⊆ ℂ )
4 cnex ℂ ∈ V
5 4 ssex ( 𝑋 ⊆ ℂ → 𝑋 ∈ V )
6 1 3 5 3syl ( 𝜑𝑋 ∈ V )
7 cncff ( 𝐹 ∈ ( 𝑋cn→ ℂ ) → 𝐹 : 𝑋 ⟶ ℂ )
8 1 7 syl ( 𝜑𝐹 : 𝑋 ⟶ ℂ )
9 8 ffvelrnda ( ( 𝜑𝑥𝑋 ) → ( 𝐹𝑥 ) ∈ ℂ )
10 cncff ( 𝐺 ∈ ( 𝑋cn→ ( ℂ ∖ { 0 } ) ) → 𝐺 : 𝑋 ⟶ ( ℂ ∖ { 0 } ) )
11 2 10 syl ( 𝜑𝐺 : 𝑋 ⟶ ( ℂ ∖ { 0 } ) )
12 11 ffvelrnda ( ( 𝜑𝑥𝑋 ) → ( 𝐺𝑥 ) ∈ ( ℂ ∖ { 0 } ) )
13 8 feqmptd ( 𝜑𝐹 = ( 𝑥𝑋 ↦ ( 𝐹𝑥 ) ) )
14 11 feqmptd ( 𝜑𝐺 = ( 𝑥𝑋 ↦ ( 𝐺𝑥 ) ) )
15 6 9 12 13 14 offval2 ( 𝜑 → ( 𝐹f / 𝐺 ) = ( 𝑥𝑋 ↦ ( ( 𝐹𝑥 ) / ( 𝐺𝑥 ) ) ) )
16 13 1 eqeltrrd ( 𝜑 → ( 𝑥𝑋 ↦ ( 𝐹𝑥 ) ) ∈ ( 𝑋cn→ ℂ ) )
17 14 2 eqeltrrd ( 𝜑 → ( 𝑥𝑋 ↦ ( 𝐺𝑥 ) ) ∈ ( 𝑋cn→ ( ℂ ∖ { 0 } ) ) )
18 16 17 divcncf ( 𝜑 → ( 𝑥𝑋 ↦ ( ( 𝐹𝑥 ) / ( 𝐺𝑥 ) ) ) ∈ ( 𝑋cn→ ℂ ) )
19 15 18 eqeltrd ( 𝜑 → ( 𝐹f / 𝐺 ) ∈ ( 𝑋cn→ ℂ ) )