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

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 ) ) 𝐴 · ⦋ 𝑁 / 𝑘 ⦌ 𝐴 ) )