Metamath Proof Explorer

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