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
climlimsupcex.2 Z = M
climlimsupcex.3 F =
Assertion climlimsupcex ¬ −∞ F : Z F dom ¬ F lim sup F

Proof

Step Hyp Ref Expression
1 climlimsupcex.1 ¬ M
2 climlimsupcex.2 Z = M
3 climlimsupcex.3 F =
4 f0 :
5 uz0 ¬ M M =
6 1 5 ax-mp M =
7 2 6 eqtri Z =
8 3 7 feq12i F : Z :
9 4 8 mpbir F : Z
10 9 a1i ¬ −∞ F : Z
11 climrel Rel
12 11 a1i Rel
13 0cnv
14 3 13 eqbrtrid F
15 releldm Rel F F dom
16 12 14 15 syl2anc F dom
17 16 adantr ¬ −∞ F dom
18 13 adantr F lim sup F
19 18 adantlr ¬ −∞ F lim sup F
20 simpr F lim sup F
21 3 fveq2i lim sup F = lim sup
22 limsup0 lim sup = −∞
23 21 22 eqtri lim sup F = −∞
24 3 23 breq12i F lim sup F −∞
25 24 biimpi F lim sup F −∞
26 25 adantr F lim sup F −∞
27 climuni −∞ = −∞
28 20 26 27 syl2anc F lim sup F = −∞
29 28 adantll ¬ −∞ F lim sup F = −∞
30 nelneq ¬ −∞ ¬ = −∞
31 30 ad2antrr ¬ −∞ F lim sup F ¬ = −∞
32 29 31 pm2.65da ¬ −∞ F lim sup F ¬
33 19 32 pm2.65da ¬ −∞ ¬ F lim sup F
34 10 17 33 3jca ¬ −∞ F : Z F dom ¬ F lim sup F