Metamath Proof Explorer


Theorem fprodm1s

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

Ref Expression
Hypotheses fprodm1s.1 ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
fprodm1s.2 ( ( 𝜑𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
Assertion fprodm1s ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ( ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 · 𝑁 / 𝑘 𝐴 ) )

Proof

Step Hyp Ref Expression
1 fprodm1s.1 ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
2 fprodm1s.2 ( ( 𝜑𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
3 2 ralrimiva ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∈ ℂ )
4 nfcsb1v 𝑘 𝑚 / 𝑘 𝐴
5 4 nfel1 𝑘 𝑚 / 𝑘 𝐴 ∈ ℂ
6 csbeq1a ( 𝑘 = 𝑚𝐴 = 𝑚 / 𝑘 𝐴 )
7 6 eleq1d ( 𝑘 = 𝑚 → ( 𝐴 ∈ ℂ ↔ 𝑚 / 𝑘 𝐴 ∈ ℂ ) )
8 5 7 rspc ( 𝑚 ∈ ( 𝑀 ... 𝑁 ) → ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∈ ℂ → 𝑚 / 𝑘 𝐴 ∈ ℂ ) )
9 3 8 mpan9 ( ( 𝜑𝑚 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑚 / 𝑘 𝐴 ∈ ℂ )
10 csbeq1 ( 𝑚 = 𝑁 𝑚 / 𝑘 𝐴 = 𝑁 / 𝑘 𝐴 )
11 1 9 10 fprodm1 ( 𝜑 → ∏ 𝑚 ∈ ( 𝑀 ... 𝑁 ) 𝑚 / 𝑘 𝐴 = ( ∏ 𝑚 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝑚 / 𝑘 𝐴 · 𝑁 / 𝑘 𝐴 ) )
12 nfcv 𝑚 𝐴
13 12 4 6 cbvprodi 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ∏ 𝑚 ∈ ( 𝑀 ... 𝑁 ) 𝑚 / 𝑘 𝐴
14 12 4 6 cbvprodi 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 = ∏ 𝑚 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝑚 / 𝑘 𝐴
15 14 oveq1i ( ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 · 𝑁 / 𝑘 𝐴 ) = ( ∏ 𝑚 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝑚 / 𝑘 𝐴 · 𝑁 / 𝑘 𝐴 )
16 11 13 15 3eqtr4g ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ( ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 · 𝑁 / 𝑘 𝐴 ) )