Metamath Proof Explorer


Theorem dvmptdiv

Description: Function-builder for derivative, quotient rule. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dvmptdiv.s φS
dvmptdiv.a φxXA
dvmptdiv.b φxXBV
dvmptdiv.da φdxXAdSx=xXB
dvmptdiv.c φxXC0
dvmptdiv.d φxXD
dvmptdiv.dc φdxXCdSx=xXD
Assertion dvmptdiv φdxXACdSx=xXBCDAC2

Proof

Step Hyp Ref Expression
1 dvmptdiv.s φS
2 dvmptdiv.a φxXA
3 dvmptdiv.b φxXBV
4 dvmptdiv.da φdxXAdSx=xXB
5 dvmptdiv.c φxXC0
6 dvmptdiv.d φxXD
7 dvmptdiv.dc φdxXCdSx=xXD
8 5 eldifad φxXC
9 eldifsn C0CC0
10 5 9 sylib φxXCC0
11 10 simprd φxXC0
12 2 8 11 divrecd φxXAC=A1C
13 12 mpteq2dva φxXAC=xXA1C
14 13 oveq2d φdxXACdSx=dxXA1CdSx
15 8 11 reccld φxX1C
16 1cnd φxX1
17 16 6 mulcld φxX1D
18 8 sqcld φxXC2
19 11 neneqd φxX¬C=0
20 sqeq0 CC2=0C=0
21 8 20 syl φxXC2=0C=0
22 19 21 mtbird φxX¬C2=0
23 22 neqned φxXC20
24 17 18 23 divcld φxX1DC2
25 24 negcld φxX1DC2
26 1cnd φ1
27 1 26 5 6 7 dvrecg φdxX1CdSx=xX1DC2
28 1 2 3 4 15 25 27 dvmptmul φdxXA1CdSx=xXB1C+1DC2A
29 1 2 3 4 dvmptcl φxXB
30 29 8 mulcld φxXBC
31 30 18 23 divcld φxXBCC2
32 6 2 mulcld φxXDA
33 32 18 23 divcld φxXDAC2
34 31 33 negsubd φxXBCC2+DAC2=BCC2DAC2
35 29 16 8 11 div12d φxXB1C=1BC
36 29 8 11 divcld φxXBC
37 36 mulid2d φxX1BC=BC
38 8 sqvald φxXC2=CC
39 38 oveq2d φxXBCC2=BCCC
40 29 8 8 11 11 divcan5rd φxXBCCC=BC
41 39 40 eqtr2d φxXBC=BCC2
42 35 37 41 3eqtrd φxXB1C=BCC2
43 6 mulid2d φxX1D=D
44 43 oveq1d φxX1DC2=DC2
45 44 negeqd φxX1DC2=DC2
46 45 oveq1d φxX1DC2A=DC2A
47 6 18 23 divcld φxXDC2
48 47 2 mulneg1d φxXDC2A=DC2A
49 6 2 18 23 div23d φxXDAC2=DC2A
50 49 eqcomd φxXDC2A=DAC2
51 50 negeqd φxXDC2A=DAC2
52 46 48 51 3eqtrd φxX1DC2A=DAC2
53 42 52 oveq12d φxXB1C+1DC2A=BCC2+DAC2
54 30 32 18 23 divsubdird φxXBCDAC2=BCC2DAC2
55 34 53 54 3eqtr4d φxXB1C+1DC2A=BCDAC2
56 55 mpteq2dva φxXB1C+1DC2A=xXBCDAC2
57 14 28 56 3eqtrd φdxXACdSx=xXBCDAC2