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 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
limsupgtlem.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
limsupgtlem.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
limsupgtlem.r ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ )
limsupgtlem.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
Assertion limsupgtlem ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) − 𝑋 ) < ( lim sup ‘ 𝐹 ) )

Proof

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