This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isummulc2

Description: An infinite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005) (Revised by Mario Carneiro, 23-Apr-2014)

Ref Expression
Hypotheses isumcl.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
isumcl.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
isumcl.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
isumcl.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
isumcl.5 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
summulc.6 ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
Assertion isummulc2 ( 𝜑 → ( 𝐵 · Σ 𝑘 ∈ 𝑍 𝐴 ) = Σ 𝑘 ∈ 𝑍 ( 𝐵 · 𝐴 ) )

Proof

Step Hyp Ref Expression
1 isumcl.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 isumcl.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 isumcl.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
4 isumcl.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
5 isumcl.5 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
6 summulc.6 ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
7 eqidd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑚 ) )
8 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
9 8 4 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐵 · 𝐴 ) ∈ ℂ )
10 9 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) : 𝑍 ⟶ ℂ )
11 10 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑚 ) ∈ ℂ )
12 1 2 3 4 5 isumclim2 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ Σ 𝑘 ∈ 𝑍 𝐴 )
13 3 4 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
14 13 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
15 fveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) )
16 15 eleq1d ⊢ ( 𝑘 = 𝑚 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑚 ) ∈ ℂ ) )
17 16 rspccva ⊢ ( ( ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ℂ )
18 14 17 sylan ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ℂ )
19 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ 𝑍 )
20 ovex ⊢ ( 𝐵 · 𝐴 ) ∈ V
21 eqid ⊢ ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) = ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) )
22 21 fvmpt2 ⊢ ( ( 𝑘 ∈ 𝑍 ∧ ( 𝐵 · 𝐴 ) ∈ V ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑘 ) = ( 𝐵 · 𝐴 ) )
23 19 20 22 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑘 ) = ( 𝐵 · 𝐴 ) )
24 3 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐵 · ( 𝐹 ‘ 𝑘 ) ) = ( 𝐵 · 𝐴 ) )
25 23 24 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑘 ) = ( 𝐵 · ( 𝐹 ‘ 𝑘 ) ) )
26 25 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑘 ) = ( 𝐵 · ( 𝐹 ‘ 𝑘 ) ) )
27 nffvmpt1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑚 )
28 27 nfeq1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑚 ) = ( 𝐵 · ( 𝐹 ‘ 𝑚 ) )
29 fveq2 ⊢ ( 𝑘 = 𝑚 → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑚 ) )
30 15 oveq2d ⊢ ( 𝑘 = 𝑚 → ( 𝐵 · ( 𝐹 ‘ 𝑘 ) ) = ( 𝐵 · ( 𝐹 ‘ 𝑚 ) ) )
31 29 30 eqeq12d ⊢ ( 𝑘 = 𝑚 → ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑘 ) = ( 𝐵 · ( 𝐹 ‘ 𝑘 ) ) ↔ ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑚 ) = ( 𝐵 · ( 𝐹 ‘ 𝑚 ) ) ) )
32 28 31 rspc ⊢ ( 𝑚 ∈ 𝑍 → ( ∀ 𝑘 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑘 ) = ( 𝐵 · ( 𝐹 ‘ 𝑘 ) ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑚 ) = ( 𝐵 · ( 𝐹 ‘ 𝑚 ) ) ) )
33 26 32 mpan9 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑚 ) = ( 𝐵 · ( 𝐹 ‘ 𝑚 ) ) )
34 1 2 6 12 18 33 isermulc2 ⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ) ⇝ ( 𝐵 · Σ 𝑘 ∈ 𝑍 𝐴 ) )
35 1 2 7 11 34 isumclim ⊢ ( 𝜑 → Σ 𝑚 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑚 ) = ( 𝐵 · Σ 𝑘 ∈ 𝑍 𝐴 ) )
36 sumfc ⊢ Σ 𝑚 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐵 · 𝐴 ) ) ‘ 𝑚 ) = Σ 𝑘 ∈ 𝑍 ( 𝐵 · 𝐴 )
37 35 36 eqtr3di ⊢ ( 𝜑 → ( 𝐵 · Σ 𝑘 ∈ 𝑍 𝐴 ) = Σ 𝑘 ∈ 𝑍 ( 𝐵 · 𝐴 ) )