liminflelimsupuz

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

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

Proof

Step	Hyp	Ref	Expression
1		liminflelimsupuz.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		liminflelimsupuz.2	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
3		liminflelimsupuz.3	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ^* )
4	2	fvexi	⊢ 𝑍 ∈ V
5	4	a1i	⊢ ( 𝜑 → 𝑍 ∈ V )
6	3 5	fexd	⊢ ( 𝜑 → 𝐹 ∈ V )
7	1 2	uzubico2	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ ( 𝑘 [,) +∞ ) 𝑗 ∈ 𝑍 )
8	3	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝑍 )
9	8	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐹 Fn 𝑍 )
10		simpr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝑍 )
11		id	⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ 𝑍 )
12	2 11	uzxrd	⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ℝ^* )
13		pnfxr	⊢ +∞ ∈ ℝ^*
14	13	a1i	⊢ ( 𝑗 ∈ 𝑍 → +∞ ∈ ℝ^* )
15	12	xrleidd	⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ≤ 𝑗 )
16	2 11	uzred	⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ℝ )
17		ltpnf	⊢ ( 𝑗 ∈ ℝ → 𝑗 < +∞ )
18	16 17	syl	⊢ ( 𝑗 ∈ 𝑍 → 𝑗 < +∞ )
19	12 14 12 15 18	elicod	⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ( 𝑗 [,) +∞ ) )
20	19	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ ( 𝑗 [,) +∞ ) )
21	9 10 20	fnfvimad	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ( 𝐹 “ ( 𝑗 [,) +∞ ) ) )
22	3	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ^* )
23	21 22	elind	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) )
24	23	ne0d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) ≠ ∅ )
25	24	ex	⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 → ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) ≠ ∅ ) )
26	25	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ ( 𝑘 [,) +∞ ) ) → ( 𝑗 ∈ 𝑍 → ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) ≠ ∅ ) )
27	26	reximdva	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → ( ∃ 𝑗 ∈ ( 𝑘 [,) +∞ ) 𝑗 ∈ 𝑍 → ∃ 𝑗 ∈ ( 𝑘 [,) +∞ ) ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) ≠ ∅ ) )
28	27	ralimdva	⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ ( 𝑘 [,) +∞ ) 𝑗 ∈ 𝑍 → ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ ( 𝑘 [,) +∞ ) ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) ≠ ∅ ) )
29	7 28	mpd	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ ( 𝑘 [,) +∞ ) ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) ≠ ∅ )
30	6 29	liminflelimsup	⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ≤ ( lim sup ‘ 𝐹 ) )

Metamath Proof Explorer

Theorem liminflelimsupuz

Proof