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 ‘ ( ( 𝑓 ‘ 𝑘 ) − 𝑦 ) ) < 𝑥 ) ) }