Theorem climcn1

Description: Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014)

	Ref	Expression
Hypotheses	climcn1.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climcn1.2	$$⊢\phi \to M\in \mathbb{Z}$$
	climcn1.3	$$⊢\phi \to A\in B$$
	climcn1.4	$$⊢\left(\phi \wedge z\in B\right)\to F\left(z\right)\in ℂ$$
	climcn1.5	$$⊢\phi \to G⇝A$$
	climcn1.6	$$⊢\phi \to H\in W$$
	climcn1.7	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \exists y\in {ℝ}^{+}\forall z\in B\left(\left|z-A\right|<y\to \left|F\left(z\right)-F\left(A\right)\right|<x\right)$$
	climcn1.8	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)\in B$$
	climcn1.9	$$⊢\left(\phi \wedge k\in Z\right)\to H\left(k\right)=F\left(G\left(k\right)\right)$$
Assertion	climcn1	$$⊢\phi \to H⇝F\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		climcn1.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		climcn1.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		climcn1.3	$$⊢\phi \to A\in B$$
4		climcn1.4	$$⊢\left(\phi \wedge z\in B\right)\to F\left(z\right)\in ℂ$$
5		climcn1.5	$$⊢\phi \to G⇝A$$
6		climcn1.6	$$⊢\phi \to H\in W$$
7		climcn1.7	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \exists y\in {ℝ}^{+}\forall z\in B\left(\left|z-A\right|<y\to \left|F\left(z\right)-F\left(A\right)\right|<x\right)$$
8		climcn1.8	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)\in B$$
9		climcn1.9	$$⊢\left(\phi \wedge k\in Z\right)\to H\left(k\right)=F\left(G\left(k\right)\right)$$
10	2	adantr	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to M\in \mathbb{Z}$$
11		simpr	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to y\in {ℝ}^{+}$$
12		eqidd	$$⊢\left(\left(\phi \wedge y\in {ℝ}^{+}\right)\wedge k\in Z\right)\to G\left(k\right)=G\left(k\right)$$
13	5	adantr	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to G⇝A$$
14	1 10 11 12 13	climi2	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|G\left(k\right)-A\right|<y$$
15	1	uztrn2	$$⊢\left(j\in Z\wedge k\in {\mathbb{Z}}_{\ge j}\right)\to k\in Z$$
16	8	adantlr	$$⊢\left(\left(\phi \wedge y\in {ℝ}^{+}\right)\wedge k\in Z\right)\to G\left(k\right)\in B$$
17		fvoveq1	$$⊢z=G\left(k\right)\to \left|z-A\right|=\left|G\left(k\right)-A\right|$$
18	17	breq1d	$$⊢z=G\left(k\right)\to \left(\left|z-A\right|<y\leftrightarrow \left|G\left(k\right)-A\right|<y\right)$$
19	18	imbrov2fvoveq	$$⊢z=G\left(k\right)\to \left(\left(\left|z-A\right|<y\to \left|F\left(z\right)-F\left(A\right)\right|<x\right)\leftrightarrow \left(\left|G\left(k\right)-A\right|<y\to \left|F\left(G\left(k\right)\right)-F\left(A\right)\right|<x\right)\right)$$
20	19	rspcva	$$⊢\left(G\left(k\right)\in B\wedge \forall z\in B\left(\left|z-A\right|<y\to \left|F\left(z\right)-F\left(A\right)\right|<x\right)\right)\to \left(\left|G\left(k\right)-A\right|<y\to \left|F\left(G\left(k\right)\right)-F\left(A\right)\right|<x\right)$$
21	16 20	sylan	$$⊢\left(\left(\left(\phi \wedge y\in {ℝ}^{+}\right)\wedge k\in Z\right)\wedge \forall z\in B\left(\left|z-A\right|<y\to \left|F\left(z\right)-F\left(A\right)\right|<x\right)\right)\to \left(\left|G\left(k\right)-A\right|<y\to \left|F\left(G\left(k\right)\right)-F\left(A\right)\right|<x\right)$$
22	21	an32s	$$⊢\left(\left(\left(\phi \wedge y\in {ℝ}^{+}\right)\wedge \forall z\in B\left(\left|z-A\right|<y\to \left|F\left(z\right)-F\left(A\right)\right|<x\right)\right)\wedge k\in Z\right)\to \left(\left|G\left(k\right)-A\right|<y\to \left|F\left(G\left(k\right)\right)-F\left(A\right)\right|<x\right)$$
23	15 22	sylan2	$$⊢\left(\left(\left(\phi \wedge y\in {ℝ}^{+}\right)\wedge \forall z\in B\left(\left|z-A\right|<y\to \left|F\left(z\right)-F\left(A\right)\right|<x\right)\right)\wedge \left(j\in Z\wedge k\in {\mathbb{Z}}_{\ge j}\right)\right)\to \left(\left|G\left(k\right)-A\right|<y\to \left|F\left(G\left(k\right)\right)-F\left(A\right)\right|<x\right)$$
24	23	anassrs	$$⊢\left(\left(\left(\left(\phi \wedge y\in {ℝ}^{+}\right)\wedge \forall z\in B\left(\left|z-A\right|<y\to \left|F\left(z\right)-F\left(A\right)\right|<x\right)\right)\wedge j\in Z\right)\wedge k\in {\mathbb{Z}}_{\ge j}\right)\to \left(\left|G\left(k\right)-A\right|<y\to \left|F\left(G\left(k\right)\right)-F\left(A\right)\right|<x\right)$$
25	24	ralimdva	$$⊢\left(\left(\left(\phi \wedge y\in {ℝ}^{+}\right)\wedge \forall z\in B\left(\left|z-A\right|<y\to \left|F\left(z\right)-F\left(A\right)\right|<x\right)\right)\wedge j\in Z\right)\to \left(\forall k\in {\mathbb{Z}}_{\ge j}\left|G\left(k\right)-A\right|<y\to \forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(G\left(k\right)\right)-F\left(A\right)\right|<x\right)$$
26	25	reximdva	$$⊢\left(\left(\phi \wedge y\in {ℝ}^{+}\right)\wedge \forall z\in B\left(\left|z-A\right|<y\to \left|F\left(z\right)-F\left(A\right)\right|<x\right)\right)\to \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|G\left(k\right)-A\right|<y\to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(G\left(k\right)\right)-F\left(A\right)\right|<x\right)$$
27	26	ex	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \left(\forall z\in B\left(\left|z-A\right|<y\to \left|F\left(z\right)-F\left(A\right)\right|<x\right)\to \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|G\left(k\right)-A\right|<y\to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(G\left(k\right)\right)-F\left(A\right)\right|<x\right)\right)$$
28	14 27	mpid	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \left(\forall z\in B\left(\left|z-A\right|<y\to \left|F\left(z\right)-F\left(A\right)\right|<x\right)\to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(G\left(k\right)\right)-F\left(A\right)\right|<x\right)$$
29	28	rexlimdva	$$⊢\phi \to \left(\exists y\in {ℝ}^{+}\forall z\in B\left(\left|z-A\right|<y\to \left|F\left(z\right)-F\left(A\right)\right|<x\right)\to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(G\left(k\right)\right)-F\left(A\right)\right|<x\right)$$
30	29	adantr	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \left(\exists y\in {ℝ}^{+}\forall z\in B\left(\left|z-A\right|<y\to \left|F\left(z\right)-F\left(A\right)\right|<x\right)\to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(G\left(k\right)\right)-F\left(A\right)\right|<x\right)$$
31	7 30	mpd	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(G\left(k\right)\right)-F\left(A\right)\right|<x$$
32	31	ralrimiva	$$⊢\phi \to \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(G\left(k\right)\right)-F\left(A\right)\right|<x$$
33		fveq2	$$⊢z=A\to F\left(z\right)=F\left(A\right)$$
34	33	eleq1d	$$⊢z=A\to \left(F\left(z\right)\in ℂ\leftrightarrow F\left(A\right)\in ℂ\right)$$
35	4	ralrimiva	$$⊢\phi \to \forall z\in BF\left(z\right)\in ℂ$$
36	34 35 3	rspcdva	$$⊢\phi \to F\left(A\right)\in ℂ$$
37		fveq2	$$⊢z=G\left(k\right)\to F\left(z\right)=F\left(G\left(k\right)\right)$$
38	37	eleq1d	$$⊢z=G\left(k\right)\to \left(F\left(z\right)\in ℂ\leftrightarrow F\left(G\left(k\right)\right)\in ℂ\right)$$
39	35	adantr	$$⊢\left(\phi \wedge k\in Z\right)\to \forall z\in BF\left(z\right)\in ℂ$$
40	38 39 8	rspcdva	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(G\left(k\right)\right)\in ℂ$$
41	1 2 6 9 36 40	clim2c	$$⊢\phi \to \left(H⇝F\left(A\right)\leftrightarrow \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(G\left(k\right)\right)-F\left(A\right)\right|<x\right)$$
42	32 41	mpbird	$$⊢\phi \to H⇝F\left(A\right)$$