Theorem caurcvgr

Description: A Cauchy sequence of real numbers converges to its limit supremum. The third hypothesis specifies that F is a Cauchy sequence. (Contributed by Mario Carneiro, 7-May-2016) (Revised by AV, 12-Sep-2020)

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

Proof

Step	Hyp	Ref	Expression
1		caurcvgr.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		caurcvgr.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
3		caurcvgr.3	⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
4		caurcvgr.4	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
5		1rp	⊢ 1 ∈ ℝ+
6	5	a1i	⊢ ( 𝜑 → 1 ∈ ℝ+ )
7	1 2 3 4 6	caucvgrlem	⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝐴 ( ( lim sup ‘ 𝐹 ) ∈ ℝ ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · 1 ) ) ) )
8		simpl	⊢ ( ( ( lim sup ‘ 𝐹 ) ∈ ℝ ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · 1 ) ) ) → ( lim sup ‘ 𝐹 ) ∈ ℝ )
9	8	rexlimivw	⊢ ( ∃ 𝑗 ∈ 𝐴 ( ( lim sup ‘ 𝐹 ) ∈ ℝ ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · 1 ) ) ) → ( lim sup ‘ 𝐹 ) ∈ ℝ )
10	7 9	syl	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ )
11	10	recnd	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℂ )
12	1	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝐴 ⊆ ℝ )
13	2	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝐹 : 𝐴 ⟶ ℝ )
14	3	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → sup ( 𝐴 , ℝ* , < ) = +∞ )
15	4	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
16		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ+ )
17		3rp	⊢ 3 ∈ ℝ+
18		rpdivcl	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 3 ∈ ℝ+ ) → ( 𝑦 / 3 ) ∈ ℝ+ )
19	16 17 18	sylancl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 / 3 ) ∈ ℝ+ )
20	12 13 14 15 19	caucvgrlem	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝐴 ( ( lim sup ‘ 𝐹 ) ∈ ℝ ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · ( 𝑦 / 3 ) ) ) ) )
21		simpr	⊢ ( ( ( lim sup ‘ 𝐹 ) ∈ ℝ ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · ( 𝑦 / 3 ) ) ) ) → ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · ( 𝑦 / 3 ) ) ) )
22	21	reximi	⊢ ( ∃ 𝑗 ∈ 𝐴 ( ( lim sup ‘ 𝐹 ) ∈ ℝ ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · ( 𝑦 / 3 ) ) ) ) → ∃ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · ( 𝑦 / 3 ) ) ) )
23	20 22	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · ( 𝑦 / 3 ) ) ) )
24		ssrexv	⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · ( 𝑦 / 3 ) ) ) → ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · ( 𝑦 / 3 ) ) ) ) )
25	12 23 24	sylc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · ( 𝑦 / 3 ) ) ) )
26		rpcn	⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℂ )
27	26	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℂ )
28		3cn	⊢ 3 ∈ ℂ
29	28	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 3 ∈ ℂ )
30		3ne0	⊢ 3 ≠ 0
31	30	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 3 ≠ 0 )
32	27 29 31	divcan2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 3 · ( 𝑦 / 3 ) ) = 𝑦 )
33	32	breq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · ( 𝑦 / 3 ) ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < 𝑦 ) )
34	33	imbi2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · ( 𝑦 / 3 ) ) ) ↔ ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < 𝑦 ) ) )
35	34	rexralbidv	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < ( 3 · ( 𝑦 / 3 ) ) ) ↔ ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < 𝑦 ) ) )
36	25 35	mpbid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < 𝑦 ) )
37	36	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ+ ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < 𝑦 ) )
38		ax-resscn	⊢ ℝ ⊆ ℂ
39		fss	⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ )
40	2 38 39	sylancl	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
41		eqidd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
42	40 1 41	rlim	⊢ ( 𝜑 → ( 𝐹 ⇝𝑟 ( lim sup ‘ 𝐹 ) ↔ ( ( lim sup ‘ 𝐹 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < 𝑦 ) ) ) )
43	11 37 42	mpbir2and	⊢ ( 𝜑 → 𝐹 ⇝𝑟 ( lim sup ‘ 𝐹 ) )