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)$$