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 𝑍 = ( ℤ𝑀 )
isermulc2.2 ( 𝜑𝑀 ∈ ℤ )
isermulc2.4 ( 𝜑𝐶 ∈ ℂ )
isermulc2.5 ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ 𝐴 )
isermulc2.6 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℂ )
isermulc2.7 ( ( 𝜑𝑘𝑍 ) → ( 𝐺𝑘 ) = ( 𝐶 · ( 𝐹𝑘 ) ) )
Assertion isermulc2 ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ⇝ ( 𝐶 · 𝐴 ) )

Proof

Step Hyp Ref Expression
1 clim2ser.1 𝑍 = ( ℤ𝑀 )
2 isermulc2.2 ( 𝜑𝑀 ∈ ℤ )
3 isermulc2.4 ( 𝜑𝐶 ∈ ℂ )
4 isermulc2.5 ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ 𝐴 )
5 isermulc2.6 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℂ )
6 isermulc2.7 ( ( 𝜑𝑘𝑍 ) → ( 𝐺𝑘 ) = ( 𝐶 · ( 𝐹𝑘 ) ) )
7 seqex seq 𝑀 ( + , 𝐺 ) ∈ V
8 7 a1i ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ∈ V )
9 1 2 5 serf ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℂ )
10 9 ffvelrnda ( ( 𝜑𝑗𝑍 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ∈ ℂ )
11 addcl ( ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑘 + 𝑥 ) ∈ ℂ )
12 11 adantl ( ( ( 𝜑𝑗𝑍 ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑘 + 𝑥 ) ∈ ℂ )
13 3 adantr ( ( 𝜑𝑗𝑍 ) → 𝐶 ∈ ℂ )
14 adddi ( ( 𝐶 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝐶 · ( 𝑘 + 𝑥 ) ) = ( ( 𝐶 · 𝑘 ) + ( 𝐶 · 𝑥 ) ) )
15 14 3expb ( ( 𝐶 ∈ ℂ ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝐶 · ( 𝑘 + 𝑥 ) ) = ( ( 𝐶 · 𝑘 ) + ( 𝐶 · 𝑥 ) ) )
16 13 15 sylan ( ( ( 𝜑𝑗𝑍 ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝐶 · ( 𝑘 + 𝑥 ) ) = ( ( 𝐶 · 𝑘 ) + ( 𝐶 · 𝑥 ) ) )
17 simpr ( ( 𝜑𝑗𝑍 ) → 𝑗𝑍 )
18 17 1 eleqtrdi ( ( 𝜑𝑗𝑍 ) → 𝑗 ∈ ( ℤ𝑀 ) )
19 elfzuz ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ ( ℤ𝑀 ) )
20 19 1 eleqtrrdi ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘𝑍 )
21 20 5 sylan2 ( ( 𝜑𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐹𝑘 ) ∈ ℂ )
22 21 adantlr ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐹𝑘 ) ∈ ℂ )
23 20 6 sylan2 ( ( 𝜑𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐺𝑘 ) = ( 𝐶 · ( 𝐹𝑘 ) ) )
24 23 adantlr ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐺𝑘 ) = ( 𝐶 · ( 𝐹𝑘 ) ) )
25 12 16 18 22 24 seqdistr ( ( 𝜑𝑗𝑍 ) → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) = ( 𝐶 · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) )
26 1 2 4 3 8 10 25 climmulc2 ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ⇝ ( 𝐶 · 𝐴 ) )