Metamath Proof Explorer

Theorem jumpncnp

Description: Jump discontinuity or discontinuity of the first kind: if the left and the right limit don't match, the function is discontinuous at the point. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses jumpncnp.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
jumpncnp.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
jumpncnp.3 ⊢ 𝐽 = ( topGen ‘ ran (,) )
jumpncnp.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
jumpncnp.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
jumpncnp.lpt1 ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) )
jumpncnp.lpt2 ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) )
jumpncnp.8 ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) limℂ 𝐵 ) )
jumpncnp.9 ⊢ ( 𝜑 → 𝑅 ∈ ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) limℂ 𝐵 ) )
jumpncnp.lner ⊢ ( 𝜑 → 𝐿 ≠ 𝑅 )
Assertion jumpncnp ( 𝜑 → ¬ 𝐹 ∈ ( ( 𝐽 CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 jumpncnp.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
2 jumpncnp.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3 jumpncnp.3 ⊢ 𝐽 = ( topGen ‘ ran (,) )
4 jumpncnp.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
5 jumpncnp.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
6 jumpncnp.lpt1 ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) )
7 jumpncnp.lpt2 ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) )
8 jumpncnp.8 ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) limℂ 𝐵 ) )
9 jumpncnp.9 ⊢ ( 𝜑 → 𝑅 ∈ ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) limℂ 𝐵 ) )
10 jumpncnp.lner ⊢ ( 𝜑 → 𝐿 ≠ 𝑅 )
11 1 2 3 4 6 7 8 9 10 limclner ⊢ ( 𝜑 → ( 𝐹 limℂ 𝐵 ) = ∅ )
12 ne0i ⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 limℂ 𝐵 ) → ( 𝐹 limℂ 𝐵 ) ≠ ∅ )
13 12 necon2bi ⊢ ( ( 𝐹 limℂ 𝐵 ) = ∅ → ¬ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 limℂ 𝐵 ) )
14 11 13 syl ⊢ ( 𝜑 → ¬ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 limℂ 𝐵 ) )
15 14 intnand ⊢ ( 𝜑 → ¬ ( 𝐹 : ℝ ⟶ ℂ ∧ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 limℂ 𝐵 ) ) )
16 ax-resscn ⊢ ℝ ⊆ ℂ
17 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
18 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
19 3 18 eqtri ⊢ 𝐽 = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
20 17 19 cnplimc ⊢ ( ( ℝ ⊆ ℂ ∧ 𝐵 ∈ ℝ ) → ( 𝐹 ∈ ( ( 𝐽 CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐵 ) ↔ ( 𝐹 : ℝ ⟶ ℂ ∧ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 limℂ 𝐵 ) ) ) )
21 16 5 20 sylancr ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝐽 CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐵 ) ↔ ( 𝐹 : ℝ ⟶ ℂ ∧ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 limℂ 𝐵 ) ) ) )
22 15 21 mtbird ⊢ ( 𝜑 → ¬ 𝐹 ∈ ( ( 𝐽 CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐵 ) )