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
|- ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( ( I + S ) mod N ) = ( ( J + S ) mod N ) <-> I = J ) )

Proof

Step Hyp Ref Expression
1 elfzoelz
 |-  ( I e. ( 0 ..^ N ) -> I e. ZZ )
2 1 zred
 |-  ( I e. ( 0 ..^ N ) -> I e. RR )
3 2 3ad2ant1
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> I e. RR )
4 simp3
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> S e. ZZ )
5 4 zred
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> S e. RR )
6 elfzo0
 |-  ( I e. ( 0 ..^ N ) <-> ( I e. NN0 /\ N e. NN /\ I < N ) )
7 6 simp2bi
 |-  ( I e. ( 0 ..^ N ) -> N e. NN )
8 7 nnrpd
 |-  ( I e. ( 0 ..^ N ) -> N e. RR+ )
9 8 3ad2ant1
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> N e. RR+ )
10 modaddmod
 |-  ( ( I e. RR /\ S e. RR /\ N e. RR+ ) -> ( ( ( I mod N ) + S ) mod N ) = ( ( I + S ) mod N ) )
11 3 5 9 10 syl3anc
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( ( I mod N ) + S ) mod N ) = ( ( I + S ) mod N ) )
12 11 eqcomd
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( I + S ) mod N ) = ( ( ( I mod N ) + S ) mod N ) )
13 elfzoelz
 |-  ( J e. ( 0 ..^ N ) -> J e. ZZ )
14 13 zred
 |-  ( J e. ( 0 ..^ N ) -> J e. RR )
15 14 3ad2ant2
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> J e. RR )
16 modaddmod
 |-  ( ( J e. RR /\ S e. RR /\ N e. RR+ ) -> ( ( ( J mod N ) + S ) mod N ) = ( ( J + S ) mod N ) )
17 15 5 9 16 syl3anc
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( ( J mod N ) + S ) mod N ) = ( ( J + S ) mod N ) )
18 17 eqcomd
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( J + S ) mod N ) = ( ( ( J mod N ) + S ) mod N ) )
19 12 18 eqeq12d
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( ( I + S ) mod N ) = ( ( J + S ) mod N ) <-> ( ( ( I mod N ) + S ) mod N ) = ( ( ( J mod N ) + S ) mod N ) ) )
20 nn0re
 |-  ( I e. NN0 -> I e. RR )
21 nnrp
 |-  ( N e. NN -> N e. RR+ )
22 20 21 anim12i
 |-  ( ( I e. NN0 /\ N e. NN ) -> ( I e. RR /\ N e. RR+ ) )
23 22 3adant3
 |-  ( ( I e. NN0 /\ N e. NN /\ I < N ) -> ( I e. RR /\ N e. RR+ ) )
24 modcl
 |-  ( ( I e. RR /\ N e. RR+ ) -> ( I mod N ) e. RR )
25 23 24 syl
 |-  ( ( I e. NN0 /\ N e. NN /\ I < N ) -> ( I mod N ) e. RR )
26 6 25 sylbi
 |-  ( I e. ( 0 ..^ N ) -> ( I mod N ) e. RR )
27 26 3ad2ant1
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( I mod N ) e. RR )
28 27 5 readdcld
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( I mod N ) + S ) e. RR )
29 modcl
 |-  ( ( ( ( I mod N ) + S ) e. RR /\ N e. RR+ ) -> ( ( ( I mod N ) + S ) mod N ) e. RR )
30 29 recnd
 |-  ( ( ( ( I mod N ) + S ) e. RR /\ N e. RR+ ) -> ( ( ( I mod N ) + S ) mod N ) e. CC )
31 28 9 30 syl2anc
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( ( I mod N ) + S ) mod N ) e. CC )
32 elfzo0
 |-  ( J e. ( 0 ..^ N ) <-> ( J e. NN0 /\ N e. NN /\ J < N ) )
33 nn0re
 |-  ( J e. NN0 -> J e. RR )
34 33 21 anim12i
 |-  ( ( J e. NN0 /\ N e. NN ) -> ( J e. RR /\ N e. RR+ ) )
