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	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( 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	ffvelrnda	⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( 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 · 𝑅 ) ) ) )

Metamath Proof Explorer

Theorem caucvgrlem

Proof