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 
|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )
divcncf.2 
|- ( ph -> ( x e. X |-> B ) e. ( X -cn-> ( CC \ { 0 } ) ) )
Assertion divcncf 
|- ( ph -> ( x e. X |-> ( A / B ) ) e. ( X -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 divcncf.1 
 |-  ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )
2 divcncf.2 
 |-  ( ph -> ( x e. X |-> B ) e. ( X -cn-> ( CC \ { 0 } ) ) )
3 cncff 
 |-  ( ( x e. X |-> A ) e. ( X -cn-> CC ) -> ( x e. X |-> A ) : X --> CC )
4 1 3 syl 
 |-  ( ph -> ( x e. X |-> A ) : X --> CC )
5 4 fvmptelrn 
 |-  ( ( ph /\ x e. X ) -> A e. CC )
6 cncff 
 |-  ( ( x e. X |-> B ) e. ( X -cn-> ( CC \ { 0 } ) ) -> ( x e. X |-> B ) : X --> ( CC \ { 0 } ) )
7 2 6 syl 
 |-  ( ph -> ( x e. X |-> B ) : X --> ( CC \ { 0 } ) )
8 7 fvmptelrn 
 |-  ( ( ph /\ x e. X ) -> B e. ( CC \ { 0 } ) )
9 8 eldifad 
 |-  ( ( ph /\ x e. X ) -> B e. CC )
10 eldifsni 
 |-  ( B e. ( CC \ { 0 } ) -> B =/= 0 )
11 8 10 syl 
 |-  ( ( ph /\ x e. X ) -> B =/= 0 )
12 5 9 11 divrecd 
 |-  ( ( ph /\ x e. X ) -> ( A / B ) = ( A x. ( 1 / B ) ) )
13 12 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( A / B ) ) = ( x e. X |-> ( A x. ( 1 / B ) ) ) )
14 8 ralrimiva 
 |-  ( ph -> A. x e. X B e. ( CC \ { 0 } ) )
15 eqidd 
 |-  ( ph -> ( x e. X |-> B ) = ( x e. X |-> B ) )
16 eqidd 
 |-  ( ph -> ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) = ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) )
17 14 15 16 fmptcos 
 |-  ( ph -> ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) o. ( x e. X |-> B ) ) = ( x e. X |-> [_ B / y ]_ ( 1 / y ) ) )
18 csbov2g 
 |-  ( B e. CC -> [_ B / y ]_ ( 1 / y ) = ( 1 / [_ B / y ]_ y ) )
19 9 18 syl 
 |-  ( ( ph /\ x e. X ) -> [_ B / y ]_ ( 1 / y ) = ( 1 / [_ B / y ]_ y ) )
20 csbvarg 
 |-  ( B e. CC -> [_ B / y ]_ y = B )
21 9 20 syl 
 |-  ( ( ph /\ x e. X ) -> [_ B / y ]_ y = B )
22 21 oveq2d 
 |-  ( ( ph /\ x e. X ) -> ( 1 / [_ B / y ]_ y ) = ( 1 / B ) )
23 19 22 eqtrd 
 |-  ( ( ph /\ x e. X ) -> [_ B / y ]_ ( 1 / y ) = ( 1 / B ) )
24 23 mpteq2dva 
 |-  ( ph -> ( x e. X |-> [_ B / y ]_ ( 1 / y ) ) = ( x e. X |-> ( 1 / B ) ) )
25 17 24 eqtr2d 
 |-  ( ph -> ( x e. X |-> ( 1 / B ) ) = ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) o. ( x e. X |-> B ) ) )
26 ax-1cn 
 |-  1 e. CC
27 eqid 
 |-  ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) = ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) )
28 27 cdivcncf 
 |-  ( 1 e. CC -> ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) e. ( ( CC \ { 0 } ) -cn-> CC ) )
29 26 28 mp1i 
 |-  ( ph -> ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) e. ( ( CC \ { 0 } ) -cn-> CC ) )
30 2 29 cncfco 
 |-  ( ph -> ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) o. ( x e. X |-> B ) ) e. ( X -cn-> CC ) )
31 25 30 eqeltrd 
 |-  ( ph -> ( x e. X |-> ( 1 / B ) ) e. ( X -cn-> CC ) )
32 1 31 mulcncf 
 |-  ( ph -> ( x e. X |-> ( A x. ( 1 / B ) ) ) e. ( X -cn-> CC ) )
33 13 32 eqeltrd 
 |-  ( ph -> ( x e. X |-> ( A / B ) ) e. ( X -cn-> CC ) )