35 34 3adant3
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( J e. RR /\ N e. RR+ ) )
36 modcl
 |-  ( ( J e. RR /\ N e. RR+ ) -> ( J mod N ) e. RR )
37 35 36 syl
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( J mod N ) e. RR )
38 32 37 sylbi
 |-  ( J e. ( 0 ..^ N ) -> ( J mod N ) e. RR )
39 38 3ad2ant2
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( J mod N ) e. RR )
40 39 5 readdcld
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( J mod N ) + S ) e. RR )
41 modcl
 |-  ( ( ( ( J mod N ) + S ) e. RR /\ N e. RR+ ) -> ( ( ( J mod N ) + S ) mod N ) e. RR )
42 41 recnd
 |-  ( ( ( ( J mod N ) + S ) e. RR /\ N e. RR+ ) -> ( ( ( J mod N ) + S ) mod N ) e. CC )
43 40 9 42 syl2anc
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( ( J mod N ) + S ) mod N ) e. CC )
44 31 43 subeq0ad
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( ( ( ( I mod N ) + S ) mod N ) - ( ( ( J mod N ) + S ) mod N ) ) = 0 <-> ( ( ( I mod N ) + S ) mod N ) = ( ( ( J mod N ) + S ) mod N ) ) )
45 oveq1
 |-  ( ( ( ( ( I mod N ) + S ) mod N ) - ( ( ( J mod N ) + S ) mod N ) ) = 0 -> ( ( ( ( ( I mod N ) + S ) mod N ) - ( ( ( J mod N ) + S ) mod N ) ) mod N ) = ( 0 mod N ) )
46 modsubmodmod
 |-  ( ( ( ( I mod N ) + S ) e. RR /\ ( ( J mod N ) + S ) e. RR /\ N e. RR+ ) -> ( ( ( ( ( I mod N ) + S ) mod N ) - ( ( ( J mod N ) + S ) mod N ) ) mod N ) = ( ( ( ( I mod N ) + S ) - ( ( J mod N ) + S ) ) mod N ) )
47 28 40 9 46 syl3anc
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( ( ( ( I mod N ) + S ) mod N ) - ( ( ( J mod N ) + S ) mod N ) ) mod N ) = ( ( ( ( I mod N ) + S ) - ( ( J mod N ) + S ) ) mod N ) )
48 26 recnd
 |-  ( I e. ( 0 ..^ N ) -> ( I mod N ) e. CC )
49 48 3ad2ant1
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( I mod N ) e. CC )
50 38 recnd
 |-  ( J e. ( 0 ..^ N ) -> ( J mod N ) e. CC )
51 50 3ad2ant2
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( J mod N ) e. CC )
52 4 zcnd
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> S e. CC )
53 49 51 52 pnpcan2d
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( ( I mod N ) + S ) - ( ( J mod N ) + S ) ) = ( ( I mod N ) - ( J mod N ) ) )
54 53 oveq1d
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( ( ( I mod N ) + S ) - ( ( J mod N ) + S ) ) mod N ) = ( ( ( I mod N ) - ( J mod N ) ) mod N ) )
55 47 54 eqtrd
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( ( ( ( I mod N ) + S ) mod N ) - ( ( ( J mod N ) + S ) mod N ) ) mod N ) = ( ( ( I mod N ) - ( J mod N ) ) mod N ) )
56 32 simp2bi
 |-  ( J e. ( 0 ..^ N ) -> N e. NN )
57 56 nnrpd
 |-  ( J e. ( 0 ..^ N ) -> N e. RR+ )
58 0mod
 |-  ( N e. RR+ -> ( 0 mod N ) = 0 )
59 57 58 syl
 |-  ( J e. ( 0 ..^ N ) -> ( 0 mod N ) = 0 )
60 59 3ad2ant2
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( 0 mod N ) = 0 )
61 55 60 eqeq12d
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( ( ( ( ( I mod N ) + S ) mod N ) - ( ( ( J mod N ) + S ) mod N ) ) mod N ) = ( 0 mod N ) <-> ( ( ( I mod N ) - ( J mod N ) ) mod N ) = 0 ) )
62 zmodidfzoimp
 |-  ( I e. ( 0 ..^ N ) -> ( I mod N ) = I )
