Metamath Proof Explorer


Theorem esummulc2

Description: An extended sum multiplied by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017)

Ref Expression
Hypotheses esummulc2.a ( 𝜑𝐴𝑉 )
esummulc2.b ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
esummulc2.c ( 𝜑𝐶 ∈ ( 0 [,) +∞ ) )
Assertion esummulc2 ( 𝜑 → ( 𝐶 ·e Σ* 𝑘𝐴 𝐵 ) = Σ* 𝑘𝐴 ( 𝐶 ·e 𝐵 ) )

Proof

Step Hyp Ref Expression
1 esummulc2.a ( 𝜑𝐴𝑉 )
2 esummulc2.b ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
3 esummulc2.c ( 𝜑𝐶 ∈ ( 0 [,) +∞ ) )
4 icossxr ( 0 [,) +∞ ) ⊆ ℝ*
5 4 3 sselid ( 𝜑𝐶 ∈ ℝ* )
6 iccssxr ( 0 [,] +∞ ) ⊆ ℝ*
7 2 ralrimiva ( 𝜑 → ∀ 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
8 nfcv 𝑘 𝐴
9 8 esumcl ( ( 𝐴𝑉 ∧ ∀ 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
10 1 7 9 syl2anc ( 𝜑 → Σ* 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
11 6 10 sselid ( 𝜑 → Σ* 𝑘𝐴 𝐵 ∈ ℝ* )
12 xmulcom ( ( 𝐶 ∈ ℝ* ∧ Σ* 𝑘𝐴 𝐵 ∈ ℝ* ) → ( 𝐶 ·e Σ* 𝑘𝐴 𝐵 ) = ( Σ* 𝑘𝐴 𝐵 ·e 𝐶 ) )
13 5 11 12 syl2anc ( 𝜑 → ( 𝐶 ·e Σ* 𝑘𝐴 𝐵 ) = ( Σ* 𝑘𝐴 𝐵 ·e 𝐶 ) )
14 1 2 3 esummulc1 ( 𝜑 → ( Σ* 𝑘𝐴 𝐵 ·e 𝐶 ) = Σ* 𝑘𝐴 ( 𝐵 ·e 𝐶 ) )
15 6 2 sselid ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℝ* )
16 5 adantr ( ( 𝜑𝑘𝐴 ) → 𝐶 ∈ ℝ* )
17 xmulcom ( ( 𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝐵 ·e 𝐶 ) = ( 𝐶 ·e 𝐵 ) )
18 15 16 17 syl2anc ( ( 𝜑𝑘𝐴 ) → ( 𝐵 ·e 𝐶 ) = ( 𝐶 ·e 𝐵 ) )
19 18 esumeq2dv ( 𝜑 → Σ* 𝑘𝐴 ( 𝐵 ·e 𝐶 ) = Σ* 𝑘𝐴 ( 𝐶 ·e 𝐵 ) )
20 13 14 19 3eqtrd ( 𝜑 → ( 𝐶 ·e Σ* 𝑘𝐴 𝐵 ) = Σ* 𝑘𝐴 ( 𝐶 ·e 𝐵 ) )