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	birani	⊢ ( ( 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ∧ ∅ ⇝ ∅ ) → ∅ ⇝ -∞ )
26		climuni	⊢ ( ( ∅ ⇝ ∅ ∧ ∅ ⇝ -∞ ) → ∅ = -∞ )
27	20 25 26	syl2anc	⊢ ( ( 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ∧ ∅ ⇝ ∅ ) → ∅ = -∞ )
28	27	adantll	⊢ ( ( ( ( ∅ ∈ ℂ ∧ ¬ -∞ ∈ ℂ ) ∧ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ) ∧ ∅ ⇝ ∅ ) → ∅ = -∞ )
29		nelneq	⊢ ( ( ∅ ∈ ℂ ∧ ¬ -∞ ∈ ℂ ) → ¬ ∅ = -∞ )
30	29	ad2antrr	⊢ ( ( ( ( ∅ ∈ ℂ ∧ ¬ -∞ ∈ ℂ ) ∧ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ) ∧ ∅ ⇝ ∅ ) → ¬ ∅ = -∞ )
31	28 30	pm2.65da	⊢ ( ( ( ∅ ∈ ℂ ∧ ¬ -∞ ∈ ℂ ) ∧ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ) → ¬ ∅ ⇝ ∅ )
32	19 31	pm2.65da	⊢ ( ( ∅ ∈ ℂ ∧ ¬ -∞ ∈ ℂ ) → ¬ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) )
33	10 17 32	3jca	⊢ ( ( ∅ ∈ ℂ ∧ ¬ -∞ ∈ ℂ ) → ( 𝐹 : 𝑍 ⟶ ℝ ∧ 𝐹 ∈ dom ⇝ ∧ ¬ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ) )