63 62 3ad2ant1
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( I mod N ) = I )
64 zmodidfzoimp
 |-  ( J e. ( 0 ..^ N ) -> ( J mod N ) = J )
65 64 3ad2ant2
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( J mod N ) = J )
66 63 65 oveq12d
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( I mod N ) - ( J mod N ) ) = ( I - J ) )
67 66 oveq1d
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( ( I mod N ) - ( J mod N ) ) mod N ) = ( ( I - J ) mod N ) )
68 67 eqeq1d
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( ( ( I mod N ) - ( J mod N ) ) mod N ) = 0 <-> ( ( I - J ) mod N ) = 0 ) )
69 zsubcl
 |-  ( ( I e. ZZ /\ J e. ZZ ) -> ( I - J ) e. ZZ )
70 1 13 69 syl2an
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( I - J ) e. ZZ )
71 70 zred
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( I - J ) e. RR )
72 8 adantr
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> N e. RR+ )
73 mod0
 |-  ( ( ( I - J ) e. RR /\ N e. RR+ ) -> ( ( ( I - J ) mod N ) = 0 <-> ( ( I - J ) / N ) e. ZZ ) )
74 71 72 73 syl2anc
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( ( ( I - J ) mod N ) = 0 <-> ( ( I - J ) / N ) e. ZZ ) )
75 zdiv
 |-  ( ( N e. NN /\ ( I - J ) e. ZZ ) -> ( E. k e. ZZ ( N x. k ) = ( I - J ) <-> ( ( I - J ) / N ) e. ZZ ) )
76 7 70 75 syl2an2r
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( E. k e. ZZ ( N x. k ) = ( I - J ) <-> ( ( I - J ) / N ) e. ZZ ) )
77 oveq2
 |-  ( k = 0 -> ( N x. k ) = ( N x. 0 ) )
78 elfzoel2
 |-  ( I e. ( 0 ..^ N ) -> N e. ZZ )
79 78 zcnd
 |-  ( I e. ( 0 ..^ N ) -> N e. CC )
80 79 mul01d
 |-  ( I e. ( 0 ..^ N ) -> ( N x. 0 ) = 0 )
81 80 adantr
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( N x. 0 ) = 0 )
82 81 adantr
 |-  ( ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) /\ k e. ZZ ) -> ( N x. 0 ) = 0 )
83 77 82 sylan9eq
 |-  ( ( k = 0 /\ ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) /\ k e. ZZ ) ) -> ( N x. k ) = 0 )
84 83 eqeq1d
 |-  ( ( k = 0 /\ ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) /\ k e. ZZ ) ) -> ( ( N x. k ) = ( I - J ) <-> 0 = ( I - J ) ) )
85 eqcom
 |-  ( 0 = ( I - J ) <-> ( I - J ) = 0 )
86 1 zcnd
 |-  ( I e. ( 0 ..^ N ) -> I e. CC )
87 13 zcnd
 |-  ( J e. ( 0 ..^ N ) -> J e. CC )
88 subeq0
 |-  ( ( I e. CC /\ J e. CC ) -> ( ( I - J ) = 0 <-> I = J ) )
89 86 87 88 syl2an
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( ( I - J ) = 0 <-> I = J ) )
90 89 biimpd
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( ( I - J ) = 0 -> I = J ) )
91 85 90 syl5bi
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( 0 = ( I - J ) -> I = J ) )
92 91 adantr
 |-  ( ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) /\ k e. ZZ ) -> ( 0 = ( I - J ) -> I = J ) )
93 92 adantl
 |-  ( ( k = 0 /\ ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) /\ k e. ZZ ) ) -> ( 0 = ( I - J ) -> I = J ) )
94 84 93 sylbid
 |-  ( ( k = 0 /\ ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) /\ k e. ZZ ) ) -> ( ( N x. k ) = ( I - J ) -> I = J ) )
95 94 ex
 |-  ( k = 0 -> ( ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) /\ k e. ZZ ) -> ( ( N x. k ) = ( I - J ) -> I = J ) ) )
96 subfzo0
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( -u N < ( I - J ) /\ ( I - J ) < N ) )
97 96 adantr
 |-  ( ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) /\ k e. ZZ ) -> ( -u N < ( I - J ) /\ ( I - J ) < N ) )
