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