# Metamath Proof Explorer

## Theorem climmulc2

Description: Limit of a sequence multiplied by a constant C . Corollary 12-2.2 of Gleason p. 171. (Contributed by NM, 24-Sep-2005) (Revised by Mario Carneiro, 3-Feb-2014)

Ref Expression
Hypotheses climadd.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
climadd.2 ${⊢}{\phi }\to {M}\in ℤ$
climadd.4 ${⊢}{\phi }\to {F}⇝{A}$
climaddc1.5 ${⊢}{\phi }\to {C}\in ℂ$
climaddc1.6 ${⊢}{\phi }\to {G}\in {W}$
climaddc1.7 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)\in ℂ$
climmulc2.h ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right)={C}{F}\left({k}\right)$
Assertion climmulc2 ${⊢}{\phi }\to {G}⇝{C}{A}$

### Proof

Step Hyp Ref Expression
1 climadd.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 climadd.2 ${⊢}{\phi }\to {M}\in ℤ$
3 climadd.4 ${⊢}{\phi }\to {F}⇝{A}$
4 climaddc1.5 ${⊢}{\phi }\to {C}\in ℂ$
5 climaddc1.6 ${⊢}{\phi }\to {G}\in {W}$
6 climaddc1.7 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)\in ℂ$
7 climmulc2.h ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right)={C}{F}\left({k}\right)$
8 0z ${⊢}0\in ℤ$
9 uzssz ${⊢}{ℤ}_{\ge 0}\subseteq ℤ$
10 zex ${⊢}ℤ\in \mathrm{V}$
11 9 10 climconst2 ${⊢}\left({C}\in ℂ\wedge 0\in ℤ\right)\to \left(ℤ×\left\{{C}\right\}\right)⇝{C}$
12 4 8 11 sylancl ${⊢}{\phi }\to \left(ℤ×\left\{{C}\right\}\right)⇝{C}$
13 eluzelz ${⊢}{k}\in {ℤ}_{\ge {M}}\to {k}\in ℤ$
14 13 1 eleq2s ${⊢}{k}\in {Z}\to {k}\in ℤ$
15 fvconst2g ${⊢}\left({C}\in ℂ\wedge {k}\in ℤ\right)\to \left(ℤ×\left\{{C}\right\}\right)\left({k}\right)={C}$
16 4 14 15 syl2an ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left(ℤ×\left\{{C}\right\}\right)\left({k}\right)={C}$
17 4 adantr ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {C}\in ℂ$
18 16 17 eqeltrd ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left(ℤ×\left\{{C}\right\}\right)\left({k}\right)\in ℂ$
19 16 oveq1d ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left(ℤ×\left\{{C}\right\}\right)\left({k}\right){F}\left({k}\right)={C}{F}\left({k}\right)$
20 7 19 eqtr4d ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right)=\left(ℤ×\left\{{C}\right\}\right)\left({k}\right){F}\left({k}\right)$
21 1 2 12 5 3 18 6 20 climmul ${⊢}{\phi }\to {G}⇝{C}{A}$