Theorem etransclem6

Description: A change of bound variable, often used in proofs for etransc . (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Assertion	etransclem6	⊢ ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑦 − 𝑘 ) ↑ 𝑃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ↑ ( 𝑃 − 1 ) ) = ( 𝑦 ↑ ( 𝑃 − 1 ) ) )
2		oveq2	⊢ ( 𝑗 = 𝑘 → ( 𝑥 − 𝑗 ) = ( 𝑥 − 𝑘 ) )
3	2	oveq1d	⊢ ( 𝑗 = 𝑘 → ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) = ( ( 𝑥 − 𝑘 ) ↑ 𝑃 ) )
4	3	cbvprodv	⊢ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) = ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑘 ) ↑ 𝑃 )
5		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 − 𝑘 ) = ( 𝑦 − 𝑘 ) )
6	5	oveq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 − 𝑘 ) ↑ 𝑃 ) = ( ( 𝑦 − 𝑘 ) ↑ 𝑃 ) )
7	6	prodeq2ad	⊢ ( 𝑥 = 𝑦 → ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑘 ) ↑ 𝑃 ) = ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑦 − 𝑘 ) ↑ 𝑃 ) )
8	4 7	eqtrid	⊢ ( 𝑥 = 𝑦 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) = ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑦 − 𝑘 ) ↑ 𝑃 ) )
9	1 8	oveq12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) = ( ( 𝑦 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑦 − 𝑘 ) ↑ 𝑃 ) ) )
10	9	cbvmptv	⊢ ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑦 − 𝑘 ) ↑ 𝑃 ) ) )