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 ⊢ φ ∧ x ∈ X → A ∈ ℂ
dvmptdiv.b ⊢ φ ∧ x ∈ X → B ∈ V
dvmptdiv.da ⊢ φ → dx ∈ X A dS x = x ∈ X ⟼ B
dvmptdiv.c ⊢ φ ∧ x ∈ X → C ∈ ℂ ∖ 0
dvmptdiv.d ⊢ φ ∧ x ∈ X → D ∈ ℂ
dvmptdiv.dc ⊢ φ → dx ∈ X C dS x = x ∈ X ⟼ D
Assertion dvmptdiv ⊢ φ → dx ∈ X A C dS x = x ∈ X ⟼ B ⁢ C − D ⁢ A C 2

Proof

Step Hyp Ref Expression
1 dvmptdiv.s ⊢ φ → S ∈ ℝ ℂ
2 dvmptdiv.a ⊢ φ ∧ x ∈ X → A ∈ ℂ
3 dvmptdiv.b ⊢ φ ∧ x ∈ X → B ∈ V
4 dvmptdiv.da ⊢ φ → dx ∈ X A dS x = x ∈ X ⟼ B
5 dvmptdiv.c ⊢ φ ∧ x ∈ X → C ∈ ℂ ∖ 0
6 dvmptdiv.d ⊢ φ ∧ x ∈ X → D ∈ ℂ
7 dvmptdiv.dc ⊢ φ → dx ∈ X C dS x = x ∈ X ⟼ D
8 5 eldifad ⊢ φ ∧ x ∈ X → C ∈ ℂ
9 eldifsn ⊢ C ∈ ℂ ∖ 0 ↔ C ∈ ℂ ∧ C ≠ 0
10 5 9 sylib ⊢ φ ∧ x ∈ X → C ∈ ℂ ∧ C ≠ 0
11 10 simprd ⊢ φ ∧ x ∈ X → C ≠ 0
12 2 8 11 divrecd ⊢ φ ∧ x ∈ X → A C = A ⁢ 1 C
13 12 mpteq2dva ⊢ φ → x ∈ X ⟼ A C = x ∈ X ⟼ A ⁢ 1 C
14 13 oveq2d ⊢ φ → dx ∈ X A C dS x = dx ∈ X A ⁢ 1 C dS x
15 8 11 reccld ⊢ φ ∧ x ∈ X → 1 C ∈ ℂ
16 1cnd ⊢ φ ∧ x ∈ X → 1 ∈ ℂ
17 16 6 mulcld ⊢ φ ∧ x ∈ X → 1 ⁢ D ∈ ℂ
18 8 sqcld ⊢ φ ∧ x ∈ X → C 2 ∈ ℂ
19 11 neneqd ⊢ φ ∧ x ∈ X → ¬ C = 0
20 sqeq0 ⊢ C ∈ ℂ → C 2 = 0 ↔ C = 0
21 8 20 syl ⊢ φ ∧ x ∈ X → C 2 = 0 ↔ C = 0
22 19 21 mtbird ⊢ φ ∧ x ∈ X → ¬ C 2 = 0
23 22 neqned ⊢ φ ∧ x ∈ X → C 2 ≠ 0
24 17 18 23 divcld ⊢ φ ∧ x ∈ X → 1 ⁢ D C 2 ∈ ℂ
25 24 negcld ⊢ φ ∧ x ∈ X → − 1 ⁢ D C 2 ∈ ℂ
26 1cnd ⊢ φ → 1 ∈ ℂ
27 1 26 5 6 7 dvrecg ⊢ φ → dx ∈ X 1 C dS x = x ∈ X ⟼ − 1 ⁢ D C 2
28 1 2 3 4 15 25 27 dvmptmul ⊢ φ → dx ∈ X A ⁢ 1 C dS x = x ∈ X ⟼ B ⁢ 1 C + − 1 ⁢ D C 2 ⁢ A
29 1 2 3 4 dvmptcl ⊢ φ ∧ x ∈ X → B ∈ ℂ
30 29 8 mulcld ⊢ φ ∧ x ∈ X → B ⁢ C ∈ ℂ
31 30 18 23 divcld ⊢ φ ∧ x ∈ X → B ⁢ C C 2 ∈ ℂ
32 6 2 mulcld ⊢ φ ∧ x ∈ X → D ⁢ A ∈ ℂ
33 32 18 23 divcld ⊢ φ ∧ x ∈ X → D ⁢ A C 2 ∈ ℂ
34 31 33 negsubd ⊢ φ ∧ x ∈ X → B ⁢ C C 2 + − D ⁢ A C 2 = B ⁢ C C 2 − D ⁢ A C 2
35 29 16 8 11 div12d ⊢ φ ∧ x ∈ X → B ⁢ 1 C = 1 ⁢ B C
36 29 8 11 divcld ⊢ φ ∧ x ∈ X → B C ∈ ℂ
37 36 mulid2d ⊢ φ ∧ x ∈ X → 1 ⁢ B C = B C
38 8 sqvald ⊢ φ ∧ x ∈ X → C 2 = C ⁢ C
39 38 oveq2d ⊢ φ ∧ x ∈ X → B ⁢ C C 2 = B ⁢ C C ⁢ C
40 29 8 8 11 11 divcan5rd ⊢ φ ∧ x ∈ X → B ⁢ C C ⁢ C = B C
41 39 40 eqtr2d ⊢ φ ∧ x ∈ X → B C = B ⁢ C C 2
42 35 37 41 3eqtrd ⊢ φ ∧ x ∈ X → B ⁢ 1 C = B ⁢ C C 2
43 6 mulid2d ⊢ φ ∧ x ∈ X → 1 ⁢ D = D
44 43 oveq1d ⊢ φ ∧ x ∈ X → 1 ⁢ D C 2 = D C 2
45 44 negeqd ⊢ φ ∧ x ∈ X → − 1 ⁢ D C 2 = − D C 2
46 45 oveq1d ⊢ φ ∧ x ∈ X → − 1 ⁢ D C 2 ⁢ A = − D C 2 ⁢ A
47 6 18 23 divcld ⊢ φ ∧ x ∈ X → D C 2 ∈ ℂ
48 47 2 mulneg1d ⊢ φ ∧ x ∈ X → − D C 2 ⁢ A = − D C 2 ⁢ A
49 6 2 18 23 div23d ⊢ φ ∧ x ∈ X → D ⁢ A C 2 = D C 2 ⁢ A
50 49 eqcomd ⊢ φ ∧ x ∈ X → D C 2 ⁢ A = D ⁢ A C 2
51 50 negeqd ⊢ φ ∧ x ∈ X → − D C 2 ⁢ A = − D ⁢ A C 2
52 46 48 51 3eqtrd ⊢ φ ∧ x ∈ X → − 1 ⁢ D C 2 ⁢ A = − D ⁢ A C 2
53 42 52 oveq12d ⊢ φ ∧ x ∈ X → B ⁢ 1 C + − 1 ⁢ D C 2 ⁢ A = B ⁢ C C 2 + − D ⁢ A C 2
54 30 32 18 23 divsubdird ⊢ φ ∧ x ∈ X → B ⁢ C − D ⁢ A C 2 = B ⁢ C C 2 − D ⁢ A C 2
55 34 53 54 3eqtr4d ⊢ φ ∧ x ∈ X → B ⁢ 1 C + − 1 ⁢ D C 2 ⁢ A = B ⁢ C − D ⁢ A C 2
56 55 mpteq2dva ⊢ φ → x ∈ X ⟼ B ⁢ 1 C + − 1 ⁢ D C 2 ⁢ A = x ∈ X ⟼ B ⁢ C − D ⁢ A C 2
57 14 28 56 3eqtrd ⊢ φ → dx ∈ X A C dS x = x ∈ X ⟼ B ⁢ C − D ⁢ A C 2