dvdivf

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

	Ref	Expression
Hypotheses	dvdivf.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	dvdivf.f	$⊢ φ \to F : X ⟶ ℂ$
	dvdivf.g	$⊢ φ \to G : X ⟶ ℂ ∖ \{0\}$
	dvdivf.fdv	$⊢ φ \to dom F_{S}^{'} = X$
	dvdivf.gdv	$⊢ φ \to dom G_{S}^{'} = X$
Assertion	dvdivf	$⊢ φ \to S D (F \div_{f} G) = ((F_{S}^{'} \times_{f} G) -_{f} (G_{S}^{'} \times_{f} F)) \div_{f} (G \times_{f} G)$

Proof

Step	Hyp	Ref	Expression
1		dvdivf.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		dvdivf.f	$⊢ φ \to F : X ⟶ ℂ$
3		dvdivf.g	$⊢ φ \to G : X ⟶ ℂ ∖ \{0\}$
4		dvdivf.fdv	$⊢ φ \to dom F_{S}^{'} = X$
5		dvdivf.gdv	$⊢ φ \to dom G_{S}^{'} = X$
6	2	ffvelrnda	$⊢ (φ \land x \in X) \to F (x) \in ℂ$
7		dvfg	$⊢ S \in \{ℝ, ℂ\} \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
8	1 7	syl	$⊢ φ \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
9	4	feq2d	$⊢ φ \to (F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ \leftrightarrow F_{S}^{'} : X ⟶ ℂ)$
10	8 9	mpbid	$⊢ φ \to F_{S}^{'} : X ⟶ ℂ$
11	10	ffvelrnda	$⊢ (φ \land x \in X) \to F_{S}^{'} (x) \in ℂ$
12	2	feqmptd	$⊢ φ \to F = (x \in X ⟼ F (x))$
13	12	oveq2d	$⊢ φ \to S D F = \frac{d (x \in X⟼ F (x))}{d_{S} x}$
14	10	feqmptd	$⊢ φ \to S D F = (x \in X ⟼ F_{S}^{'} (x))$
15	13 14	eqtr3d	$⊢ φ \to \frac{d (x \in X⟼ F (x))}{d_{S} x} = (x \in X ⟼ F_{S}^{'} (x))$
16	3	ffvelrnda	$⊢ (φ \land x \in X) \to G (x) \in (ℂ ∖ \{0\})$
17		dvfg	$⊢ S \in \{ℝ, ℂ\} \to G_{S}^{'} : dom G_{S}^{'} ⟶ ℂ$
18	1 17	syl	$⊢ φ \to G_{S}^{'} : dom G_{S}^{'} ⟶ ℂ$
19	5	feq2d	$⊢ φ \to (G_{S}^{'} : dom G_{S}^{'} ⟶ ℂ \leftrightarrow G_{S}^{'} : X ⟶ ℂ)$
20	18 19	mpbid	$⊢ φ \to G_{S}^{'} : X ⟶ ℂ$
21	20	ffvelrnda	$⊢ (φ \land x \in X) \to G_{S}^{'} (x) \in ℂ$
22	3	feqmptd	$⊢ φ \to G = (x \in X ⟼ G (x))$
23	22	oveq2d	$⊢ φ \to S D G = \frac{d (x \in X⟼ G (x))}{d_{S} x}$
24	20	feqmptd	$⊢ φ \to S D G = (x \in X ⟼ G_{S}^{'} (x))$
25	23 24	eqtr3d	$⊢ φ \to \frac{d (x \in X⟼ G (x))}{d_{S} x} = (x \in X ⟼ G_{S}^{'} (x))$
26	1 6 11 15 16 21 25	dvmptdiv	$⊢ φ \to \frac{d (x \in X⟼ \frac{F (x)}{G (x)})}{d_{S} x} = (x \in X ⟼ \frac{F_{S}^{'} (x) G (x) - G_{S}^{'} (x) F (x)}{{G (x)}^{2}})$
27		ovex	$⊢ S D F \in V$
28	27	dmex	$⊢ dom F_{S}^{'} \in V$
29	4 28	eqeltrrdi	$⊢ φ \to X \in V$
30	29 6 16 12 22	offval2	$⊢ φ \to F \div_{f} G = (x \in X ⟼ \frac{F (x)}{G (x)})$
31	30	oveq2d	$⊢ φ \to S D (F \div_{f} G) = \frac{d (x \in X⟼ \frac{F (x)}{G (x)})}{d_{S} x}$
32		ovexd	$⊢ (φ \land x \in X) \to F_{S}^{'} (x) G (x) - G_{S}^{'} (x) F (x) \in V$
33	16	eldifad	$⊢ (φ \land x \in X) \to G (x) \in ℂ$
34	33	sqcld	$⊢ (φ \land x \in X) \to {G (x)}^{2} \in ℂ$
35	11 33	mulcld	$⊢ (φ \land x \in X) \to F_{S}^{'} (x) G (x) \in ℂ$
36	21 6	mulcld	$⊢ (φ \land x \in X) \to G_{S}^{'} (x) F (x) \in ℂ$
37	29 11 33 14 22	offval2	$⊢ φ \to F_{S}^{'} \times_{f} G = (x \in X ⟼ F_{S}^{'} (x) G (x))$
38	29 21 6 24 12	offval2	$⊢ φ \to G_{S}^{'} \times_{f} F = (x \in X ⟼ G_{S}^{'} (x) F (x))$
39	29 35 36 37 38	offval2	$⊢ φ \to (F_{S}^{'} \times_{f} G) -_{f} (G_{S}^{'} \times_{f} F) = (x \in X ⟼ F_{S}^{'} (x) G (x) - G_{S}^{'} (x) F (x))$
40	29 16 16 22 22	offval2	$⊢ φ \to G \times_{f} G = (x \in X ⟼ G (x) G (x))$
41	33	sqvald	$⊢ (φ \land x \in X) \to {G (x)}^{2} = G (x) G (x)$
42	41	mpteq2dva	$⊢ φ \to (x \in X ⟼ {G (x)}^{2}) = (x \in X ⟼ G (x) G (x))$
43	40 42	eqtr4d	$⊢ φ \to G \times_{f} G = (x \in X ⟼ {G (x)}^{2})$
44	29 32 34 39 43	offval2	$⊢ φ \to ((F_{S}^{'} \times_{f} G) -_{f} (G_{S}^{'} \times_{f} F)) \div_{f} (G \times_{f} G) = (x \in X ⟼ \frac{F_{S}^{'} (x) G (x) - G_{S}^{'} (x) F (x)}{{G (x)}^{2}})$
45	26 31 44	3eqtr4d	$⊢ φ \to S D (F \div_{f} G) = ((F_{S}^{'} \times_{f} G) -_{f} (G_{S}^{'} \times_{f} F)) \div_{f} (G \times_{f} G)$

Metamath Proof Explorer

Theorem dvdivf

Proof