Metamath Proof Explorer

Theorem elqaalem2

Description: Lemma for elqaa . (Contributed by Mario Carneiro, 23-Jul-2014) (Revised by AV, 3-Oct-2020)

Ref Expression
Hypotheses elqaa.1 
|- ( ph -> A e. CC )
elqaa.2 
|- ( ph -> F e. ( ( Poly ` QQ ) \ { 0p } ) )
elqaa.3 
|- ( ph -> ( F ` A ) = 0 )
elqaa.4 
|- B = ( coeff ` F )
elqaa.5 
|- N = ( k e. NN0 |-> inf ( { n e. NN | ( ( B ` k ) x. n ) e. ZZ } , RR , < ) )
elqaa.6 
|- R = ( seq 0 ( x. , N ) ` ( deg ` F ) )
elqaa.7 
|- P = ( x e. _V , y e. _V |-> ( ( x x. y ) mod ( N ` K ) ) )
Assertion elqaalem2 
|- ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) -> ( R mod ( N ` K ) ) = 0 )

Proof

Step Hyp Ref Expression
1 elqaa.1 
 |-  ( ph -> A e. CC )
2 elqaa.2 
 |-  ( ph -> F e. ( ( Poly ` QQ ) \ { 0p } ) )
3 elqaa.3 
 |-  ( ph -> ( F ` A ) = 0 )
4 elqaa.4 
 |-  B = ( coeff ` F )
5 elqaa.5 
 |-  N = ( k e. NN0 |-> inf ( { n e. NN | ( ( B ` k ) x. n ) e. ZZ } , RR , < ) )
6 elqaa.6 
 |-  R = ( seq 0 ( x. , N ) ` ( deg ` F ) )
7 elqaa.7 
 |-  P = ( x e. _V , y e. _V |-> ( ( x x. y ) mod ( N ` K ) ) )
8 elfznn0 
 |-  ( K e. ( 0 ... ( deg ` F ) ) -> K e. NN0 )
9 6 fveq2i 
 |-  ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` R ) = ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` ( seq 0 ( x. , N ) ` ( deg ` F ) ) )
10 nnmulcl 
 |-  ( ( i e. NN /\ j e. NN ) -> ( i x. j ) e. NN )
11 10 adantl 
 |-  ( ( ( ph /\ K e. NN0 ) /\ ( i e. NN /\ j e. NN ) ) -> ( i x. j ) e. NN )
12 elfznn0 
 |-  ( i e. ( 0 ... ( deg ` F ) ) -> i e. NN0 )
13 1 2 3 4 5 6 elqaalem1 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( N ` i ) e. NN /\ ( ( B ` i ) x. ( N ` i ) ) e. ZZ ) )
14 13 simpld 
 |-  ( ( ph /\ i e. NN0 ) -> ( N ` i ) e. NN )
15 14 adantlr 
 |-  ( ( ( ph /\ K e. NN0 ) /\ i e. NN0 ) -> ( N ` i ) e. NN )
