Theorem liminfreuz

Description: Given a function on the reals, its inferior limit is real if and only if two condition holds: 1. there is a real number that is greater than or equal to the function, infinitely often; 2. there is a real number that is smaller than or equal to the function. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	liminfreuz.1	⊢ Ⅎ 𝑗 𝐹
	liminfreuz.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	liminfreuz.3	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	liminfreuz.4	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
Assertion	liminfreuz	⊢ ( 𝜑 → ( ( lim inf ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		liminfreuz.1	⊢ Ⅎ 𝑗 𝐹
2		liminfreuz.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		liminfreuz.3	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4		liminfreuz.4	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
5		nfcv	⊢ Ⅎ 𝑙 𝐹
6	5 2 3 4	liminfreuzlem	⊢ ( 𝜑 → ( ( lim inf ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑙 ∈ 𝑍 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ) )
7		breq2	⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
8	7	rexbidv	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
9	8	ralbidv	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
10		fveq2	⊢ ( 𝑖 = 𝑘 → ( ℤ≥ ‘ 𝑖 ) = ( ℤ≥ ‘ 𝑘 ) )
11	10	rexeqdv	⊢ ( 𝑖 = 𝑘 → ( ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
12		nfcv	⊢ Ⅎ 𝑗 𝑙
13	1 12	nffv	⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 )
14		nfcv	⊢ Ⅎ 𝑗 ≤
15		nfcv	⊢ Ⅎ 𝑗 𝑥
16	13 14 15	nfbr	⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥
17		nfv	⊢ Ⅎ 𝑙 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥
18		fveq2	⊢ ( 𝑙 = 𝑗 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑗 ) )
19	18	breq1d	⊢ ( 𝑙 = 𝑗 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
20	16 17 19	cbvrexw	⊢ ( ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
21	20	a1i	⊢ ( 𝑖 = 𝑘 → ( ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
22	11 21	bitrd	⊢ ( 𝑖 = 𝑘 → ( ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
23	22	cbvralvw	⊢ ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
24	23	a1i	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
25	9 24	bitrd	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
26	25	cbvrexvw	⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
27		breq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) )
28	27	ralbidv	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑙 ∈ 𝑍 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∀ 𝑙 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) )
29	15 14 13	nfbr	⊢ Ⅎ 𝑗 𝑥 ≤ ( 𝐹 ‘ 𝑙 )
30		nfv	⊢ Ⅎ 𝑙 𝑥 ≤ ( 𝐹 ‘ 𝑗 )
31	18	breq2d	⊢ ( 𝑙 = 𝑗 → ( 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
32	29 30 31	cbvralw	⊢ ( ∀ 𝑙 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
33	32	a1i	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑙 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
34	28 33	bitrd	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑙 ∈ 𝑍 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
35	34	cbvrexvw	⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑙 ∈ 𝑍 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
36	26 35	anbi12i	⊢ ( ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑙 ∈ 𝑍 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
37	36	a1i	⊢ ( 𝜑 → ( ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑙 ∈ 𝑍 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
38	6 37	bitrd	⊢ ( 𝜑 → ( ( lim inf ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )