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