16 12 15 sylan2 
 |-  ( ( ( ph /\ K e. NN0 ) /\ i e. ( 0 ... ( deg ` F ) ) ) -> ( N ` i ) e. NN )
17 eldifi 
 |-  ( F e. ( ( Poly ` QQ ) \ { 0p } ) -> F e. ( Poly ` QQ ) )
18 dgrcl 
 |-  ( F e. ( Poly ` QQ ) -> ( deg ` F ) e. NN0 )
19 2 17 18 3syl 
 |-  ( ph -> ( deg ` F ) e. NN0 )
20 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
21 19 20 eleqtrdi 
 |-  ( ph -> ( deg ` F ) e. ( ZZ>= ` 0 ) )
22 21 adantr 
 |-  ( ( ph /\ K e. NN0 ) -> ( deg ` F ) e. ( ZZ>= ` 0 ) )
23 nnz 
 |-  ( i e. NN -> i e. ZZ )
24 23 ad2antrl 
 |-  ( ( ( ph /\ K e. NN0 ) /\ ( i e. NN /\ j e. NN ) ) -> i e. ZZ )
25 1 2 3 4 5 6 elqaalem1 
 |-  ( ( ph /\ K e. NN0 ) -> ( ( N ` K ) e. NN /\ ( ( B ` K ) x. ( N ` K ) ) e. ZZ ) )
26 25 simpld 
 |-  ( ( ph /\ K e. NN0 ) -> ( N ` K ) e. NN )
27 26 adantr 
 |-  ( ( ( ph /\ K e. NN0 ) /\ ( i e. NN /\ j e. NN ) ) -> ( N ` K ) e. NN )
28 24 27 zmodcld 
 |-  ( ( ( ph /\ K e. NN0 ) /\ ( i e. NN /\ j e. NN ) ) -> ( i mod ( N ` K ) ) e. NN0 )
29 28 nn0zd 
 |-  ( ( ( ph /\ K e. NN0 ) /\ ( i e. NN /\ j e. NN ) ) -> ( i mod ( N ` K ) ) e. ZZ )
30 nnz 
 |-  ( j e. NN -> j e. ZZ )
31 30 ad2antll 
 |-  ( ( ( ph /\ K e. NN0 ) /\ ( i e. NN /\ j e. NN ) ) -> j e. ZZ )
32 31 27 zmodcld 
 |-  ( ( ( ph /\ K e. NN0 ) /\ ( i e. NN /\ j e. NN ) ) -> ( j mod ( N ` K ) ) e. NN0 )
33 32 nn0zd 
 |-  ( ( ( ph /\ K e. NN0 ) /\ ( i e. NN /\ j e. NN ) ) -> ( j mod ( N ` K ) ) e. ZZ )
34 27 nnrpd 
 |-  ( ( ( ph /\ K e. NN0 ) /\ ( i e. NN /\ j e. NN ) ) -> ( N ` K ) e. RR+ )
35 nnre 
 |-  ( i e. NN -> i e. RR )
36 35 ad2antrl 
 |-  ( ( ( ph /\ K e. NN0 ) /\ ( i e. NN /\ j e. NN ) ) -> i e. RR )
37 modabs2 
 |-  ( ( i e. RR /\ ( N ` K ) e. RR+ ) -> ( ( i mod ( N ` K ) ) mod ( N ` K ) ) = ( i mod ( N ` K ) ) )
38 36 34 37 syl2anc 
 |-  ( ( ( ph /\ K e. NN0 ) /\ ( i e. NN /\ j e. NN ) ) -> ( ( i mod ( N ` K ) ) mod ( N ` K ) ) = ( i mod ( N ` K ) ) )
39 nnre 
 |-  ( j e. NN -> j e. RR )
40 39 ad2antll 
 |-  ( ( ( ph /\ K e. NN0 ) /\ ( i e. NN /\ j e. NN ) ) -> j e. RR )
41 modabs2 
 |-  ( ( j e. RR /\ ( N ` K ) e. RR+ ) -> ( ( j mod ( N ` K ) ) mod ( N ` K ) ) = ( j mod ( N ` K ) ) )
42 40 34 41 syl2anc 
 |-  ( ( ( ph /\ K e. NN0 ) /\ ( i e. NN /\ j e. NN ) ) -> ( ( j mod ( N ` K ) ) mod ( N ` K ) ) = ( j mod ( N ` K ) ) )
43 29 24 33 31 34 38 42 modmul12d 
 |-  ( ( ( ph /\ K e. NN0 ) /\ ( i e. NN /\ j e. NN ) ) -> ( ( ( i mod ( N ` K ) ) x. ( j mod ( N ` K ) ) ) mod ( N ` K ) ) = ( ( i x. j ) mod ( N ` K ) ) )
44 oveq1 
 |-  ( k = i -> ( k mod ( N ` K ) ) = ( i mod ( N ` K ) ) )
45 eqid 
 |-  ( k e. NN |-> ( k mod ( N ` K ) ) ) = ( k e. NN |-> ( k mod ( N ` K ) ) )
46 ovex 
 |-  ( i mod ( N ` K ) ) e. _V
47 44 45 46 fvmpt 
 |-  ( i e. NN -> ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` i ) = ( i mod ( N ` K ) ) )
