liminfgelimsupuz

Description: The inferior limit is greater than or equal to the superior limit if and only if they are equal. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	liminfgelimsupuz.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	liminfgelimsupuz.2	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
	liminfgelimsupuz.3	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ^* )
Assertion	liminfgelimsupuz	⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ↔ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		liminfgelimsupuz.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		liminfgelimsupuz.2	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
3		liminfgelimsupuz.3	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ^* )
4	2	fvexi	⊢ 𝑍 ∈ V
5	4	a1i	⊢ ( 𝜑 → 𝑍 ∈ V )
6	3 5	fexd	⊢ ( 𝜑 → 𝐹 ∈ V )
7	6	liminfcld	⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ∈ ℝ^* )
8	7	adantr	⊢ ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ) → ( lim inf ‘ 𝐹 ) ∈ ℝ^* )
9	6	limsupcld	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ^* )
10	9	adantr	⊢ ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ) → ( lim sup ‘ 𝐹 ) ∈ ℝ^* )
11	1 2 3	liminflelimsupuz	⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ≤ ( lim sup ‘ 𝐹 ) )
12	11	adantr	⊢ ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ) → ( lim inf ‘ 𝐹 ) ≤ ( lim sup ‘ 𝐹 ) )
13		simpr	⊢ ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ) → ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) )
14	8 10 12 13	xrletrid	⊢ ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ) → ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) )
15	9	adantr	⊢ ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) → ( lim sup ‘ 𝐹 ) ∈ ℝ^* )
16		id	⊢ ( ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) → ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) )
17	16	eqcomd	⊢ ( ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) → ( lim sup ‘ 𝐹 ) = ( lim inf ‘ 𝐹 ) )
18	17	adantl	⊢ ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) → ( lim sup ‘ 𝐹 ) = ( lim inf ‘ 𝐹 ) )
19	15 18	xreqled	⊢ ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) → ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) )
20	14 19	impbida	⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ↔ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) )

Metamath Proof Explorer

Theorem liminfgelimsupuz

Proof