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