48 47 ad2antrl 
 |-  ( ( ( ph /\ K e. NN0 ) /\ ( i e. NN /\ j e. NN ) ) -> ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` i ) = ( i mod ( N ` K ) ) )
49 oveq1 
 |-  ( k = j -> ( k mod ( N ` K ) ) = ( j mod ( N ` K ) ) )
50 ovex 
 |-  ( j mod ( N ` K ) ) e. _V
51 49 45 50 fvmpt 
 |-  ( j e. NN -> ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` j ) = ( j mod ( N ` K ) ) )
52 51 ad2antll 
 |-  ( ( ( ph /\ K e. NN0 ) /\ ( i e. NN /\ j e. NN ) ) -> ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` j ) = ( j mod ( N ` K ) ) )
53 48 52 oveq12d 
 |-  ( ( ( ph /\ K e. NN0 ) /\ ( i e. NN /\ j e. NN ) ) -> ( ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` i ) P ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` j ) ) = ( ( i mod ( N ` K ) ) P ( j mod ( N ` K ) ) ) )
54 oveq12 
 |-  ( ( x = ( i mod ( N ` K ) ) /\ y = ( j mod ( N ` K ) ) ) -> ( x x. y ) = ( ( i mod ( N ` K ) ) x. ( j mod ( N ` K ) ) ) )
55 54 oveq1d 
 |-  ( ( x = ( i mod ( N ` K ) ) /\ y = ( j mod ( N ` K ) ) ) -> ( ( x x. y ) mod ( N ` K ) ) = ( ( ( i mod ( N ` K ) ) x. ( j mod ( N ` K ) ) ) mod ( N ` K ) ) )
56 ovex 
 |-  ( ( ( i mod ( N ` K ) ) x. ( j mod ( N ` K ) ) ) mod ( N ` K ) ) e. _V
57 55 7 56 ovmpoa 
 |-  ( ( ( i mod ( N ` K ) ) e. _V /\ ( j mod ( N ` K ) ) e. _V ) -> ( ( i mod ( N ` K ) ) P ( j mod ( N ` K ) ) ) = ( ( ( i mod ( N ` K ) ) x. ( j mod ( N ` K ) ) ) mod ( N ` K ) ) )
58 46 50 57 mp2an 
 |-  ( ( i mod ( N ` K ) ) P ( j mod ( N ` K ) ) ) = ( ( ( i mod ( N ` K ) ) x. ( j mod ( N ` K ) ) ) mod ( N ` K ) )
59 53 58 eqtrdi 
 |-  ( ( ( ph /\ K e. NN0 ) /\ ( i e. NN /\ j e. NN ) ) -> ( ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` i ) P ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` j ) ) = ( ( ( i mod ( N ` K ) ) x. ( j mod ( N ` K ) ) ) mod ( N ` K ) ) )
60 oveq1 
 |-  ( k = ( i x. j ) -> ( k mod ( N ` K ) ) = ( ( i x. j ) mod ( N ` K ) ) )
61 ovex 
 |-  ( ( i x. j ) mod ( N ` K ) ) e. _V
62 60 45 61 fvmpt 
 |-  ( ( i x. j ) e. NN -> ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` ( i x. j ) ) = ( ( i x. j ) mod ( N ` K ) ) )
63 11 62 syl 
 |-  ( ( ( ph /\ K e. NN0 ) /\ ( i e. NN /\ j e. NN ) ) -> ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` ( i x. j ) ) = ( ( i x. j ) mod ( N ` K ) ) )