98 elz
 |-  ( k e. ZZ <-> ( k e. RR /\ ( k = 0 \/ k e. NN \/ -u k e. NN ) ) )
99 pm2.24
 |-  ( k = 0 -> ( -. k = 0 -> ( ( N x. k ) = ( I - J ) -> I = J ) ) )
100 99 a1d
 |-  ( k = 0 -> ( ( -u N < ( I - J ) /\ ( I - J ) < N ) -> ( -. k = 0 -> ( ( N x. k ) = ( I - J ) -> I = J ) ) ) )
101 100 2a1d
 |-  ( k = 0 -> ( k e. RR -> ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( ( -u N < ( I - J ) /\ ( I - J ) < N ) -> ( -. k = 0 -> ( ( N x. k ) = ( I - J ) -> I = J ) ) ) ) ) )
102 breq1
 |-  ( ( N x. k ) = ( I - J ) -> ( ( N x. k ) < N <-> ( I - J ) < N ) )
103 nncn
 |-  ( N e. NN -> N e. CC )
104 103 mulid1d
 |-  ( N e. NN -> ( N x. 1 ) = N )
105 104 adantr
 |-  ( ( N e. NN /\ k e. NN ) -> ( N x. 1 ) = N )
106 105 eqcomd
 |-  ( ( N e. NN /\ k e. NN ) -> N = ( N x. 1 ) )
107 106 breq2d
 |-  ( ( N e. NN /\ k e. NN ) -> ( ( N x. k ) < N <-> ( N x. k ) < ( N x. 1 ) ) )
108 nnre
 |-  ( k e. NN -> k e. RR )
109 108 adantl
 |-  ( ( N e. NN /\ k e. NN ) -> k e. RR )
110 1red
 |-  ( ( N e. NN /\ k e. NN ) -> 1 e. RR )
111 21 adantr
 |-  ( ( N e. NN /\ k e. NN ) -> N e. RR+ )
112 109 110 111 ltmul2d
 |-  ( ( N e. NN /\ k e. NN ) -> ( k < 1 <-> ( N x. k ) < ( N x. 1 ) ) )
113 nnge1
 |-  ( k e. NN -> 1 <_ k )
114 1red
 |-  ( k e. NN -> 1 e. RR )
115 114 108 lenltd
 |-  ( k e. NN -> ( 1 <_ k <-> -. k < 1 ) )
116 pm2.21
 |-  ( -. k < 1 -> ( k < 1 -> I = J ) )
117 115 116 syl6bi
 |-  ( k e. NN -> ( 1 <_ k -> ( k < 1 -> I = J ) ) )
118 113 117 mpd
 |-  ( k e. NN -> ( k < 1 -> I = J ) )
119 118 adantl
 |-  ( ( N e. NN /\ k e. NN ) -> ( k < 1 -> I = J ) )
120 112 119 sylbird
 |-  ( ( N e. NN /\ k e. NN ) -> ( ( N x. k ) < ( N x. 1 ) -> I = J ) )
121 107 120 sylbid
 |-  ( ( N e. NN /\ k e. NN ) -> ( ( N x. k ) < N -> I = J ) )
122 121 ex
 |-  ( N e. NN -> ( k e. NN -> ( ( N x. k ) < N -> I = J ) ) )
123 122 3ad2ant2
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( k e. NN -> ( ( N x. k ) < N -> I = J ) ) )
124 32 123 sylbi
 |-  ( J e. ( 0 ..^ N ) -> ( k e. NN -> ( ( N x. k ) < N -> I = J ) ) )
125 124 adantl
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( k e. NN -> ( ( N x. k ) < N -> I = J ) ) )
126 125 com13
 |-  ( ( N x. k ) < N -> ( k e. NN -> ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> I = J ) ) )
127 126 a1dd
 |-  ( ( N x. k ) < N -> ( k e. NN -> ( -. k = 0 -> ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> I = J ) ) ) )
128 102 127 syl6bir
 |-  ( ( N x. k ) = ( I - J ) -> ( ( I - J ) < N -> ( k e. NN -> ( -. k = 0 -> ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> I = J ) ) ) ) )
