climuz

Description: Express the predicate: The limit of complex number sequence F is A , or F converges to A . (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	climuz.k	⊢ Ⅎ 𝑘 𝐹
	climuz.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climuz.z	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
	climuz.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℂ )
Assertion	climuz	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		climuz.k	⊢ Ⅎ 𝑘 𝐹
2		climuz.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		climuz.z	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
4		climuz.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℂ )
5	2 3 4	climuzlem	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑦 ) ) )
6		breq2	⊢ ( 𝑦 = 𝑥 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥 ) )
7	6	ralbidv	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑦 ↔ ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥 ) )
8	7	rexbidv	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑦 ↔ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥 ) )
9		fveq2	⊢ ( 𝑖 = 𝑗 → ( ℤ_≥ ‘ 𝑖 ) = ( ℤ_≥ ‘ 𝑗 ) )
10	9	raleqdv	⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥 ↔ ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥 ) )
11		nfcv	⊢ Ⅎ 𝑘 abs
12		nfcv	⊢ Ⅎ 𝑘 𝑙
13	1 12	nffv	⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑙 )
14		nfcv	⊢ Ⅎ 𝑘 −
15		nfcv	⊢ Ⅎ 𝑘 𝐴
16	13 14 15	nfov	⊢ Ⅎ 𝑘 ( ( 𝐹 ‘ 𝑙 ) − 𝐴 )
17	11 16	nffv	⊢ Ⅎ 𝑘 ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) )
18		nfcv	⊢ Ⅎ 𝑘 <
19		nfcv	⊢ Ⅎ 𝑘 𝑥
20	17 18 19	nfbr	⊢ Ⅎ 𝑘 ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥
21		nfv	⊢ Ⅎ 𝑙 ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥
22		fveq2	⊢ ( 𝑙 = 𝑘 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑘 ) )
23	22	fvoveq1d	⊢ ( 𝑙 = 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
24	23	breq1d	⊢ ( 𝑙 = 𝑘 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
25	20 21 24	cbvralw	⊢ ( ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 )
26	25	a1i	⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
27	10 26	bitrd	⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
28	27	cbvrexvw	⊢ ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 )
29	28	a1i	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
30	8 29	bitrd	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑦 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
31	30	cbvralvw	⊢ ( ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑦 ↔ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 )
32	31	anbi2i	⊢ ( ( 𝐴 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑦 ) ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
33	32	a1i	⊢ ( 𝜑 → ( ( 𝐴 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑦 ) ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
34	5 33	bitrd	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )

Metamath Proof Explorer

Theorem climuz

Proof