Metamath Proof Explorer

Theorem etransclem41

Description: P does not divide the P-1 -th derivative of F applied to 0 . This is the first part of case 2: proven in in Juillerat p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem41.m 
|- ( ph -> M e. NN0 )
etransclem41.p 
|- ( ph -> P e. Prime )
etransclem41.mp 
|- ( ph -> ( ! ` M ) < P )
etransclem41.f 
|- F = ( x e. RR |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
Assertion etransclem41 
|- ( ph -> -. P || ( ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) / ( ! ` ( P - 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 etransclem41.m 
 |-  ( ph -> M e. NN0 )
2 etransclem41.p 
 |-  ( ph -> P e. Prime )
3 etransclem41.mp 
 |-  ( ph -> ( ! ` M ) < P )
4 etransclem41.f 
 |-  F = ( x e. RR |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
5 1 faccld 
 |-  ( ph -> ( ! ` M ) e. NN )
6 5 nnred 
 |-  ( ph -> ( ! ` M ) e. RR )
7 prmnn 
 |-  ( P e. Prime -> P e. NN )
8 2 7 syl 
 |-  ( ph -> P e. NN )
9 8 nnred 
 |-  ( ph -> P e. RR )
10 6 9 ltnled 
 |-  ( ph -> ( ( ! ` M ) < P <-> -. P <_ ( ! ` M ) ) )
11 3 10 mpbid 
 |-  ( ph -> -. P <_ ( ! ` M ) )
12 8 nnzd 
 |-  ( ph -> P e. ZZ )
13 12 5 jca 
 |-  ( ph -> ( P e. ZZ /\ ( ! ` M ) e. NN ) )
14 13 adantr 
 |-  ( ( ph /\ P || ( ! ` M ) ) -> ( P e. ZZ /\ ( ! ` M ) e. NN ) )
15 simpr 
 |-  ( ( ph /\ P || ( ! ` M ) ) -> P || ( ! ` M ) )
16 dvdsle 
 |-  ( ( P e. ZZ /\ ( ! ` M ) e. NN ) -> ( P || ( ! ` M ) -> P <_ ( ! ` M ) ) )
17 14 15 16 sylc 
 |-  ( ( ph /\ P || ( ! ` M ) ) -> P <_ ( ! ` M ) )
18 11 17 mtand 
 |-  ( ph -> -. P || ( ! ` M ) )
19 fzfid 
 |-  ( T. -> ( 1 ... M ) e. Fin )
20 elfzelz 
 |-  ( j e. ( 1 ... M ) -> j e. ZZ )
21 20 znegcld 
 |-  ( j e. ( 1 ... M ) -> -u j e. ZZ )
22 21 zcnd 
 |-  ( j e. ( 1 ... M ) -> -u j e. CC )
23 22 adantl 
 |-  ( ( T. /\ j e. ( 1 ... M ) ) -> -u j e. CC )
24 19 23 fprodabs2 
 |-  ( T. -> ( abs ` prod_ j e. ( 1 ... M ) -u j ) = prod_ j e. ( 1 ... M ) ( abs ` -u j ) )
25 24 mptru 
 |-  ( abs ` prod_ j e. ( 1 ... M ) -u j ) = prod_ j e. ( 1 ... M ) ( abs ` -u j )
26 20 zcnd 
 |-  ( j e. ( 1 ... M ) -> j e. CC )
27 26 absnegd 
 |-  ( j e. ( 1 ... M ) -> ( abs ` -u j ) = ( abs ` j ) )
28 20 zred 
 |-  ( j e. ( 1 ... M ) -> j e. RR )
29 0red 
 |-  ( j e. ( 1 ... M ) -> 0 e. RR )
30 1red 
 |-  ( j e. ( 1 ... M ) -> 1 e. RR )
31 0lt1 
 |-  0 < 1
32 31 a1i 
 |-  ( j e. ( 1 ... M ) -> 0 < 1 )
33 elfzle1 
 |-  ( j e. ( 1 ... M ) -> 1 <_ j )
34 29 30 28 32 33 ltletrd 
 |-  ( j e. ( 1 ... M ) -> 0 < j )
35 29 28 34 ltled 
 |-  ( j e. ( 1 ... M ) -> 0 <_ j )
36 28 35 absidd 
 |-  ( j e. ( 1 ... M ) -> ( abs ` j ) = j )
37 27 36 eqtrd 
 |-  ( j e. ( 1 ... M ) -> ( abs ` -u j ) = j )
38 37 prodeq2i 
 |-  prod_ j e. ( 1 ... M ) ( abs ` -u j ) = prod_ j e. ( 1 ... M ) j
39 25 38 eqtri 
 |-  ( abs ` prod_ j e. ( 1 ... M ) -u j ) = prod_ j e. ( 1 ... M ) j
40 fprodfac 
 |-  ( M e. NN0 -> ( ! ` M ) = prod_ j e. ( 1 ... M ) j )
41 1 40 syl 
 |-  ( ph -> ( ! ` M ) = prod_ j e. ( 1 ... M ) j )
42 39 41 eqtr4id 
 |-  ( ph -> ( abs ` prod_ j e. ( 1 ... M ) -u j ) = ( ! ` M ) )
43 42 breq2d 
 |-  ( ph -> ( P || ( abs ` prod_ j e. ( 1 ... M ) -u j ) <-> P || ( ! ` M ) ) )
44 18 43 mtbird 
 |-  ( ph -> -. P || ( abs ` prod_ j e. ( 1 ... M ) -u j ) )
45 fzfid 
 |-  ( ph -> ( 1 ... M ) e. Fin )
46 21 adantl 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> -u j e. ZZ )
47 45 46 fprodzcl 
 |-  ( ph -> prod_ j e. ( 1 ... M ) -u j e. ZZ )
48 dvdsabsb 
 |-  ( ( P e. ZZ /\ prod_ j e. ( 1 ... M ) -u j e. ZZ ) -> ( P || prod_ j e. ( 1 ... M ) -u j <-> P || ( abs ` prod_ j e. ( 1 ... M ) -u j ) ) )
49 12 47 48 syl2anc 
 |-  ( ph -> ( P || prod_ j e. ( 1 ... M ) -u j <-> P || ( abs ` prod_ j e. ( 1 ... M ) -u j ) ) )
50 44 49 mtbird 
 |-  ( ph -> -. P || prod_ j e. ( 1 ... M ) -u j )
51 prmdvdsexp 
 |-  ( ( P e. Prime /\ prod_ j e. ( 1 ... M ) -u j e. ZZ /\ P e. NN ) -> ( P || ( prod_ j e. ( 1 ... M ) -u j ^ P ) <-> P || prod_ j e. ( 1 ... M ) -u j ) )
52 2 47 8 51 syl3anc 
 |-  ( ph -> ( P || ( prod_ j e. ( 1 ... M ) -u j ^ P ) <-> P || prod_ j e. ( 1 ... M ) -u j ) )
53 50 52 mtbird 
 |-  ( ph -> -. P || ( prod_ j e. ( 1 ... M ) -u j ^ P ) )
54 etransclem11 
 |-  ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } )
