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 ${⊢}\left({x}\in ℝ⟼{{x}}^{{P}-1}\prod _{{j}=1}^{{M}}{\left({x}-{j}\right)}^{{P}}\right)=\left({y}\in ℝ⟼{{y}}^{{P}-1}\prod _{{k}=1}^{{M}}{\left({y}-{k}\right)}^{{P}}\right)$

Proof

Step Hyp Ref Expression
1 oveq1 ${⊢}{x}={y}\to {{x}}^{{P}-1}={{y}}^{{P}-1}$
2 oveq2 ${⊢}{j}={k}\to {x}-{j}={x}-{k}$
3 2 oveq1d ${⊢}{j}={k}\to {\left({x}-{j}\right)}^{{P}}={\left({x}-{k}\right)}^{{P}}$
4 3 cbvprodv ${⊢}\prod _{{j}=1}^{{M}}{\left({x}-{j}\right)}^{{P}}=\prod _{{k}=1}^{{M}}{\left({x}-{k}\right)}^{{P}}$
5 oveq1 ${⊢}{x}={y}\to {x}-{k}={y}-{k}$
6 5 oveq1d ${⊢}{x}={y}\to {\left({x}-{k}\right)}^{{P}}={\left({y}-{k}\right)}^{{P}}$
7 6 prodeq2ad ${⊢}{x}={y}\to \prod _{{k}=1}^{{M}}{\left({x}-{k}\right)}^{{P}}=\prod _{{k}=1}^{{M}}{\left({y}-{k}\right)}^{{P}}$
8 4 7 syl5eq ${⊢}{x}={y}\to \prod _{{j}=1}^{{M}}{\left({x}-{j}\right)}^{{P}}=\prod _{{k}=1}^{{M}}{\left({y}-{k}\right)}^{{P}}$
9 1 8 oveq12d ${⊢}{x}={y}\to {{x}}^{{P}-1}\prod _{{j}=1}^{{M}}{\left({x}-{j}\right)}^{{P}}={{y}}^{{P}-1}\prod _{{k}=1}^{{M}}{\left({y}-{k}\right)}^{{P}}$
10 9 cbvmptv ${⊢}\left({x}\in ℝ⟼{{x}}^{{P}-1}\prod _{{j}=1}^{{M}}{\left({x}-{j}\right)}^{{P}}\right)=\left({y}\in ℝ⟼{{y}}^{{P}-1}\prod _{{k}=1}^{{M}}{\left({y}-{k}\right)}^{{P}}\right)$