Theorem clim0cf

Description: Express the predicate F converges to 0 . Similar to clim , but without the disjoint var constraint F k . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	clim0cf.nf	$$⊢\underset{\_}{Ⅎ}kF$$
	clim0cf.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	clim0cf.m	$$⊢\phi \to M\in \mathbb{Z}$$
	clim0cf.f	$$⊢\phi \to F\in V$$
	clim0cf.fv	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=B$$
	clim0cf.b	$$⊢\left(\phi \wedge k\in Z\right)\to B\in ℂ$$
Assertion	clim0cf	$$⊢\phi \to \left(F⇝0\leftrightarrow \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|B\right|<x\right)$$

Proof

Step	Hyp	Ref	Expression
1		clim0cf.nf	$$⊢\underset{\_}{Ⅎ}kF$$
2		clim0cf.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3		clim0cf.m	$$⊢\phi \to M\in \mathbb{Z}$$
4		clim0cf.f	$$⊢\phi \to F\in V$$
5		clim0cf.fv	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=B$$
6		clim0cf.b	$$⊢\left(\phi \wedge k\in Z\right)\to B\in ℂ$$
7		0cnd	$$⊢\phi \to 0\in ℂ$$
8	1 2 3 4 5 7 6	clim2cf	$$⊢\phi \to \left(F⇝0\leftrightarrow \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|B-0\right|<x\right)$$
9	2	uztrn2	$$⊢\left(j\in Z\wedge k\in {\mathbb{Z}}_{\ge j}\right)\to k\in Z$$
10	6	subid1d	$$⊢\left(\phi \wedge k\in Z\right)\to B-0=B$$
11	10	fveq2d	$$⊢\left(\phi \wedge k\in Z\right)\to \left|B-0\right|=\left|B\right|$$
12	11	breq1d	$$⊢\left(\phi \wedge k\in Z\right)\to \left(\left|B-0\right|<x\leftrightarrow \left|B\right|<x\right)$$
13	9 12	sylan2	$$⊢\left(\phi \wedge \left(j\in Z\wedge k\in {\mathbb{Z}}_{\ge j}\right)\right)\to \left(\left|B-0\right|<x\leftrightarrow \left|B\right|<x\right)$$
14	13	anassrs	$$⊢\left(\left(\phi \wedge j\in Z\right)\wedge k\in {\mathbb{Z}}_{\ge j}\right)\to \left(\left|B-0\right|<x\leftrightarrow \left|B\right|<x\right)$$
15	14	ralbidva	$$⊢\left(\phi \wedge j\in Z\right)\to \left(\forall k\in {\mathbb{Z}}_{\ge j}\left|B-0\right|<x\leftrightarrow \forall k\in {\mathbb{Z}}_{\ge j}\left|B\right|<x\right)$$
16	15	rexbidva	$$⊢\phi \to \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|B-0\right|<x\leftrightarrow \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|B\right|<x\right)$$
17	16	ralbidv	$$⊢\phi \to \left(\forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|B-0\right|<x\leftrightarrow \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|B\right|<x\right)$$
18	8 17	bitrd	$$⊢\phi \to \left(F⇝0\leftrightarrow \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|B\right|<x\right)$$