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