This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem caucvgrlem

Description: Lemma for caurcvgr . (Contributed by Mario Carneiro, 15-Feb-2014) (Revised by AV, 12-Sep-2020)

Ref Expression
Hypotheses caurcvgr.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
caurcvgr.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
caurcvgr.3 ⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
caurcvgr.4 ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
caucvgrlem.4 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
Assertion caucvgrlem ( 𝜑 → ∃ 𝑗 ∈ 𝐴 ( ( lim sup ‘ 𝐹 ) ∈ ℝ ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · 𝑅 ) ) ) )

Proof

Step Hyp Ref Expression
1 caurcvgr.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 caurcvgr.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
3 caurcvgr.3 ⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
4 caurcvgr.4 ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
5 caucvgrlem.4 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
6 reex ⊢ ℝ ∈ V
7 6 ssex ⊢ ( 𝐴 ⊆ ℝ → 𝐴 ∈ V )
8 1 7 syl ⊢ ( 𝜑 → 𝐴 ∈ V )
9 6 a1i ⊢ ( 𝜑 → ℝ ∈ V )
10 fex2 ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ V ∧ ℝ ∈ V ) → 𝐹 ∈ V )
11 2 8 9 10 syl3anc ⊢ ( 𝜑 → 𝐹 ∈ V )
12 limsupcl ⊢ ( 𝐹 ∈ V → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
13 11 12 syl ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
14 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
15 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → 𝐹 : 𝐴 ⟶ ℝ )
16 simprl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → 𝑗 ∈ 𝐴 )
17 15 16 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
18 5 rpred ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
19 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → 𝑅 ∈ ℝ )
20 17 19 readdcld ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → ( ( 𝐹 ‘ 𝑗 ) + 𝑅 ) ∈ ℝ )
21 mnfxr ⊢ -∞ ∈ ℝ*
22 21 a1i ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → -∞ ∈ ℝ* )
23 17 19 resubcld ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) ∈ ℝ )
24 23 rexrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) ∈ ℝ* )
25 23 mnfltd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → -∞ < ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) )
26 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → 𝐴 ⊆ ℝ )
27 ressxr ⊢ ℝ ⊆ ℝ*
28 fss ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ ℝ ⊆ ℝ* ) → 𝐹 : 𝐴 ⟶ ℝ* )
29 2 27 28 sylancl ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
30 29 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → 𝐹 : 𝐴 ⟶ ℝ* )
31 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → sup ( 𝐴 , ℝ* , < ) = +∞ )
32 26 16 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → 𝑗 ∈ ℝ )
33 simprr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) )
34 breq2 ⊢ ( 𝑘 = 𝑚 → ( 𝑗 ≤ 𝑘 ↔ 𝑗 ≤ 𝑚 ) )
35 34 imbrov2fvoveq ⊢ ( 𝑘 = 𝑚 → ( ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ↔ ( 𝑗 ≤ 𝑚 → ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) )
36 35 cbvralvw ⊢ ( ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ↔ ∀ 𝑚 ∈ 𝐴 ( 𝑗 ≤ 𝑚 → ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) )
37 33 36 sylib ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → ∀ 𝑚 ∈ 𝐴 ( 𝑗 ≤ 𝑚 → ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) )
38 15 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ 𝑚 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑚 ) ∈ ℝ )
39 17 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ 𝑚 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
40 38 39 resubcld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ )
41 40 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ∈ ℂ )
42 41 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ 𝑚 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ )
43 19 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ 𝑚 ∈ 𝐴 ) → 𝑅 ∈ ℝ )
44 ltle ⊢ ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) ≤ 𝑅 ) )
45 42 43 44 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) ≤ 𝑅 ) )
46 38 39 43 absdifled ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) ≤ 𝑅 ↔ ( ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) ≤ ( 𝐹 ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑚 ) ≤ ( ( 𝐹 ‘ 𝑗 ) + 𝑅 ) ) ) )
47 45 46 sylibd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 → ( ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) ≤ ( 𝐹 ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑚 ) ≤ ( ( 𝐹 ‘ 𝑗 ) + 𝑅 ) ) ) )
48 simpl ⊢ ( ( ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) ≤ ( 𝐹 ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑚 ) ≤ ( ( 𝐹 ‘ 𝑗 ) + 𝑅 ) ) → ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) ≤ ( 𝐹 ‘ 𝑚 ) )
49 47 48 syl6 ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 → ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) ≤ ( 𝐹 ‘ 𝑚 ) ) )
50 49 imim2d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( 𝑗 ≤ 𝑚 → ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) → ( 𝑗 ≤ 𝑚 → ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) ≤ ( 𝐹 ‘ 𝑚 ) ) ) )
51 50 ralimdva ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → ( ∀ 𝑚 ∈ 𝐴 ( 𝑗 ≤ 𝑚 → ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) → ∀ 𝑚 ∈ 𝐴 ( 𝑗 ≤ 𝑚 → ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) ≤ ( 𝐹 ‘ 𝑚 ) ) ) )
52 37 51 mpd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → ∀ 𝑚 ∈ 𝐴 ( 𝑗 ≤ 𝑚 → ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) ≤ ( 𝐹 ‘ 𝑚 ) ) )
53 breq1 ⊢ ( 𝑛 = 𝑗 → ( 𝑛 ≤ 𝑚 ↔ 𝑗 ≤ 𝑚 ) )
54 53 rspceaimv ⊢ ( ( 𝑗 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝐴 ( 𝑗 ≤ 𝑚 → ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) ≤ ( 𝐹 ‘ 𝑚 ) ) ) → ∃ 𝑛 ∈ ℝ ∀ 𝑚 ∈ 𝐴 ( 𝑛 ≤ 𝑚 → ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) ≤ ( 𝐹 ‘ 𝑚 ) ) )
55 32 52 54 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → ∃ 𝑛 ∈ ℝ ∀ 𝑚 ∈ 𝐴 ( 𝑛 ≤ 𝑚 → ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) ≤ ( 𝐹 ‘ 𝑚 ) ) )
56 26 30 24 31 55 limsupbnd2 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) ≤ ( lim sup ‘ 𝐹 ) )
57 22 24 14 25 56 xrltletrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → -∞ < ( lim sup ‘ 𝐹 ) )
58 20 rexrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → ( ( 𝐹 ‘ 𝑗 ) + 𝑅 ) ∈ ℝ* )
59 42 adantrr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ )
60 19 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → 𝑅 ∈ ℝ )
61 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → 𝑗 ≤ 𝑚 )
62 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) )
63 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → 𝑚 ∈ 𝐴 )
64 35 62 63 rspcdva ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( 𝑗 ≤ 𝑚 → ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) )
65 61 64 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 )
66 59 60 65 ltled ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) ≤ 𝑅 )
67 38 adantrr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( 𝐹 ‘ 𝑚 ) ∈ ℝ )
68 17 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
69 67 68 60 absdifled ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( 𝐹 ‘ 𝑗 ) ) ) ≤ 𝑅 ↔ ( ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) ≤ ( 𝐹 ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑚 ) ≤ ( ( 𝐹 ‘ 𝑗 ) + 𝑅 ) ) ) )
70 66 69 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) ≤ ( 𝐹 ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑚 ) ≤ ( ( 𝐹 ‘ 𝑗 ) + 𝑅 ) ) )
71 70 simprd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( 𝐹 ‘ 𝑚 ) ≤ ( ( 𝐹 ‘ 𝑗 ) + 𝑅 ) )
72 71 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ 𝑚 ∈ 𝐴 ) → ( 𝑗 ≤ 𝑚 → ( 𝐹 ‘ 𝑚 ) ≤ ( ( 𝐹 ‘ 𝑗 ) + 𝑅 ) ) )
73 72 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → ∀ 𝑚 ∈ 𝐴 ( 𝑗 ≤ 𝑚 → ( 𝐹 ‘ 𝑚 ) ≤ ( ( 𝐹 ‘ 𝑗 ) + 𝑅 ) ) )
74 53 rspceaimv ⊢ ( ( 𝑗 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝐴 ( 𝑗 ≤ 𝑚 → ( 𝐹 ‘ 𝑚 ) ≤ ( ( 𝐹 ‘ 𝑗 ) + 𝑅 ) ) ) → ∃ 𝑛 ∈ ℝ ∀ 𝑚 ∈ 𝐴 ( 𝑛 ≤ 𝑚 → ( 𝐹 ‘ 𝑚 ) ≤ ( ( 𝐹 ‘ 𝑗 ) + 𝑅 ) ) )
75 32 73 74 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → ∃ 𝑛 ∈ ℝ ∀ 𝑚 ∈ 𝐴 ( 𝑛 ≤ 𝑚 → ( 𝐹 ‘ 𝑚 ) ≤ ( ( 𝐹 ‘ 𝑗 ) + 𝑅 ) ) )
76 26 30 58 75 limsupbnd1 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → ( lim sup ‘ 𝐹 ) ≤ ( ( 𝐹 ‘ 𝑗 ) + 𝑅 ) )
77 xrre ⊢ ( ( ( ( lim sup ‘ 𝐹 ) ∈ ℝ* ∧ ( ( 𝐹 ‘ 𝑗 ) + 𝑅 ) ∈ ℝ ) ∧ ( -∞ < ( lim sup ‘ 𝐹 ) ∧ ( lim sup ‘ 𝐹 ) ≤ ( ( 𝐹 ‘ 𝑗 ) + 𝑅 ) ) ) → ( lim sup ‘ 𝐹 ) ∈ ℝ )
78 14 20 57 76 77 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → ( lim sup ‘ 𝐹 ) ∈ ℝ )
79 78 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( lim sup ‘ 𝐹 ) ∈ ℝ )
80 67 79 resubcld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑚 ) − ( lim sup ‘ 𝐹 ) ) ∈ ℝ )
81 80 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑚 ) − ( lim sup ‘ 𝐹 ) ) ∈ ℂ )
82 81 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( lim sup ‘ 𝐹 ) ) ) ∈ ℝ )
83 2re ⊢ 2 ∈ ℝ
84 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( 2 · 𝑅 ) ∈ ℝ )
85 83 60 84 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( 2 · 𝑅 ) ∈ ℝ )
86 3re ⊢ 3 ∈ ℝ
87 remulcl ⊢ ( ( 3 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( 3 · 𝑅 ) ∈ ℝ )
88 86 60 87 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( 3 · 𝑅 ) ∈ ℝ )
89 67 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( 𝐹 ‘ 𝑚 ) ∈ ℂ )
90 79 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( lim sup ‘ 𝐹 ) ∈ ℂ )
91 89 90 abssubd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( lim sup ‘ 𝐹 ) ) ) = ( abs ‘ ( ( lim sup ‘ 𝐹 ) − ( 𝐹 ‘ 𝑚 ) ) ) )
92 67 85 resubcld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑚 ) − ( 2 · 𝑅 ) ) ∈ ℝ )
93 23 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) ∈ ℝ )
94 60 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → 𝑅 ∈ ℂ )
95 94 2timesd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( 2 · 𝑅 ) = ( 𝑅 + 𝑅 ) )
96 95 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑚 ) − ( 2 · 𝑅 ) ) = ( ( 𝐹 ‘ 𝑚 ) − ( 𝑅 + 𝑅 ) ) )
97 89 94 94 subsub4d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( ( 𝐹 ‘ 𝑚 ) − 𝑅 ) − 𝑅 ) = ( ( 𝐹 ‘ 𝑚 ) − ( 𝑅 + 𝑅 ) ) )
98 96 97 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑚 ) − ( 2 · 𝑅 ) ) = ( ( ( 𝐹 ‘ 𝑚 ) − 𝑅 ) − 𝑅 ) )
99 67 60 resubcld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑚 ) − 𝑅 ) ∈ ℝ )
100 67 60 68 lesubaddd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( ( 𝐹 ‘ 𝑚 ) − 𝑅 ) ≤ ( 𝐹 ‘ 𝑗 ) ↔ ( 𝐹 ‘ 𝑚 ) ≤ ( ( 𝐹 ‘ 𝑗 ) + 𝑅 ) ) )
101 71 100 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑚 ) − 𝑅 ) ≤ ( 𝐹 ‘ 𝑗 ) )
102 99 68 60 101 lesub1dd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( ( 𝐹 ‘ 𝑚 ) − 𝑅 ) − 𝑅 ) ≤ ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) )
103 98 102 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑚 ) − ( 2 · 𝑅 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) )
104 56 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) ≤ ( lim sup ‘ 𝐹 ) )
105 92 93 79 103 104 letrd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑚 ) − ( 2 · 𝑅 ) ) ≤ ( lim sup ‘ 𝐹 ) )
106 20 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑗 ) + 𝑅 ) ∈ ℝ )
107 67 85 readdcld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑚 ) + ( 2 · 𝑅 ) ) ∈ ℝ )
108 76 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( lim sup ‘ 𝐹 ) ≤ ( ( 𝐹 ‘ 𝑗 ) + 𝑅 ) )
109 67 60 readdcld ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑚 ) + 𝑅 ) ∈ ℝ )
110 70 48 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) ≤ ( 𝐹 ‘ 𝑚 ) )
111 68 60 67 lesubaddd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( ( 𝐹 ‘ 𝑗 ) − 𝑅 ) ≤ ( 𝐹 ‘ 𝑚 ) ↔ ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝐹 ‘ 𝑚 ) + 𝑅 ) ) )
112 110 111 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝐹 ‘ 𝑚 ) + 𝑅 ) )
113 68 109 60 112 leadd1dd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑗 ) + 𝑅 ) ≤ ( ( ( 𝐹 ‘ 𝑚 ) + 𝑅 ) + 𝑅 ) )
114 89 94 94 addassd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( ( 𝐹 ‘ 𝑚 ) + 𝑅 ) + 𝑅 ) = ( ( 𝐹 ‘ 𝑚 ) + ( 𝑅 + 𝑅 ) ) )
115 95 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑚 ) + ( 2 · 𝑅 ) ) = ( ( 𝐹 ‘ 𝑚 ) + ( 𝑅 + 𝑅 ) ) )
116 114 115 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( ( 𝐹 ‘ 𝑚 ) + 𝑅 ) + 𝑅 ) = ( ( 𝐹 ‘ 𝑚 ) + ( 2 · 𝑅 ) ) )
117 113 116 breqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑗 ) + 𝑅 ) ≤ ( ( 𝐹 ‘ 𝑚 ) + ( 2 · 𝑅 ) ) )
118 79 106 107 108 117 letrd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( lim sup ‘ 𝐹 ) ≤ ( ( 𝐹 ‘ 𝑚 ) + ( 2 · 𝑅 ) ) )
119 79 67 85 absdifled ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( ( abs ‘ ( ( lim sup ‘ 𝐹 ) − ( 𝐹 ‘ 𝑚 ) ) ) ≤ ( 2 · 𝑅 ) ↔ ( ( ( 𝐹 ‘ 𝑚 ) − ( 2 · 𝑅 ) ) ≤ ( lim sup ‘ 𝐹 ) ∧ ( lim sup ‘ 𝐹 ) ≤ ( ( 𝐹 ‘ 𝑚 ) + ( 2 · 𝑅 ) ) ) ) )
120 105 118 119 mpbir2and ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( abs ‘ ( ( lim sup ‘ 𝐹 ) − ( 𝐹 ‘ 𝑚 ) ) ) ≤ ( 2 · 𝑅 ) )
121 91 120 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( lim sup ‘ 𝐹 ) ) ) ≤ ( 2 · 𝑅 ) )
122 2lt3 ⊢ 2 < 3
123 83 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → 2 ∈ ℝ )
124 86 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → 3 ∈ ℝ )
125 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → 𝑅 ∈ ℝ+ )
126 125 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → 𝑅 ∈ ℝ+ )
127 123 124 126 ltmul1d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( 2 < 3 ↔ ( 2 · 𝑅 ) < ( 3 · 𝑅 ) ) )
128 122 127 mpbii ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( 2 · 𝑅 ) < ( 3 · 𝑅 ) )
129 82 85 88 121 128 lelttrd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑗 ≤ 𝑚 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · 𝑅 ) )
130 129 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) ∧ 𝑚 ∈ 𝐴 ) → ( 𝑗 ≤ 𝑚 → ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · 𝑅 ) ) )
131 130 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → ∀ 𝑚 ∈ 𝐴 ( 𝑗 ≤ 𝑚 → ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · 𝑅 ) ) )
132 34 imbrov2fvoveq ⊢ ( 𝑘 = 𝑚 → ( ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · 𝑅 ) ) ↔ ( 𝑗 ≤ 𝑚 → ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · 𝑅 ) ) ) )
133 132 cbvralvw ⊢ ( ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · 𝑅 ) ) ↔ ∀ 𝑚 ∈ 𝐴 ( 𝑗 ≤ 𝑚 → ( abs ‘ ( ( 𝐹 ‘ 𝑚 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · 𝑅 ) ) )
134 131 133 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · 𝑅 ) ) )
135 78 134 jca ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) ) → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · 𝑅 ) ) ) )
136 breq2 ⊢ ( 𝑥 = 𝑅 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) )
137 136 imbi2d ⊢ ( 𝑥 = 𝑅 → ( ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) )
138 137 rexralbidv ⊢ ( 𝑥 = 𝑅 → ( ∃ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) ) )
139 138 4 5 rspcdva ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑅 ) )
140 135 139 reximddv ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝐴 ( ( lim sup ‘ 𝐹 ) ∈ ℝ ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · 𝑅 ) ) ) )