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