64 43 59 63 3eqtr4rd 
 |-  ( ( ( ph /\ K e. NN0 ) /\ ( i e. NN /\ j e. NN ) ) -> ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` ( i x. j ) ) = ( ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` i ) P ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` j ) ) )
65 oveq1 
 |-  ( k = ( N ` i ) -> ( k mod ( N ` K ) ) = ( ( N ` i ) mod ( N ` K ) ) )
66 ovex 
 |-  ( ( N ` i ) mod ( N ` K ) ) e. _V
67 65 45 66 fvmpt 
 |-  ( ( N ` i ) e. NN -> ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` ( N ` i ) ) = ( ( N ` i ) mod ( N ` K ) ) )
68 15 67 syl 
 |-  ( ( ( ph /\ K e. NN0 ) /\ i e. NN0 ) -> ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` ( N ` i ) ) = ( ( N ` i ) mod ( N ` K ) ) )
69 fveq2 
 |-  ( k = i -> ( N ` k ) = ( N ` i ) )
70 69 oveq1d 
 |-  ( k = i -> ( ( N ` k ) mod ( N ` K ) ) = ( ( N ` i ) mod ( N ` K ) ) )
71 eqid 
 |-  ( k e. NN0 |-> ( ( N ` k ) mod ( N ` K ) ) ) = ( k e. NN0 |-> ( ( N ` k ) mod ( N ` K ) ) )
72 70 71 66 fvmpt 
 |-  ( i e. NN0 -> ( ( k e. NN0 |-> ( ( N ` k ) mod ( N ` K ) ) ) ` i ) = ( ( N ` i ) mod ( N ` K ) ) )
73 72 adantl 
 |-  ( ( ( ph /\ K e. NN0 ) /\ i e. NN0 ) -> ( ( k e. NN0 |-> ( ( N ` k ) mod ( N ` K ) ) ) ` i ) = ( ( N ` i ) mod ( N ` K ) ) )
74 68 73 eqtr4d 
 |-  ( ( ( ph /\ K e. NN0 ) /\ i e. NN0 ) -> ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` ( N ` i ) ) = ( ( k e. NN0 |-> ( ( N ` k ) mod ( N ` K ) ) ) ` i ) )
75 12 74 sylan2 
 |-  ( ( ( ph /\ K e. NN0 ) /\ i e. ( 0 ... ( deg ` F ) ) ) -> ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` ( N ` i ) ) = ( ( k e. NN0 |-> ( ( N ` k ) mod ( N ` K ) ) ) ` i ) )
76 11 16 22 64 75 seqhomo 
 |-  ( ( ph /\ K e. NN0 ) -> ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` ( seq 0 ( x. , N ) ` ( deg ` F ) ) ) = ( seq 0 ( P , ( k e. NN0 |-> ( ( N ` k ) mod ( N ` K ) ) ) ) ` ( deg ` F ) ) )
77 9 76 eqtrid 
 |-  ( ( ph /\ K e. NN0 ) -> ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` R ) = ( seq 0 ( P , ( k e. NN0 |-> ( ( N ` k ) mod ( N ` K ) ) ) ) ` ( deg ` F ) ) )
78 8 77 sylan2 
 |-  ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) -> ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` R ) = ( seq 0 ( P , ( k e. NN0 |-> ( ( N ` k ) mod ( N ` K ) ) ) ) ` ( deg ` F ) ) )
79 0zd 
 |-  ( ph -> 0 e. ZZ )
80 10 adantl 
 |-  ( ( ph /\ ( i e. NN /\ j e. NN ) ) -> ( i x. j ) e. NN )
81 20 79 14 80 seqf 
 |-  ( ph -> seq 0 ( x. , N ) : NN0 --> NN )
82 81 19 ffvelrnd 
 |-  ( ph -> ( seq 0 ( x. , N ) ` ( deg ` F ) ) e. NN )
