Metamath Proof Explorer

Theorem xlimmnfmpt

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

Proof

Step Hyp Ref Expression
1 xlimmnfmpt.k ⊢ Ⅎ 𝑘 𝜑
2 xlimmnfmpt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 xlimmnfmpt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 xlimmnfmpt.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ* )
5 xlimmnfmpt.f ⊢ 𝐹 = ( 𝑘 ∈ 𝑍 ↦ 𝐵 )
6 nfmpt1 ⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝑍 ↦ 𝐵 )
7 5 6 nfcxfr ⊢ Ⅎ 𝑘 𝐹
8 1 4 5 fmptdf ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
9 7 2 3 8 xlimmnf ⊢ ( 𝜑 → ( 𝐹 ~~>* -∞ ↔ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑦 ) )
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 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( 𝐹 ‘ 𝑘 ) ≤ 𝑦 ↔ 𝐵 ≤ 𝑦 ) )
19 11 18 ralbida ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑦 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 ) )
20 19 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑦 ↔ ∃ 𝑖 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 ) )
21 20 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑦 ↔ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 ) )
22 breq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐵 ≤ 𝑦 ↔ 𝐵 ≤ 𝑥 ) )
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 ⊢ ( 𝜑 → ( 𝐹 ~~>* -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝐵 ≤ 𝑥 ) )