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