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

Metamath Proof Explorer

Theorem prodfmul

Description: The product of two infinite products. (Contributed by Scott Fenton, 18-Dec-2017)

Ref Expression
Hypotheses prodfmul.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
prodfmul.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
prodfmul.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
prodfmul.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
Assertion prodfmul ( 𝜑 → ( seq 𝑀 ( · , 𝐻 ) ‘ 𝑁 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq 𝑀 ( · , 𝐺 ) ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 prodfmul.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 prodfmul.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
3 prodfmul.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
4 prodfmul.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
5 mulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
6 5 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
7 mulcom ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) )
8 7 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) )
9 mulass ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
10 9 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
11 6 8 10 1 2 3 4 seqcaopr ⊢ ( 𝜑 → ( seq 𝑀 ( · , 𝐻 ) ‘ 𝑁 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq 𝑀 ( · , 𝐺 ) ‘ 𝑁 ) ) )