Metamath Proof Explorer

Theorem 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 ⊢ φ → M ∈ ℤ
climliminflimsupd.2 ⊢ Z = ℤ ≥ M
climliminflimsupd.3 ⊢ φ → F : Z ⟶ ℝ
climliminflimsupd.4 ⊢ φ → F ∈ dom ⁡ ⇝
Assertion climliminflimsupd ⊢ φ → lim inf ⁡ F = lim sup ⁡ F

Proof

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