Theorem 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	$$⊢\underset{\_}{Ⅎ}kF$$
	climuz.m	$$⊢\phi \to M\in \mathbb{Z}$$
	climuz.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climuz.f	$$⊢\phi \to F:Z⟶ℂ$$
Assertion	climuz	$$⊢\phi \to \left(F⇝A\leftrightarrow \left(A\in ℂ\wedge \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)-A\right|<x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		climuz.k	$$⊢\underset{\_}{Ⅎ}kF$$
2		climuz.m	$$⊢\phi \to M\in \mathbb{Z}$$
3		climuz.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
4		climuz.f	$$⊢\phi \to F:Z⟶ℂ$$
5	2 3 4	climuzlem	$$⊢\phi \to \left(F⇝A\leftrightarrow \left(A\in ℂ\wedge \forall y\in {ℝ}^{+}\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}\left|F\left(l\right)-A\right|<y\right)\right)$$
6		breq2	$$⊢y=x\to \left(\left|F\left(l\right)-A\right|<y\leftrightarrow \left|F\left(l\right)-A\right|<x\right)$$
7	6	ralbidv	$$⊢y=x\to \left(\forall l\in {\mathbb{Z}}_{\ge i}\left|F\left(l\right)-A\right|<y\leftrightarrow \forall l\in {\mathbb{Z}}_{\ge i}\left|F\left(l\right)-A\right|<x\right)$$
8	7	rexbidv	$$⊢y=x\to \left(\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}\left|F\left(l\right)-A\right|<y\leftrightarrow \exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}\left|F\left(l\right)-A\right|<x\right)$$
9		fveq2	$$⊢i=j\to {\mathbb{Z}}_{\ge i}={\mathbb{Z}}_{\ge j}$$
10	9	raleqdv	$$⊢i=j\to \left(\forall l\in {\mathbb{Z}}_{\ge i}\left|F\left(l\right)-A\right|<x\leftrightarrow \forall l\in {\mathbb{Z}}_{\ge j}\left|F\left(l\right)-A\right|<x\right)$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}k\mathrm{abs}$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}kl$$
13	1 12	nffv	$$⊢\underset{\_}{Ⅎ}kF\left(l\right)$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}k-$$
15		nfcv	$$⊢\underset{\_}{Ⅎ}kA$$
16	13 14 15	nfov	$$⊢\underset{\_}{Ⅎ}k\left(F\left(l\right)-A\right)$$
17	11 16	nffv	$$⊢\underset{\_}{Ⅎ}k\left|F\left(l\right)-A\right|$$
18		nfcv	$$⊢\underset{\_}{Ⅎ}k<$$
19		nfcv	$$⊢\underset{\_}{Ⅎ}kx$$
20	17 18 19	nfbr	$$⊢Ⅎk\left|F\left(l\right)-A\right|<x$$
21		nfv	$$⊢Ⅎl\left|F\left(k\right)-A\right|<x$$
22		fveq2	$$⊢l=k\to F\left(l\right)=F\left(k\right)$$
23	22	fvoveq1d	$$⊢l=k\to \left|F\left(l\right)-A\right|=\left|F\left(k\right)-A\right|$$
24	23	breq1d	$$⊢l=k\to \left(\left|F\left(l\right)-A\right|<x\leftrightarrow \left|F\left(k\right)-A\right|<x\right)$$
25	20 21 24	cbvralw	$$⊢\forall l\in {\mathbb{Z}}_{\ge j}\left|F\left(l\right)-A\right|<x\leftrightarrow \forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)-A\right|<x$$
26	25	a1i	$$⊢i=j\to \left(\forall l\in {\mathbb{Z}}_{\ge j}\left|F\left(l\right)-A\right|<x\leftrightarrow \forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)-A\right|<x\right)$$
27	10 26	bitrd	$$⊢i=j\to \left(\forall l\in {\mathbb{Z}}_{\ge i}\left|F\left(l\right)-A\right|<x\leftrightarrow \forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)-A\right|<x\right)$$
28	27	cbvrexvw	$$⊢\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}\left|F\left(l\right)-A\right|<x\leftrightarrow \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)-A\right|<x$$
29	28	a1i	$$⊢y=x\to \left(\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}\left|F\left(l\right)-A\right|<x\leftrightarrow \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)-A\right|<x\right)$$
30	8 29	bitrd	$$⊢y=x\to \left(\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}\left|F\left(l\right)-A\right|<y\leftrightarrow \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)-A\right|<x\right)$$
31	30	cbvralvw	$$⊢\forall y\in {ℝ}^{+}\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}\left|F\left(l\right)-A\right|<y\leftrightarrow \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)-A\right|<x$$
32	31	anbi2i	$$⊢\left(A\in ℂ\wedge \forall y\in {ℝ}^{+}\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}\left|F\left(l\right)-A\right|<y\right)\leftrightarrow \left(A\in ℂ\wedge \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)-A\right|<x\right)$$
33	32	a1i	$$⊢\phi \to \left(\left(A\in ℂ\wedge \forall y\in {ℝ}^{+}\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}\left|F\left(l\right)-A\right|<y\right)\leftrightarrow \left(A\in ℂ\wedge \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)-A\right|<x\right)\right)$$
34	5 33	bitrd	$$⊢\phi \to \left(F⇝A\leftrightarrow \left(A\in ℂ\wedge \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)-A\right|<x\right)\right)$$