Metamath Proof Explorer


Theorem caurcvg2

Description: A Cauchy sequence of real numbers converges, existence version. (Contributed by NM, 4-Apr-2005) (Revised by Mario Carneiro, 7-Sep-2014)

Ref Expression
Hypotheses caucvg.1 𝑍 = ( ℤ𝑀 )
caurcvg2.2 ( 𝜑𝐹𝑉 )
caurcvg2.3 ( 𝜑 → ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) )
Assertion caurcvg2 ( 𝜑𝐹 ∈ dom ⇝ )

Proof

Step Hyp Ref Expression
1 caucvg.1 𝑍 = ( ℤ𝑀 )
2 caurcvg2.2 ( 𝜑𝐹𝑉 )
3 caurcvg2.3 ( 𝜑 → ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) )
4 1rp 1 ∈ ℝ+
5 4 ne0ii + ≠ ∅
6 r19.2z ( ( ℝ+ ≠ ∅ ∧ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ) → ∃ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) )
7 5 3 6 sylancr ( 𝜑 → ∃ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) )
8 simpl ( ( ( 𝐹𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ( 𝐹𝑘 ) ∈ ℝ )
9 8 ralimi ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℝ )
10 eqid ( ℤ𝑗 ) = ( ℤ𝑗 )
11 simprr ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℝ ) ) → ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℝ )
12 fveq2 ( 𝑘 = 𝑛 → ( 𝐹𝑘 ) = ( 𝐹𝑛 ) )
13 12 eleq1d ( 𝑘 = 𝑛 → ( ( 𝐹𝑘 ) ∈ ℝ ↔ ( 𝐹𝑛 ) ∈ ℝ ) )
14 13 rspccva ( ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℝ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) → ( 𝐹𝑛 ) ∈ ℝ )
15 11 14 sylan ( ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℝ ) ) ∧ 𝑛 ∈ ( ℤ𝑗 ) ) → ( 𝐹𝑛 ) ∈ ℝ )
16 15 fmpttd ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℝ ) ) → ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) : ( ℤ𝑗 ) ⟶ ℝ )
17 fveq2 ( 𝑗 = 𝑚 → ( ℤ𝑗 ) = ( ℤ𝑚 ) )
18 fveq2 ( 𝑗 = 𝑚 → ( 𝐹𝑗 ) = ( 𝐹𝑚 ) )
19 18 oveq2d ( 𝑗 = 𝑚 → ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) = ( ( 𝐹𝑘 ) − ( 𝐹𝑚 ) ) )
20 19 fveq2d ( 𝑗 = 𝑚 → ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) = ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑚 ) ) ) )
21 20 breq1d ( 𝑗 = 𝑚 → ( ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) )
22 21 anbi2d ( 𝑗 = 𝑚 → ( ( ( 𝐹𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ↔ ( ( 𝐹𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) ) )
23 17 22 raleqbidv ( 𝑗 = 𝑚 → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ𝑚 ) ( ( 𝐹𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) ) )
24 23 cbvrexvw ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) ↔ ∃ 𝑚𝑍𝑘 ∈ ( ℤ𝑚 ) ( ( 𝐹𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) )
25 fveq2 ( 𝑘 = 𝑖 → ( 𝐹𝑘 ) = ( 𝐹𝑖 ) )
26 25 eleq1d ( 𝑘 = 𝑖 → ( ( 𝐹𝑘 ) ∈ ℝ ↔ ( 𝐹𝑖 ) ∈ ℝ ) )
27 25 fvoveq1d ( 𝑘 = 𝑖 → ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑚 ) ) ) = ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) )
28 27 breq1d ( 𝑘 = 𝑖 → ( ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) )
29 26 28 anbi12d ( 𝑘 = 𝑖 → ( ( ( 𝐹𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) ↔ ( ( 𝐹𝑖 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) ) )
30 29 cbvralvw ( ∀ 𝑘 ∈ ( ℤ𝑚 ) ( ( 𝐹𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) ↔ ∀ 𝑖 ∈ ( ℤ𝑚 ) ( ( 𝐹𝑖 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) )
31 recn ( ( 𝐹𝑖 ) ∈ ℝ → ( 𝐹𝑖 ) ∈ ℂ )
32 31 anim1i ( ( ( 𝐹𝑖 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) → ( ( 𝐹𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) )
33 32 ralimi ( ∀ 𝑖 ∈ ( ℤ𝑚 ) ( ( 𝐹𝑖 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) → ∀ 𝑖 ∈ ( ℤ𝑚 ) ( ( 𝐹𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) )
34 30 33 sylbi ( ∀ 𝑘 ∈ ( ℤ𝑚 ) ( ( 𝐹𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) → ∀ 𝑖 ∈ ( ℤ𝑚 ) ( ( 𝐹𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) )
35 34 reximi ( ∃ 𝑚𝑍𝑘 ∈ ( ℤ𝑚 ) ( ( 𝐹𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) → ∃ 𝑚𝑍𝑖 ∈ ( ℤ𝑚 ) ( ( 𝐹𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) )
36 24 35 sylbi ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ∃ 𝑚𝑍𝑖 ∈ ( ℤ𝑚 ) ( ( 𝐹𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) )
37 36 ralimi ( ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+𝑚𝑍𝑖 ∈ ( ℤ𝑚 ) ( ( 𝐹𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) )
38 3 37 syl ( 𝜑 → ∀ 𝑥 ∈ ℝ+𝑚𝑍𝑖 ∈ ( ℤ𝑚 ) ( ( 𝐹𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) )
39 38 adantr ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℝ ) ) → ∀ 𝑥 ∈ ℝ+𝑚𝑍𝑖 ∈ ( ℤ𝑚 ) ( ( 𝐹𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) )
40 1 10 cau4 ( 𝑗𝑍 → ( ∀ 𝑥 ∈ ℝ+𝑚𝑍𝑖 ∈ ( ℤ𝑚 ) ( ( 𝐹𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+𝑚 ∈ ( ℤ𝑗 ) ∀ 𝑖 ∈ ( ℤ𝑚 ) ( ( 𝐹𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) ) )
41 40 ad2antrl ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℝ ) ) → ( ∀ 𝑥 ∈ ℝ+𝑚𝑍𝑖 ∈ ( ℤ𝑚 ) ( ( 𝐹𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+𝑚 ∈ ( ℤ𝑗 ) ∀ 𝑖 ∈ ( ℤ𝑚 ) ( ( 𝐹𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) ) )
42 39 41 mpbid ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℝ ) ) → ∀ 𝑥 ∈ ℝ+𝑚 ∈ ( ℤ𝑗 ) ∀ 𝑖 ∈ ( ℤ𝑚 ) ( ( 𝐹𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) )
43 simpr ( ( ( 𝐹𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) → ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 )
44 10 uztrn2 ( ( 𝑚 ∈ ( ℤ𝑗 ) ∧ 𝑖 ∈ ( ℤ𝑚 ) ) → 𝑖 ∈ ( ℤ𝑗 ) )
45 fveq2 ( 𝑛 = 𝑖 → ( 𝐹𝑛 ) = ( 𝐹𝑖 ) )
46 eqid ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) = ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) )
47 fvex ( 𝐹𝑖 ) ∈ V
48 45 46 47 fvmpt ( 𝑖 ∈ ( ℤ𝑗 ) → ( ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ‘ 𝑖 ) = ( 𝐹𝑖 ) )
49 44 48 syl ( ( 𝑚 ∈ ( ℤ𝑗 ) ∧ 𝑖 ∈ ( ℤ𝑚 ) ) → ( ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ‘ 𝑖 ) = ( 𝐹𝑖 ) )
50 fveq2 ( 𝑛 = 𝑚 → ( 𝐹𝑛 ) = ( 𝐹𝑚 ) )
51 fvex ( 𝐹𝑚 ) ∈ V
52 50 46 51 fvmpt ( 𝑚 ∈ ( ℤ𝑗 ) → ( ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ‘ 𝑚 ) = ( 𝐹𝑚 ) )
53 52 adantr ( ( 𝑚 ∈ ( ℤ𝑗 ) ∧ 𝑖 ∈ ( ℤ𝑚 ) ) → ( ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ‘ 𝑚 ) = ( 𝐹𝑚 ) )
54 49 53 oveq12d ( ( 𝑚 ∈ ( ℤ𝑗 ) ∧ 𝑖 ∈ ( ℤ𝑚 ) ) → ( ( ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ‘ 𝑖 ) − ( ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ‘ 𝑚 ) ) = ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) )
55 54 fveq2d ( ( 𝑚 ∈ ( ℤ𝑗 ) ∧ 𝑖 ∈ ( ℤ𝑚 ) ) → ( abs ‘ ( ( ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ‘ 𝑖 ) − ( ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ‘ 𝑚 ) ) ) = ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) )
56 55 breq1d ( ( 𝑚 ∈ ( ℤ𝑗 ) ∧ 𝑖 ∈ ( ℤ𝑚 ) ) → ( ( abs ‘ ( ( ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ‘ 𝑖 ) − ( ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ‘ 𝑚 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) )
57 43 56 syl5ibr ( ( 𝑚 ∈ ( ℤ𝑗 ) ∧ 𝑖 ∈ ( ℤ𝑚 ) ) → ( ( ( 𝐹𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) → ( abs ‘ ( ( ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ‘ 𝑖 ) − ( ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ‘ 𝑚 ) ) ) < 𝑥 ) )
58 57 ralimdva ( 𝑚 ∈ ( ℤ𝑗 ) → ( ∀ 𝑖 ∈ ( ℤ𝑚 ) ( ( 𝐹𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) → ∀ 𝑖 ∈ ( ℤ𝑚 ) ( abs ‘ ( ( ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ‘ 𝑖 ) − ( ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ‘ 𝑚 ) ) ) < 𝑥 ) )
59 58 reximia ( ∃ 𝑚 ∈ ( ℤ𝑗 ) ∀ 𝑖 ∈ ( ℤ𝑚 ) ( ( 𝐹𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) → ∃ 𝑚 ∈ ( ℤ𝑗 ) ∀ 𝑖 ∈ ( ℤ𝑚 ) ( abs ‘ ( ( ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ‘ 𝑖 ) − ( ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ‘ 𝑚 ) ) ) < 𝑥 )
60 59 ralimi ( ∀ 𝑥 ∈ ℝ+𝑚 ∈ ( ℤ𝑗 ) ∀ 𝑖 ∈ ( ℤ𝑚 ) ( ( 𝐹𝑖 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑖 ) − ( 𝐹𝑚 ) ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+𝑚 ∈ ( ℤ𝑗 ) ∀ 𝑖 ∈ ( ℤ𝑚 ) ( abs ‘ ( ( ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ‘ 𝑖 ) − ( ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ‘ 𝑚 ) ) ) < 𝑥 )
61 42 60 syl ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℝ ) ) → ∀ 𝑥 ∈ ℝ+𝑚 ∈ ( ℤ𝑗 ) ∀ 𝑖 ∈ ( ℤ𝑚 ) ( abs ‘ ( ( ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ‘ 𝑖 ) − ( ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ‘ 𝑚 ) ) ) < 𝑥 )
62 10 16 61 caurcvg ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℝ ) ) → ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ⇝ ( lim sup ‘ ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ) )
63 eluzelz ( 𝑗 ∈ ( ℤ𝑀 ) → 𝑗 ∈ ℤ )
64 63 1 eleq2s ( 𝑗𝑍𝑗 ∈ ℤ )
65 64 ad2antrl ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℝ ) ) → 𝑗 ∈ ℤ )
66 2 adantr ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℝ ) ) → 𝐹𝑉 )
67 fveq2 ( 𝑛 = 𝑘 → ( 𝐹𝑛 ) = ( 𝐹𝑘 ) )
68 67 cbvmptv ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) = ( 𝑘 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑘 ) )
69 10 68 climmpt ( ( 𝑗 ∈ ℤ ∧ 𝐹𝑉 ) → ( 𝐹 ⇝ ( lim sup ‘ ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ) ↔ ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ⇝ ( lim sup ‘ ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ) ) )
70 65 66 69 syl2anc ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℝ ) ) → ( 𝐹 ⇝ ( lim sup ‘ ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ) ↔ ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ⇝ ( lim sup ‘ ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ) ) )
71 62 70 mpbird ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℝ ) ) → 𝐹 ⇝ ( lim sup ‘ ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ) )
72 climrel Rel ⇝
73 72 releldmi ( 𝐹 ⇝ ( lim sup ‘ ( 𝑛 ∈ ( ℤ𝑗 ) ↦ ( 𝐹𝑛 ) ) ) → 𝐹 ∈ dom ⇝ )
74 71 73 syl ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℝ ) ) → 𝐹 ∈ dom ⇝ )
75 74 expr ( ( 𝜑𝑗𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐹𝑘 ) ∈ ℝ → 𝐹 ∈ dom ⇝ ) )
76 9 75 syl5 ( ( 𝜑𝑗𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → 𝐹 ∈ dom ⇝ ) )
77 76 rexlimdva ( 𝜑 → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → 𝐹 ∈ dom ⇝ ) )
78 77 rexlimdvw ( 𝜑 → ( ∃ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → 𝐹 ∈ dom ⇝ ) )
79 7 78 mpd ( 𝜑𝐹 ∈ dom ⇝ )