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

Metamath Proof Explorer

Theorem dvrecg

Description: Derivative of the reciprocal of a function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dvrecg.s 
|- ( ph -> S e. { RR , CC } )
dvrecg.a 
|- ( ph -> A e. CC )
dvrecg.b 
|- ( ( ph /\ x e. X ) -> B e. ( CC \ { 0 } ) )
dvrecg.c 
|- ( ( ph /\ x e. X ) -> C e. V )
dvrecg.db 
|- ( ph -> ( S _D ( x e. X |-> B ) ) = ( x e. X |-> C ) )
Assertion dvrecg 
|- ( ph -> ( S _D ( x e. X |-> ( A / B ) ) ) = ( x e. X |-> -u ( ( A x. C ) / ( B ^ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 dvrecg.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvrecg.a 
 |-  ( ph -> A e. CC )
3 dvrecg.b 
 |-  ( ( ph /\ x e. X ) -> B e. ( CC \ { 0 } ) )
4 dvrecg.c 
 |-  ( ( ph /\ x e. X ) -> C e. V )
5 dvrecg.db 
 |-  ( ph -> ( S _D ( x e. X |-> B ) ) = ( x e. X |-> C ) )
6 cnelprrecn 
 |-  CC e. { RR , CC }
7 6 a1i 
 |-  ( ph -> CC e. { RR , CC } )
8 2 adantr 
 |-  ( ( ph /\ y e. ( CC \ { 0 } ) ) -> A e. CC )
9 eldifi 
 |-  ( y e. ( CC \ { 0 } ) -> y e. CC )
10 9 adantl 
 |-  ( ( ph /\ y e. ( CC \ { 0 } ) ) -> y e. CC )
11 eldifsni 
 |-  ( y e. ( CC \ { 0 } ) -> y =/= 0 )
12 11 adantl 
 |-  ( ( ph /\ y e. ( CC \ { 0 } ) ) -> y =/= 0 )
13 8 10 12 divcld 
 |-  ( ( ph /\ y e. ( CC \ { 0 } ) ) -> ( A / y ) e. CC )
14 10 sqcld 
 |-  ( ( ph /\ y e. ( CC \ { 0 } ) ) -> ( y ^ 2 ) e. CC )
15 2z 
 |-  2 e. ZZ
16 15 a1i 
 |-  ( ( ph /\ y e. ( CC \ { 0 } ) ) -> 2 e. ZZ )
17 10 12 16 expne0d 
 |-  ( ( ph /\ y e. ( CC \ { 0 } ) ) -> ( y ^ 2 ) =/= 0 )
18 8 14 17 divcld 
 |-  ( ( ph /\ y e. ( CC \ { 0 } ) ) -> ( A / ( y ^ 2 ) ) e. CC )
19 18 negcld 
 |-  ( ( ph /\ y e. ( CC \ { 0 } ) ) -> -u ( A / ( y ^ 2 ) ) e. CC )
20 dvrec 
 |-  ( A e. CC -> ( CC _D ( y e. ( CC \ { 0 } ) |-> ( A / y ) ) ) = ( y e. ( CC \ { 0 } ) |-> -u ( A / ( y ^ 2 ) ) ) )
21 2 20 syl 
 |-  ( ph -> ( CC _D ( y e. ( CC \ { 0 } ) |-> ( A / y ) ) ) = ( y e. ( CC \ { 0 } ) |-> -u ( A / ( y ^ 2 ) ) ) )
22 oveq2 
 |-  ( y = B -> ( A / y ) = ( A / B ) )
23 oveq1 
 |-  ( y = B -> ( y ^ 2 ) = ( B ^ 2 ) )
24 23 oveq2d 
 |-  ( y = B -> ( A / ( y ^ 2 ) ) = ( A / ( B ^ 2 ) ) )
25 24 negeqd 
 |-  ( y = B -> -u ( A / ( y ^ 2 ) ) = -u ( A / ( B ^ 2 ) ) )
26 1 7 3 4 13 19 5 21 22 25 dvmptco 
 |-  ( ph -> ( S _D ( x e. X |-> ( A / B ) ) ) = ( x e. X |-> ( -u ( A / ( B ^ 2 ) ) x. C ) ) )
27 2 adantr 
 |-  ( ( ph /\ x e. X ) -> A e. CC )
28 eldifi 
 |-  ( B e. ( CC \ { 0 } ) -> B e. CC )
29 3 28 syl 
 |-  ( ( ph /\ x e. X ) -> B e. CC )
30 29 sqcld 
 |-  ( ( ph /\ x e. X ) -> ( B ^ 2 ) e. CC )
31 eldifsn 
 |-  ( B e. ( CC \ { 0 } ) <-> ( B e. CC /\ B =/= 0 ) )
32 3 31 sylib 
 |-  ( ( ph /\ x e. X ) -> ( B e. CC /\ B =/= 0 ) )
33 32 simprd 
 |-  ( ( ph /\ x e. X ) -> B =/= 0 )
34 15 a1i 
 |-  ( ( ph /\ x e. X ) -> 2 e. ZZ )
35 29 33 34 expne0d 
 |-  ( ( ph /\ x e. X ) -> ( B ^ 2 ) =/= 0 )
36 27 30 35 divcld 
 |-  ( ( ph /\ x e. X ) -> ( A / ( B ^ 2 ) ) e. CC )
37 1 29 4 5 dvmptcl 
 |-  ( ( ph /\ x e. X ) -> C e. CC )
38 36 37 mulneg1d 
 |-  ( ( ph /\ x e. X ) -> ( -u ( A / ( B ^ 2 ) ) x. C ) = -u ( ( A / ( B ^ 2 ) ) x. C ) )
39 27 37 30 35 div23d 
 |-  ( ( ph /\ x e. X ) -> ( ( A x. C ) / ( B ^ 2 ) ) = ( ( A / ( B ^ 2 ) ) x. C ) )
40 39 eqcomd 
 |-  ( ( ph /\ x e. X ) -> ( ( A / ( B ^ 2 ) ) x. C ) = ( ( A x. C ) / ( B ^ 2 ) ) )
41 40 negeqd 
 |-  ( ( ph /\ x e. X ) -> -u ( ( A / ( B ^ 2 ) ) x. C ) = -u ( ( A x. C ) / ( B ^ 2 ) ) )
42 38 41 eqtrd 
 |-  ( ( ph /\ x e. X ) -> ( -u ( A / ( B ^ 2 ) ) x. C ) = -u ( ( A x. C ) / ( B ^ 2 ) ) )
43 42 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( -u ( A / ( B ^ 2 ) ) x. C ) ) = ( x e. X |-> -u ( ( A x. C ) / ( B ^ 2 ) ) ) )
44 26 43 eqtrd 
 |-  ( ph -> ( S _D ( x e. X |-> ( A / B ) ) ) = ( x e. X |-> -u ( ( A x. C ) / ( B ^ 2 ) ) ) )