83 6 82 eqeltrid 
 |-  ( ph -> R e. NN )
84 83 adantr 
 |-  ( ( ph /\ K e. NN0 ) -> R e. NN )
85 oveq1 
 |-  ( k = R -> ( k mod ( N ` K ) ) = ( R mod ( N ` K ) ) )
86 ovex 
 |-  ( R mod ( N ` K ) ) e. _V
87 85 45 86 fvmpt 
 |-  ( R e. NN -> ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` R ) = ( R mod ( N ` K ) ) )
88 84 87 syl 
 |-  ( ( ph /\ K e. NN0 ) -> ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` R ) = ( R mod ( N ` K ) ) )
89 8 88 sylan2 
 |-  ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) -> ( ( k e. NN |-> ( k mod ( N ` K ) ) ) ` R ) = ( R mod ( N ` K ) ) )
90 oveq12 
 |-  ( ( x = i /\ y = j ) -> ( x x. y ) = ( i x. j ) )
91 90 oveq1d 
 |-  ( ( x = i /\ y = j ) -> ( ( x x. y ) mod ( N ` K ) ) = ( ( i x. j ) mod ( N ` K ) ) )
92 91 7 61 ovmpoa 
 |-  ( ( i e. _V /\ j e. _V ) -> ( i P j ) = ( ( i x. j ) mod ( N ` K ) ) )
93 92 el2v 
 |-  ( i P j ) = ( ( i x. j ) mod ( N ` K ) )
94 nn0mulcl 
 |-  ( ( i e. NN0 /\ j e. NN0 ) -> ( i x. j ) e. NN0 )
95 94 nn0zd 
 |-  ( ( i e. NN0 /\ j e. NN0 ) -> ( i x. j ) e. ZZ )
96 8 26 sylan2 
 |-  ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) -> ( N ` K ) e. NN )
97 zmodcl 
 |-  ( ( ( i x. j ) e. ZZ /\ ( N ` K ) e. NN ) -> ( ( i x. j ) mod ( N ` K ) ) e. NN0 )
98 95 96 97 syl2anr 
 |-  ( ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) /\ ( i e. NN0 /\ j e. NN0 ) ) -> ( ( i x. j ) mod ( N ` K ) ) e. NN0 )
99 93 98 eqeltrid 
 |-  ( ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) /\ ( i e. NN0 /\ j e. NN0 ) ) -> ( i P j ) e. NN0 )
100 fveq2 
 |-  ( k = m -> ( B ` k ) = ( B ` m ) )
101 100 oveq1d 
 |-  ( k = m -> ( ( B ` k ) x. n ) = ( ( B ` m ) x. n ) )
102 101 eleq1d 
 |-  ( k = m -> ( ( ( B ` k ) x. n ) e. ZZ <-> ( ( B ` m ) x. n ) e. ZZ ) )
103 102 rabbidv 
 |-  ( k = m -> { n e. NN | ( ( B ` k ) x. n ) e. ZZ } = { n e. NN | ( ( B ` m ) x. n ) e. ZZ } )
104 103 infeq1d 
 |-  ( k = m -> inf ( { n e. NN | ( ( B ` k ) x. n ) e. ZZ } , RR , < ) = inf ( { n e. NN | ( ( B ` m ) x. n ) e. ZZ } , RR , < ) )
105 104 cbvmptv 
 |-  ( k e. NN0 |-> inf ( { n e. NN | ( ( B ` k ) x. n ) e. ZZ } , RR , < ) ) = ( m e. NN0 |-> inf ( { n e. NN | ( ( B ` m ) x. n ) e. ZZ } , RR , < ) )
