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	$⊢ \neg M \in ℤ$
	climlimsupcex.2	$⊢ Z = ℤ_{\geq M}$
	climlimsupcex.3	$⊢ F = \emptyset$
Assertion	climlimsupcex	$⊢ (\emptyset \in ℂ \land \neg −∞ \in ℂ) \to (F : Z ⟶ ℝ \land F \in dom ⇝ \land \neg F ⇝ lim sup (F))$

Proof

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

Metamath Proof Explorer

Theorem climlimsupcex

Proof