Metamath Proof Explorer

Theorem etransclem44

Description: The given finite sum is nonzero. This is the claim proved after equation (7) in Juillerat p. 12 . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem44.a 
|- ( ph -> A : NN0 --> ZZ )
etransclem44.a0 
|- ( ph -> ( A ` 0 ) =/= 0 )
etransclem44.m 
|- ( ph -> M e. NN0 )
etransclem44.p 
|- ( ph -> P e. Prime )
etransclem44.ap 
|- ( ph -> ( abs ` ( A ` 0 ) ) < P )
etransclem44.mp 
|- ( ph -> ( ! ` M ) < P )
etransclem44.f 
|- F = ( x e. RR |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
etransclem44.k 
|- K = ( sum_ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) )
Assertion etransclem44 
|- ( ph -> K =/= 0 )

Proof

Step Hyp Ref Expression
1 etransclem44.a 
 |-  ( ph -> A : NN0 --> ZZ )
2 etransclem44.a0 
 |-  ( ph -> ( A ` 0 ) =/= 0 )
3 etransclem44.m 
 |-  ( ph -> M e. NN0 )
4 etransclem44.p 
 |-  ( ph -> P e. Prime )
5 etransclem44.ap 
 |-  ( ph -> ( abs ` ( A ` 0 ) ) < P )
6 etransclem44.mp 
 |-  ( ph -> ( ! ` M ) < P )
7 etransclem44.f 
 |-  F = ( x e. RR |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
8 etransclem44.k 
 |-  K = ( sum_ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) )
9 8 a1i 
 |-  ( ph -> K = ( sum_ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) )
10 nfv 
 |-  F/ k ph
11 nfcv 
 |-  F/_ k ( ( A ` 0 ) x. ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) )
12 fzfi 
 |-  ( 0 ... M ) e. Fin
13 fzfi 
 |-  ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) e. Fin
14 xpfi 
 |-  ( ( ( 0 ... M ) e. Fin /\ ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) e. Fin ) -> ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) e. Fin )
15 12 13 14 mp2an 
 |-  ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) e. Fin
16 15 a1i 
 |-  ( ph -> ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) e. Fin )
17 1 adantr 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> A : NN0 --> ZZ )
18 fzssnn0 
 |-  ( 0 ... M ) C_ NN0
19 xp1st 
 |-  ( k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) -> ( 1st ` k ) e. ( 0 ... M ) )
20 18 19 sseldi 
 |-  ( k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) -> ( 1st ` k ) e. NN0 )
21 20 adantl 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> ( 1st ` k ) e. NN0 )
22 17 21 ffvelrnd 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> ( A ` ( 1st ` k ) ) e. ZZ )
23 reelprrecn 
 |-  RR e. { RR , CC }
24 23 a1i 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> RR e. { RR , CC } )
25 reopn 
 |-  RR e. ( topGen ` ran (,) )
26 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
27 26 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
28 25 27 eleqtri 
 |-  RR e. ( ( TopOpen ` CCfld ) |`t RR )
29 28 a1i 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> RR e. ( ( TopOpen ` CCfld ) |`t RR ) )
30 prmnn 
 |-  ( P e. Prime -> P e. NN )
31 4 30 syl 
 |-  ( ph -> P e. NN )
32 31 adantr 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> P e. NN )
33 3 adantr 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> M e. NN0 )
34 xp2nd 
 |-  ( k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) -> ( 2nd ` k ) e. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) )
35 elfznn0 
 |-  ( ( 2nd ` k ) e. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) -> ( 2nd ` k ) e. NN0 )
36 34 35 syl 
 |-  ( k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) -> ( 2nd ` k ) e. NN0 )
37 36 adantl 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> ( 2nd ` k ) e. NN0 )
38 21 nn0red 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> ( 1st ` k ) e. RR )
39 21 nn0zd 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> ( 1st ` k ) e. ZZ )
40 24 29 32 33 7 37 38 39 etransclem42 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) e. ZZ )
41 22 40 zmulcld 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) e. ZZ )
42 41 zcnd 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) e. CC )
43 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
44 3 43 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
45 eluzfz1 
 |-  ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
46 44 45 syl 
 |-  ( ph -> 0 e. ( 0 ... M ) )
47 0zd 
 |-  ( ph -> 0 e. ZZ )
48 3 nn0zd 
 |-  ( ph -> M e. ZZ )
49 31 nnzd 
 |-  ( ph -> P e. ZZ )
50 48 49 zmulcld 
 |-  ( ph -> ( M x. P ) e. ZZ )