106 5 105 eqtri 
 |-  N = ( m e. NN0 |-> inf ( { n e. NN | ( ( B ` m ) x. n ) e. ZZ } , RR , < ) )
107 1 2 3 4 106 6 elqaalem1 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( N ` k ) e. NN /\ ( ( B ` k ) x. ( N ` k ) ) e. ZZ ) )
108 107 simpld 
 |-  ( ( ph /\ k e. NN0 ) -> ( N ` k ) e. NN )
109 108 adantlr 
 |-  ( ( ( ph /\ K e. NN0 ) /\ k e. NN0 ) -> ( N ` k ) e. NN )
110 109 nnzd 
 |-  ( ( ( ph /\ K e. NN0 ) /\ k e. NN0 ) -> ( N ` k ) e. ZZ )
111 26 adantr 
 |-  ( ( ( ph /\ K e. NN0 ) /\ k e. NN0 ) -> ( N ` K ) e. NN )
112 110 111 zmodcld 
 |-  ( ( ( ph /\ K e. NN0 ) /\ k e. NN0 ) -> ( ( N ` k ) mod ( N ` K ) ) e. NN0 )
113 112 fmpttd 
 |-  ( ( ph /\ K e. NN0 ) -> ( k e. NN0 |-> ( ( N ` k ) mod ( N ` K ) ) ) : NN0 --> NN0 )
114 8 113 sylan2 
 |-  ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) -> ( k e. NN0 |-> ( ( N ` k ) mod ( N ` K ) ) ) : NN0 --> NN0 )
115 ffvelrn 
 |-  ( ( ( k e. NN0 |-> ( ( N ` k ) mod ( N ` K ) ) ) : NN0 --> NN0 /\ i e. NN0 ) -> ( ( k e. NN0 |-> ( ( N ` k ) mod ( N ` K ) ) ) ` i ) e. NN0 )
116 114 12 115 syl2an 
 |-  ( ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) /\ i e. ( 0 ... ( deg ` F ) ) ) -> ( ( k e. NN0 |-> ( ( N ` k ) mod ( N ` K ) ) ) ` i ) e. NN0 )
117 c0ex 
 |-  0 e. _V
118 vex 
 |-  i e. _V
119 oveq12 
 |-  ( ( x = 0 /\ y = i ) -> ( x x. y ) = ( 0 x. i ) )
120 119 oveq1d 
 |-  ( ( x = 0 /\ y = i ) -> ( ( x x. y ) mod ( N ` K ) ) = ( ( 0 x. i ) mod ( N ` K ) ) )
121 ovex 
 |-  ( ( 0 x. i ) mod ( N ` K ) ) e. _V
122 120 7 121 ovmpoa 
 |-  ( ( 0 e. _V /\ i e. _V ) -> ( 0 P i ) = ( ( 0 x. i ) mod ( N ` K ) ) )
123 117 118 122 mp2an 
 |-  ( 0 P i ) = ( ( 0 x. i ) mod ( N ` K ) )
124 nn0cn 
 |-  ( i e. NN0 -> i e. CC )
125 124 mul02d 
 |-  ( i e. NN0 -> ( 0 x. i ) = 0 )
126 125 oveq1d 
 |-  ( i e. NN0 -> ( ( 0 x. i ) mod ( N ` K ) ) = ( 0 mod ( N ` K ) ) )
127 96 nnrpd 
 |-  ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) -> ( N ` K ) e. RR+ )
128 0mod 
 |-  ( ( N ` K ) e. RR+ -> ( 0 mod ( N ` K ) ) = 0 )
129 127 128 syl 
 |-  ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) -> ( 0 mod ( N ` K ) ) = 0 )
130 126 129 sylan9eqr 
 |-  ( ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) /\ i e. NN0 ) -> ( ( 0 x. i ) mod ( N ` K ) ) = 0 )
131 123 130 eqtrid 
 |-  ( ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) /\ i e. NN0 ) -> ( 0 P i ) = 0 )
132 oveq12 
 |-  ( ( x = i /\ y = 0 ) -> ( x x. y ) = ( i x. 0 ) )
133 132 oveq1d 
 |-  ( ( x = i /\ y = 0 ) -> ( ( x x. y ) mod ( N ` K ) ) = ( ( i x. 0 ) mod ( N ` K ) ) )
134 ovex 
 |-  ( ( i x. 0 ) mod ( N ` K ) ) e. _V
