This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-clim

Description: Define the limit relation for complex number sequences. See clim for its relational expression. (Contributed by NM, 28-Aug-2005)

Ref Expression
Assertion df-clim ⇝ = { ⟨ 𝑓 , 𝑦 ⟩ ∣ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑓 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑓 ‘ 𝑘 ) − 𝑦 ) ) < 𝑥 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cli ⊢ ⇝
1 vf ⊢ 𝑓
2 vy ⊢ 𝑦
3 2 cv ⊢ 𝑦
4 cc ⊢ ℂ
5 3 4 wcel ⊢ 𝑦 ∈ ℂ
6 vx ⊢ 𝑥
7 crp ⊢ ℝ+
8 vj ⊢ 𝑗
9 cz ⊢ ℤ
10 vk ⊢ 𝑘
11 cuz ⊢ ℤ≥
12 8 cv ⊢ 𝑗
13 12 11 cfv ⊢ ( ℤ≥ ‘ 𝑗 )
14 1 cv ⊢ 𝑓
15 10 cv ⊢ 𝑘
16 15 14 cfv ⊢ ( 𝑓 ‘ 𝑘 )
17 16 4 wcel ⊢ ( 𝑓 ‘ 𝑘 ) ∈ ℂ
18 cabs ⊢ abs
19 cmin ⊢ −
20 16 3 19 co ⊢ ( ( 𝑓 ‘ 𝑘 ) − 𝑦 )
21 20 18 cfv ⊢ ( abs ‘ ( ( 𝑓 ‘ 𝑘 ) − 𝑦 ) )
22 clt ⊢ <
23 6 cv ⊢ 𝑥
24 21 23 22 wbr ⊢ ( abs ‘ ( ( 𝑓 ‘ 𝑘 ) − 𝑦 ) ) < 𝑥
25 17 24 wa ⊢ ( ( 𝑓 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑓 ‘ 𝑘 ) − 𝑦 ) ) < 𝑥 )
26 25 10 13 wral ⊢ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑓 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑓 ‘ 𝑘 ) − 𝑦 ) ) < 𝑥 )
27 26 8 9 wrex ⊢ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑓 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑓 ‘ 𝑘 ) − 𝑦 ) ) < 𝑥 )
28 27 6 7 wral ⊢ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑓 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑓 ‘ 𝑘 ) − 𝑦 ) ) < 𝑥 )
29 5 28 wa ⊢ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑓 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑓 ‘ 𝑘 ) − 𝑦 ) ) < 𝑥 ) )
30 29 1 2 copab ⊢ { ⟨ 𝑓 , 𝑦 ⟩ ∣ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑓 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑓 ‘ 𝑘 ) − 𝑦 ) ) < 𝑥 ) ) }
31 0 30 wceq ⊢ ⇝ = { ⟨ 𝑓 , 𝑦 ⟩ ∣ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑓 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑓 ‘ 𝑘 ) − 𝑦 ) ) < 𝑥 ) ) }