55 eqeq1 
 |-  ( k = j -> ( k = 0 <-> j = 0 ) )
56 55 ifbid 
 |-  ( k = j -> if ( k = 0 , ( P - 1 ) , 0 ) = if ( j = 0 , ( P - 1 ) , 0 ) )
57 56 cbvmptv 
 |-  ( k e. ( 0 ... M ) |-> if ( k = 0 , ( P - 1 ) , 0 ) ) = ( j e. ( 0 ... M ) |-> if ( j = 0 , ( P - 1 ) , 0 ) )
58 8 1 4 54 57 etransclem35 
 |-  ( ph -> ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) = ( ( ! ` ( P - 1 ) ) x. ( prod_ j e. ( 1 ... M ) -u j ^ P ) ) )
59 58 oveq1d 
 |-  ( ph -> ( ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) / ( ! ` ( P - 1 ) ) ) = ( ( ( ! ` ( P - 1 ) ) x. ( prod_ j e. ( 1 ... M ) -u j ^ P ) ) / ( ! ` ( P - 1 ) ) ) )
60 22 adantl 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> -u j e. CC )
61 45 60 fprodcl 
 |-  ( ph -> prod_ j e. ( 1 ... M ) -u j e. CC )
62 8 nnnn0d 
 |-  ( ph -> P e. NN0 )
63 61 62 expcld 
 |-  ( ph -> ( prod_ j e. ( 1 ... M ) -u j ^ P ) e. CC )
64 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
65 8 64 syl 
 |-  ( ph -> ( P - 1 ) e. NN0 )
66 65 faccld 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. NN )
67 66 nncnd 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. CC )
68 66 nnne0d 
 |-  ( ph -> ( ! ` ( P - 1 ) ) =/= 0 )
69 63 67 68 divcan3d 
 |-  ( ph -> ( ( ( ! ` ( P - 1 ) ) x. ( prod_ j e. ( 1 ... M ) -u j ^ P ) ) / ( ! ` ( P - 1 ) ) ) = ( prod_ j e. ( 1 ... M ) -u j ^ P ) )
70 59 69 eqtrd 
 |-  ( ph -> ( ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) / ( ! ` ( P - 1 ) ) ) = ( prod_ j e. ( 1 ... M ) -u j ^ P ) )
71 70 breq2d 
 |-  ( ph -> ( P || ( ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) / ( ! ` ( P - 1 ) ) ) <-> P || ( prod_ j e. ( 1 ... M ) -u j ^ P ) ) )
72 53 71 mtbird 
 |-  ( ph -> -. P || ( ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) / ( ! ` ( P - 1 ) ) ) )