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