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 Β· 𝑅 ) ) ) )