Theorem xlimmnf

Description: A function converges to minus infinity if it eventually becomes (and stays) smaller than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	xlimmnf.k	⊢ Ⅎ 𝑘 𝐹
	xlimmnf.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	xlimmnf.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	xlimmnf.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
Assertion	xlimmnf	⊢ ( 𝜑 → ( 𝐹 ~~>* -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		xlimmnf.k	⊢ Ⅎ 𝑘 𝐹
2		xlimmnf.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		xlimmnf.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4		xlimmnf.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
5	2 3 4	xlimmnfv	⊢ ( 𝜑 → ( 𝐹 ~~>* -∞ ↔ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) )
6		breq2	⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
7	6	rexralbidv	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
8		fveq2	⊢ ( 𝑖 = 𝑗 → ( ℤ≥ ‘ 𝑖 ) = ( ℤ≥ ‘ 𝑗 ) )
9	8	raleqdv	⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
10		nfcv	⊢ Ⅎ 𝑘 𝑙
11	1 10	nffv	⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑙 )
12		nfcv	⊢ Ⅎ 𝑘 ≤
13		nfcv	⊢ Ⅎ 𝑘 𝑥
14	11 12 13	nfbr	⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥
15		nfv	⊢ Ⅎ 𝑙 ( 𝐹 ‘ 𝑘 ) ≤ 𝑥
16		fveq2	⊢ ( 𝑙 = 𝑘 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑘 ) )
17	16	breq1d	⊢ ( 𝑙 = 𝑘 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) )
18	14 15 17	cbvralw	⊢ ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 )
19	9 18	bitrdi	⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) )
20	19	cbvrexvw	⊢ ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 )
21	7 20	bitrdi	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) )
22	21	cbvralvw	⊢ ( ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 )
23	5 22	bitrdi	⊢ ( 𝜑 → ( 𝐹 ~~>* -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) )