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