Metamath Proof Explorer

Theorem climlimsupcex

Description: Counterexample for climlimsup , showing that the first hypothesis is needed, if the empty set is a complex number (see 0ncn and its comment). (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses climlimsupcex.1 
|- -. M e. ZZ
climlimsupcex.2 
|- Z = ( ZZ>= ` M )
climlimsupcex.3 
|- F = (/)
Assertion climlimsupcex 
|- ( ( (/) e. CC /\ -. -oo e. CC ) -> ( F : Z --> RR /\ F e. dom ~~> /\ -. F ~~> ( limsup ` F ) ) )

Proof

Step Hyp Ref Expression
1 climlimsupcex.1 
 |-  -. M e. ZZ
2 climlimsupcex.2 
 |-  Z = ( ZZ>= ` M )
3 climlimsupcex.3 
 |-  F = (/)
4 f0 
 |-  (/) : (/) --> RR
5 uz0 
 |-  ( -. M e. ZZ -> ( ZZ>= ` M ) = (/) )
6 1 5 ax-mp 
 |-  ( ZZ>= ` M ) = (/)
7 2 6 eqtri 
 |-  Z = (/)
8 3 7 feq12i 
 |-  ( F : Z --> RR <-> (/) : (/) --> RR )
9 4 8 mpbir 
 |-  F : Z --> RR
10 9 a1i 
 |-  ( ( (/) e. CC /\ -. -oo e. CC ) -> F : Z --> RR )
11 climrel 
 |-  Rel ~~>
12 11 a1i 
 |-  ( (/) e. CC -> Rel ~~> )
13 0cnv 
 |-  ( (/) e. CC -> (/) ~~> (/) )
14 3 13 eqbrtrid 
 |-  ( (/) e. CC -> F ~~> (/) )
15 releldm 
 |-  ( ( Rel ~~> /\ F ~~> (/) ) -> F e. dom ~~> )
16 12 14 15 syl2anc 
 |-  ( (/) e. CC -> F e. dom ~~> )
17 16 adantr 
 |-  ( ( (/) e. CC /\ -. -oo e. CC ) -> F e. dom ~~> )
18 13 adantr 
 |-  ( ( (/) e. CC /\ F ~~> ( limsup ` F ) ) -> (/) ~~> (/) )
19 18 adantlr 
 |-  ( ( ( (/) e. CC /\ -. -oo e. CC ) /\ F ~~> ( limsup ` F ) ) -> (/) ~~> (/) )
20 simpr 
 |-  ( ( F ~~> ( limsup ` F ) /\ (/) ~~> (/) ) -> (/) ~~> (/) )
21 3 fveq2i 
 |-  ( limsup ` F ) = ( limsup ` (/) )
22 limsup0 
 |-  ( limsup ` (/) ) = -oo
23 21 22 eqtri 
 |-  ( limsup ` F ) = -oo
24 3 23 breq12i 
 |-  ( F ~~> ( limsup ` F ) <-> (/) ~~> -oo )
25 24 biimpi 
 |-  ( F ~~> ( limsup ` F ) -> (/) ~~> -oo )
26 25 adantr 
 |-  ( ( F ~~> ( limsup ` F ) /\ (/) ~~> (/) ) -> (/) ~~> -oo )
27 climuni 
 |-  ( ( (/) ~~> (/) /\ (/) ~~> -oo ) -> (/) = -oo )
28 20 26 27 syl2anc 
 |-  ( ( F ~~> ( limsup ` F ) /\ (/) ~~> (/) ) -> (/) = -oo )
29 28 adantll 
 |-  ( ( ( ( (/) e. CC /\ -. -oo e. CC ) /\ F ~~> ( limsup ` F ) ) /\ (/) ~~> (/) ) -> (/) = -oo )
30 nelneq 
 |-  ( ( (/) e. CC /\ -. -oo e. CC ) -> -. (/) = -oo )
31 30 ad2antrr 
 |-  ( ( ( ( (/) e. CC /\ -. -oo e. CC ) /\ F ~~> ( limsup ` F ) ) /\ (/) ~~> (/) ) -> -. (/) = -oo )
32 29 31 pm2.65da 
 |-  ( ( ( (/) e. CC /\ -. -oo e. CC ) /\ F ~~> ( limsup ` F ) ) -> -. (/) ~~> (/) )
33 19 32 pm2.65da 
 |-  ( ( (/) e. CC /\ -. -oo e. CC ) -> -. F ~~> ( limsup ` F ) )
34 10 17 33 3jca 
 |-  ( ( (/) e. CC /\ -. -oo e. CC ) -> ( F : Z --> RR /\ F e. dom ~~> /\ -. F ~~> ( limsup ` F ) ) )