# Metamath Proof Explorer

## Theorem limsupgtlem

Description: For any positive real, the superior limit of F is larger than any of its values at large enough arguments, up to that positive real. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses limsupgtlem.m $⊢ φ → M ∈ ℤ$
limsupgtlem.z $⊢ Z = ℤ ≥ M$
limsupgtlem.f $⊢ φ → F : Z ⟶ ℝ$
limsupgtlem.r $⊢ φ → lim sup ⁡ F ∈ ℝ$
limsupgtlem.x $⊢ φ → X ∈ ℝ +$
Assertion limsupgtlem $⊢ φ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j F ⁡ k − X < lim sup ⁡ F$

### Proof

Step Hyp Ref Expression
1 limsupgtlem.m $⊢ φ → M ∈ ℤ$
2 limsupgtlem.z $⊢ Z = ℤ ≥ M$
3 limsupgtlem.f $⊢ φ → F : Z ⟶ ℝ$
4 limsupgtlem.r $⊢ φ → lim sup ⁡ F ∈ ℝ$
5 limsupgtlem.x $⊢ φ → X ∈ ℝ +$
6 nfv $⊢ Ⅎ j φ$
7 1 2 uzn0d $⊢ φ → Z ≠ ∅$
8 rnresss $⊢ ran ⁡ F ↾ ℤ ≥ j ⊆ ran ⁡ F$
9 8 a1i $⊢ φ → ran ⁡ F ↾ ℤ ≥ j ⊆ ran ⁡ F$
10 3 frexr $⊢ φ → F : Z ⟶ ℝ *$
11 10 frnd $⊢ φ → ran ⁡ F ⊆ ℝ *$
12 9 11 sstrd $⊢ φ → ran ⁡ F ↾ ℤ ≥ j ⊆ ℝ *$
13 12 supxrcld $⊢ φ → sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ∈ ℝ *$
14 13 adantr $⊢ φ ∧ j ∈ Z → sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ∈ ℝ *$
15 nfcv $⊢ Ⅎ _ k F$
16 15 1 2 3 limsupreuz $⊢ φ → lim sup ⁡ F ∈ ℝ ↔ ∃ x ∈ ℝ ∀ j ∈ Z ∃ k ∈ ℤ ≥ j x ≤ F ⁡ k ∧ ∃ x ∈ ℝ ∀ k ∈ Z F ⁡ k ≤ x$
17 4 16 mpbid $⊢ φ → ∃ x ∈ ℝ ∀ j ∈ Z ∃ k ∈ ℤ ≥ j x ≤ F ⁡ k ∧ ∃ x ∈ ℝ ∀ k ∈ Z F ⁡ k ≤ x$
18 17 simpld $⊢ φ → ∃ x ∈ ℝ ∀ j ∈ Z ∃ k ∈ ℤ ≥ j x ≤ F ⁡ k$
19 rexr $⊢ x ∈ ℝ → x ∈ ℝ *$
20 19 ad4antlr $⊢ φ ∧ x ∈ ℝ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j ∧ x ≤ F ⁡ k → x ∈ ℝ *$
21 3 ad2antrr $⊢ φ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j → F : Z ⟶ ℝ$
22 2 uztrn2 $⊢ j ∈ Z ∧ k ∈ ℤ ≥ j → k ∈ Z$
23 22 adantll $⊢ φ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j → k ∈ Z$
24 21 23 ffvelrnd $⊢ φ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j → F ⁡ k ∈ ℝ$
25 24 rexrd $⊢ φ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j → F ⁡ k ∈ ℝ *$
26 25 3impa $⊢ φ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j → F ⁡ k ∈ ℝ *$
27 26 ad5ant134 $⊢ φ ∧ x ∈ ℝ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j ∧ x ≤ F ⁡ k → F ⁡ k ∈ ℝ *$
28 13 ad4antr $⊢ φ ∧ x ∈ ℝ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j ∧ x ≤ F ⁡ k → sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ∈ ℝ *$
29 simpr $⊢ φ ∧ x ∈ ℝ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j ∧ x ≤ F ⁡ k → x ≤ F ⁡ k$
30 12 ad2antrr $⊢ φ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j → ran ⁡ F ↾ ℤ ≥ j ⊆ ℝ *$
31 fvres $⊢ k ∈ ℤ ≥ j → F ↾ ℤ ≥ j ⁡ k = F ⁡ k$
32 31 eqcomd $⊢ k ∈ ℤ ≥ j → F ⁡ k = F ↾ ℤ ≥ j ⁡ k$
33 32 adantl $⊢ φ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j → F ⁡ k = F ↾ ℤ ≥ j ⁡ k$
34 3 ffnd $⊢ φ → F Fn Z$
35 34 adantr $⊢ φ ∧ j ∈ Z → F Fn Z$
36 23 ssd $⊢ φ ∧ j ∈ Z → ℤ ≥ j ⊆ Z$
37 fnssres $⊢ F Fn Z ∧ ℤ ≥ j ⊆ Z → F ↾ ℤ ≥ j Fn ℤ ≥ j$
38 35 36 37 syl2anc $⊢ φ ∧ j ∈ Z → F ↾ ℤ ≥ j Fn ℤ ≥ j$
39 38 adantr $⊢ φ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j → F ↾ ℤ ≥ j Fn ℤ ≥ j$
40 simpr $⊢ φ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j → k ∈ ℤ ≥ j$
41 39 40 fnfvelrnd $⊢ φ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j → F ↾ ℤ ≥ j ⁡ k ∈ ran ⁡ F ↾ ℤ ≥ j$
42 33 41 eqeltrd $⊢ φ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j → F ⁡ k ∈ ran ⁡ F ↾ ℤ ≥ j$
43 eqid $⊢ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < = sup ran ⁡ F ↾ ℤ ≥ j ℝ * <$
44 30 42 43 supxrubd $⊢ φ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j → F ⁡ k ≤ sup ran ⁡ F ↾ ℤ ≥ j ℝ * <$
45 44 3impa $⊢ φ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j → F ⁡ k ≤ sup ran ⁡ F ↾ ℤ ≥ j ℝ * <$
46 45 ad5ant134 $⊢ φ ∧ x ∈ ℝ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j ∧ x ≤ F ⁡ k → F ⁡ k ≤ sup ran ⁡ F ↾ ℤ ≥ j ℝ * <$
47 20 27 28 29 46 xrletrd $⊢ φ ∧ x ∈ ℝ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j ∧ x ≤ F ⁡ k → x ≤ sup ran ⁡ F ↾ ℤ ≥ j ℝ * <$
48 47 rexlimdva2 $⊢ φ ∧ x ∈ ℝ ∧ j ∈ Z → ∃ k ∈ ℤ ≥ j x ≤ F ⁡ k → x ≤ sup ran ⁡ F ↾ ℤ ≥ j ℝ * <$
49 48 ralimdva $⊢ φ ∧ x ∈ ℝ → ∀ j ∈ Z ∃ k ∈ ℤ ≥ j x ≤ F ⁡ k → ∀ j ∈ Z x ≤ sup ran ⁡ F ↾ ℤ ≥ j ℝ * <$
50 49 reximdva $⊢ φ → ∃ x ∈ ℝ ∀ j ∈ Z ∃ k ∈ ℤ ≥ j x ≤ F ⁡ k → ∃ x ∈ ℝ ∀ j ∈ Z x ≤ sup ran ⁡ F ↾ ℤ ≥ j ℝ * <$
51 18 50 mpd $⊢ φ → ∃ x ∈ ℝ ∀ j ∈ Z x ≤ sup ran ⁡ F ↾ ℤ ≥ j ℝ * <$
52 5 rphalfcld $⊢ φ → X 2 ∈ ℝ +$
53 6 7 14 51 52 infrpgernmpt $⊢ φ → ∃ j ∈ Z sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ≤ sup ran ⁡ j ∈ Z ⟼ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ℝ * < + 𝑒 X 2$
54 simp3 $⊢ φ ∧ j ∈ Z ∧ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ≤ sup ran ⁡ j ∈ Z ⟼ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ℝ * < + 𝑒 X 2 → sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ≤ sup ran ⁡ j ∈ Z ⟼ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ℝ * < + 𝑒 X 2$
55 1 2 10 limsupvaluz $⊢ φ → lim sup ⁡ F = sup ran ⁡ j ∈ Z ⟼ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ℝ * <$
56 55 eqcomd $⊢ φ → sup ran ⁡ j ∈ Z ⟼ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ℝ * < = lim sup ⁡ F$
57 56 oveq1d $⊢ φ → sup ran ⁡ j ∈ Z ⟼ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ℝ * < + 𝑒 X 2 = lim sup ⁡ F + 𝑒 X 2$
58 57 3ad2ant1 $⊢ φ ∧ j ∈ Z ∧ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ≤ sup ran ⁡ j ∈ Z ⟼ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ℝ * < + 𝑒 X 2 → sup ran ⁡ j ∈ Z ⟼ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ℝ * < + 𝑒 X 2 = lim sup ⁡ F + 𝑒 X 2$
59 54 58 breqtrd $⊢ φ ∧ j ∈ Z ∧ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ≤ sup ran ⁡ j ∈ Z ⟼ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ℝ * < + 𝑒 X 2 → sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ≤ lim sup ⁡ F + 𝑒 X 2$
60 25 3adantl3 $⊢ φ ∧ j ∈ Z ∧ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ≤ lim sup ⁡ F + 𝑒 X 2 ∧ k ∈ ℤ ≥ j → F ⁡ k ∈ ℝ *$
61 simpl1 $⊢ φ ∧ j ∈ Z ∧ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ≤ lim sup ⁡ F + 𝑒 X 2 ∧ k ∈ ℤ ≥ j → φ$
62 61 13 syl $⊢ φ ∧ j ∈ Z ∧ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ≤ lim sup ⁡ F + 𝑒 X 2 ∧ k ∈ ℤ ≥ j → sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ∈ ℝ *$
63 2 fvexi $⊢ Z ∈ V$
64 63 a1i $⊢ φ → Z ∈ V$
65 3 64 fexd $⊢ φ → F ∈ V$
66 65 limsupcld $⊢ φ → lim sup ⁡ F ∈ ℝ *$
67 5 rpred $⊢ φ → X ∈ ℝ$
68 67 rehalfcld $⊢ φ → X 2 ∈ ℝ$
69 68 rexrd $⊢ φ → X 2 ∈ ℝ *$
70 66 69 xaddcld $⊢ φ → lim sup ⁡ F + 𝑒 X 2 ∈ ℝ *$
71 61 70 syl $⊢ φ ∧ j ∈ Z ∧ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ≤ lim sup ⁡ F + 𝑒 X 2 ∧ k ∈ ℤ ≥ j → lim sup ⁡ F + 𝑒 X 2 ∈ ℝ *$
72 44 3adantl3 $⊢ φ ∧ j ∈ Z ∧ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ≤ lim sup ⁡ F + 𝑒 X 2 ∧ k ∈ ℤ ≥ j → F ⁡ k ≤ sup ran ⁡ F ↾ ℤ ≥ j ℝ * <$
73 simpl3 $⊢ φ ∧ j ∈ Z ∧ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ≤ lim sup ⁡ F + 𝑒 X 2 ∧ k ∈ ℤ ≥ j → sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ≤ lim sup ⁡ F + 𝑒 X 2$
74 60 62 71 72 73 xrletrd $⊢ φ ∧ j ∈ Z ∧ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ≤ lim sup ⁡ F + 𝑒 X 2 ∧ k ∈ ℤ ≥ j → F ⁡ k ≤ lim sup ⁡ F + 𝑒 X 2$
75 4 68 rexaddd $⊢ φ → lim sup ⁡ F + 𝑒 X 2 = lim sup ⁡ F + X 2$
76 61 75 syl $⊢ φ ∧ j ∈ Z ∧ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ≤ lim sup ⁡ F + 𝑒 X 2 ∧ k ∈ ℤ ≥ j → lim sup ⁡ F + 𝑒 X 2 = lim sup ⁡ F + X 2$
77 74 76 breqtrd $⊢ φ ∧ j ∈ Z ∧ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ≤ lim sup ⁡ F + 𝑒 X 2 ∧ k ∈ ℤ ≥ j → F ⁡ k ≤ lim sup ⁡ F + X 2$
78 68 ad2antrr $⊢ φ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j → X 2 ∈ ℝ$
79 4 ad2antrr $⊢ φ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j → lim sup ⁡ F ∈ ℝ$
80 24 78 79 lesubaddd $⊢ φ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j → F ⁡ k − X 2 ≤ lim sup ⁡ F ↔ F ⁡ k ≤ lim sup ⁡ F + X 2$
81 80 3adantl3 $⊢ φ ∧ j ∈ Z ∧ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ≤ lim sup ⁡ F + 𝑒 X 2 ∧ k ∈ ℤ ≥ j → F ⁡ k − X 2 ≤ lim sup ⁡ F ↔ F ⁡ k ≤ lim sup ⁡ F + X 2$
82 77 81 mpbird $⊢ φ ∧ j ∈ Z ∧ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ≤ lim sup ⁡ F + 𝑒 X 2 ∧ k ∈ ℤ ≥ j → F ⁡ k − X 2 ≤ lim sup ⁡ F$
83 82 ralrimiva $⊢ φ ∧ j ∈ Z ∧ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ≤ lim sup ⁡ F + 𝑒 X 2 → ∀ k ∈ ℤ ≥ j F ⁡ k − X 2 ≤ lim sup ⁡ F$
84 59 83 syld3an3 $⊢ φ ∧ j ∈ Z ∧ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ≤ sup ran ⁡ j ∈ Z ⟼ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ℝ * < + 𝑒 X 2 → ∀ k ∈ ℤ ≥ j F ⁡ k − X 2 ≤ lim sup ⁡ F$
85 84 3exp $⊢ φ → j ∈ Z → sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ≤ sup ran ⁡ j ∈ Z ⟼ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ℝ * < + 𝑒 X 2 → ∀ k ∈ ℤ ≥ j F ⁡ k − X 2 ≤ lim sup ⁡ F$
86 6 85 reximdai $⊢ φ → ∃ j ∈ Z sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ≤ sup ran ⁡ j ∈ Z ⟼ sup ran ⁡ F ↾ ℤ ≥ j ℝ * < ℝ * < + 𝑒 X 2 → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j F ⁡ k − X 2 ≤ lim sup ⁡ F$
87 53 86 mpd $⊢ φ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j F ⁡ k − X 2 ≤ lim sup ⁡ F$
88 simpll $⊢ φ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j → φ$
89 3 ffvelrnda $⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℝ$
90 67 adantr $⊢ φ ∧ k ∈ Z → X ∈ ℝ$
91 89 90 resubcld $⊢ φ ∧ k ∈ Z → F ⁡ k − X ∈ ℝ$
92 91 adantr $⊢ φ ∧ k ∈ Z ∧ F ⁡ k − X 2 ≤ lim sup ⁡ F → F ⁡ k − X ∈ ℝ$
93 68 adantr $⊢ φ ∧ k ∈ Z → X 2 ∈ ℝ$
94 89 93 resubcld $⊢ φ ∧ k ∈ Z → F ⁡ k − X 2 ∈ ℝ$
95 94 adantr $⊢ φ ∧ k ∈ Z ∧ F ⁡ k − X 2 ≤ lim sup ⁡ F → F ⁡ k − X 2 ∈ ℝ$
96 4 ad2antrr $⊢ φ ∧ k ∈ Z ∧ F ⁡ k − X 2 ≤ lim sup ⁡ F → lim sup ⁡ F ∈ ℝ$
97 5 rphalfltd $⊢ φ → X 2 < X$
98 97 adantr $⊢ φ ∧ k ∈ Z → X 2 < X$
99 93 90 89 98 ltsub2dd $⊢ φ ∧ k ∈ Z → F ⁡ k − X < F ⁡ k − X 2$
100 99 adantr $⊢ φ ∧ k ∈ Z ∧ F ⁡ k − X 2 ≤ lim sup ⁡ F → F ⁡ k − X < F ⁡ k − X 2$
101 simpr $⊢ φ ∧ k ∈ Z ∧ F ⁡ k − X 2 ≤ lim sup ⁡ F → F ⁡ k − X 2 ≤ lim sup ⁡ F$
102 92 95 96 100 101 ltletrd $⊢ φ ∧ k ∈ Z ∧ F ⁡ k − X 2 ≤ lim sup ⁡ F → F ⁡ k − X < lim sup ⁡ F$
103 102 ex $⊢ φ ∧ k ∈ Z → F ⁡ k − X 2 ≤ lim sup ⁡ F → F ⁡ k − X < lim sup ⁡ F$
104 88 23 103 syl2anc $⊢ φ ∧ j ∈ Z ∧ k ∈ ℤ ≥ j → F ⁡ k − X 2 ≤ lim sup ⁡ F → F ⁡ k − X < lim sup ⁡ F$
105 104 ralimdva $⊢ φ ∧ j ∈ Z → ∀ k ∈ ℤ ≥ j F ⁡ k − X 2 ≤ lim sup ⁡ F → ∀ k ∈ ℤ ≥ j F ⁡ k − X < lim sup ⁡ F$
106 105 reximdva $⊢ φ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j F ⁡ k − X 2 ≤ lim sup ⁡ F → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j F ⁡ k − X < lim sup ⁡ F$
107 87 106 mpd $⊢ φ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j F ⁡ k − X < lim sup ⁡ F$