Metamath Proof Explorer

Theorem etransclem4

Description: F expressed as a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem4.a 
|- ( ph -> A C_ CC )
etransclem4.p 
|- ( ph -> P e. NN )
etransclem4.M 
|- ( ph -> M e. NN0 )
etransclem4.f 
|- F = ( x e. A |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
etransclem4.h 
|- H = ( j e. ( 0 ... M ) |-> ( x e. A |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
etransclem4.e 
|- E = ( x e. A |-> prod_ j e. ( 0 ... M ) ( ( H ` j ) ` x ) )
Assertion etransclem4 
|- ( ph -> F = E )

Proof

Step Hyp Ref Expression
1 etransclem4.a 
 |-  ( ph -> A C_ CC )
2 etransclem4.p 
 |-  ( ph -> P e. NN )
3 etransclem4.M 
 |-  ( ph -> M e. NN0 )
4 etransclem4.f 
 |-  F = ( x e. A |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
5 etransclem4.h 
 |-  H = ( j e. ( 0 ... M ) |-> ( x e. A |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
6 etransclem4.e 
 |-  E = ( x e. A |-> prod_ j e. ( 0 ... M ) ( ( H ` j ) ` x ) )
7 simpr 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> j e. ( 0 ... M ) )
8 cnex 
 |-  CC e. _V
9 8 ssex 
 |-  ( A C_ CC -> A e. _V )
10 mptexg 
 |-  ( A e. _V -> ( x e. A |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) e. _V )
11 1 9 10 3syl 
 |-  ( ph -> ( x e. A |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) e. _V )
12 11 adantr 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( x e. A |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) e. _V )
13 5 fvmpt2 
 |-  ( ( j e. ( 0 ... M ) /\ ( x e. A |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) e. _V ) -> ( H ` j ) = ( x e. A |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
14 7 12 13 syl2anc 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( H ` j ) = ( x e. A |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
15 ovexd 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. A ) -> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) e. _V )
16 14 15 fvmpt2d 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. A ) -> ( ( H ` j ) ` x ) = ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) )
17 16 an32s 
 |-  ( ( ( ph /\ x e. A ) /\ j e. ( 0 ... M ) ) -> ( ( H ` j ) ` x ) = ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) )
18 17 prodeq2dv 
 |-  ( ( ph /\ x e. A ) -> prod_ j e. ( 0 ... M ) ( ( H ` j ) ` x ) = prod_ j e. ( 0 ... M ) ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) )
19 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
20 3 19 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
21 20 adantr 
 |-  ( ( ph /\ x e. A ) -> M e. ( ZZ>= ` 0 ) )
22 1 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. CC )
23 22 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ j e. ( 0 ... M ) ) -> x e. CC )
24 elfzelz 
 |-  ( j e. ( 0 ... M ) -> j e. ZZ )
25 24 zcnd 
 |-  ( j e. ( 0 ... M ) -> j e. CC )
26 25 adantl 
 |-  ( ( ( ph /\ x e. A ) /\ j e. ( 0 ... M ) ) -> j e. CC )
27 23 26 subcld 
 |-  ( ( ( ph /\ x e. A ) /\ j e. ( 0 ... M ) ) -> ( x - j ) e. CC )
28 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
29 2 28 syl 
 |-  ( ph -> ( P - 1 ) e. NN0 )
30 2 nnnn0d 
 |-  ( ph -> P e. NN0 )
31 29 30 ifcld 
 |-  ( ph -> if ( j = 0 , ( P - 1 ) , P ) e. NN0 )
32 31 ad2antrr 
 |-  ( ( ( ph /\ x e. A ) /\ j e. ( 0 ... M ) ) -> if ( j = 0 , ( P - 1 ) , P ) e. NN0 )
33 27 32 expcld 
 |-  ( ( ( ph /\ x e. A ) /\ j e. ( 0 ... M ) ) -> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) e. CC )
34 oveq2 
 |-  ( j = 0 -> ( x - j ) = ( x - 0 ) )
35 iftrue 
 |-  ( j = 0 -> if ( j = 0 , ( P - 1 ) , P ) = ( P - 1 ) )
36 34 35 oveq12d 
 |-  ( j = 0 -> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) = ( ( x - 0 ) ^ ( P - 1 ) ) )
37 21 33 36 fprod1p 
 |-  ( ( ph /\ x e. A ) -> prod_ j e. ( 0 ... M ) ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) = ( ( ( x - 0 ) ^ ( P - 1 ) ) x. prod_ j e. ( ( 0 + 1 ) ... M ) ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
38 22 subid1d 
 |-  ( ( ph /\ x e. A ) -> ( x - 0 ) = x )
39 38 oveq1d 
 |-  ( ( ph /\ x e. A ) -> ( ( x - 0 ) ^ ( P - 1 ) ) = ( x ^ ( P - 1 ) ) )
40 0p1e1 
 |-  ( 0 + 1 ) = 1
41 40 oveq1i 
 |-  ( ( 0 + 1 ) ... M ) = ( 1 ... M )
42 41 a1i 
 |-  ( ph -> ( ( 0 + 1 ) ... M ) = ( 1 ... M ) )
43 0red 
 |-  ( j e. ( 1 ... M ) -> 0 e. RR )
44 1red 
 |-  ( j e. ( 1 ... M ) -> 1 e. RR )
45 elfzelz 
 |-  ( j e. ( 1 ... M ) -> j e. ZZ )
46 45 zred 
 |-  ( j e. ( 1 ... M ) -> j e. RR )
47 0lt1 
 |-  0 < 1
48 47 a1i 
 |-  ( j e. ( 1 ... M ) -> 0 < 1 )
49 elfzle1 
 |-  ( j e. ( 1 ... M ) -> 1 <_ j )
50 43 44 46 48 49 ltletrd 
 |-  ( j e. ( 1 ... M ) -> 0 < j )
51 50 gt0ne0d 
 |-  ( j e. ( 1 ... M ) -> j =/= 0 )
52 51 neneqd 
 |-  ( j e. ( 1 ... M ) -> -. j = 0 )
53 52 iffalsed 
 |-  ( j e. ( 1 ... M ) -> if ( j = 0 , ( P - 1 ) , P ) = P )
54 53 oveq2d 
 |-  ( j e. ( 1 ... M ) -> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) = ( ( x - j ) ^ P ) )
55 54 adantl 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) = ( ( x - j ) ^ P ) )
56 42 55 prodeq12rdv 
 |-  ( ph -> prod_ j e. ( ( 0 + 1 ) ... M ) ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) = prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) )
57 56 adantr 
 |-  ( ( ph /\ x e. A ) -> prod_ j e. ( ( 0 + 1 ) ... M ) ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) = prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) )
58 39 57 oveq12d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( x - 0 ) ^ ( P - 1 ) ) x. prod_ j e. ( ( 0 + 1 ) ... M ) ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) = ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
59 18 37 58 3eqtrrd 
 |-  ( ( ph /\ x e. A ) -> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) = prod_ j e. ( 0 ... M ) ( ( H ` j ) ` x ) )
60 59 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) ) = ( x e. A |-> prod_ j e. ( 0 ... M ) ( ( H ` j ) ` x ) ) )
61 60 4 6 3eqtr4g 
 |-  ( ph -> F = E )