129 128 com15
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( ( I - J ) < N -> ( k e. NN -> ( -. k = 0 -> ( ( N x. k ) = ( I - J ) -> I = J ) ) ) ) )
130 129 com12
 |-  ( ( I - J ) < N -> ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( k e. NN -> ( -. k = 0 -> ( ( N x. k ) = ( I - J ) -> I = J ) ) ) ) )
131 130 adantl
 |-  ( ( -u N < ( I - J ) /\ ( I - J ) < N ) -> ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( k e. NN -> ( -. k = 0 -> ( ( N x. k ) = ( I - J ) -> I = J ) ) ) ) )
132 131 com13
 |-  ( k e. NN -> ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( ( -u N < ( I - J ) /\ ( I - J ) < N ) -> ( -. k = 0 -> ( ( N x. k ) = ( I - J ) -> I = J ) ) ) ) )
133 132 a1d
 |-  ( k e. NN -> ( k e. RR -> ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( ( -u N < ( I - J ) /\ ( I - J ) < N ) -> ( -. k = 0 -> ( ( N x. k ) = ( I - J ) -> I = J ) ) ) ) ) )
134 breq2
 |-  ( ( N x. k ) = ( I - J ) -> ( -u N < ( N x. k ) <-> -u N < ( I - J ) ) )
135 nnre
 |-  ( N e. NN -> N e. RR )
136 simpr
 |-  ( ( -u k e. NN /\ k e. RR ) -> k e. RR )
137 remulcl
 |-  ( ( N e. RR /\ k e. RR ) -> ( N x. k ) e. RR )
138 135 136 137 syl2an
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> ( N x. k ) e. RR )
139 135 adantr
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> N e. RR )
140 138 139 possumd
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> ( 0 < ( ( N x. k ) + N ) <-> -u N < ( N x. k ) ) )
141 103 adantr
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> N e. CC )
142 141 mulid1d
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> ( N x. 1 ) = N )
143 142 eqcomd
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> N = ( N x. 1 ) )
144 143 oveq2d
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> ( ( N x. k ) + N ) = ( ( N x. k ) + ( N x. 1 ) ) )
145 recn
 |-  ( k e. RR -> k e. CC )
146 145 adantl
 |-  ( ( -u k e. NN /\ k e. RR ) -> k e. CC )
147 146 adantl
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> k e. CC )
148 1cnd
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> 1 e. CC )
149 141 147 148 adddid
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> ( N x. ( k + 1 ) ) = ( ( N x. k ) + ( N x. 1 ) ) )
150 144 149 eqtr4d
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> ( ( N x. k ) + N ) = ( N x. ( k + 1 ) ) )
151 150 breq2d
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> ( 0 < ( ( N x. k ) + N ) <-> 0 < ( N x. ( k + 1 ) ) ) )
152 peano2re
 |-  ( k e. RR -> ( k + 1 ) e. RR )
153 152 adantl
 |-  ( ( -u k e. NN /\ k e. RR ) -> ( k + 1 ) e. RR )
154 153 adantl
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> ( k + 1 ) e. RR )
155 139 154 remulcld
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> ( N x. ( k + 1 ) ) e. RR )
156 0red
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> 0 e. RR )
157 nnnn0
 |-  ( N e. NN -> N e. NN0 )
158 157 nn0ge0d
 |-  ( N e. NN -> 0 <_ N )
159 nnge1
 |-  ( -u k e. NN -> 1 <_ -u k )
160 id
 |-  ( k e. CC -> k e. CC )
161 1cnd
 |-  ( k e. CC -> 1 e. CC )
162 160 161 addcomd
 |-  ( k e. CC -> ( k + 1 ) = ( 1 + k ) )
163 161 160 subnegd
 |-  ( k e. CC -> ( 1 - -u k ) = ( 1 + k ) )
164 162 163 eqtr4d
 |-  ( k e. CC -> ( k + 1 ) = ( 1 - -u k ) )
165 145 164 syl
 |-  ( k e. RR -> ( k + 1 ) = ( 1 - -u k ) )
166 165 adantl
 |-  ( ( 1 <_ -u k /\ k e. RR ) -> ( k + 1 ) = ( 1 - -u k ) )
