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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 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 𝑀 ( + , 𝐺 ) ⇝ ( 𝐶 · 𝐴 ) )