Metamath Proof Explorer

Theorem climliminflimsup

Description: A sequence of real numbers converges if and only if its inferior limit is real and it is greater than or equal to its superior limit (in such a case, they are actually equal, see liminfgelimsupuz ). (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses climliminflimsup.1 ⊢ φ → M ∈ ℤ
climliminflimsup.2 ⊢ Z = ℤ ≥ M
climliminflimsup.3 ⊢ φ → F : Z ⟶ ℝ
Assertion climliminflimsup ⊢ φ → F ∈ dom ⁡ ⇝ ↔ lim inf ⁡ F ∈ ℝ ∧ lim sup ⁡ F ≤ lim inf ⁡ F

Proof

Step Hyp Ref Expression
1 climliminflimsup.1 ⊢ φ → M ∈ ℤ
2 climliminflimsup.2 ⊢ Z = ℤ ≥ M
3 climliminflimsup.3 ⊢ φ → F : Z ⟶ ℝ
4 1 adantr ⊢ φ ∧ F ∈ dom ⁡ ⇝ → M ∈ ℤ
5 1 2 3 climliminf ⊢ φ → F ∈ dom ⁡ ⇝ ↔ F ⇝ lim inf ⁡ F
6 5 biimpd ⊢ φ → F ∈ dom ⁡ ⇝ → F ⇝ lim inf ⁡ F
7 6 imp ⊢ φ ∧ F ∈ dom ⁡ ⇝ → F ⇝ lim inf ⁡ F
8 3 adantr ⊢ φ ∧ F ∈ dom ⁡ ⇝ → F : Z ⟶ ℝ
9 8 ffvelcdmda ⊢ φ ∧ F ∈ dom ⁡ ⇝ ∧ k ∈ Z → F ⁡ k ∈ ℝ
10 2 4 7 9 climrecl ⊢ φ ∧ F ∈ dom ⁡ ⇝ → lim inf ⁡ F ∈ ℝ
11 simpr ⊢ φ ∧ F ∈ dom ⁡ ⇝ → F ∈ dom ⁡ ⇝
12 11 limsupcld ⊢ φ ∧ F ∈ dom ⁡ ⇝ → lim sup ⁡ F ∈ ℝ *
13 4 2 8 11 climliminflimsupd ⊢ φ ∧ F ∈ dom ⁡ ⇝ → lim inf ⁡ F = lim sup ⁡ F
14 13 eqcomd ⊢ φ ∧ F ∈ dom ⁡ ⇝ → lim sup ⁡ F = lim inf ⁡ F
15 12 14 xreqled ⊢ φ ∧ F ∈ dom ⁡ ⇝ → lim sup ⁡ F ≤ lim inf ⁡ F
16 10 15 jca ⊢ φ ∧ F ∈ dom ⁡ ⇝ → lim inf ⁡ F ∈ ℝ ∧ lim sup ⁡ F ≤ lim inf ⁡ F
17 1 adantr ⊢ φ ∧ lim inf ⁡ F ∈ ℝ ∧ lim sup ⁡ F ≤ lim inf ⁡ F → M ∈ ℤ
18 3 adantr ⊢ φ ∧ lim inf ⁡ F ∈ ℝ ∧ lim sup ⁡ F ≤ lim inf ⁡ F → F : Z ⟶ ℝ
19 simprl ⊢ φ ∧ lim inf ⁡ F ∈ ℝ ∧ lim sup ⁡ F ≤ lim inf ⁡ F → lim inf ⁡ F ∈ ℝ
20 simprr ⊢ φ ∧ lim inf ⁡ F ∈ ℝ ∧ lim sup ⁡ F ≤ lim inf ⁡ F → lim sup ⁡ F ≤ lim inf ⁡ F
21 17 2 18 19 20 liminflimsupclim ⊢ φ ∧ lim inf ⁡ F ∈ ℝ ∧ lim sup ⁡ F ≤ lim inf ⁡ F → F ∈ dom ⁡ ⇝
22 16 21 impbida ⊢ φ → F ∈ dom ⁡ ⇝ ↔ lim inf ⁡ F ∈ ℝ ∧ lim sup ⁡ F ≤ lim inf ⁡ F