Metamath Proof Explorer

Theorem xlimpnfmpt

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 xlimpnfmpt.k ⊢ Ⅎ 𝑘 𝜑
xlimpnfmpt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
xlimpnfmpt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
xlimpnfmpt.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ* )
xlimpnfmpt.f ⊢ 𝐹 = ( 𝑘 ∈ 𝑍 ↦ 𝐵 )
Assertion xlimpnfmpt ( 𝜑 → ( 𝐹 ~~>* +∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 xlimpnfmpt.k ⊢ Ⅎ 𝑘 𝜑
2 xlimpnfmpt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 xlimpnfmpt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 xlimpnfmpt.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ* )
5 xlimpnfmpt.f ⊢ 𝐹 = ( 𝑘 ∈ 𝑍 ↦ 𝐵 )
6 nfmpt1 ⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝑍 ↦ 𝐵 )
7 5 6 nfcxfr ⊢ Ⅎ 𝑘 𝐹
8 1 4 5 fmptdf ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
9 7 2 3 8 xlimpnf ⊢ ( 𝜑 → ( 𝐹 ~~>* +∞ ↔ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑘 ) ) )
10 nfv ⊢ Ⅎ 𝑘 𝑖 ∈ 𝑍
11 1 10 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑖 ∈ 𝑍 )
12 3 uztrn2 ⊢ ( ( 𝑖 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑘 ∈ 𝑍 )
13 12 adantll ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑘 ∈ 𝑍 )
14 simpll ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝜑 )
15 14 13 4 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝐵 ∈ ℝ* )
16 5 fvmpt2 ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝐵 ∈ ℝ* ) → ( 𝐹 ‘ 𝑘 ) = 𝐵 )
17 13 15 16 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝐵 )
18 17 breq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( 𝑦 ≤ ( 𝐹 ‘ 𝑘 ) ↔ 𝑦 ≤ 𝐵 ) )
19 11 18 ralbida ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ 𝐵 ) )
20 19 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑘 ) ↔ ∃ 𝑖 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ 𝐵 ) )
21 20 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑘 ) ↔ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ 𝐵 ) )
22 breq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ≤ 𝐵 ↔ 𝑥 ≤ 𝐵 ) )
23 22 rexralbidv ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ 𝐵 ↔ ∃ 𝑖 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ 𝐵 ) )
24 fveq2 ⊢ ( 𝑖 = 𝑗 → ( ℤ≥ ‘ 𝑖 ) = ( ℤ≥ ‘ 𝑗 ) )
25 24 raleqdv ⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ 𝐵 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ 𝐵 ) )
26 25 cbvrexvw ⊢ ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ 𝐵 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ 𝐵 )
27 23 26 bitrdi ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ 𝐵 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ 𝐵 ) )
28 27 cbvralvw ⊢ ( ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ 𝐵 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ 𝐵 )
29 28 a1i ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ 𝐵 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ 𝐵 ) )
30 9 21 29 3bitrd ⊢ ( 𝜑 → ( 𝐹 ~~>* +∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ 𝐵 ) )