climliminflimsupd

Description: If a sequence of real numbers converges, its inferior limit and its superior limit are equal. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	climliminflimsupd.1	$⊢ φ \to M \in ℤ$
	climliminflimsupd.2	$⊢ Z = ℤ_{\geq M}$
	climliminflimsupd.3	$⊢ φ \to F : Z ⟶ ℝ$
	climliminflimsupd.4	$⊢ φ \to F \in dom ⇝$
Assertion	climliminflimsupd	$⊢ φ \to lim inf (F) = lim sup (F)$

Proof

Step	Hyp	Ref	Expression
1		climliminflimsupd.1	$⊢ φ \to M \in ℤ$
2		climliminflimsupd.2	$⊢ Z = ℤ_{\geq M}$
3		climliminflimsupd.3	$⊢ φ \to F : Z ⟶ ℝ$
4		climliminflimsupd.4	$⊢ φ \to F \in dom ⇝$
5	3	feqmptd	$⊢ φ \to F = (k \in Z ⟼ F (k))$
6	5	fveq2d	$⊢ φ \to lim inf (F) = lim inf ((k \in Z ⟼ F (k)))$
7	2	fvexi	$⊢ Z \in V$
8	7	mptex	$⊢ (k \in Z ⟼ F (k)) \in V$
9		liminfcl	$⊢ (k \in Z ⟼ F (k)) \in V \to lim inf ((k \in Z ⟼ F (k))) \in ℝ^{*}$
10	8 9	ax-mp	$⊢ lim inf ((k \in Z ⟼ F (k))) \in ℝ^{*}$
11	10	a1i	$⊢ φ \to lim inf ((k \in Z ⟼ F (k))) \in ℝ^{*}$
12	6 11	eqeltrd	$⊢ φ \to lim inf (F) \in ℝ^{*}$
13		nfv	$⊢ Ⅎ k φ$
14	3	ffvelrnda	$⊢ (φ \land k \in Z) \to F (k) \in ℝ$
15	14	renegcld	$⊢ (φ \land k \in Z) \to - F (k) \in ℝ$
16	13 1 2 15	limsupvaluz4	$⊢ φ \to lim sup ((k \in Z ⟼ - F (k))) = - lim inf ((k \in Z ⟼ - (- F (k))))$
17		climrel	$⊢ Rel ⇝$
18	17	a1i	$⊢ φ \to Rel ⇝$
19		nfcv	$⊢ \underline{Ⅎ} k F$
20	1 2 3	climlimsup	$⊢ φ \to (F \in dom ⇝ \leftrightarrow F ⇝ lim sup (F))$
21	4 20	mpbid	$⊢ φ \to F ⇝ lim sup (F)$
22	14	recnd	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
23	13 19 2 1 21 22	climneg	$⊢ φ \to (k \in Z ⟼ - F (k)) ⇝ (- lim sup (F))$
24		releldm	$⊢ (Rel ⇝ \land (k \in Z ⟼ - F (k)) ⇝ (- lim sup (F))) \to (k \in Z ⟼ - F (k)) \in dom ⇝$
25	18 23 24	syl2anc	$⊢ φ \to (k \in Z ⟼ - F (k)) \in dom ⇝$
26	15	fmpttd	$⊢ φ \to (k \in Z ⟼ - F (k)) : Z ⟶ ℝ$
27	1 2 26	climlimsup	$⊢ φ \to ((k \in Z ⟼ - F (k)) \in dom ⇝ \leftrightarrow (k \in Z ⟼ - F (k)) ⇝ lim sup ((k \in Z ⟼ - F (k))))$
28	25 27	mpbid	$⊢ φ \to (k \in Z ⟼ - F (k)) ⇝ lim sup ((k \in Z ⟼ - F (k)))$
29		climuni	$⊢ ((k \in Z ⟼ - F (k)) ⇝ lim sup ((k \in Z ⟼ - F (k))) \land (k \in Z ⟼ - F (k)) ⇝ (- lim sup (F))) \to lim sup ((k \in Z ⟼ - F (k))) = - lim sup (F)$
30	28 23 29	syl2anc	$⊢ φ \to lim sup ((k \in Z ⟼ - F (k))) = - lim sup (F)$
31	22	negnegd	$⊢ (φ \land k \in Z) \to - (- F (k)) = F (k)$
32	31	mpteq2dva	$⊢ φ \to (k \in Z ⟼ - (- F (k))) = (k \in Z ⟼ F (k))$
33	32 5	eqtr4d	$⊢ φ \to (k \in Z ⟼ - (- F (k))) = F$
34	33	fveq2d	$⊢ φ \to lim inf ((k \in Z ⟼ - (- F (k)))) = lim inf (F)$
35	34	xnegeqd	$⊢ φ \to - lim inf ((k \in Z ⟼ - (- F (k)))) = - lim inf (F)$
36	16 30 35	3eqtr3d	$⊢ φ \to - lim sup (F) = - lim inf (F)$
37	2 1 21 14	climrecl	$⊢ φ \to lim sup (F) \in ℝ$
38	37	renegcld	$⊢ φ \to - lim sup (F) \in ℝ$
39	36 38	eqeltrrd	$⊢ φ \to - lim inf (F) \in ℝ$
40		xnegrecl2	$⊢ (lim inf (F) \in ℝ^{*} \land - lim inf (F) \in ℝ) \to lim inf (F) \in ℝ$
41	12 39 40	syl2anc	$⊢ φ \to lim inf (F) \in ℝ$
42	41	recnd	$⊢ φ \to lim inf (F) \in ℂ$
43	37	recnd	$⊢ φ \to lim sup (F) \in ℂ$
44	41	rexnegd	$⊢ φ \to - lim inf (F) = - lim inf (F)$
45	36 44	eqtr2d	$⊢ φ \to - lim inf (F) = - lim sup (F)$
46	42 43 45	neg11d	$⊢ φ \to lim inf (F) = lim sup (F)$

Metamath Proof Explorer

Theorem climliminflimsupd

Proof