Metamath Proof Explorer

Theorem unbdqndv1

Description: If the difference quotient ( ( ( Fz ) - ( FA ) ) / ( z - A ) ) is unbounded near A then F is not differentiable at A . (Contributed by Asger C. Ipsen, 12-May-2021)

Ref Expression
Hypotheses unbdqndv1.g ⊢ 𝐺 = ( 𝑧 ∈ ( 𝑋 ∖ { 𝐴 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) )
unbdqndv1.1 ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
unbdqndv1.2 ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
unbdqndv1.3 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
unbdqndv1.4 ⊢ ( 𝜑 → ∀ 𝑏 ∈ ℝ+ ∀ 𝑑 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑋 ∖ { 𝐴 } ) ( ( abs ‘ ( 𝑥 − 𝐴 ) ) < 𝑑 ∧ 𝑏 ≤ ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
Assertion unbdqndv1 ( 𝜑 → ¬ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) )

Proof

Step Hyp Ref Expression
1 unbdqndv1.g ⊢ 𝐺 = ( 𝑧 ∈ ( 𝑋 ∖ { 𝐴 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) )
2 unbdqndv1.1 ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
3 unbdqndv1.2 ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
4 unbdqndv1.3 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
5 unbdqndv1.4 ⊢ ( 𝜑 → ∀ 𝑏 ∈ ℝ+ ∀ 𝑑 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑋 ∖ { 𝐴 } ) ( ( abs ‘ ( 𝑥 − 𝐴 ) ) < 𝑑 ∧ 𝑏 ≤ ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
6 noel ⊢ ¬ 𝑦 ∈ ∅
7 6 a1i ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ) → ¬ 𝑦 ∈ ∅ )
8 3 2 sstrd ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
9 8 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ) → 𝑋 ⊆ ℂ )
10 9 ssdifssd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ) → ( 𝑋 ∖ { 𝐴 } ) ⊆ ℂ )
11 4 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ) → 𝐹 : 𝑋 ⟶ ℂ )
12 2 4 3 dvbss ⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) ⊆ 𝑋 )
13 12 sselda ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ) → 𝐴 ∈ 𝑋 )
14 11 9 13 dvlem ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ) ∧ 𝑧 ∈ ( 𝑋 ∖ { 𝐴 } ) ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) ∈ ℂ )
15 14 1 fmptd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ) → 𝐺 : ( 𝑋 ∖ { 𝐴 } ) ⟶ ℂ )
16 9 13 sseldd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ) → 𝐴 ∈ ℂ )
17 5 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ) → ∀ 𝑏 ∈ ℝ+ ∀ 𝑑 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑋 ∖ { 𝐴 } ) ( ( abs ‘ ( 𝑥 − 𝐴 ) ) < 𝑑 ∧ 𝑏 ≤ ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
18 10 15 16 17 unblimceq0 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ) → ( 𝐺 limℂ 𝐴 ) = ∅ )
19 7 18 neleqtrrd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ) → ¬ 𝑦 ∈ ( 𝐺 limℂ 𝐴 ) )
20 19 intnand ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ) → ¬ ( 𝐴 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) ∧ 𝑦 ∈ ( 𝐺 limℂ 𝐴 ) ) )
21 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
22 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
23 21 22 1 2 4 3 eldv ⊢ ( 𝜑 → ( 𝐴 ( 𝑆 D 𝐹 ) 𝑦 ↔ ( 𝐴 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) ∧ 𝑦 ∈ ( 𝐺 limℂ 𝐴 ) ) ) )
24 23 notbid ⊢ ( 𝜑 → ( ¬ 𝐴 ( 𝑆 D 𝐹 ) 𝑦 ↔ ¬ ( 𝐴 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) ∧ 𝑦 ∈ ( 𝐺 limℂ 𝐴 ) ) ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ) → ( ¬ 𝐴 ( 𝑆 D 𝐹 ) 𝑦 ↔ ¬ ( 𝐴 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) ∧ 𝑦 ∈ ( 𝐺 limℂ 𝐴 ) ) ) )
26 20 25 mpbird ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ) → ¬ 𝐴 ( 𝑆 D 𝐹 ) 𝑦 )
27 26 alrimiv ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ) → ∀ 𝑦 ¬ 𝐴 ( 𝑆 D 𝐹 ) 𝑦 )
28 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ) → 𝐴 ∈ dom ( 𝑆 D 𝐹 ) )
29 eldmg ⊢ ( 𝐴 ∈ dom ( 𝑆 D 𝐹 ) → ( 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ↔ ∃ 𝑦 𝐴 ( 𝑆 D 𝐹 ) 𝑦 ) )
30 28 29 syl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ) → ( 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ↔ ∃ 𝑦 𝐴 ( 𝑆 D 𝐹 ) 𝑦 ) )
31 30 notbid ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ) → ( ¬ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ↔ ¬ ∃ 𝑦 𝐴 ( 𝑆 D 𝐹 ) 𝑦 ) )
32 alnex ⊢ ( ∀ 𝑦 ¬ 𝐴 ( 𝑆 D 𝐹 ) 𝑦 ↔ ¬ ∃ 𝑦 𝐴 ( 𝑆 D 𝐹 ) 𝑦 )
33 32 a1i ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ) → ( ∀ 𝑦 ¬ 𝐴 ( 𝑆 D 𝐹 ) 𝑦 ↔ ¬ ∃ 𝑦 𝐴 ( 𝑆 D 𝐹 ) 𝑦 ) )
34 33 bicomd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ) → ( ¬ ∃ 𝑦 𝐴 ( 𝑆 D 𝐹 ) 𝑦 ↔ ∀ 𝑦 ¬ 𝐴 ( 𝑆 D 𝐹 ) 𝑦 ) )
35 31 34 bitrd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ) → ( ¬ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ↔ ∀ 𝑦 ¬ 𝐴 ( 𝑆 D 𝐹 ) 𝑦 ) )
36 27 35 mpbird ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) ) → ¬ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) )
37 36 pm2.01da ⊢ ( 𝜑 → ¬ 𝐴 ∈ dom ( 𝑆 D 𝐹 ) )