Theorem dvcnp

Description: The difference quotient is continuous at B when the original function is differentiable at B . (Contributed by Mario Carneiro, 8-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016)

	Ref	Expression
Hypotheses	dvcnp.j	⊢ 𝐽 = ( 𝐾 ↾t 𝐴 )
	dvcnp.k	⊢ 𝐾 = ( TopOpen ‘ ℂfld )
	dvcnp.g	⊢ 𝐺 = ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 = 𝐵 , ( ( 𝑆 D 𝐹 ) ‘ 𝐵 ) , ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ) )
Assertion	dvcnp	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ∈ dom ( 𝑆 D 𝐹 ) ) → 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		dvcnp.j	⊢ 𝐽 = ( 𝐾 ↾t 𝐴 )
2		dvcnp.k	⊢ 𝐾 = ( TopOpen ‘ ℂfld )
3		dvcnp.g	⊢ 𝐺 = ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 = 𝐵 , ( ( 𝑆 D 𝐹 ) ‘ 𝐵 ) , ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ) )
4		dvfg	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
5	4	3ad2ant1	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
6		ffun	⊢ ( ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ → Fun ( 𝑆 D 𝐹 ) )
7		funfvbrb	⊢ ( Fun ( 𝑆 D 𝐹 ) → ( 𝐵 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝐵 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝐵 ) ) )
8	5 6 7	3syl	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ( 𝐵 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝐵 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝐵 ) ) )
9		eqid	⊢ ( 𝐾 ↾t 𝑆 ) = ( 𝐾 ↾t 𝑆 )
10		eqid	⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) )
11		recnprss	⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
12	11	3ad2ant1	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → 𝑆 ⊆ ℂ )
13		simp2	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → 𝐹 : 𝐴 ⟶ ℂ )
14		simp3	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → 𝐴 ⊆ 𝑆 )
15	9 2 10 12 13 14	eldv	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ( 𝐵 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝐵 ) ↔ ( 𝐵 ∈ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ 𝐴 ) ∧ ( ( 𝑆 D 𝐹 ) ‘ 𝐵 ) ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ) limℂ 𝐵 ) ) ) )
16	8 15	bitrd	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ( 𝐵 ∈ dom ( 𝑆 D 𝐹 ) ↔ ( 𝐵 ∈ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ 𝐴 ) ∧ ( ( 𝑆 D 𝐹 ) ‘ 𝐵 ) ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ) limℂ 𝐵 ) ) ) )
17	16	simplbda	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ∈ dom ( 𝑆 D 𝐹 ) ) → ( ( 𝑆 D 𝐹 ) ‘ 𝐵 ) ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ) limℂ 𝐵 ) )
18	14 12	sstrd	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → 𝐴 ⊆ ℂ )
19	18	adantr	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ∈ dom ( 𝑆 D 𝐹 ) ) → 𝐴 ⊆ ℂ )
20	12 13 14	dvbss	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → dom ( 𝑆 D 𝐹 ) ⊆ 𝐴 )
21	20	sselda	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ∈ dom ( 𝑆 D 𝐹 ) ) → 𝐵 ∈ 𝐴 )
22		eldifsn	⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵 ) )
23	13	adantr	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ∈ dom ( 𝑆 D 𝐹 ) ) → 𝐹 : 𝐴 ⟶ ℂ )
24	23 19 21	dvlem	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ∈ dom ( 𝑆 D 𝐹 ) ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ∈ ℂ )
25	22 24	sylan2br	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ∈ dom ( 𝑆 D 𝐹 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ∈ ℂ )
26	19 21 25 1 2	limcmpt2	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ∈ dom ( 𝑆 D 𝐹 ) ) → ( ( ( 𝑆 D 𝐹 ) ‘ 𝐵 ) ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ) limℂ 𝐵 ) ↔ ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 = 𝐵 , ( ( 𝑆 D 𝐹 ) ‘ 𝐵 ) , ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) )
27	17 26	mpbid	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ∈ dom ( 𝑆 D 𝐹 ) ) → ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 = 𝐵 , ( ( 𝑆 D 𝐹 ) ‘ 𝐵 ) , ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) )
28	3 27	eqeltrid	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ∈ dom ( 𝑆 D 𝐹 ) ) → 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) )