167 1red
 |-  ( k e. RR -> 1 e. RR )
168 renegcl
 |-  ( k e. RR -> -u k e. RR )
169 167 168 suble0d
 |-  ( k e. RR -> ( ( 1 - -u k ) <_ 0 <-> 1 <_ -u k ) )
170 169 biimparc
 |-  ( ( 1 <_ -u k /\ k e. RR ) -> ( 1 - -u k ) <_ 0 )
171 166 170 eqbrtrd
 |-  ( ( 1 <_ -u k /\ k e. RR ) -> ( k + 1 ) <_ 0 )
172 159 171 sylan
 |-  ( ( -u k e. NN /\ k e. RR ) -> ( k + 1 ) <_ 0 )
173 158 172 anim12i
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> ( 0 <_ N /\ ( k + 1 ) <_ 0 ) )
174 173 olcd
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> ( ( N <_ 0 /\ 0 <_ ( k + 1 ) ) \/ ( 0 <_ N /\ ( k + 1 ) <_ 0 ) ) )
175 mulle0b
 |-  ( ( N e. RR /\ ( k + 1 ) e. RR ) -> ( ( N x. ( k + 1 ) ) <_ 0 <-> ( ( N <_ 0 /\ 0 <_ ( k + 1 ) ) \/ ( 0 <_ N /\ ( k + 1 ) <_ 0 ) ) ) )
176 135 153 175 syl2an
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> ( ( N x. ( k + 1 ) ) <_ 0 <-> ( ( N <_ 0 /\ 0 <_ ( k + 1 ) ) \/ ( 0 <_ N /\ ( k + 1 ) <_ 0 ) ) ) )
177 174 176 mpbird
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> ( N x. ( k + 1 ) ) <_ 0 )
178 155 156 177 lensymd
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> -. 0 < ( N x. ( k + 1 ) ) )
179 178 pm2.21d
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> ( 0 < ( N x. ( k + 1 ) ) -> I = J ) )
180 151 179 sylbid
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> ( 0 < ( ( N x. k ) + N ) -> I = J ) )
181 140 180 sylbird
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> ( -u N < ( N x. k ) -> I = J ) )
182 181 a1d
 |-  ( ( N e. NN /\ ( -u k e. NN /\ k e. RR ) ) -> ( -. k = 0 -> ( -u N < ( N x. k ) -> I = J ) ) )
183 182 ex
 |-  ( N e. NN -> ( ( -u k e. NN /\ k e. RR ) -> ( -. k = 0 -> ( -u N < ( N x. k ) -> I = J ) ) ) )
184 183 3ad2ant2
 |-  ( ( I e. NN0 /\ N e. NN /\ I < N ) -> ( ( -u k e. NN /\ k e. RR ) -> ( -. k = 0 -> ( -u N < ( N x. k ) -> I = J ) ) ) )
185 6 184 sylbi
 |-  ( I e. ( 0 ..^ N ) -> ( ( -u k e. NN /\ k e. RR ) -> ( -. k = 0 -> ( -u N < ( N x. k ) -> I = J ) ) ) )
186 185 adantr
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( ( -u k e. NN /\ k e. RR ) -> ( -. k = 0 -> ( -u N < ( N x. k ) -> I = J ) ) ) )
187 186 com14
 |-  ( -u N < ( N x. k ) -> ( ( -u k e. NN /\ k e. RR ) -> ( -. k = 0 -> ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> I = J ) ) ) )
188 134 187 syl6bir
 |-  ( ( N x. k ) = ( I - J ) -> ( -u N < ( I - J ) -> ( ( -u k e. NN /\ k e. RR ) -> ( -. k = 0 -> ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> I = J ) ) ) ) )
189 188 com15
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( -u N < ( I - J ) -> ( ( -u k e. NN /\ k e. RR ) -> ( -. k = 0 -> ( ( N x. k ) = ( I - J ) -> I = J ) ) ) ) )
190 189 com12
 |-  ( -u N < ( I - J ) -> ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( ( -u k e. NN /\ k e. RR ) -> ( -. k = 0 -> ( ( N x. k ) = ( I - J ) -> I = J ) ) ) ) )
