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 φ A
elqaa.2 φ F Poly 0 𝑝
elqaa.3 φ F A = 0
elqaa.4 B = coeff F
elqaa.5 N = k 0 sup n | B k n <
elqaa.6 R = seq 0 × N deg F
elqaa.7 P = x V , y V x y mod N K
Assertion elqaalem2 φ K 0 deg F R mod N K = 0

Proof

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