51 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
52 31 51 syl 
 |-  ( ph -> ( P - 1 ) e. NN0 )
53 52 nn0zd 
 |-  ( ph -> ( P - 1 ) e. ZZ )
54 50 53 zaddcld 
 |-  ( ph -> ( ( M x. P ) + ( P - 1 ) ) e. ZZ )
55 47 54 53 3jca 
 |-  ( ph -> ( 0 e. ZZ /\ ( ( M x. P ) + ( P - 1 ) ) e. ZZ /\ ( P - 1 ) e. ZZ ) )
56 52 nn0ge0d 
 |-  ( ph -> 0 <_ ( P - 1 ) )
57 31 nnnn0d 
 |-  ( ph -> P e. NN0 )
58 3 57 nn0mulcld 
 |-  ( ph -> ( M x. P ) e. NN0 )
59 58 nn0ge0d 
 |-  ( ph -> 0 <_ ( M x. P ) )
60 52 nn0red 
 |-  ( ph -> ( P - 1 ) e. RR )
61 50 zred 
 |-  ( ph -> ( M x. P ) e. RR )
62 60 61 addge02d 
 |-  ( ph -> ( 0 <_ ( M x. P ) <-> ( P - 1 ) <_ ( ( M x. P ) + ( P - 1 ) ) ) )
63 59 62 mpbid 
 |-  ( ph -> ( P - 1 ) <_ ( ( M x. P ) + ( P - 1 ) ) )
64 55 56 63 jca32 
 |-  ( ph -> ( ( 0 e. ZZ /\ ( ( M x. P ) + ( P - 1 ) ) e. ZZ /\ ( P - 1 ) e. ZZ ) /\ ( 0 <_ ( P - 1 ) /\ ( P - 1 ) <_ ( ( M x. P ) + ( P - 1 ) ) ) ) )
65 elfz2 
 |-  ( ( P - 1 ) e. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) <-> ( ( 0 e. ZZ /\ ( ( M x. P ) + ( P - 1 ) ) e. ZZ /\ ( P - 1 ) e. ZZ ) /\ ( 0 <_ ( P - 1 ) /\ ( P - 1 ) <_ ( ( M x. P ) + ( P - 1 ) ) ) ) )
66 64 65 sylibr 
 |-  ( ph -> ( P - 1 ) e. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) )
67 opelxp 
 |-  ( <. 0 , ( P - 1 ) >. e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) <-> ( 0 e. ( 0 ... M ) /\ ( P - 1 ) e. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) )
68 46 66 67 sylanbrc 
 |-  ( ph -> <. 0 , ( P - 1 ) >. e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) )
69 fveq2 
 |-  ( k = <. 0 , ( P - 1 ) >. -> ( 1st ` k ) = ( 1st ` <. 0 , ( P - 1 ) >. ) )
70 0re 
 |-  0 e. RR
71 ovex 
 |-  ( P - 1 ) e. _V
72 op1stg 
 |-  ( ( 0 e. RR /\ ( P - 1 ) e. _V ) -> ( 1st ` <. 0 , ( P - 1 ) >. ) = 0 )
73 70 71 72 mp2an 
 |-  ( 1st ` <. 0 , ( P - 1 ) >. ) = 0
74 69 73 eqtrdi 
 |-  ( k = <. 0 , ( P - 1 ) >. -> ( 1st ` k ) = 0 )
75 74 fveq2d 
 |-  ( k = <. 0 , ( P - 1 ) >. -> ( A ` ( 1st ` k ) ) = ( A ` 0 ) )
76 fveq2 
 |-  ( k = <. 0 , ( P - 1 ) >. -> ( 2nd ` k ) = ( 2nd ` <. 0 , ( P - 1 ) >. ) )
77 op2ndg 
 |-  ( ( 0 e. RR /\ ( P - 1 ) e. _V ) -> ( 2nd ` <. 0 , ( P - 1 ) >. ) = ( P - 1 ) )
78 70 71 77 mp2an 
 |-  ( 2nd ` <. 0 , ( P - 1 ) >. ) = ( P - 1 )
79 76 78 eqtrdi 
 |-  ( k = <. 0 , ( P - 1 ) >. -> ( 2nd ` k ) = ( P - 1 ) )
80 79 fveq2d 
 |-  ( k = <. 0 , ( P - 1 ) >. -> ( ( RR Dn F ) ` ( 2nd ` k ) ) = ( ( RR Dn F ) ` ( P - 1 ) ) )
81 80 74 fveq12d 
 |-  ( k = <. 0 , ( P - 1 ) >. -> ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) = ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) )
82 75 81 oveq12d 
 |-  ( k = <. 0 , ( P - 1 ) >. -> ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) = ( ( A ` 0 ) x. ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) ) )
83 10 11 16 42 68 82 fsumsplit1 
 |-  ( ph -> sum_ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) = ( ( ( A ` 0 ) x. ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) ) + sum_ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) ) )
