Metamath Proof Explorer

Theorem xlimmnfv

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

Proof

Step Hyp Ref Expression
1 xlimmnfv.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 xlimmnfv.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 xlimmnfv.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
4 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* -∞ ) ∧ 𝑥 ∈ ℝ ) → 𝑀 ∈ ℤ )
5 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* -∞ ) ∧ 𝑥 ∈ ℝ ) → 𝐹 : 𝑍 ⟶ ℝ* )
6 simplr ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* -∞ ) ∧ 𝑥 ∈ ℝ ) → 𝐹 ~~>* -∞ )
7 simpr ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* -∞ ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
8 4 2 5 6 7 xlimmnfvlem1 ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* -∞ ) ∧ 𝑥 ∈ ℝ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 )
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 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝐹 : 𝑍 ⟶ ℝ* )
27 2 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
28 27 3adant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
29 26 28 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
30 29 ad5ant134 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝐹 ‘ 𝑘 ) ≤ ( 𝑦 − 1 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
31 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝐹 ‘ 𝑘 ) ≤ ( 𝑦 − 1 ) ) → 𝑦 ∈ ℝ )
32 peano2rem ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 − 1 ) ∈ ℝ )
33 32 rexrd ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 − 1 ) ∈ ℝ* )
34 31 33 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝐹 ‘ 𝑘 ) ≤ ( 𝑦 − 1 ) ) → ( 𝑦 − 1 ) ∈ ℝ* )
35 rexr ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℝ* )
36 35 ad4antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝐹 ‘ 𝑘 ) ≤ ( 𝑦 − 1 ) ) → 𝑦 ∈ ℝ* )
37 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝐹 ‘ 𝑘 ) ≤ ( 𝑦 − 1 ) ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝑦 − 1 ) )
38 31 ltm1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝐹 ‘ 𝑘 ) ≤ ( 𝑦 − 1 ) ) → ( 𝑦 − 1 ) < 𝑦 )
39 30 34 36 37 38 xrlelttrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝐹 ‘ 𝑘 ) ≤ ( 𝑦 − 1 ) ) → ( 𝐹 ‘ 𝑘 ) < 𝑦 )
40 39 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐹 ‘ 𝑘 ) ≤ ( 𝑦 − 1 ) → ( 𝐹 ‘ 𝑘 ) < 𝑦 ) )
41 40 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ ( 𝑦 − 1 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) < 𝑦 ) )
42 41 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ ( 𝑦 − 1 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) < 𝑦 )
43 42 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ ( 𝑦 − 1 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) < 𝑦 )
44 43 3impa ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ ( 𝑦 − 1 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) < 𝑦 )
45 32 adantl ⊢ ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ∧ 𝑦 ∈ ℝ ) → ( 𝑦 − 1 ) ∈ ℝ )
46 simpl ⊢ ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ∧ 𝑦 ∈ ℝ ) → ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 )
47 breq2 ⊢ ( 𝑥 = ( 𝑦 − 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 xlimmnfvlem2 ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) → 𝐹 ~~>* -∞ )
56 9 55 impbida ⊢ ( 𝜑 → ( 𝐹 ~~>* -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) )