# Metamath Proof Explorer

## Theorem dvdivf

Description: The quotient rule for everywhere-differentiable functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dvdivf.s
`|- ( ph -> S e. { RR , CC } )`
dvdivf.f
`|- ( ph -> F : X --> CC )`
dvdivf.g
`|- ( ph -> G : X --> ( CC \ { 0 } ) )`
dvdivf.fdv
`|- ( ph -> dom ( S _D F ) = X )`
dvdivf.gdv
`|- ( ph -> dom ( S _D G ) = X )`
Assertion dvdivf
`|- ( ph -> ( S _D ( F oF / G ) ) = ( ( ( ( S _D F ) oF x. G ) oF - ( ( S _D G ) oF x. F ) ) oF / ( G oF x. G ) ) )`

### Proof

Step Hyp Ref Expression
1 dvdivf.s
` |-  ( ph -> S e. { RR , CC } )`
2 dvdivf.f
` |-  ( ph -> F : X --> CC )`
3 dvdivf.g
` |-  ( ph -> G : X --> ( CC \ { 0 } ) )`
4 dvdivf.fdv
` |-  ( ph -> dom ( S _D F ) = X )`
5 dvdivf.gdv
` |-  ( ph -> dom ( S _D G ) = X )`
6 2 ffvelrnda
` |-  ( ( ph /\ x e. X ) -> ( F ` x ) e. CC )`
7 dvfg
` |-  ( S e. { RR , CC } -> ( S _D F ) : dom ( S _D F ) --> CC )`
8 1 7 syl
` |-  ( ph -> ( S _D F ) : dom ( S _D F ) --> CC )`
9 4 feq2d
` |-  ( ph -> ( ( S _D F ) : dom ( S _D F ) --> CC <-> ( S _D F ) : X --> CC ) )`
10 8 9 mpbid
` |-  ( ph -> ( S _D F ) : X --> CC )`
11 10 ffvelrnda
` |-  ( ( ph /\ x e. X ) -> ( ( S _D F ) ` x ) e. CC )`
12 2 feqmptd
` |-  ( ph -> F = ( x e. X |-> ( F ` x ) ) )`
13 12 oveq2d
` |-  ( ph -> ( S _D F ) = ( S _D ( x e. X |-> ( F ` x ) ) ) )`
14 10 feqmptd
` |-  ( ph -> ( S _D F ) = ( x e. X |-> ( ( S _D F ) ` x ) ) )`
15 13 14 eqtr3d
` |-  ( ph -> ( S _D ( x e. X |-> ( F ` x ) ) ) = ( x e. X |-> ( ( S _D F ) ` x ) ) )`
16 3 ffvelrnda
` |-  ( ( ph /\ x e. X ) -> ( G ` x ) e. ( CC \ { 0 } ) )`
17 dvfg
` |-  ( S e. { RR , CC } -> ( S _D G ) : dom ( S _D G ) --> CC )`
18 1 17 syl
` |-  ( ph -> ( S _D G ) : dom ( S _D G ) --> CC )`
19 5 feq2d
` |-  ( ph -> ( ( S _D G ) : dom ( S _D G ) --> CC <-> ( S _D G ) : X --> CC ) )`
20 18 19 mpbid
` |-  ( ph -> ( S _D G ) : X --> CC )`
21 20 ffvelrnda
` |-  ( ( ph /\ x e. X ) -> ( ( S _D G ) ` x ) e. CC )`
22 3 feqmptd
` |-  ( ph -> G = ( x e. X |-> ( G ` x ) ) )`
23 22 oveq2d
` |-  ( ph -> ( S _D G ) = ( S _D ( x e. X |-> ( G ` x ) ) ) )`
24 20 feqmptd
` |-  ( ph -> ( S _D G ) = ( x e. X |-> ( ( S _D G ) ` x ) ) )`
25 23 24 eqtr3d
` |-  ( ph -> ( S _D ( x e. X |-> ( G ` x ) ) ) = ( x e. X |-> ( ( S _D G ) ` x ) ) )`
26 1 6 11 15 16 21 25 dvmptdiv
` |-  ( ph -> ( S _D ( x e. X |-> ( ( F ` x ) / ( G ` x ) ) ) ) = ( x e. X |-> ( ( ( ( ( S _D F ) ` x ) x. ( G ` x ) ) - ( ( ( S _D G ) ` x ) x. ( F ` x ) ) ) / ( ( G ` x ) ^ 2 ) ) ) )`
27 ovex
` |-  ( S _D F ) e. _V`
28 27 dmex
` |-  dom ( S _D F ) e. _V`
29 4 28 eqeltrrdi
` |-  ( ph -> X e. _V )`
30 29 6 16 12 22 offval2
` |-  ( ph -> ( F oF / G ) = ( x e. X |-> ( ( F ` x ) / ( G ` x ) ) ) )`
31 30 oveq2d
` |-  ( ph -> ( S _D ( F oF / G ) ) = ( S _D ( x e. X |-> ( ( F ` x ) / ( G ` x ) ) ) ) )`
32 ovexd
` |-  ( ( ph /\ x e. X ) -> ( ( ( ( S _D F ) ` x ) x. ( G ` x ) ) - ( ( ( S _D G ) ` x ) x. ( F ` x ) ) ) e. _V )`
` |-  ( ( ph /\ x e. X ) -> ( G ` x ) e. CC )`
34 33 sqcld
` |-  ( ( ph /\ x e. X ) -> ( ( G ` x ) ^ 2 ) e. CC )`
35 11 33 mulcld
` |-  ( ( ph /\ x e. X ) -> ( ( ( S _D F ) ` x ) x. ( G ` x ) ) e. CC )`
36 21 6 mulcld
` |-  ( ( ph /\ x e. X ) -> ( ( ( S _D G ) ` x ) x. ( F ` x ) ) e. CC )`
37 29 11 33 14 22 offval2
` |-  ( ph -> ( ( S _D F ) oF x. G ) = ( x e. X |-> ( ( ( S _D F ) ` x ) x. ( G ` x ) ) ) )`
38 29 21 6 24 12 offval2
` |-  ( ph -> ( ( S _D G ) oF x. F ) = ( x e. X |-> ( ( ( S _D G ) ` x ) x. ( F ` x ) ) ) )`
39 29 35 36 37 38 offval2
` |-  ( ph -> ( ( ( S _D F ) oF x. G ) oF - ( ( S _D G ) oF x. F ) ) = ( x e. X |-> ( ( ( ( S _D F ) ` x ) x. ( G ` x ) ) - ( ( ( S _D G ) ` x ) x. ( F ` x ) ) ) ) )`
40 29 16 16 22 22 offval2
` |-  ( ph -> ( G oF x. G ) = ( x e. X |-> ( ( G ` x ) x. ( G ` x ) ) ) )`
41 33 sqvald
` |-  ( ( ph /\ x e. X ) -> ( ( G ` x ) ^ 2 ) = ( ( G ` x ) x. ( G ` x ) ) )`
42 41 mpteq2dva
` |-  ( ph -> ( x e. X |-> ( ( G ` x ) ^ 2 ) ) = ( x e. X |-> ( ( G ` x ) x. ( G ` x ) ) ) )`
43 40 42 eqtr4d
` |-  ( ph -> ( G oF x. G ) = ( x e. X |-> ( ( G ` x ) ^ 2 ) ) )`
44 29 32 34 39 43 offval2
` |-  ( ph -> ( ( ( ( S _D F ) oF x. G ) oF - ( ( S _D G ) oF x. F ) ) oF / ( G oF x. G ) ) = ( x e. X |-> ( ( ( ( ( S _D F ) ` x ) x. ( G ` x ) ) - ( ( ( S _D G ) ` x ) x. ( F ` x ) ) ) / ( ( G ` x ) ^ 2 ) ) ) )`
45 26 31 44 3eqtr4d
` |-  ( ph -> ( S _D ( F oF / G ) ) = ( ( ( ( S _D F ) oF x. G ) oF - ( ( S _D G ) oF x. F ) ) oF / ( G oF x. G ) ) )`