# 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}\in ℤ$
climlimsupcex.2 ${⊢}{Z}={ℤ}_{\ge {M}}$
climlimsupcex.3 ${⊢}{F}=\varnothing$
Assertion climlimsupcex ${⊢}\left(\varnothing \in ℂ\wedge ¬\mathrm{-\infty }\in ℂ\right)\to \left({F}:{Z}⟶ℝ\wedge {F}\in \mathrm{dom}⇝\wedge ¬{F}⇝\mathrm{lim sup}\left({F}\right)\right)$

### Proof

Step Hyp Ref Expression
1 climlimsupcex.1 ${⊢}¬{M}\in ℤ$
2 climlimsupcex.2 ${⊢}{Z}={ℤ}_{\ge {M}}$
3 climlimsupcex.3 ${⊢}{F}=\varnothing$
4 f0 ${⊢}\varnothing :\varnothing ⟶ℝ$
5 uz0 ${⊢}¬{M}\in ℤ\to {ℤ}_{\ge {M}}=\varnothing$
6 1 5 ax-mp ${⊢}{ℤ}_{\ge {M}}=\varnothing$
7 2 6 eqtri ${⊢}{Z}=\varnothing$
8 3 7 feq12i ${⊢}{F}:{Z}⟶ℝ↔\varnothing :\varnothing ⟶ℝ$
9 4 8 mpbir ${⊢}{F}:{Z}⟶ℝ$
10 9 a1i ${⊢}\left(\varnothing \in ℂ\wedge ¬\mathrm{-\infty }\in ℂ\right)\to {F}:{Z}⟶ℝ$
11 climrel ${⊢}\mathrm{Rel}⇝$
12 11 a1i ${⊢}\varnothing \in ℂ\to \mathrm{Rel}⇝$
13 0cnv ${⊢}\varnothing \in ℂ\to \varnothing ⇝\varnothing$
14 3 13 eqbrtrid ${⊢}\varnothing \in ℂ\to {F}⇝\varnothing$
15 releldm ${⊢}\left(\mathrm{Rel}⇝\wedge {F}⇝\varnothing \right)\to {F}\in \mathrm{dom}⇝$
16 12 14 15 syl2anc ${⊢}\varnothing \in ℂ\to {F}\in \mathrm{dom}⇝$
17 16 adantr ${⊢}\left(\varnothing \in ℂ\wedge ¬\mathrm{-\infty }\in ℂ\right)\to {F}\in \mathrm{dom}⇝$
18 13 adantr ${⊢}\left(\varnothing \in ℂ\wedge {F}⇝\mathrm{lim sup}\left({F}\right)\right)\to \varnothing ⇝\varnothing$
19 18 adantlr ${⊢}\left(\left(\varnothing \in ℂ\wedge ¬\mathrm{-\infty }\in ℂ\right)\wedge {F}⇝\mathrm{lim sup}\left({F}\right)\right)\to \varnothing ⇝\varnothing$
20 simpr ${⊢}\left({F}⇝\mathrm{lim sup}\left({F}\right)\wedge \varnothing ⇝\varnothing \right)\to \varnothing ⇝\varnothing$
21 3 fveq2i ${⊢}\mathrm{lim sup}\left({F}\right)=\mathrm{lim sup}\left(\varnothing \right)$
22 limsup0 ${⊢}\mathrm{lim sup}\left(\varnothing \right)=\mathrm{-\infty }$
23 21 22 eqtri ${⊢}\mathrm{lim sup}\left({F}\right)=\mathrm{-\infty }$
24 3 23 breq12i ${⊢}{F}⇝\mathrm{lim sup}\left({F}\right)↔\varnothing ⇝\mathrm{-\infty }$
25 24 biimpi ${⊢}{F}⇝\mathrm{lim sup}\left({F}\right)\to \varnothing ⇝\mathrm{-\infty }$
26 25 adantr ${⊢}\left({F}⇝\mathrm{lim sup}\left({F}\right)\wedge \varnothing ⇝\varnothing \right)\to \varnothing ⇝\mathrm{-\infty }$
27 climuni ${⊢}\left(\varnothing ⇝\varnothing \wedge \varnothing ⇝\mathrm{-\infty }\right)\to \varnothing =\mathrm{-\infty }$
28 20 26 27 syl2anc ${⊢}\left({F}⇝\mathrm{lim sup}\left({F}\right)\wedge \varnothing ⇝\varnothing \right)\to \varnothing =\mathrm{-\infty }$
29 28 adantll ${⊢}\left(\left(\left(\varnothing \in ℂ\wedge ¬\mathrm{-\infty }\in ℂ\right)\wedge {F}⇝\mathrm{lim sup}\left({F}\right)\right)\wedge \varnothing ⇝\varnothing \right)\to \varnothing =\mathrm{-\infty }$
30 nelneq ${⊢}\left(\varnothing \in ℂ\wedge ¬\mathrm{-\infty }\in ℂ\right)\to ¬\varnothing =\mathrm{-\infty }$
31 30 ad2antrr ${⊢}\left(\left(\left(\varnothing \in ℂ\wedge ¬\mathrm{-\infty }\in ℂ\right)\wedge {F}⇝\mathrm{lim sup}\left({F}\right)\right)\wedge \varnothing ⇝\varnothing \right)\to ¬\varnothing =\mathrm{-\infty }$
32 29 31 pm2.65da ${⊢}\left(\left(\varnothing \in ℂ\wedge ¬\mathrm{-\infty }\in ℂ\right)\wedge {F}⇝\mathrm{lim sup}\left({F}\right)\right)\to ¬\varnothing ⇝\varnothing$
33 19 32 pm2.65da ${⊢}\left(\varnothing \in ℂ\wedge ¬\mathrm{-\infty }\in ℂ\right)\to ¬{F}⇝\mathrm{lim sup}\left({F}\right)$
34 10 17 33 3jca ${⊢}\left(\varnothing \in ℂ\wedge ¬\mathrm{-\infty }\in ℂ\right)\to \left({F}:{Z}⟶ℝ\wedge {F}\in \mathrm{dom}⇝\wedge ¬{F}⇝\mathrm{lim sup}\left({F}\right)\right)$