dvdivcncf

Description: A sufficient condition for the derivative of a quotient to be continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		dvdivcncf.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		dvdivcncf.f	$⊢ φ \to F : X ⟶ ℂ$
3		dvdivcncf.g	$⊢ φ \to G : X ⟶ ℂ ∖ \{0\}$
4		dvdivcncf.fdv	$⊢ φ \to F_{S}^{'} : X \underset{cn}{⟶} ℂ$
5		dvdivcncf.gdv	$⊢ φ \to G_{S}^{'} : X \underset{cn}{⟶} ℂ$
6		cncff	$⊢ F_{S}^{'} : X \underset{cn}{⟶} ℂ \to F_{S}^{'} : X ⟶ ℂ$
7		fdm	$⊢ F_{S}^{'} : X ⟶ ℂ \to dom F_{S}^{'} = X$
8	4 6 7	3syl	$⊢ φ \to dom F_{S}^{'} = X$
9		cncff	$⊢ G_{S}^{'} : X \underset{cn}{⟶} ℂ \to G_{S}^{'} : X ⟶ ℂ$
10		fdm	$⊢ G_{S}^{'} : X ⟶ ℂ \to dom G_{S}^{'} = X$
11	5 9 10	3syl	$⊢ φ \to dom G_{S}^{'} = X$
12	1 2 3 8 11	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)$
13		ax-resscn	$⊢ ℝ \subseteq ℂ$
14		sseq1	$⊢ S = ℝ \to (S \subseteq ℂ \leftrightarrow ℝ \subseteq ℂ)$
15	13 14	mpbiri	$⊢ S = ℝ \to S \subseteq ℂ$
16		eqimss	$⊢ S = ℂ \to S \subseteq ℂ$
17	15 16	pm3.2i	$⊢ ((S = ℝ \to S \subseteq ℂ) \land (S = ℂ \to S \subseteq ℂ))$
18		elpri	$⊢ S \in \{ℝ, ℂ\} \to (S = ℝ \lor S = ℂ)$
19	1 18	syl	$⊢ φ \to (S = ℝ \lor S = ℂ)$
20		pm3.44	$⊢ ((S = ℝ \to S \subseteq ℂ) \land (S = ℂ \to S \subseteq ℂ)) \to ((S = ℝ \lor S = ℂ) \to S \subseteq ℂ)$
21	17 19 20	mpsyl	$⊢ φ \to S \subseteq ℂ$
22		difssd	$⊢ φ \to ℂ ∖ \{0\} \subseteq ℂ$
23	3 22	fssd	$⊢ φ \to G : X ⟶ ℂ$
24		dvbsss	$⊢ dom F_{S}^{'} \subseteq S$
25	8 24	eqsstrrdi	$⊢ φ \to X \subseteq S$
26		dvcn	$⊢ ((S \subseteq ℂ \land G : X ⟶ ℂ \land X \subseteq S) \land dom G_{S}^{'} = X) \to G : X \underset{cn}{⟶} ℂ$
27	21 23 25 11 26	syl31anc	$⊢ φ \to G : X \underset{cn}{⟶} ℂ$
28	4 27	mulcncff	$⊢ φ \to (F_{S}^{'} \times_{f} G) : X \underset{cn}{⟶} ℂ$
29		dvcn	$⊢ ((S \subseteq ℂ \land F : X ⟶ ℂ \land X \subseteq S) \land dom F_{S}^{'} = X) \to F : X \underset{cn}{⟶} ℂ$
30	21 2 25 8 29	syl31anc	$⊢ φ \to F : X \underset{cn}{⟶} ℂ$
31	5 30	mulcncff	$⊢ φ \to (G_{S}^{'} \times_{f} F) : X \underset{cn}{⟶} ℂ$
32	28 31	subcncff	$⊢ φ \to ((F_{S}^{'} \times_{f} G) -_{f} (G_{S}^{'} \times_{f} F)) : X \underset{cn}{⟶} ℂ$
33		eldifi	$⊢ x \in (ℂ ∖ \{0\}) \to x \in ℂ$
34	33	adantr	$⊢ (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\})) \to x \in ℂ$
35		eldifi	$⊢ y \in (ℂ ∖ \{0\}) \to y \in ℂ$
36	35	adantl	$⊢ (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\})) \to y \in ℂ$
37	34 36	mulcld	$⊢ (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\})) \to x y \in ℂ$
38		eldifsni	$⊢ x \in (ℂ ∖ \{0\}) \to x \neq 0$
39	38	adantr	$⊢ (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\})) \to x \neq 0$
40		eldifsni	$⊢ y \in (ℂ ∖ \{0\}) \to y \neq 0$
41	40	adantl	$⊢ (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\})) \to y \neq 0$
42	34 36 39 41	mulne0d	$⊢ (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\})) \to x y \neq 0$
43		eldifsn	$⊢ x y \in (ℂ ∖ \{0\}) \leftrightarrow (x y \in ℂ \land x y \neq 0)$
44	37 42 43	sylanbrc	$⊢ (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\})) \to x y \in (ℂ ∖ \{0\})$
45	44	adantl	$⊢ (φ \land (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\}))) \to x y \in (ℂ ∖ \{0\})$
46	1 25	ssexd	$⊢ φ \to X \in V$
47		inidm	$⊢ X \cap X = X$
48	45 3 3 46 46 47	off	$⊢ φ \to (G \times_{f} G) : X ⟶ ℂ ∖ \{0\}$
49	27 27	mulcncff	$⊢ φ \to (G \times_{f} G) : X \underset{cn}{⟶} ℂ$
50		cncfcdm	$⊢ (ℂ ∖ \{0\} \subseteq ℂ \land (G \times_{f} G) : X \underset{cn}{⟶} ℂ) \to ((G \times_{f} G) : X \underset{cn}{⟶} (ℂ ∖ \{0\}) \leftrightarrow (G \times_{f} G) : X ⟶ ℂ ∖ \{0\})$
51	22 49 50	syl2anc	$⊢ φ \to ((G \times_{f} G) : X \underset{cn}{⟶} (ℂ ∖ \{0\}) \leftrightarrow (G \times_{f} G) : X ⟶ ℂ ∖ \{0\})$
52	48 51	mpbird	$⊢ φ \to (G \times_{f} G) : X \underset{cn}{⟶} (ℂ ∖ \{0\})$
53	32 52	divcncff	$⊢ φ \to (((F_{S}^{'} \times_{f} G) -_{f} (G_{S}^{'} \times_{f} F)) \div_{f} (G \times_{f} G)) : X \underset{cn}{⟶} ℂ$
54	12 53	eqeltrd	$⊢ φ \to {(F \div_{f} G)}_{S}^{'} : X \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem dvdivcncf

Proof