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

Proof

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