84 83 oveq1d 
 |-  ( ph -> ( sum_ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) = ( ( ( ( A ` 0 ) x. ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) ) + sum_ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) ) / ( ! ` ( P - 1 ) ) ) )
85 18 46 sseldi 
 |-  ( ph -> 0 e. NN0 )
86 1 85 ffvelrnd 
 |-  ( ph -> ( A ` 0 ) e. ZZ )
87 23 a1i 
 |-  ( ph -> RR e. { RR , CC } )
88 28 a1i 
 |-  ( ph -> RR e. ( ( TopOpen ` CCfld ) |`t RR ) )
89 70 a1i 
 |-  ( ph -> 0 e. RR )
90 87 88 31 3 7 52 89 47 etransclem42 
 |-  ( ph -> ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) e. ZZ )
91 86 90 zmulcld 
 |-  ( ph -> ( ( A ` 0 ) x. ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) ) e. ZZ )
92 91 zcnd 
 |-  ( ph -> ( ( A ` 0 ) x. ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) ) e. CC )
93 difss 
 |-  ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) C_ ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) )
94 ssfi 
 |-  ( ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) e. Fin /\ ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) C_ ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) e. Fin )
95 15 93 94 mp2an 
 |-  ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) e. Fin
96 95 a1i 
 |-  ( ph -> ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) e. Fin )
97 eldifi 
 |-  ( k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) -> k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) )
98 97 41 sylan2 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) e. ZZ )
99 96 98 fsumzcl 
 |-  ( ph -> sum_ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) e. ZZ )
100 99 zcnd 
 |-  ( ph -> sum_ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) e. CC )
101 52 faccld 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. NN )
102 101 nncnd 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. CC )
103 101 nnne0d 
 |-  ( ph -> ( ! ` ( P - 1 ) ) =/= 0 )
104 92 100 102 103 divdird 
 |-  ( ph -> ( ( ( ( A ` 0 ) x. ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) ) + sum_ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) ) / ( ! ` ( P - 1 ) ) ) = ( ( ( ( A ` 0 ) x. ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) ) / ( ! ` ( P - 1 ) ) ) + ( sum_ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) ) )
105 9 84 104 3eqtrd 
 |-  ( ph -> K = ( ( ( ( A ` 0 ) x. ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) ) / ( ! ` ( P - 1 ) ) ) + ( sum_ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) ) )
106 31 nnne0d 
 |-  ( ph -> P =/= 0 )
107 86 zcnd 
 |-  ( ph -> ( A ` 0 ) e. CC )
108 90 zcnd 
 |-  ( ph -> ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) e. CC )
109 107 108 102 103 divassd 
 |-  ( ph -> ( ( ( A ` 0 ) x. ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) ) / ( ! ` ( P - 1 ) ) ) = ( ( A ` 0 ) x. ( ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) / ( ! ` ( P - 1 ) ) ) ) )
110 etransclem5 
 |-  ( k e. ( 0 ... M ) |-> ( y e. RR |-> ( ( y - k ) ^ if ( k = 0 , ( P - 1 ) , P ) ) ) ) = ( j e. ( 0 ... M ) |-> ( x e. RR |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
111 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 } )
112 87 88 31 3 7 52 110 111 46 89 etransclem37 
 |-  ( ph -> ( ! ` ( P - 1 ) ) || ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) )
113 101 nnzd 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. ZZ )
114 dvdsval2 
 |-  ( ( ( ! ` ( P - 1 ) ) e. ZZ /\ ( ! ` ( P - 1 ) ) =/= 0 /\ ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) e. ZZ ) -> ( ( ! ` ( P - 1 ) ) || ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) <-> ( ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) / ( ! ` ( P - 1 ) ) ) e. ZZ ) )
115 113 103 90 114 syl3anc 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) || ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) <-> ( ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) / ( ! ` ( P - 1 ) ) ) e. ZZ ) )
116 112 115 mpbid 
 |-  ( ph -> ( ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) / ( ! ` ( P - 1 ) ) ) e. ZZ )
