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 imbitrrid ⊢ ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( ( 𝐹 ‘ 𝑖 ) ∈ ℂ ∧ ( 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 ⇝ )