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

Metamath Proof Explorer

Theorem fprodp1

Description: Multiply in the last term in a finite product. (Contributed by Scott Fenton, 24-Dec-2017)

Ref Expression
Hypotheses fprodp1.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
fprodp1.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ ℂ )
fprodp1.3 ⊢ ( 𝑘 = ( 𝑁 + 1 ) → 𝐴 = 𝐵 )
Assertion fprodp1 ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐴 = ( ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 · 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fprodp1.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 fprodp1.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ ℂ )
3 fprodp1.3 ⊢ ( 𝑘 = ( 𝑁 + 1 ) → 𝐴 = 𝐵 )
4 peano2uz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
5 1 4 syl ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
6 5 2 3 fprodm1 ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐴 = ( ∏ 𝑘 ∈ ( 𝑀 ... ( ( 𝑁 + 1 ) − 1 ) ) 𝐴 · 𝐵 ) )
7 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
8 1 7 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
9 8 zcnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
10 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
11 9 10 pncand ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
12 11 oveq2d ⊢ ( 𝜑 → ( 𝑀 ... ( ( 𝑁 + 1 ) − 1 ) ) = ( 𝑀 ... 𝑁 ) )
13 12 prodeq1d ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... ( ( 𝑁 + 1 ) − 1 ) ) 𝐴 = ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 )
14 13 oveq1d ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 𝑀 ... ( ( 𝑁 + 1 ) − 1 ) ) 𝐴 · 𝐵 ) = ( ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 · 𝐵 ) )
15 6 14 eqtrd ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐴 = ( ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 · 𝐵 ) )