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 
|- K = ( TopOpen ` CCfld )
jumpncnp.a 
|- ( ph -> A C_ RR )
jumpncnp.3 
|- J = ( topGen ` ran (,) )
jumpncnp.f 
|- ( ph -> F : A --> CC )
jumpncnp.b 
|- ( ph -> B e. RR )
jumpncnp.lpt1 
|- ( ph -> B e. ( ( limPt ` J ) ` ( A i^i ( -oo (,) B ) ) ) )
jumpncnp.lpt2 
|- ( ph -> B e. ( ( limPt ` J ) ` ( A i^i ( B (,) +oo ) ) ) )
jumpncnp.8 
|- ( ph -> L e. ( ( F |` ( -oo (,) B ) ) limCC B ) )
jumpncnp.9 
|- ( ph -> R e. ( ( F |` ( B (,) +oo ) ) limCC B ) )
jumpncnp.lner 
|- ( ph -> L =/= R )
Assertion jumpncnp 
|- ( ph -> -. F e. ( ( J CnP ( TopOpen ` CCfld ) ) ` B ) )

Proof

Step Hyp Ref Expression
1 jumpncnp.k 
 |-  K = ( TopOpen ` CCfld )
2 jumpncnp.a 
 |-  ( ph -> A C_ RR )
3 jumpncnp.3 
 |-  J = ( topGen ` ran (,) )
4 jumpncnp.f 
 |-  ( ph -> F : A --> CC )
5 jumpncnp.b 
 |-  ( ph -> B e. RR )
6 jumpncnp.lpt1 
 |-  ( ph -> B e. ( ( limPt ` J ) ` ( A i^i ( -oo (,) B ) ) ) )
7 jumpncnp.lpt2 
 |-  ( ph -> B e. ( ( limPt ` J ) ` ( A i^i ( B (,) +oo ) ) ) )
8 jumpncnp.8 
 |-  ( ph -> L e. ( ( F |` ( -oo (,) B ) ) limCC B ) )
9 jumpncnp.9 
 |-  ( ph -> R e. ( ( F |` ( B (,) +oo ) ) limCC B ) )
10 jumpncnp.lner 
 |-  ( ph -> L =/= R )
11 1 2 3 4 6 7 8 9 10 limclner 
 |-  ( ph -> ( F limCC B ) = (/) )
12 ne0i 
 |-  ( ( F ` B ) e. ( F limCC B ) -> ( F limCC B ) =/= (/) )
13 12 necon2bi 
 |-  ( ( F limCC B ) = (/) -> -. ( F ` B ) e. ( F limCC B ) )
14 11 13 syl 
 |-  ( ph -> -. ( F ` B ) e. ( F limCC B ) )
15 14 intnand 
 |-  ( ph -> -. ( F : RR --> CC /\ ( F ` B ) e. ( F limCC B ) ) )
16 ax-resscn 
 |-  RR C_ CC
17 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
18 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
19 3 18 eqtri 
 |-  J = ( ( TopOpen ` CCfld ) |`t RR )
20 17 19 cnplimc 
 |-  ( ( RR C_ CC /\ B e. RR ) -> ( F e. ( ( J CnP ( TopOpen ` CCfld ) ) ` B ) <-> ( F : RR --> CC /\ ( F ` B ) e. ( F limCC B ) ) ) )
21 16 5 20 sylancr 
 |-  ( ph -> ( F e. ( ( J CnP ( TopOpen ` CCfld ) ) ` B ) <-> ( F : RR --> CC /\ ( F ` B ) e. ( F limCC B ) ) ) )
22 15 21 mtbird 
 |-  ( ph -> -. F e. ( ( J CnP ( TopOpen ` CCfld ) ) ` B ) )