117 86 116 zmulcld 
 |-  ( ph -> ( ( A ` 0 ) x. ( ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) / ( ! ` ( P - 1 ) ) ) ) e. ZZ )
118 109 117 eqeltrd 
 |-  ( ph -> ( ( ( A ` 0 ) x. ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) ) / ( ! ` ( P - 1 ) ) ) e. ZZ )
119 97 42 sylan2 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) e. CC )
120 96 102 119 103 fsumdivc 
 |-  ( ph -> ( sum_ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) = sum_ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ( ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) )
121 22 zcnd 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> ( A ` ( 1st ` k ) ) e. CC )
122 97 121 sylan2 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> ( A ` ( 1st ` k ) ) e. CC )
123 97 40 sylan2 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) e. ZZ )
124 123 zcnd 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) e. CC )
125 102 adantr 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> ( ! ` ( P - 1 ) ) e. CC )
126 103 adantr 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> ( ! ` ( P - 1 ) ) =/= 0 )
127 122 124 125 126 divassd 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> ( ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) = ( ( A ` ( 1st ` k ) ) x. ( ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) / ( ! ` ( P - 1 ) ) ) ) )
128 97 22 sylan2 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> ( A ` ( 1st ` k ) ) e. ZZ )
129 23 a1i 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> RR e. { RR , CC } )
130 28 a1i 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> RR e. ( ( TopOpen ` CCfld ) |`t RR ) )
131 31 adantr 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> P e. NN )
132 3 adantr 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> M e. NN0 )
133 97 adantl 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) )
134 133 36 syl 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> ( 2nd ` k ) e. NN0 )
135 133 19 syl 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> ( 1st ` k ) e. ( 0 ... M ) )
136 97 38 sylan2 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> ( 1st ` k ) e. RR )
137 129 130 131 132 7 134 110 111 135 136 etransclem37 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> ( ! ` ( P - 1 ) ) || ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) )
138 113 adantr 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> ( ! ` ( P - 1 ) ) e. ZZ )
139 dvdsval2 
 |-  ( ( ( ! ` ( P - 1 ) ) e. ZZ /\ ( ! ` ( P - 1 ) ) =/= 0 /\ ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) e. ZZ ) -> ( ( ! ` ( P - 1 ) ) || ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) <-> ( ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) / ( ! ` ( P - 1 ) ) ) e. ZZ ) )
140 138 126 123 139 syl3anc 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> ( ( ! ` ( P - 1 ) ) || ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) <-> ( ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) / ( ! ` ( P - 1 ) ) ) e. ZZ ) )
141 137 140 mpbid 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> ( ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) / ( ! ` ( P - 1 ) ) ) e. ZZ )
142 128 141 zmulcld 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> ( ( A ` ( 1st ` k ) ) x. ( ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) / ( ! ` ( P - 1 ) ) ) ) e. ZZ )
143 127 142 eqeltrd 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> ( ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) e. ZZ )
144 96 143 fsumzcl 
 |-  ( ph -> sum_ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ( ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) e. ZZ )
145 120 144 eqeltrd 
 |-  ( ph -> ( sum_ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) e. ZZ )
146 1zzd 
 |-  ( ph -> 1 e. ZZ )
147 zabscl 
 |-  ( ( A ` 0 ) e. ZZ -> ( abs ` ( A ` 0 ) ) e. ZZ )
148 86 147 syl 
 |-  ( ph -> ( abs ` ( A ` 0 ) ) e. ZZ )
149 146 53 148 3jca 
 |-  ( ph -> ( 1 e. ZZ /\ ( P - 1 ) e. ZZ /\ ( abs ` ( A ` 0 ) ) e. ZZ ) )
150 nn0abscl 
 |-  ( ( A ` 0 ) e. ZZ -> ( abs ` ( A ` 0 ) ) e. NN0 )
151 86 150 syl 
 |-  ( ph -> ( abs ` ( A ` 0 ) ) e. NN0 )
152 107 2 absne0d 
 |-  ( ph -> ( abs ` ( A ` 0 ) ) =/= 0 )
153 elnnne0 
 |-  ( ( abs ` ( A ` 0 ) ) e. NN <-> ( ( abs ` ( A ` 0 ) ) e. NN0 /\ ( abs ` ( A ` 0 ) ) =/= 0 ) )
154 151 152 153 sylanbrc 
 |-  ( ph -> ( abs ` ( A ` 0 ) ) e. NN )
155 154 nnge1d 
 |-  ( ph -> 1 <_ ( abs ` ( A ` 0 ) ) )
