Theorem climcn1lem

Description: The limit of a continuous function, theorem form. (Contributed by Mario Carneiro, 9-Feb-2014)

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

Proof

Step	Hyp	Ref	Expression
1		climcn1lem.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		climcn1lem.2	$$⊢\phi \to F⇝A$$
3		climcn1lem.4	$$⊢\phi \to G\in W$$
4		climcn1lem.5	$$⊢\phi \to M\in \mathbb{Z}$$
5		climcn1lem.6	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
6		climcn1lem.7	$$⊢H:ℂ⟶ℂ$$
7		climcn1lem.8	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to \exists y\in {ℝ}^{+}\forall z\in ℂ\left(\left|z-A\right|<y\to \left|H\left(z\right)-H\left(A\right)\right|<x\right)$$
8		climcn1lem.9	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)=H\left(F\left(k\right)\right)$$
9		climcl	$$⊢F⇝A\to A\in ℂ$$
10	2 9	syl	$$⊢\phi \to A\in ℂ$$
11	6	ffvelcdmi	$$⊢z\in ℂ\to H\left(z\right)\in ℂ$$
12	11	adantl	$$⊢\left(\phi \wedge z\in ℂ\right)\to H\left(z\right)\in ℂ$$
13	10 7	sylan	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \exists y\in {ℝ}^{+}\forall z\in ℂ\left(\left|z-A\right|<y\to \left|H\left(z\right)-H\left(A\right)\right|<x\right)$$
14	1 4 10 12 2 3 13 5 8	climcn1	$$⊢\phi \to G⇝H\left(A\right)$$