Theorem fprodp1s

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

	Ref	Expression
Hypotheses	fprodp1s.1	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
	fprodp1s.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ ℂ )
Assertion	fprodp1s	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐴 = ( ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 · ⦋ ( 𝑁 + 1 ) / 𝑘 ⦌ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		fprodp1s.1	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2		fprodp1s.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ ℂ )
3	2	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐴 ∈ ℂ )
4		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ 𝐴
5	4	nfel1	⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ 𝐴 ∈ ℂ
6		csbeq1a	⊢ ( 𝑘 = 𝑚 → 𝐴 = ⦋ 𝑚 / 𝑘 ⦌ 𝐴 )
7	6	eleq1d	⊢ ( 𝑘 = 𝑚 → ( 𝐴 ∈ ℂ ↔ ⦋ 𝑚 / 𝑘 ⦌ 𝐴 ∈ ℂ ) )
8	5 7	rspc	⊢ ( 𝑚 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) → ( ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐴 ∈ ℂ → ⦋ 𝑚 / 𝑘 ⦌ 𝐴 ∈ ℂ ) )
9	3 8	mpan9	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐴 ∈ ℂ )
10		csbeq1	⊢ ( 𝑚 = ( 𝑁 + 1 ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐴 = ⦋ ( 𝑁 + 1 ) / 𝑘 ⦌ 𝐴 )
11	1 9 10	fprodp1	⊢ ( 𝜑 → ∏ 𝑚 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ⦋ 𝑚 / 𝑘 ⦌ 𝐴 = ( ∏ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ⦋ 𝑚 / 𝑘 ⦌ 𝐴 · ⦋ ( 𝑁 + 1 ) / 𝑘 ⦌ 𝐴 ) )
12		nfcv	⊢ Ⅎ 𝑚 𝐴
13	12 4 6	cbvprodi	⊢ ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐴 = ∏ 𝑚 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ⦋ 𝑚 / 𝑘 ⦌ 𝐴
14	12 4 6	cbvprodi	⊢ ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ∏ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ⦋ 𝑚 / 𝑘 ⦌ 𝐴
15	14	oveq1i	⊢ ( ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 · ⦋ ( 𝑁 + 1 ) / 𝑘 ⦌ 𝐴 ) = ( ∏ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ⦋ 𝑚 / 𝑘 ⦌ 𝐴 · ⦋ ( 𝑁 + 1 ) / 𝑘 ⦌ 𝐴 )
16	11 13 15	3eqtr4g	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐴 = ( ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 · ⦋ ( 𝑁 + 1 ) / 𝑘 ⦌ 𝐴 ) )