156 zltlem1 
 |-  ( ( ( abs ` ( A ` 0 ) ) e. ZZ /\ P e. ZZ ) -> ( ( abs ` ( A ` 0 ) ) < P <-> ( abs ` ( A ` 0 ) ) <_ ( P - 1 ) ) )
157 148 49 156 syl2anc 
 |-  ( ph -> ( ( abs ` ( A ` 0 ) ) < P <-> ( abs ` ( A ` 0 ) ) <_ ( P - 1 ) ) )
158 5 157 mpbid 
 |-  ( ph -> ( abs ` ( A ` 0 ) ) <_ ( P - 1 ) )
159 149 155 158 jca32 
 |-  ( ph -> ( ( 1 e. ZZ /\ ( P - 1 ) e. ZZ /\ ( abs ` ( A ` 0 ) ) e. ZZ ) /\ ( 1 <_ ( abs ` ( A ` 0 ) ) /\ ( abs ` ( A ` 0 ) ) <_ ( P - 1 ) ) ) )
160 elfz2 
 |-  ( ( abs ` ( A ` 0 ) ) e. ( 1 ... ( P - 1 ) ) <-> ( ( 1 e. ZZ /\ ( P - 1 ) e. ZZ /\ ( abs ` ( A ` 0 ) ) e. ZZ ) /\ ( 1 <_ ( abs ` ( A ` 0 ) ) /\ ( abs ` ( A ` 0 ) ) <_ ( P - 1 ) ) ) )
161 159 160 sylibr 
 |-  ( ph -> ( abs ` ( A ` 0 ) ) e. ( 1 ... ( P - 1 ) ) )
162 fzm1ndvds 
 |-  ( ( P e. NN /\ ( abs ` ( A ` 0 ) ) e. ( 1 ... ( P - 1 ) ) ) -> -. P || ( abs ` ( A ` 0 ) ) )
163 31 161 162 syl2anc 
 |-  ( ph -> -. P || ( abs ` ( A ` 0 ) ) )
164 dvdsabsb 
 |-  ( ( P e. ZZ /\ ( A ` 0 ) e. ZZ ) -> ( P || ( A ` 0 ) <-> P || ( abs ` ( A ` 0 ) ) ) )
165 49 86 164 syl2anc 
 |-  ( ph -> ( P || ( A ` 0 ) <-> P || ( abs ` ( A ` 0 ) ) ) )
166 163 165 mtbird 
 |-  ( ph -> -. P || ( A ` 0 ) )
167 3 4 6 7 etransclem41 
 |-  ( ph -> -. P || ( ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) / ( ! ` ( P - 1 ) ) ) )
168 166 167 jca 
 |-  ( ph -> ( -. P || ( A ` 0 ) /\ -. P || ( ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) / ( ! ` ( P - 1 ) ) ) ) )
169 pm4.56 
 |-  ( ( -. P || ( A ` 0 ) /\ -. P || ( ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) / ( ! ` ( P - 1 ) ) ) ) <-> -. ( P || ( A ` 0 ) \/ P || ( ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) / ( ! ` ( P - 1 ) ) ) ) )
170 168 169 sylib 
 |-  ( ph -> -. ( P || ( A ` 0 ) \/ P || ( ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) / ( ! ` ( P - 1 ) ) ) ) )
171 euclemma 
 |-  ( ( P e. Prime /\ ( A ` 0 ) e. ZZ /\ ( ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) / ( ! ` ( P - 1 ) ) ) e. ZZ ) -> ( P || ( ( A ` 0 ) x. ( ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) / ( ! ` ( P - 1 ) ) ) ) <-> ( P || ( A ` 0 ) \/ P || ( ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) / ( ! ` ( P - 1 ) ) ) ) ) )
172 4 86 116 171 syl3anc 
 |-  ( ph -> ( P || ( ( A ` 0 ) x. ( ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) / ( ! ` ( P - 1 ) ) ) ) <-> ( P || ( A ` 0 ) \/ P || ( ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) / ( ! ` ( P - 1 ) ) ) ) ) )
173 170 172 mtbird 
 |-  ( ph -> -. P || ( ( A ` 0 ) x. ( ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) / ( ! ` ( P - 1 ) ) ) ) )
174 109 breq2d 
 |-  ( ph -> ( P || ( ( ( A ` 0 ) x. ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) ) / ( ! ` ( P - 1 ) ) ) <-> P || ( ( A ` 0 ) x. ( ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) / ( ! ` ( P - 1 ) ) ) ) ) )
175 173 174 mtbird 
 |-  ( ph -> -. P || ( ( ( A ` 0 ) x. ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) ) / ( ! ` ( P - 1 ) ) ) )
176 49 adantr 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> P e. ZZ )
177 176 128 141 3jca 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> ( P e. ZZ /\ ( A ` ( 1st ` k ) ) e. ZZ /\ ( ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) / ( ! ` ( P - 1 ) ) ) e. ZZ ) )
178 eldifn 
 |-  ( k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) -> -. k e. { <. 0 , ( P - 1 ) >. } )
