Theorem 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	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	dvdivcncf.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
	dvdivcncf.g	⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ( ℂ ∖ { 0 } ) )
	dvdivcncf.fdv	⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) ∈ ( 𝑋 –cn→ ℂ ) )
	dvdivcncf.gdv	⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) ∈ ( 𝑋 –cn→ ℂ ) )
Assertion	dvdivcncf	⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f / 𝐺 ) ) ∈ ( 𝑋 –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		dvdivcncf.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		dvdivcncf.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
3		dvdivcncf.g	⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ( ℂ ∖ { 0 } ) )
4		dvdivcncf.fdv	⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) ∈ ( 𝑋 –cn→ ℂ ) )
5		dvdivcncf.gdv	⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) ∈ ( 𝑋 –cn→ ℂ ) )
6		cncff	⊢ ( ( 𝑆 D 𝐹 ) ∈ ( 𝑋 –cn→ ℂ ) → ( 𝑆 D 𝐹 ) : 𝑋 ⟶ ℂ )
7		fdm	⊢ ( ( 𝑆 D 𝐹 ) : 𝑋 ⟶ ℂ → dom ( 𝑆 D 𝐹 ) = 𝑋 )
8	4 6 7	3syl	⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) = 𝑋 )
9		cncff	⊢ ( ( 𝑆 D 𝐺 ) ∈ ( 𝑋 –cn→ ℂ ) → ( 𝑆 D 𝐺 ) : 𝑋 ⟶ ℂ )
10		fdm	⊢ ( ( 𝑆 D 𝐺 ) : 𝑋 ⟶ ℂ → dom ( 𝑆 D 𝐺 ) = 𝑋 )
11	5 9 10	3syl	⊢ ( 𝜑 → dom ( 𝑆 D 𝐺 ) = 𝑋 )
12	1 2 3 8 11	dvdivf	⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f / 𝐺 ) ) = ( ( ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) ∘f − ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) ) ∘f / ( 𝐺 ∘f · 𝐺 ) ) )
13		ax-resscn	⊢ ℝ ⊆ ℂ
14		sseq1	⊢ ( 𝑆 = ℝ → ( 𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ ) )
15	13 14	mpbiri	⊢ ( 𝑆 = ℝ → 𝑆 ⊆ ℂ )
16		eqimss	⊢ ( 𝑆 = ℂ → 𝑆 ⊆ ℂ )
17	15 16	pm3.2i	⊢ ( ( 𝑆 = ℝ → 𝑆 ⊆ ℂ ) ∧ ( 𝑆 = ℂ → 𝑆 ⊆ ℂ ) )
18		elpri	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) )
19	1 18	syl	⊢ ( 𝜑 → ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) )
20		pm3.44	⊢ ( ( ( 𝑆 = ℝ → 𝑆 ⊆ ℂ ) ∧ ( 𝑆 = ℂ → 𝑆 ⊆ ℂ ) ) → ( ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) → 𝑆 ⊆ ℂ ) )
21	17 19 20	mpsyl	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
22		difssd	⊢ ( 𝜑 → ( ℂ ∖ { 0 } ) ⊆ ℂ )
23	3 22	fssd	⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
24		dvbsss	⊢ dom ( 𝑆 D 𝐹 ) ⊆ 𝑆
25	8 24	eqsstrrdi	⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
26		dvcn	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐺 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ 𝑆 ) ∧ dom ( 𝑆 D 𝐺 ) = 𝑋 ) → 𝐺 ∈ ( 𝑋 –cn→ ℂ ) )
27	21 23 25 11 26	syl31anc	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 –cn→ ℂ ) )
28	4 27	mulcncff	⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) ∈ ( 𝑋 –cn→ ℂ ) )
29		dvcn	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ 𝑆 ) ∧ dom ( 𝑆 D 𝐹 ) = 𝑋 ) → 𝐹 ∈ ( 𝑋 –cn→ ℂ ) )
30	21 2 25 8 29	syl31anc	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 –cn→ ℂ ) )
31	5 30	mulcncff	⊢ ( 𝜑 → ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) ∈ ( 𝑋 –cn→ ℂ ) )
32	28 31	subcncff	⊢ ( 𝜑 → ( ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) ∘f − ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) ) ∈ ( 𝑋 –cn→ ℂ ) )
33		eldifi	⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → 𝑥 ∈ ℂ )
34	33	adantr	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑥 ∈ ℂ )
35		eldifi	⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → 𝑦 ∈ ℂ )
36	35	adantl	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑦 ∈ ℂ )
37	34 36	mulcld	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
38		eldifsni	⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → 𝑥 ≠ 0 )
39	38	adantr	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑥 ≠ 0 )
40		eldifsni	⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → 𝑦 ≠ 0 )
41	40	adantl	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑦 ≠ 0 )
42	34 36 39 41	mulne0d	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
43		eldifsn	⊢ ( ( 𝑥 · 𝑦 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝑥 · 𝑦 ) ∈ ℂ ∧ ( 𝑥 · 𝑦 ) ≠ 0 ) )
44	37 42 43	sylanbrc	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ∈ ( ℂ ∖ { 0 } ) )
45	44	adantl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ) → ( 𝑥 · 𝑦 ) ∈ ( ℂ ∖ { 0 } ) )
46	1 25	ssexd	⊢ ( 𝜑 → 𝑋 ∈ V )
47		inidm	⊢ ( 𝑋 ∩ 𝑋 ) = 𝑋
48	45 3 3 46 46 47	off	⊢ ( 𝜑 → ( 𝐺 ∘f · 𝐺 ) : 𝑋 ⟶ ( ℂ ∖ { 0 } ) )
49	27 27	mulcncff	⊢ ( 𝜑 → ( 𝐺 ∘f · 𝐺 ) ∈ ( 𝑋 –cn→ ℂ ) )
50		cncfcdm	⊢ ( ( ( ℂ ∖ { 0 } ) ⊆ ℂ ∧ ( 𝐺 ∘f · 𝐺 ) ∈ ( 𝑋 –cn→ ℂ ) ) → ( ( 𝐺 ∘f · 𝐺 ) ∈ ( 𝑋 –cn→ ( ℂ ∖ { 0 } ) ) ↔ ( 𝐺 ∘f · 𝐺 ) : 𝑋 ⟶ ( ℂ ∖ { 0 } ) ) )
51	22 49 50	syl2anc	⊢ ( 𝜑 → ( ( 𝐺 ∘f · 𝐺 ) ∈ ( 𝑋 –cn→ ( ℂ ∖ { 0 } ) ) ↔ ( 𝐺 ∘f · 𝐺 ) : 𝑋 ⟶ ( ℂ ∖ { 0 } ) ) )
52	48 51	mpbird	⊢ ( 𝜑 → ( 𝐺 ∘f · 𝐺 ) ∈ ( 𝑋 –cn→ ( ℂ ∖ { 0 } ) ) )
53	32 52	divcncff	⊢ ( 𝜑 → ( ( ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) ∘f − ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) ) ∘f / ( 𝐺 ∘f · 𝐺 ) ) ∈ ( 𝑋 –cn→ ℂ ) )
54	12 53	eqeltrd	⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f / 𝐺 ) ) ∈ ( 𝑋 –cn→ ℂ ) )