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	⊢ ( 𝜑 → ( 𝐵 · Σ 𝑘 ∈ 𝑍 𝐴 ) = Σ 𝑘 ∈ 𝑍 ( 𝐵 · 𝐴 ) )