135 133 7 134 ovmpoa 
 |-  ( ( i e. _V /\ 0 e. _V ) -> ( i P 0 ) = ( ( i x. 0 ) mod ( N ` K ) ) )
136 118 117 135 mp2an 
 |-  ( i P 0 ) = ( ( i x. 0 ) mod ( N ` K ) )
137 124 mul01d 
 |-  ( i e. NN0 -> ( i x. 0 ) = 0 )
138 137 oveq1d 
 |-  ( i e. NN0 -> ( ( i x. 0 ) mod ( N ` K ) ) = ( 0 mod ( N ` K ) ) )
139 138 129 sylan9eqr 
 |-  ( ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) /\ i e. NN0 ) -> ( ( i x. 0 ) mod ( N ` K ) ) = 0 )
140 136 139 eqtrid 
 |-  ( ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) /\ i e. NN0 ) -> ( i P 0 ) = 0 )
141 simpr 
 |-  ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) -> K e. ( 0 ... ( deg ` F ) ) )
142 19 adantr 
 |-  ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) -> ( deg ` F ) e. NN0 )
143 8 adantl 
 |-  ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) -> K e. NN0 )
144 fveq2 
 |-  ( k = K -> ( N ` k ) = ( N ` K ) )
145 144 oveq1d 
 |-  ( k = K -> ( ( N ` k ) mod ( N ` K ) ) = ( ( N ` K ) mod ( N ` K ) ) )
146 ovex 
 |-  ( ( N ` K ) mod ( N ` K ) ) e. _V
147 145 71 146 fvmpt 
 |-  ( K e. NN0 -> ( ( k e. NN0 |-> ( ( N ` k ) mod ( N ` K ) ) ) ` K ) = ( ( N ` K ) mod ( N ` K ) ) )
148 143 147 syl 
 |-  ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) -> ( ( k e. NN0 |-> ( ( N ` k ) mod ( N ` K ) ) ) ` K ) = ( ( N ` K ) mod ( N ` K ) ) )
149 96 nncnd 
 |-  ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) -> ( N ` K ) e. CC )
150 96 nnne0d 
 |-  ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) -> ( N ` K ) =/= 0 )
151 149 150 dividd 
 |-  ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) -> ( ( N ` K ) / ( N ` K ) ) = 1 )
152 1z 
 |-  1 e. ZZ
153 151 152 eqeltrdi 
 |-  ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) -> ( ( N ` K ) / ( N ` K ) ) e. ZZ )
154 96 nnred 
 |-  ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) -> ( N ` K ) e. RR )
155 mod0 
 |-  ( ( ( N ` K ) e. RR /\ ( N ` K ) e. RR+ ) -> ( ( ( N ` K ) mod ( N ` K ) ) = 0 <-> ( ( N ` K ) / ( N ` K ) ) e. ZZ ) )
156 154 127 155 syl2anc 
 |-  ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) -> ( ( ( N ` K ) mod ( N ` K ) ) = 0 <-> ( ( N ` K ) / ( N ` K ) ) e. ZZ ) )
157 153 156 mpbird 
 |-  ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) -> ( ( N ` K ) mod ( N ` K ) ) = 0 )
158 148 157 eqtrd 
 |-  ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) -> ( ( k e. NN0 |-> ( ( N ` k ) mod ( N ` K ) ) ) ` K ) = 0 )
159 99 116 131 140 141 142 158 seqz 
 |-  ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) -> ( seq 0 ( P , ( k e. NN0 |-> ( ( N ` k ) mod ( N ` K ) ) ) ) ` ( deg ` F ) ) = 0 )
160 78 89 159 3eqtr3d 
 |-  ( ( ph /\ K e. ( 0 ... ( deg ` F ) ) ) -> ( R mod ( N ` K ) ) = 0 )