Metamath Proof Explorer

Theorem climcn1lem

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

Ref Expression
Hypotheses climcn1lem.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
climcn1lem.2 ${⊢}{\phi }\to {F}⇝{A}$
climcn1lem.4 ${⊢}{\phi }\to {G}\in {W}$
climcn1lem.5 ${⊢}{\phi }\to {M}\in ℤ$
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 {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in ℂ\phantom{\rule{.4em}{0ex}}\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}={ℤ}_{\ge {M}}$
2 climcn1lem.2 ${⊢}{\phi }\to {F}⇝{A}$
3 climcn1lem.4 ${⊢}{\phi }\to {G}\in {W}$
4 climcn1lem.5 ${⊢}{\phi }\to {M}\in ℤ$
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 {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in ℂ\phantom{\rule{.4em}{0ex}}\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 ffvelrni ${⊢}{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 {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in ℂ\phantom{\rule{.4em}{0ex}}\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)$