# 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
`|- ( x e. RR |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) ) = ( y e. RR |-> ( ( y ^ ( P - 1 ) ) x. prod_ k e. ( 1 ... M ) ( ( y - k ) ^ P ) ) )`

### Proof

Step Hyp Ref Expression
1 oveq1
` |-  ( x = y -> ( x ^ ( P - 1 ) ) = ( y ^ ( P - 1 ) ) )`
2 oveq2
` |-  ( j = k -> ( x - j ) = ( x - k ) )`
3 2 oveq1d
` |-  ( j = k -> ( ( x - j ) ^ P ) = ( ( x - k ) ^ P ) )`
4 3 cbvprodv
` |-  prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) = prod_ k e. ( 1 ... M ) ( ( x - k ) ^ P )`
5 oveq1
` |-  ( x = y -> ( x - k ) = ( y - k ) )`
6 5 oveq1d
` |-  ( x = y -> ( ( x - k ) ^ P ) = ( ( y - k ) ^ P ) )`
` |-  ( x = y -> prod_ k e. ( 1 ... M ) ( ( x - k ) ^ P ) = prod_ k e. ( 1 ... M ) ( ( y - k ) ^ P ) )`
` |-  ( x = y -> prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) = prod_ k e. ( 1 ... M ) ( ( y - k ) ^ P ) )`
` |-  ( x = y -> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) = ( ( y ^ ( P - 1 ) ) x. prod_ k e. ( 1 ... M ) ( ( y - k ) ^ P ) ) )`
` |-  ( x e. RR |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) ) = ( y e. RR |-> ( ( y ^ ( P - 1 ) ) x. prod_ k e. ( 1 ... M ) ( ( y - k ) ^ P ) ) )`