Metamath Proof Explorer

Theorem climliminflimsup2

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

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

Proof

Step Hyp Ref Expression
1 climliminflimsup2.1 ⊢φ→M∈ℤ
2 climliminflimsup2.2 ⊢Z=ℤ≥M
3 climliminflimsup2.3 ⊢φ→F:Z⟶ℝ
4 1 2 3 climliminflimsup ⊢φ→F∈dom⁡⇝↔lim inf⁡F∈ℝ∧lim sup⁡F≤lim inf⁡F
5 1 adantr ⊢φ∧lim inf⁡F∈ℝ∧lim sup⁡F≤lim inf⁡F→M∈ℤ
6 3 adantr ⊢φ∧lim inf⁡F∈ℝ∧lim sup⁡F≤lim inf⁡F→F:Z⟶ℝ
7 simprl ⊢φ∧lim inf⁡F∈ℝ∧lim sup⁡F≤lim inf⁡F→lim inf⁡F∈ℝ
8 simprr ⊢φ∧lim inf⁡F∈ℝ∧lim sup⁡F≤lim inf⁡F→lim sup⁡F≤lim inf⁡F
9 5 2 6 7 8 liminflimsupclim ⊢φ∧lim inf⁡F∈ℝ∧lim sup⁡F≤lim inf⁡F→F∈dom⁡⇝
10 1 adantr ⊢φ∧F∈dom⁡⇝→M∈ℤ
11 3 adantr ⊢φ∧F∈dom⁡⇝→F:Z⟶ℝ
12 simpr ⊢φ∧F∈dom⁡⇝→F∈dom⁡⇝
13 10 2 11 12 climliminflimsupd ⊢φ∧F∈dom⁡⇝→lim inf⁡F=lim sup⁡F
14 13 eqcomd ⊢φ∧F∈dom⁡⇝→lim sup⁡F=lim inf⁡F
15 9 14 syldan ⊢φ∧lim inf⁡F∈ℝ∧lim sup⁡F≤lim inf⁡F→lim sup⁡F=lim inf⁡F
16 15 7 eqeltrd ⊢φ∧lim inf⁡F∈ℝ∧lim sup⁡F≤lim inf⁡F→lim sup⁡F∈ℝ
17 16 8 jca ⊢φ∧lim inf⁡F∈ℝ∧lim sup⁡F≤lim inf⁡F→lim sup⁡F∈ℝ∧lim sup⁡F≤lim inf⁡F
18 simpr ⊢φ∧lim sup⁡F≤lim inf⁡F→lim sup⁡F≤lim inf⁡F
19 1 adantr ⊢φ∧lim sup⁡F≤lim inf⁡F→M∈ℤ
20 3 frexr ⊢φ→F:Z⟶ℝ*
21 20 adantr ⊢φ∧lim sup⁡F≤lim inf⁡F→F:Z⟶ℝ*
22 19 2 21 liminfgelimsupuz ⊢φ∧lim sup⁡F≤lim inf⁡F→lim sup⁡F≤lim inf⁡F↔lim inf⁡F=lim sup⁡F
23 18 22 mpbid ⊢φ∧lim sup⁡F≤lim inf⁡F→lim inf⁡F=lim sup⁡F
24 23 adantrl ⊢φ∧lim sup⁡F∈ℝ∧lim sup⁡F≤lim inf⁡F→lim inf⁡F=lim sup⁡F
25 simprl ⊢φ∧lim sup⁡F∈ℝ∧lim sup⁡F≤lim inf⁡F→lim sup⁡F∈ℝ
26 24 25 eqeltrd ⊢φ∧lim sup⁡F∈ℝ∧lim sup⁡F≤lim inf⁡F→lim inf⁡F∈ℝ
27 simprr ⊢φ∧lim sup⁡F∈ℝ∧lim sup⁡F≤lim inf⁡F→lim sup⁡F≤lim inf⁡F
28 26 27 jca ⊢φ∧lim sup⁡F∈ℝ∧lim sup⁡F≤lim inf⁡F→lim inf⁡F∈ℝ∧lim sup⁡F≤lim inf⁡F
29 17 28 impbida ⊢φ→lim inf⁡F∈ℝ∧lim sup⁡F≤lim inf⁡F↔lim sup⁡F∈ℝ∧lim sup⁡F≤lim inf⁡F
30 4 29 bitrd ⊢φ→F∈dom⁡⇝↔lim sup⁡F∈ℝ∧lim sup⁡F≤lim inf⁡F