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 ) )
7 6 prodeq2ad 
 |-  ( x = y -> prod_ k e. ( 1 ... M ) ( ( x - k ) ^ P ) = prod_ k e. ( 1 ... M ) ( ( y - k ) ^ P ) )
8 4 7 syl5eq 
 |-  ( x = y -> prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) = prod_ k e. ( 1 ... M ) ( ( y - k ) ^ P ) )
9 1 8 oveq12d 
 |-  ( 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 ) ) )
10 9 cbvmptv 
 |-  ( 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 ) ) )