Theorem divcncff

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

	Ref	Expression
Hypotheses	divcncff.f	|- ( ph -> F e. ( X -cn-> CC ) )
	divcncff.g	|- ( ph -> G e. ( X -cn-> ( CC \ { 0 } ) ) )
Assertion	divcncff	|- ( ph -> ( F oF / G ) e. ( X -cn-> CC ) )

Proof

Step	Hyp	Ref	Expression
1		divcncff.f	|- ( ph -> F e. ( X -cn-> CC ) )
2		divcncff.g	|- ( ph -> G e. ( X -cn-> ( CC \ { 0 } ) ) )
3		cncfrss	|- ( F e. ( X -cn-> CC ) -> X C_ CC )
4		cnex	|- CC e. _V
5	4	ssex	|- ( X C_ CC -> X e. _V )
6	1 3 5	3syl	|- ( ph -> X e. _V )
7		cncff	|- ( F e. ( X -cn-> CC ) -> F : X --> CC )
8	1 7	syl	|- ( ph -> F : X --> CC )
9	8	ffvelrnda	|- ( ( ph /\ x e. X ) -> ( F ` x ) e. CC )
10		cncff	|- ( G e. ( X -cn-> ( CC \ { 0 } ) ) -> G : X --> ( CC \ { 0 } ) )
11	2 10	syl	|- ( ph -> G : X --> ( CC \ { 0 } ) )
12	11	ffvelrnda	|- ( ( ph /\ x e. X ) -> ( G ` x ) e. ( CC \ { 0 } ) )
13	8	feqmptd	|- ( ph -> F = ( x e. X |-> ( F ` x ) ) )
14	11	feqmptd	|- ( ph -> G = ( x e. X |-> ( G ` x ) ) )
15	6 9 12 13 14	offval2	|- ( ph -> ( F oF / G ) = ( x e. X |-> ( ( F ` x ) / ( G ` x ) ) ) )
16	13 1	eqeltrrd	|- ( ph -> ( x e. X |-> ( F ` x ) ) e. ( X -cn-> CC ) )
17	14 2	eqeltrrd	|- ( ph -> ( x e. X |-> ( G ` x ) ) e. ( X -cn-> ( CC \ { 0 } ) ) )
18	16 17	divcncf	|- ( ph -> ( x e. X |-> ( ( F ` x ) / ( G ` x ) ) ) e. ( X -cn-> CC ) )
19	15 18	eqeltrd	|- ( ph -> ( F oF / G ) e. ( X -cn-> CC ) )