191 190 adantr
 |-  ( ( -u N < ( I - J ) /\ ( I - J ) < N ) -> ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( ( -u k e. NN /\ k e. RR ) -> ( -. k = 0 -> ( ( N x. k ) = ( I - J ) -> I = J ) ) ) ) )
192 191 com13
 |-  ( ( -u k e. NN /\ k e. RR ) -> ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( ( -u N < ( I - J ) /\ ( I - J ) < N ) -> ( -. k = 0 -> ( ( N x. k ) = ( I - J ) -> I = J ) ) ) ) )
193 192 ex
 |-  ( -u k e. NN -> ( k e. RR -> ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( ( -u N < ( I - J ) /\ ( I - J ) < N ) -> ( -. k = 0 -> ( ( N x. k ) = ( I - J ) -> I = J ) ) ) ) ) )
194 101 133 193 3jaoi
 |-  ( ( k = 0 \/ k e. NN \/ -u k e. NN ) -> ( k e. RR -> ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( ( -u N < ( I - J ) /\ ( I - J ) < N ) -> ( -. k = 0 -> ( ( N x. k ) = ( I - J ) -> I = J ) ) ) ) ) )
195 194 impcom
 |-  ( ( k e. RR /\ ( k = 0 \/ k e. NN \/ -u k e. NN ) ) -> ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( ( -u N < ( I - J ) /\ ( I - J ) < N ) -> ( -. k = 0 -> ( ( N x. k ) = ( I - J ) -> I = J ) ) ) ) )
196 98 195 sylbi
 |-  ( k e. ZZ -> ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( ( -u N < ( I - J ) /\ ( I - J ) < N ) -> ( -. k = 0 -> ( ( N x. k ) = ( I - J ) -> I = J ) ) ) ) )
197 196 impcom
 |-  ( ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) /\ k e. ZZ ) -> ( ( -u N < ( I - J ) /\ ( I - J ) < N ) -> ( -. k = 0 -> ( ( N x. k ) = ( I - J ) -> I = J ) ) ) )
198 97 197 mpd
 |-  ( ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) /\ k e. ZZ ) -> ( -. k = 0 -> ( ( N x. k ) = ( I - J ) -> I = J ) ) )
199 198 com12
 |-  ( -. k = 0 -> ( ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) /\ k e. ZZ ) -> ( ( N x. k ) = ( I - J ) -> I = J ) ) )
200 95 199 pm2.61i
 |-  ( ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) /\ k e. ZZ ) -> ( ( N x. k ) = ( I - J ) -> I = J ) )
201 200 rexlimdva
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( E. k e. ZZ ( N x. k ) = ( I - J ) -> I = J ) )
202 76 201 sylbird
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( ( ( I - J ) / N ) e. ZZ -> I = J ) )
203 74 202 sylbid
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( ( ( I - J ) mod N ) = 0 -> I = J ) )
204 203 3adant3
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( ( I - J ) mod N ) = 0 -> I = J ) )
205 68 204 sylbid
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( ( ( I mod N ) - ( J mod N ) ) mod N ) = 0 -> I = J ) )
206 61 205 sylbid
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( ( ( ( ( I mod N ) + S ) mod N ) - ( ( ( J mod N ) + S ) mod N ) ) mod N ) = ( 0 mod N ) -> I = J ) )
207 45 206 syl5
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( ( ( ( I mod N ) + S ) mod N ) - ( ( ( J mod N ) + S ) mod N ) ) = 0 -> I = J ) )
208 44 207 sylbird
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( ( ( I mod N ) + S ) mod N ) = ( ( ( J mod N ) + S ) mod N ) -> I = J ) )
209 19 208 sylbid
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( ( I + S ) mod N ) = ( ( J + S ) mod N ) -> I = J ) )
210 oveq1
 |-  ( I = J -> ( I + S ) = ( J + S ) )
211 210 oveq1d
 |-  ( I = J -> ( ( I + S ) mod N ) = ( ( J + S ) mod N ) )
212 209 211 impbid1
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) /\ S e. ZZ ) -> ( ( ( I + S ) mod N ) = ( ( J + S ) mod N ) <-> I = J ) )