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

Metamath Proof Explorer

Theorem jumpncnp

Proof