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