Metamath Proof Explorer


Theorem addmodlteq

Description: Two nonnegative integers less than the modulus are equal iff the sums of these integer with another integer are equal modulo the modulus. A much shorter proof exists if the "divides" relation || can be used, see addmodlteqALT . (Contributed by AV, 20-Mar-2021)

Ref Expression
Assertion addmodlteq I0..^NJ0..^NSI+SmodN=J+SmodNI=J

Proof

Step Hyp Ref Expression
1 elfzoelz I0..^NI
2 1 zred I0..^NI
3 2 3ad2ant1 I0..^NJ0..^NSI
4 simp3 I0..^NJ0..^NSS
5 4 zred I0..^NJ0..^NSS
6 elfzo0 I0..^NI0NI<N
7 6 simp2bi I0..^NN
8 7 nnrpd I0..^NN+
9 8 3ad2ant1 I0..^NJ0..^NSN+
10 modaddmod ISN+ImodN+SmodN=I+SmodN
11 3 5 9 10 syl3anc I0..^NJ0..^NSImodN+SmodN=I+SmodN
12 11 eqcomd I0..^NJ0..^NSI+SmodN=ImodN+SmodN
13 elfzoelz J0..^NJ
14 13 zred J0..^NJ
15 14 3ad2ant2 I0..^NJ0..^NSJ
16 modaddmod JSN+JmodN+SmodN=J+SmodN
17 15 5 9 16 syl3anc I0..^NJ0..^NSJmodN+SmodN=J+SmodN
18 17 eqcomd I0..^NJ0..^NSJ+SmodN=JmodN+SmodN
19 12 18 eqeq12d I0..^NJ0..^NSI+SmodN=J+SmodNImodN+SmodN=JmodN+SmodN
20 nn0re I0I
21 nnrp NN+
22 20 21 anim12i I0NIN+
23 22 3adant3 I0NI<NIN+
24 modcl IN+ImodN
25 23 24 syl I0NI<NImodN
26 6 25 sylbi I0..^NImodN
27 26 3ad2ant1 I0..^NJ0..^NSImodN
28 27 5 readdcld I0..^NJ0..^NSImodN+S
29 modcl ImodN+SN+ImodN+SmodN
30 29 recnd ImodN+SN+ImodN+SmodN
31 28 9 30 syl2anc I0..^NJ0..^NSImodN+SmodN
32 elfzo0 J0..^NJ0NJ<N
33 nn0re J0J
34 33 21 anim12i J0NJN+
35 34 3adant3 J0NJ<NJN+
36 modcl JN+JmodN
37 35 36 syl J0NJ<NJmodN
38 32 37 sylbi J0..^NJmodN
39 38 3ad2ant2 I0..^NJ0..^NSJmodN
40 39 5 readdcld I0..^NJ0..^NSJmodN+S
41 modcl JmodN+SN+JmodN+SmodN
42 41 recnd JmodN+SN+JmodN+SmodN
43 40 9 42 syl2anc I0..^NJ0..^NSJmodN+SmodN
44 31 43 subeq0ad I0..^NJ0..^NSImodN+SmodNJmodN+SmodN=0ImodN+SmodN=JmodN+SmodN
45 oveq1 ImodN+SmodNJmodN+SmodN=0ImodN+SmodNJmodN+SmodNmodN=0modN
46 modsubmodmod ImodN+SJmodN+SN+ImodN+SmodNJmodN+SmodNmodN=ImodN+S-JmodN+SmodN
47 28 40 9 46 syl3anc I0..^NJ0..^NSImodN+SmodNJmodN+SmodNmodN=ImodN+S-JmodN+SmodN
48 26 recnd I0..^NImodN
49 48 3ad2ant1 I0..^NJ0..^NSImodN
50 38 recnd J0..^NJmodN
51 50 3ad2ant2 I0..^NJ0..^NSJmodN
52 4 zcnd I0..^NJ0..^NSS
53 49 51 52 pnpcan2d I0..^NJ0..^NSImodN+S-JmodN+S=ImodNJmodN
54 53 oveq1d I0..^NJ0..^NSImodN+S-JmodN+SmodN=ImodNJmodNmodN
55 47 54 eqtrd I0..^NJ0..^NSImodN+SmodNJmodN+SmodNmodN=ImodNJmodNmodN
56 32 simp2bi J0..^NN
57 56 nnrpd J0..^NN+
58 0mod N+0modN=0
59 57 58 syl J0..^N0modN=0
60 59 3ad2ant2 I0..^NJ0..^NS0modN=0
61 55 60 eqeq12d I0..^NJ0..^NSImodN+SmodNJmodN+SmodNmodN=0modNImodNJmodNmodN=0
62 zmodidfzoimp I0..^NImodN=I
63 62 3ad2ant1 I0..^NJ0..^NSImodN=I
64 zmodidfzoimp J0..^NJmodN=J
65 64 3ad2ant2 I0..^NJ0..^NSJmodN=J
66 63 65 oveq12d I0..^NJ0..^NSImodNJmodN=IJ
67 66 oveq1d I0..^NJ0..^NSImodNJmodNmodN=IJmodN
68 67 eqeq1d I0..^NJ0..^NSImodNJmodNmodN=0IJmodN=0
69 zsubcl IJIJ
70 1 13 69 syl2an I0..^NJ0..^NIJ
71 70 zred I0..^NJ0..^NIJ
72 8 adantr I0..^NJ0..^NN+
73 mod0 IJN+IJmodN=0IJN
74 71 72 73 syl2anc I0..^NJ0..^NIJmodN=0IJN
75 zdiv NIJkNk=IJIJN
76 7 70 75 syl2an2r I0..^NJ0..^NkNk=IJIJN
77 oveq2 k=0Nk= N0
78 elfzoel2 I0..^NN
79 78 zcnd I0..^NN
80 79 mul01d I0..^N N0=0
81 80 adantr I0..^NJ0..^N N0=0
82 81 adantr I0..^NJ0..^Nk N0=0
83 77 82 sylan9eq k=0I0..^NJ0..^NkNk=0
84 83 eqeq1d k=0I0..^NJ0..^NkNk=IJ0=IJ
85 eqcom 0=IJIJ=0
86 1 zcnd I0..^NI
87 13 zcnd J0..^NJ
88 subeq0 IJIJ=0I=J
89 86 87 88 syl2an I0..^NJ0..^NIJ=0I=J
90 89 biimpd I0..^NJ0..^NIJ=0I=J
91 85 90 syl5bi I0..^NJ0..^N0=IJI=J
92 91 adantr I0..^NJ0..^Nk0=IJI=J
93 92 adantl k=0I0..^NJ0..^Nk0=IJI=J
94 84 93 sylbid k=0I0..^NJ0..^NkNk=IJI=J
95 94 ex k=0I0..^NJ0..^NkNk=IJI=J
96 subfzo0 I0..^NJ0..^NN<IJIJ<N
97 96 adantr I0..^NJ0..^NkN<IJIJ<N
98 elz kkk=0kk
99 pm2.24 k=0¬k=0Nk=IJI=J
100 99 a1d k=0N<IJIJ<N¬k=0Nk=IJI=J
101 100 2a1d k=0kI0..^NJ0..^NN<IJIJ<N¬k=0Nk=IJI=J
102 breq1 Nk=IJNk<NIJ<N
103 nncn NN
104 103 mulid1d N N1=N
105 104 adantr Nk N1=N
106 105 eqcomd NkN= N1
107 106 breq2d NkNk<NNk< N1
108 nnre kk
109 108 adantl Nkk
110 1red Nk1
111 21 adantr NkN+
112 109 110 111 ltmul2d Nkk<1Nk< N1
113 nnge1 k1k
114 1red k1
115 114 108 lenltd k1k¬k<1
116 pm2.21 ¬k<1k<1I=J
117 115 116 syl6bi k1kk<1I=J
118 113 117 mpd kk<1I=J
119 118 adantl Nkk<1I=J
120 112 119 sylbird NkNk< N1I=J
121 107 120 sylbid NkNk<NI=J
122 121 ex NkNk<NI=J
123 122 3ad2ant2 J0NJ<NkNk<NI=J
124 32 123 sylbi J0..^NkNk<NI=J
125 124 adantl I0..^NJ0..^NkNk<NI=J
126 125 com13 Nk<NkI0..^NJ0..^NI=J
127 126 a1dd Nk<Nk¬k=0I0..^NJ0..^NI=J
128 102 127 syl6bir Nk=IJIJ<Nk¬k=0I0..^NJ0..^NI=J
129 128 com15 I0..^NJ0..^NIJ<Nk¬k=0Nk=IJI=J
130 129 com12 IJ<NI0..^NJ0..^Nk¬k=0Nk=IJI=J
131 130 adantl N<IJIJ<NI0..^NJ0..^Nk¬k=0Nk=IJI=J
132 131 com13 kI0..^NJ0..^NN<IJIJ<N¬k=0Nk=IJI=J
133 132 a1d kkI0..^NJ0..^NN<IJIJ<N¬k=0Nk=IJI=J
134 breq2 Nk=IJN<NkN<IJ
135 nnre NN
136 simpr kkk
137 remulcl NkNk
138 135 136 137 syl2an NkkNk
139 135 adantr NkkN
140 138 139 possumd Nkk0<Nk+NN<Nk
141 103 adantr NkkN
142 141 mulid1d Nkk N1=N
143 142 eqcomd NkkN= N1
144 143 oveq2d NkkNk+N=Nk+ N1
145 recn kk
146 145 adantl kkk
147 146 adantl Nkkk
148 1cnd Nkk1
149 141 147 148 adddid NkkNk+1=Nk+ N1
150 144 149 eqtr4d NkkNk+N=Nk+1
151 150 breq2d Nkk0<Nk+N0<Nk+1
152 peano2re kk+1
153 152 adantl kkk+1
154 153 adantl Nkkk+1
155 139 154 remulcld NkkNk+1
156 0red Nkk0
157 nnnn0 NN0
158 157 nn0ge0d N0N
159 nnge1 k1k
160 id kk
161 1cnd k1
162 160 161 addcomd kk+1=1+k
163 161 160 subnegd k1k=1+k
164 162 163 eqtr4d kk+1=1k
165 145 164 syl kk+1=1k
166 165 adantl 1kkk+1=1k
167 1red k1
168 renegcl kk
169 167 168 suble0d k1k01k
170 169 biimparc 1kk1k0
171 166 170 eqbrtrd 1kkk+10
172 159 171 sylan kkk+10
173 158 172 anim12i Nkk0Nk+10
174 173 olcd NkkN00k+10Nk+10
175 mulle0b Nk+1Nk+10N00k+10Nk+10
176 135 153 175 syl2an NkkNk+10N00k+10Nk+10
177 174 176 mpbird NkkNk+10
178 155 156 177 lensymd Nkk¬0<Nk+1
179 178 pm2.21d Nkk0<Nk+1I=J
180 151 179 sylbid Nkk0<Nk+NI=J
181 140 180 sylbird NkkN<NkI=J
182 181 a1d Nkk¬k=0N<NkI=J
183 182 ex Nkk¬k=0N<NkI=J
184 183 3ad2ant2 I0NI<Nkk¬k=0N<NkI=J
185 6 184 sylbi I0..^Nkk¬k=0N<NkI=J
186 185 adantr I0..^NJ0..^Nkk¬k=0N<NkI=J
187 186 com14 N<Nkkk¬k=0I0..^NJ0..^NI=J
188 134 187 syl6bir Nk=IJN<IJkk¬k=0I0..^NJ0..^NI=J
189 188 com15 I0..^NJ0..^NN<IJkk¬k=0Nk=IJI=J
190 189 com12 N<IJI0..^NJ0..^Nkk¬k=0Nk=IJI=J
191 190 adantr N<IJIJ<NI0..^NJ0..^Nkk¬k=0Nk=IJI=J
192 191 com13 kkI0..^NJ0..^NN<IJIJ<N¬k=0Nk=IJI=J
193 192 ex kkI0..^NJ0..^NN<IJIJ<N¬k=0Nk=IJI=J
194 101 133 193 3jaoi k=0kkkI0..^NJ0..^NN<IJIJ<N¬k=0Nk=IJI=J
195 194 impcom kk=0kkI0..^NJ0..^NN<IJIJ<N¬k=0Nk=IJI=J
196 98 195 sylbi kI0..^NJ0..^NN<IJIJ<N¬k=0Nk=IJI=J
197 196 impcom I0..^NJ0..^NkN<IJIJ<N¬k=0Nk=IJI=J
198 97 197 mpd I0..^NJ0..^Nk¬k=0Nk=IJI=J
199 198 com12 ¬k=0I0..^NJ0..^NkNk=IJI=J
200 95 199 pm2.61i I0..^NJ0..^NkNk=IJI=J
201 200 rexlimdva I0..^NJ0..^NkNk=IJI=J
202 76 201 sylbird I0..^NJ0..^NIJNI=J
203 74 202 sylbid I0..^NJ0..^NIJmodN=0I=J
204 203 3adant3 I0..^NJ0..^NSIJmodN=0I=J
205 68 204 sylbid I0..^NJ0..^NSImodNJmodNmodN=0I=J
206 61 205 sylbid I0..^NJ0..^NSImodN+SmodNJmodN+SmodNmodN=0modNI=J
207 45 206 syl5 I0..^NJ0..^NSImodN+SmodNJmodN+SmodN=0I=J
208 44 207 sylbird I0..^NJ0..^NSImodN+SmodN=JmodN+SmodNI=J
209 19 208 sylbid I0..^NJ0..^NSI+SmodN=J+SmodNI=J
210 oveq1 I=JI+S=J+S
211 210 oveq1d I=JI+SmodN=J+SmodN
212 209 211 impbid1 I0..^NJ0..^NSI+SmodN=J+SmodNI=J