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 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climliminflimsup2.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climliminflimsup2.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
Assertion climliminflimsup2 ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ ( ( lim sup ‘ 𝐹 ) ∈ ℝ ∧ ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ) ) )

Proof

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