Theorem climabs0

Description: Convergence to zero of the absolute value is equivalent to convergence to zero. (Contributed by NM, 8-Jul-2008) (Revised by Mario Carneiro, 31-Jan-2014)

	Ref	Expression
Hypotheses	climabs0.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climabs0.2	$$⊢\phi \to M\in \mathbb{Z}$$
	climabs0.3	$$⊢\phi \to F\in V$$
	climabs0.4	$$⊢\phi \to G\in W$$
	climabs0.5	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
	climabs0.6	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)=\left|F\left(k\right)\right|$$
Assertion	climabs0	$$⊢\phi \to \left(F⇝0\leftrightarrow G⇝0\right)$$

Proof

Step	Hyp	Ref	Expression
1		climabs0.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		climabs0.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		climabs0.3	$$⊢\phi \to F\in V$$
4		climabs0.4	$$⊢\phi \to G\in W$$
5		climabs0.5	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
6		climabs0.6	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)=\left|F\left(k\right)\right|$$
7	1	uztrn2	$$⊢\left(j\in Z\wedge k\in {\mathbb{Z}}_{\ge j}\right)\to k\in Z$$
8		absidm	$$⊢F\left(k\right)\in ℂ\to \left|\left|F\left(k\right)\right|\right|=\left|F\left(k\right)\right|$$
9	5 8	syl	$$⊢\left(\phi \wedge k\in Z\right)\to \left|\left|F\left(k\right)\right|\right|=\left|F\left(k\right)\right|$$
10	9	breq1d	$$⊢\left(\phi \wedge k\in Z\right)\to \left(\left|\left|F\left(k\right)\right|\right|<x\leftrightarrow \left|F\left(k\right)\right|<x\right)$$
11	7 10	sylan2	$$⊢\left(\phi \wedge \left(j\in Z\wedge k\in {\mathbb{Z}}_{\ge j}\right)\right)\to \left(\left|\left|F\left(k\right)\right|\right|<x\leftrightarrow \left|F\left(k\right)\right|<x\right)$$
12	11	anassrs	$$⊢\left(\left(\phi \wedge j\in Z\right)\wedge k\in {\mathbb{Z}}_{\ge j}\right)\to \left(\left|\left|F\left(k\right)\right|\right|<x\leftrightarrow \left|F\left(k\right)\right|<x\right)$$
13	12	ralbidva	$$⊢\left(\phi \wedge j\in Z\right)\to \left(\forall k\in {\mathbb{Z}}_{\ge j}\left|\left|F\left(k\right)\right|\right|<x\leftrightarrow \forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\right|<x\right)$$
14	13	rexbidva	$$⊢\phi \to \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|\left|F\left(k\right)\right|\right|<x\leftrightarrow \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\right|<x\right)$$
15	14	ralbidv	$$⊢\phi \to \left(\forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|\left|F\left(k\right)\right|\right|<x\leftrightarrow \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\right|<x\right)$$
16	5	abscld	$$⊢\left(\phi \wedge k\in Z\right)\to \left|F\left(k\right)\right|\in ℝ$$
17	16	recnd	$$⊢\left(\phi \wedge k\in Z\right)\to \left|F\left(k\right)\right|\in ℂ$$
18	1 2 4 6 17	clim0c	$$⊢\phi \to \left(G⇝0\leftrightarrow \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|\left|F\left(k\right)\right|\right|<x\right)$$
19		eqidd	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=F\left(k\right)$$
20	1 2 3 19 5	clim0c	$$⊢\phi \to \left(F⇝0\leftrightarrow \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\right|<x\right)$$
21	15 18 20	3bitr4rd	$$⊢\phi \to \left(F⇝0\leftrightarrow G⇝0\right)$$