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 = ℤ ≥ M
climadd.2 ⊢ φ → M ∈ ℤ
climadd.4 ⊢ φ → F ⇝ A
climaddc1.5 ⊢ φ → C ∈ ℂ
climaddc1.6 ⊢ φ → G ∈ W
climaddc1.7 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ
climmulc2.h ⊢ φ ∧ k ∈ Z → G ⁡ k = C ⁢ F ⁡ k
Assertion climmulc2 ⊢ φ → G ⇝ C ⁢ A

Proof

Step Hyp Ref Expression
1 climadd.1 ⊢ Z = ℤ ≥ M
2 climadd.2 ⊢ φ → M ∈ ℤ
3 climadd.4 ⊢ φ → F ⇝ A
4 climaddc1.5 ⊢ φ → C ∈ ℂ
5 climaddc1.6 ⊢ φ → G ∈ W
6 climaddc1.7 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ
7 climmulc2.h ⊢ φ ∧ k ∈ Z → G ⁡ k = C ⁢ F ⁡ k
8 0z ⊢ 0 ∈ ℤ
9 uzssz ⊢ ℤ ≥ 0 ⊆ ℤ
10 zex ⊢ ℤ ∈ V
11 9 10 climconst2 ⊢ C ∈ ℂ ∧ 0 ∈ ℤ → ℤ × C ⇝ C
12 4 8 11 sylancl ⊢ φ → ℤ × C ⇝ C
13 eluzelz ⊢ k ∈ ℤ ≥ M → k ∈ ℤ
14 13 1 eleq2s ⊢ k ∈ Z → k ∈ ℤ
15 fvconst2g ⊢ C ∈ ℂ ∧ k ∈ ℤ → ℤ × C ⁡ k = C
16 4 14 15 syl2an ⊢ φ ∧ k ∈ Z → ℤ × C ⁡ k = C
17 4 adantr ⊢ φ ∧ k ∈ Z → C ∈ ℂ
18 16 17 eqeltrd ⊢ φ ∧ k ∈ Z → ℤ × C ⁡ k ∈ ℂ
19 16 oveq1d ⊢ φ ∧ k ∈ Z → ℤ × C ⁡ k ⁢ F ⁡ k = C ⁢ F ⁡ k
20 7 19 eqtr4d ⊢ φ ∧ k ∈ Z → G ⁡ k = ℤ × C ⁡ k ⁢ F ⁡ k
21 1 2 12 5 3 18 6 20 climmul ⊢ φ → G ⇝ C ⁢ A