This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐾 ) ‘ 𝐵 ) )