caurcvg

Description: A Cauchy sequence of real numbers converges to its limit supremum. The fourth hypothesis specifies that F is a Cauchy sequence. (Contributed by NM, 4-Apr-2005) (Revised by AV, 12-Sep-2020)

	Ref	Expression
Hypotheses	caurcvg.1	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
	caurcvg.3	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
	caurcvg.4	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 )
Assertion	caurcvg	⊢ ( 𝜑 → 𝐹 ⇝ ( lim sup ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		caurcvg.1	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
2		caurcvg.3	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
3		caurcvg.4	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 )
4		uzssz	⊢ ( ℤ_≥ ‘ 𝑀 ) ⊆ ℤ
5	1 4	eqsstri	⊢ 𝑍 ⊆ ℤ
6		zssre	⊢ ℤ ⊆ ℝ
7	5 6	sstri	⊢ 𝑍 ⊆ ℝ
8	7	a1i	⊢ ( 𝜑 → 𝑍 ⊆ ℝ )
9		1rp	⊢ 1 ∈ ℝ⁺
10	9	ne0ii	⊢ ℝ⁺ ≠ ∅
11		r19.2z	⊢ ( ( ℝ⁺ ≠ ∅ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) → ∃ 𝑥 ∈ ℝ⁺ ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 )
12	10 3 11	sylancr	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ⁺ ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 )
13		eluzel2	⊢ ( 𝑚 ∈ ( ℤ_≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
14	13 1	eleq2s	⊢ ( 𝑚 ∈ 𝑍 → 𝑀 ∈ ℤ )
15	1	uzsup	⊢ ( 𝑀 ∈ ℤ → sup ( 𝑍 , ℝ^* , < ) = +∞ )
16	14 15	syl	⊢ ( 𝑚 ∈ 𝑍 → sup ( 𝑍 , ℝ^* , < ) = +∞ )
17	16	a1d	⊢ ( 𝑚 ∈ 𝑍 → ( ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 → sup ( 𝑍 , ℝ^* , < ) = +∞ ) )
18	17	rexlimiv	⊢ ( ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 → sup ( 𝑍 , ℝ^* , < ) = +∞ )
19	18	rexlimivw	⊢ ( ∃ 𝑥 ∈ ℝ⁺ ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 → sup ( 𝑍 , ℝ^* , < ) = +∞ )
20	12 19	syl	⊢ ( 𝜑 → sup ( 𝑍 , ℝ^* , < ) = +∞ )
21	5	sseli	⊢ ( 𝑚 ∈ 𝑍 → 𝑚 ∈ ℤ )
22	5	sseli	⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ )
23		eluz	⊢ ( ( 𝑚 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ↔ 𝑚 ≤ 𝑘 ) )
24	21 22 23	syl2an	⊢ ( ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ↔ 𝑚 ≤ 𝑘 ) )
25	24	biimprd	⊢ ( ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑚 ≤ 𝑘 → 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ) )
26	25	expimpd	⊢ ( 𝑚 ∈ 𝑍 → ( ( 𝑘 ∈ 𝑍 ∧ 𝑚 ≤ 𝑘 ) → 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ) )
27	26	imim1d	⊢ ( 𝑚 ∈ 𝑍 → ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) → ( ( 𝑘 ∈ 𝑍 ∧ 𝑚 ≤ 𝑘 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) )
28	27	exp4a	⊢ ( 𝑚 ∈ 𝑍 → ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) → ( 𝑘 ∈ 𝑍 → ( 𝑚 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) ) )
29	28	ralimdv2	⊢ ( 𝑚 ∈ 𝑍 → ( ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 → ∀ 𝑘 ∈ 𝑍 ( 𝑚 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) )
30	29	reximia	⊢ ( ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 → ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ 𝑍 ( 𝑚 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
31	30	ralimi	⊢ ( ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 → ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ 𝑍 ( 𝑚 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
32	3 31	syl	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ 𝑍 ( 𝑚 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
33	8 2 20 32	caurcvgr	⊢ ( 𝜑 → 𝐹 ⇝_𝑟 ( lim sup ‘ 𝐹 ) )
34	14	a1d	⊢ ( 𝑚 ∈ 𝑍 → ( ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 → 𝑀 ∈ ℤ ) )
35	34	rexlimiv	⊢ ( ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 → 𝑀 ∈ ℤ )
36	35	rexlimivw	⊢ ( ∃ 𝑥 ∈ ℝ⁺ ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 → 𝑀 ∈ ℤ )
37	12 36	syl	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
38		ax-resscn	⊢ ℝ ⊆ ℂ
39		fss	⊢ ( ( 𝐹 : 𝑍 ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : 𝑍 ⟶ ℂ )
40	2 38 39	sylancl	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℂ )
41	1 37 40	rlimclim	⊢ ( 𝜑 → ( 𝐹 ⇝_𝑟 ( lim sup ‘ 𝐹 ) ↔ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ) )
42	33 41	mpbid	⊢ ( 𝜑 → 𝐹 ⇝ ( lim sup ‘ 𝐹 ) )

Metamath Proof Explorer

Theorem caurcvg

Proof