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 ⊢ ¬ 𝑀 ∈ ℤ
climlimsupcex.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climlimsupcex.3 ⊢ 𝐹 = ∅
Assertion climlimsupcex ( ( ∅ ∈ ℂ ∧ ¬ -∞ ∈ ℂ ) → ( 𝐹 : 𝑍 ⟶ ℝ ∧ 𝐹 ∈ dom ⇝ ∧ ¬ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 climlimsupcex.1 ⊢ ¬ 𝑀 ∈ ℤ
2 climlimsupcex.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 climlimsupcex.3 ⊢ 𝐹 = ∅
4 f0 ⊢ ∅ : ∅ ⟶ ℝ
5 uz0 ⊢ ( ¬ 𝑀 ∈ ℤ → ( ℤ≥ ‘ 𝑀 ) = ∅ )
6 1 5 ax-mp ⊢ ( ℤ≥ ‘ 𝑀 ) = ∅
7 2 6 eqtri ⊢ 𝑍 = ∅
8 3 7 feq12i ⊢ ( 𝐹 : 𝑍 ⟶ ℝ ↔ ∅ : ∅ ⟶ ℝ )
9 4 8 mpbir ⊢ 𝐹 : 𝑍 ⟶ ℝ
10 9 a1i ⊢ ( ( ∅ ∈ ℂ ∧ ¬ -∞ ∈ ℂ ) → 𝐹 : 𝑍 ⟶ ℝ )
11 climrel ⊢ Rel ⇝
12 11 a1i ⊢ ( ∅ ∈ ℂ → Rel ⇝ )
13 0cnv ⊢ ( ∅ ∈ ℂ → ∅ ⇝ ∅ )
14 3 13 eqbrtrid ⊢ ( ∅ ∈ ℂ → 𝐹 ⇝ ∅ )
15 releldm ⊢ ( ( Rel ⇝ ∧ 𝐹 ⇝ ∅ ) → 𝐹 ∈ dom ⇝ )
16 12 14 15 syl2anc ⊢ ( ∅ ∈ ℂ → 𝐹 ∈ dom ⇝ )
17 16 adantr ⊢ ( ( ∅ ∈ ℂ ∧ ¬ -∞ ∈ ℂ ) → 𝐹 ∈ dom ⇝ )
18 13 adantr ⊢ ( ( ∅ ∈ ℂ ∧ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ) → ∅ ⇝ ∅ )
19 18 adantlr ⊢ ( ( ( ∅ ∈ ℂ ∧ ¬ -∞ ∈ ℂ ) ∧ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ) → ∅ ⇝ ∅ )
20 simpr ⊢ ( ( 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ∧ ∅ ⇝ ∅ ) → ∅ ⇝ ∅ )
21 3 fveq2i ⊢ ( lim sup ‘ 𝐹 ) = ( lim sup ‘ ∅ )
22 limsup0 ⊢ ( lim sup ‘ ∅ ) = -∞
23 21 22 eqtri ⊢ ( lim sup ‘ 𝐹 ) = -∞
24 3 23 breq12i ⊢ ( 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ↔ ∅ ⇝ -∞ )
25 24 biimpi ⊢ ( 𝐹 ⇝ ( lim sup ‘ 𝐹 ) → ∅ ⇝ -∞ )
26 25 adantr ⊢ ( ( 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ∧ ∅ ⇝ ∅ ) → ∅ ⇝ -∞ )
27 climuni ⊢ ( ( ∅ ⇝ ∅ ∧ ∅ ⇝ -∞ ) → ∅ = -∞ )
28 20 26 27 syl2anc ⊢ ( ( 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ∧ ∅ ⇝ ∅ ) → ∅ = -∞ )
29 28 adantll ⊢ ( ( ( ( ∅ ∈ ℂ ∧ ¬ -∞ ∈ ℂ ) ∧ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ) ∧ ∅ ⇝ ∅ ) → ∅ = -∞ )
30 nelneq ⊢ ( ( ∅ ∈ ℂ ∧ ¬ -∞ ∈ ℂ ) → ¬ ∅ = -∞ )
31 30 ad2antrr ⊢ ( ( ( ( ∅ ∈ ℂ ∧ ¬ -∞ ∈ ℂ ) ∧ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ) ∧ ∅ ⇝ ∅ ) → ¬ ∅ = -∞ )
32 29 31 pm2.65da ⊢ ( ( ( ∅ ∈ ℂ ∧ ¬ -∞ ∈ ℂ ) ∧ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ) → ¬ ∅ ⇝ ∅ )
33 19 32 pm2.65da ⊢ ( ( ∅ ∈ ℂ ∧ ¬ -∞ ∈ ℂ ) → ¬ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) )
34 10 17 33 3jca ⊢ ( ( ∅ ∈ ℂ ∧ ¬ -∞ ∈ ℂ ) → ( 𝐹 : 𝑍 ⟶ ℝ ∧ 𝐹 ∈ dom ⇝ ∧ ¬ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ) )