Metamath Proof Explorer


Theorem 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 ‘ 𝐹 ) )