Metamath Proof Explorer

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 syl5eq ⊢ ( 𝑥 = 𝑦 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) = ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑦 − 𝑘 ) ↑ 𝑃 ) )
9 1 8 oveq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) = ( ( 𝑦 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑦 − 𝑘 ) ↑ 𝑃 ) ) )
10 9 cbvmptv ⊢ ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑦 − 𝑘 ) ↑ 𝑃 ) ) )