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