Metamath Proof Explorer

Theorem xlimpnfv

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 xlimpnfv.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
xlimpnfv.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
xlimpnfv.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
Assertion xlimpnfv ( 𝜑 → ( 𝐹 ~~>* +∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 xlimpnfv.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 xlimpnfv.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 xlimpnfv.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
4 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* +∞ ) ∧ 𝑥 ∈ ℝ ) → 𝑀 ∈ ℤ )
5 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* +∞ ) ∧ 𝑥 ∈ ℝ ) → 𝐹 : 𝑍 ⟶ ℝ* )
6 simplr ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* +∞ ) ∧ 𝑥 ∈ ℝ ) → 𝐹 ~~>* +∞ )
7 simpr ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* +∞ ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
8 4 2 5 6 7 xlimpnfvlem1 ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* +∞ ) ∧ 𝑥 ∈ ℝ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) )
9 8 ralrimiva ⊢ ( ( 𝜑 ∧ 𝐹 ~~>* +∞ ) → ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) )
10 nfv ⊢ Ⅎ 𝑘 𝜑
11 nfcv ⊢ Ⅎ 𝑘 ℝ
12 nfcv ⊢ Ⅎ 𝑘 𝑍
13 nfra1 ⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 )
14 12 13 nfrex ⊢ Ⅎ 𝑘 ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 )
15 11 14 nfralw ⊢ Ⅎ 𝑘 ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 )
16 10 15 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) )
17 nfv ⊢ Ⅎ 𝑗 𝜑
18 nfcv ⊢ Ⅎ 𝑗 ℝ
19 nfre1 ⊢ Ⅎ 𝑗 ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 )
20 18 19 nfralw ⊢ Ⅎ 𝑗 ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 )
21 17 20 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) )
22 1 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) → 𝑀 ∈ ℤ )
23 3 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) → 𝐹 : 𝑍 ⟶ ℝ* )
24 nfv ⊢ Ⅎ 𝑗 𝑦 ∈ ℝ
25 21 24 nfan ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑦 ∈ ℝ )
26 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝑦 + 1 ) ≤ ( 𝐹 ‘ 𝑘 ) ) → 𝑦 ∈ ℝ )
27 rexr ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℝ* )
28 26 27 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝑦 + 1 ) ≤ ( 𝐹 ‘ 𝑘 ) ) → 𝑦 ∈ ℝ* )
29 peano2re ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 + 1 ) ∈ ℝ )
30 29 rexrd ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 + 1 ) ∈ ℝ* )
31 26 30 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝑦 + 1 ) ≤ ( 𝐹 ‘ 𝑘 ) ) → ( 𝑦 + 1 ) ∈ ℝ* )
32 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝐹 : 𝑍 ⟶ ℝ* )
33 2 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
34 33 3adant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
35 32 34 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
36 35 ad5ant134 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝑦 + 1 ) ≤ ( 𝐹 ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
37 26 ltp1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝑦 + 1 ) ≤ ( 𝐹 ‘ 𝑘 ) ) → 𝑦 < ( 𝑦 + 1 ) )
38 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝑦 + 1 ) ≤ ( 𝐹 ‘ 𝑘 ) ) → ( 𝑦 + 1 ) ≤ ( 𝐹 ‘ 𝑘 ) )
39 28 31 36 37 38 xrltletrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝑦 + 1 ) ≤ ( 𝐹 ‘ 𝑘 ) ) → 𝑦 < ( 𝐹 ‘ 𝑘 ) )
40 39 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝑦 + 1 ) ≤ ( 𝐹 ‘ 𝑘 ) → 𝑦 < ( 𝐹 ‘ 𝑘 ) ) )
41 40 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑦 + 1 ) ≤ ( 𝐹 ‘ 𝑘 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑦 < ( 𝐹 ‘ 𝑘 ) ) )
42 41 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑦 + 1 ) ≤ ( 𝐹 ‘ 𝑘 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑦 < ( 𝐹 ‘ 𝑘 ) )
43 42 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑦 + 1 ) ≤ ( 𝐹 ‘ 𝑘 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑦 < ( 𝐹 ‘ 𝑘 ) )
44 43 3impa ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑦 + 1 ) ≤ ( 𝐹 ‘ 𝑘 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑦 < ( 𝐹 ‘ 𝑘 ) )
45 29 adantl ⊢ ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑦 + 1 ) ∈ ℝ )
46 simpl ⊢ ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ∧ 𝑦 ∈ ℝ ) → ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) )
47 breq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ↔ ( 𝑦 + 1 ) ≤ ( 𝐹 ‘ 𝑘 ) ) )
48 47 ralbidv ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑦 + 1 ) ≤ ( 𝐹 ‘ 𝑘 ) ) )
49 48 rexbidv ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑦 + 1 ) ≤ ( 𝐹 ‘ 𝑘 ) ) )
50 49 rspcva ⊢ ( ( ( 𝑦 + 1 ) ∈ ℝ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑦 + 1 ) ≤ ( 𝐹 ‘ 𝑘 ) )
51 45 46 50 syl2anc ⊢ ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ∧ 𝑦 ∈ ℝ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑦 + 1 ) ≤ ( 𝐹 ‘ 𝑘 ) )
52 51 adantll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑦 ∈ ℝ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑦 + 1 ) ≤ ( 𝐹 ‘ 𝑘 ) )
53 25 44 52 reximdd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑦 ∈ ℝ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑦 < ( 𝐹 ‘ 𝑘 ) )
54 53 ralrimiva ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) → ∀ 𝑦 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑦 < ( 𝐹 ‘ 𝑘 ) )
55 16 21 22 2 23 54 xlimpnfvlem2 ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) → 𝐹 ~~>* +∞ )
56 9 55 impbida ⊢ ( 𝜑 → ( 𝐹 ~~>* +∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) )