Theorem xlimpnf

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

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

Proof

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