Metamath Proof Explorer

Theorem isermulc2

Description: Multiplication of an infinite series by a constant. (Contributed by Paul Chapman, 14-Nov-2007) (Revised by Mario Carneiro, 1-Feb-2014)

Ref Expression
Hypotheses clim2ser.1 ⊢ Z = ℤ ≥ M
isermulc2.2 ⊢ φ → M ∈ ℤ
isermulc2.4 ⊢ φ → C ∈ ℂ
isermulc2.5 ⊢ φ → seq M + F ⇝ A
isermulc2.6 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ
isermulc2.7 ⊢ φ ∧ k ∈ Z → G ⁡ k = C ⁢ F ⁡ k
Assertion isermulc2 ⊢ φ → seq M + G ⇝ C ⁢ A

Proof

Step Hyp Ref Expression
1 clim2ser.1 ⊢ Z = ℤ ≥ M
2 isermulc2.2 ⊢ φ → M ∈ ℤ
3 isermulc2.4 ⊢ φ → C ∈ ℂ
4 isermulc2.5 ⊢ φ → seq M + F ⇝ A
5 isermulc2.6 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ
6 isermulc2.7 ⊢ φ ∧ k ∈ Z → G ⁡ k = C ⁢ F ⁡ k
7 seqex ⊢ seq M + G ∈ V
8 7 a1i ⊢ φ → seq M + G ∈ V
9 1 2 5 serf ⊢ φ → seq M + F : Z ⟶ ℂ
10 9 ffvelrnda ⊢ φ ∧ j ∈ Z → seq M + F ⁡ j ∈ ℂ
11 addcl ⊢ k ∈ ℂ ∧ x ∈ ℂ → k + x ∈ ℂ
12 11 adantl ⊢ φ ∧ j ∈ Z ∧ k ∈ ℂ ∧ x ∈ ℂ → k + x ∈ ℂ
13 3 adantr ⊢ φ ∧ j ∈ Z → C ∈ ℂ
14 adddi ⊢ C ∈ ℂ ∧ k ∈ ℂ ∧ x ∈ ℂ → C ⁢ k + x = C ⁢ k + C ⁢ x
15 14 3expb ⊢ C ∈ ℂ ∧ k ∈ ℂ ∧ x ∈ ℂ → C ⁢ k + x = C ⁢ k + C ⁢ x
16 13 15 sylan ⊢ φ ∧ j ∈ Z ∧ k ∈ ℂ ∧ x ∈ ℂ → C ⁢ k + x = C ⁢ k + C ⁢ x
17 simpr ⊢ φ ∧ j ∈ Z → j ∈ Z
18 17 1 eleqtrdi ⊢ φ ∧ j ∈ Z → j ∈ ℤ ≥ M
19 elfzuz ⊢ k ∈ M … j → k ∈ ℤ ≥ M
20 19 1 eleqtrrdi ⊢ k ∈ M … j → k ∈ Z
21 20 5 sylan2 ⊢ φ ∧ k ∈ M … j → F ⁡ k ∈ ℂ
22 21 adantlr ⊢ φ ∧ j ∈ Z ∧ k ∈ M … j → F ⁡ k ∈ ℂ
23 20 6 sylan2 ⊢ φ ∧ k ∈ M … j → G ⁡ k = C ⁢ F ⁡ k
24 23 adantlr ⊢ φ ∧ j ∈ Z ∧ k ∈ M … j → G ⁡ k = C ⁢ F ⁡ k
25 12 16 18 22 24 seqdistr ⊢ φ ∧ j ∈ Z → seq M + G ⁡ j = C ⁢ seq M + F ⁡ j
26 1 2 4 3 8 10 25 climmulc2 ⊢ φ → seq M + G ⇝ C ⁢ A