179 97 adantr 
 |-  ( ( k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) /\ ( ( 2nd ` k ) = ( P - 1 ) /\ ( 1st ` k ) = 0 ) ) -> k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) )
180 1st2nd2 
 |-  ( k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) -> k = <. ( 1st ` k ) , ( 2nd ` k ) >. )
181 179 180 syl 
 |-  ( ( k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) /\ ( ( 2nd ` k ) = ( P - 1 ) /\ ( 1st ` k ) = 0 ) ) -> k = <. ( 1st ` k ) , ( 2nd ` k ) >. )
182 simpr 
 |-  ( ( ( 2nd ` k ) = ( P - 1 ) /\ ( 1st ` k ) = 0 ) -> ( 1st ` k ) = 0 )
183 simpl 
 |-  ( ( ( 2nd ` k ) = ( P - 1 ) /\ ( 1st ` k ) = 0 ) -> ( 2nd ` k ) = ( P - 1 ) )
184 182 183 opeq12d 
 |-  ( ( ( 2nd ` k ) = ( P - 1 ) /\ ( 1st ` k ) = 0 ) -> <. ( 1st ` k ) , ( 2nd ` k ) >. = <. 0 , ( P - 1 ) >. )
185 184 adantl 
 |-  ( ( k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) /\ ( ( 2nd ` k ) = ( P - 1 ) /\ ( 1st ` k ) = 0 ) ) -> <. ( 1st ` k ) , ( 2nd ` k ) >. = <. 0 , ( P - 1 ) >. )
186 181 185 eqtrd 
 |-  ( ( k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) /\ ( ( 2nd ` k ) = ( P - 1 ) /\ ( 1st ` k ) = 0 ) ) -> k = <. 0 , ( P - 1 ) >. )
187 velsn 
 |-  ( k e. { <. 0 , ( P - 1 ) >. } <-> k = <. 0 , ( P - 1 ) >. )
188 186 187 sylibr 
 |-  ( ( k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) /\ ( ( 2nd ` k ) = ( P - 1 ) /\ ( 1st ` k ) = 0 ) ) -> k e. { <. 0 , ( P - 1 ) >. } )
189 178 188 mtand 
 |-  ( k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) -> -. ( ( 2nd ` k ) = ( P - 1 ) /\ ( 1st ` k ) = 0 ) )
190 189 adantl 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> -. ( ( 2nd ` k ) = ( P - 1 ) /\ ( 1st ` k ) = 0 ) )
191 131 132 7 134 135 190 111 etransclem38 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> P || ( ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) / ( ! ` ( P - 1 ) ) ) )
192 dvdsmultr2 
 |-  ( ( P e. ZZ /\ ( A ` ( 1st ` k ) ) e. ZZ /\ ( ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) / ( ! ` ( P - 1 ) ) ) e. ZZ ) -> ( P || ( ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) / ( ! ` ( P - 1 ) ) ) -> P || ( ( A ` ( 1st ` k ) ) x. ( ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) / ( ! ` ( P - 1 ) ) ) ) ) )
193 177 191 192 sylc 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> P || ( ( A ` ( 1st ` k ) ) x. ( ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) / ( ! ` ( P - 1 ) ) ) ) )
194 193 127 breqtrrd 
 |-  ( ( ph /\ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ) -> P || ( ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) )
195 96 49 143 194 fsumdvds 
 |-  ( ph -> P || sum_ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ( ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) )
196 195 120 breqtrrd 
 |-  ( ph -> P || ( sum_ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) )
197 49 106 118 145 175 196 etransclem9 
 |-  ( ph -> ( ( ( ( A ` 0 ) x. ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) ) / ( ! ` ( P - 1 ) ) ) + ( sum_ k e. ( ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) \ { <. 0 , ( P - 1 ) >. } ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) ) =/= 0 )
198 105 197 eqnetrd 
 |-  ( ph -> K =/= 0 )