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 ) )