Theorem addmodlteq 10384

Description: Two nonnegative integers less than the modulus are equal iff the sums of these integer with another integer are equal modulo the modulus. (Contributed by AV, 20-Mar-2021.)

Assertion

Ref	Expression
addmodlteq	|- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( ( I + S ) mod N ) = ( ( J + S ) mod N ) <-> I = J ) )

Proof of Theorem addmodlteq

Dummy variable k is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elfzoelz 10133	. . . . . . . 8 |- ( I e. ( 0..^ N ) -> I e. ZZ )
2	1	3ad2ant1 1018	. . . . . . 7 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> I e. ZZ )
3		zq 9615	. . . . . . 7 |- ( I e. ZZ -> I e. QQ )
4	2, 3	syl 14	. . . . . 6 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> I e. QQ )
5		simp3 999	. . . . . . 7 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> S e. ZZ )
6		zq 9615	. . . . . . 7 |- ( S e. ZZ -> S e. QQ )
7	5, 6	syl 14	. . . . . 6 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> S e. QQ )
8		elfzo0 10168	. . . . . . . . . 10 |- ( I e. ( 0..^ N ) <-> ( I e. NN0 /\ N e. NN /\ I < N ) )
9	8	biimpi 120	. . . . . . . . 9 |- ( I e. ( 0..^ N ) -> ( I e. NN0 /\ N e. NN /\ I < N ) )
10	9	3ad2ant1 1018	. . . . . . . 8 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( I e. NN0 /\ N e. NN /\ I < N ) )
11	10	simp2d 1010	. . . . . . 7 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> N e. NN )
12		nnq 9622	. . . . . . 7 |- ( N e. NN -> N e. QQ )
13	11, 12	syl 14	. . . . . 6 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> N e. QQ )
14	11	nngt0d 8952	. . . . . 6 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> 0 < N )
15		modqaddmod 10349	. . . . . 6 |- ( ( ( I e. QQ /\ S e. QQ ) /\ ( N e. QQ /\ 0 < N ) ) -> ( ( ( I mod N ) + S ) mod N ) = ( ( I + S ) mod N ) )
16	4, 7, 13, 14, 15	syl22anc 1239	. . . . 5 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( ( I mod N ) + S ) mod N ) = ( ( I + S ) mod N ) )
17	16	eqcomd 2183	. . . 4 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( I + S ) mod N ) = ( ( ( I mod N ) + S ) mod N ) )
18		elfzoelz 10133	. . . . . . . 8 |- ( J e. ( 0..^ N ) -> J e. ZZ )
19	18	3ad2ant2 1019	. . . . . . 7 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> J e. ZZ )
20		zq 9615	. . . . . . 7 |- ( J e. ZZ -> J e. QQ )
21	19, 20	syl 14	. . . . . 6 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> J e. QQ )
22		modqaddmod 10349	. . . . . 6 |- ( ( ( J e. QQ /\ S e. QQ ) /\ ( N e. QQ /\ 0 < N ) ) -> ( ( ( J mod N ) + S ) mod N ) = ( ( J + S ) mod N ) )
23	21, 7, 13, 14, 22	syl22anc 1239	. . . . 5 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( ( J mod N ) + S ) mod N ) = ( ( J + S ) mod N ) )
24	23	eqcomd 2183	. . . 4 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( J + S ) mod N ) = ( ( ( J mod N ) + S ) mod N ) )
25	17, 24	eqeq12d 2192	. . 3 |- ( ( 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 ) ) )
26	2, 11	zmodcld 10331	. . . . . . . . 9 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( I mod N ) e. NN0 )
27	26	nn0zd 9362	. . . . . . . 8 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( I mod N ) e. ZZ )
28	27, 5	zaddcld 9368	. . . . . . 7 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( I mod N ) + S ) e. ZZ )
29	28, 11	zmodcld 10331	. . . . . 6 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( ( I mod N ) + S ) mod N ) e. NN0 )
30	29	nn0cnd 9220	. . . . 5 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( ( I mod N ) + S ) mod N ) e. CC )
31	19, 11	zmodcld 10331	. . . . . . . . 9 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( J mod N ) e. NN0 )
32	31	nn0zd 9362	. . . . . . . 8 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( J mod N ) e. ZZ )
33	32, 5	zaddcld 9368	. . . . . . 7 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( J mod N ) + S ) e. ZZ )
34	33, 11	zmodcld 10331	. . . . . 6 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( ( J mod N ) + S ) mod N ) e. NN0 )
35	34	nn0cnd 9220	. . . . 5 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( ( J mod N ) + S ) mod N ) e. CC )
36	30, 35	subeq0ad 8268	. . . 4 |- ( ( 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 ) ) )
37		oveq1 5876	. . . . 5 |- ( ( ( ( ( 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 ) )
38	4, 13, 14	modqcld 10314	. . . . . . . . . 10 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( I mod N ) e. QQ )
39		qaddcl 9624	. . . . . . . . . 10 |- ( ( ( I mod N ) e. QQ /\ S e. QQ ) -> ( ( I mod N ) + S ) e. QQ )
40	38, 7, 39	syl2anc 411	. . . . . . . . 9 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( I mod N ) + S ) e. QQ )
41	21, 13, 14	modqcld 10314	. . . . . . . . . 10 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( J mod N ) e. QQ )
42		qaddcl 9624	. . . . . . . . . 10 |- ( ( ( J mod N ) e. QQ /\ S e. QQ ) -> ( ( J mod N ) + S ) e. QQ )
43	41, 7, 42	syl2anc 411	. . . . . . . . 9 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( J mod N ) + S ) e. QQ )
44		modqsubmodmod 10369	. . . . . . . . 9 |- ( ( ( ( ( I mod N ) + S ) e. QQ /\ ( ( J mod N ) + S ) e. QQ ) /\ ( N e. QQ /\ 0 < N ) ) -> ( ( ( ( ( I mod N ) + S ) mod N ) - ( ( ( J mod N ) + S ) mod N ) ) mod N ) = ( ( ( ( I mod N ) + S ) - ( ( J mod N ) + S ) ) mod N ) )
45	40, 43, 13, 14, 44	syl22anc 1239	. . . . . . . 8 |- ( ( 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 ) )
46	26	nn0cnd 9220	. . . . . . . . . 10 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( I mod N ) e. CC )
47	31	nn0cnd 9220	. . . . . . . . . 10 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( J mod N ) e. CC )
48	5	zcnd 9365	. . . . . . . . . 10 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> S e. CC )
49	46, 47, 48	pnpcan2d 8296	. . . . . . . . 9 |- ( ( 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 ) ) )
50	49	oveq1d 5884	. . . . . . . 8 |- ( ( 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 ) )
51	45, 50	eqtrd 2210	. . . . . . 7 |- ( ( 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 ) )
52		q0mod 10341	. . . . . . . 8 |- ( ( N e. QQ /\ 0 < N ) -> ( 0 mod N ) = 0 )
53	13, 14, 52	syl2anc 411	. . . . . . 7 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( 0 mod N ) = 0 )
54	51, 53	eqeq12d 2192	. . . . . 6 |- ( ( 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 ) )
55		zmodidfzoimp 10340	. . . . . . . . . . 11 |- ( I e. ( 0..^ N ) -> ( I mod N ) = I )
56	55	3ad2ant1 1018	. . . . . . . . . 10 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( I mod N ) = I )
57		zmodidfzoimp 10340	. . . . . . . . . . 11 |- ( J e. ( 0..^ N ) -> ( J mod N ) = J )
58	57	3ad2ant2 1019	. . . . . . . . . 10 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( J mod N ) = J )
59	56, 58	oveq12d 5887	. . . . . . . . 9 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( I mod N ) - ( J mod N ) ) = ( I - J ) )
60	59	oveq1d 5884	. . . . . . . 8 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( ( I mod N ) - ( J mod N ) ) mod N ) = ( ( I - J ) mod N ) )
61	60	eqeq1d 2186	. . . . . . 7 |- ( ( 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 ) )
62		qsubcl 9627	. . . . . . . . . 10 |- ( ( I e. QQ /\ J e. QQ ) -> ( I - J ) e. QQ )
63	4, 21, 62	syl2anc 411	. . . . . . . . 9 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( I - J ) e. QQ )
64		modq0 10315	. . . . . . . . 9 |- ( ( ( I - J ) e. QQ /\ N e. QQ /\ 0 < N ) -> ( ( ( I - J ) mod N ) = 0 <-> ( ( I - J ) / N ) e. ZZ ) )
65	63, 13, 14, 64	syl3anc 1238	. . . . . . . 8 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( ( I - J ) mod N ) = 0 <-> ( ( I - J ) / N ) e. ZZ ) )
66	2, 19	zsubcld 9369	. . . . . . . . . 10 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( I - J ) e. ZZ )
67		zdiv 9330	. . . . . . . . . 10 |- ( ( N e. NN /\ ( I - J ) e. ZZ ) -> ( E. k e. ZZ ( N x. k ) = ( I - J ) <-> ( ( I - J ) / N ) e. ZZ ) )
68	11, 66, 67	syl2anc 411	. . . . . . . . 9 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( E. k e. ZZ ( N x. k ) = ( I - J ) <-> ( ( I - J ) / N ) e. ZZ ) )
69		simpr 110	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ k = 0 ) -> k = 0 )
70	69	oveq2d 5885	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ k = 0 ) -> ( N x. k ) = ( N x. 0 ) )
71	11	nncnd 8922	. . . . . . . . . . . . . . . . . . 19 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> N e. CC )
72	71	mul01d 8340	. . . . . . . . . . . . . . . . . 18 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( N x. 0 ) = 0 )
73	72	ad2antrr 488	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ k = 0 ) -> ( N x. 0 ) = 0 )
74	70, 73	eqtrd 2210	. . . . . . . . . . . . . . . 16 |- ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ k = 0 ) -> ( N x. k ) = 0 )
75	74	eqeq1d 2186	. . . . . . . . . . . . . . 15 |- ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ k = 0 ) -> ( ( N x. k ) = ( I - J ) <-> 0 = ( I - J ) ) )
76		eqcom 2179	. . . . . . . . . . . . . . . 16 |- ( 0 = ( I - J ) <-> ( I - J ) = 0 )
77	10	simp1d 1009	. . . . . . . . . . . . . . . . . . . 20 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> I e. NN0 )
78	77	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ k = 0 ) -> I e. NN0 )
79	78	nn0cnd 9220	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ k = 0 ) -> I e. CC )
80		elfzo0 10168	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( J e. ( 0..^ N ) <-> ( J e. NN0 /\ N e. NN /\ J < N ) )
81	80	biimpi 120	. . . . . . . . . . . . . . . . . . . . . 22 |- ( J e. ( 0..^ N ) -> ( J e. NN0 /\ N e. NN /\ J < N ) )
82	81	3ad2ant2 1019	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( J e. NN0 /\ N e. NN /\ J < N ) )
83	82	simp1d 1009	. . . . . . . . . . . . . . . . . . . 20 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> J e. NN0 )
84	83	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ k = 0 ) -> J e. NN0 )
85	84	nn0cnd 9220	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ k = 0 ) -> J e. CC )
86	79, 85	subeq0ad 8268	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ k = 0 ) -> ( ( I - J ) = 0 <-> I = J ) )
87	86	biimpd 144	. . . . . . . . . . . . . . . 16 |- ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ k = 0 ) -> ( ( I - J ) = 0 -> I = J ) )
88	76, 87	biimtrid 152	. . . . . . . . . . . . . . 15 |- ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ k = 0 ) -> ( 0 = ( I - J ) -> I = J ) )
89	75, 88	sylbid 150	. . . . . . . . . . . . . 14 |- ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ k = 0 ) -> ( ( N x. k ) = ( I - J ) -> I = J ) )
90	89	imp 124	. . . . . . . . . . . . 13 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ k = 0 ) /\ ( N x. k ) = ( I - J ) ) -> I = J )
91	90	an32s 568	. . . . . . . . . . . 12 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ k = 0 ) -> I = J )
92		subfzo0 10228	. . . . . . . . . . . . . . . . . 18 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) ) -> ( -u N < ( I - J ) /\ ( I - J ) < N ) )
93	92	3adant3 1017	. . . . . . . . . . . . . . . . 17 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( -u N < ( I - J ) /\ ( I - J ) < N ) )
94	93	ad3antrrr 492	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ k e. NN ) -> ( -u N < ( I - J ) /\ ( I - J ) < N ) )
95	94	simprd 114	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ k e. NN ) -> ( I - J ) < N )
96		simplr 528	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ k e. NN ) -> ( N x. k ) = ( I - J ) )
97	71	mulid1d 7965	. . . . . . . . . . . . . . . 16 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( N x. 1 ) = N )
98	97	ad3antrrr 492	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ k e. NN ) -> ( N x. 1 ) = N )
99	95, 96, 98	3brtr4d 4032	. . . . . . . . . . . . . 14 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ k e. NN ) -> ( N x. k ) < ( N x. 1 ) )
100		simpllr 534	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ k e. NN ) -> k e. ZZ )
101	100	zred 9364	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ k e. NN ) -> k e. RR )
102		1red 7963	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ k e. NN ) -> 1 e. RR )
103	11	nnrpd 9681	. . . . . . . . . . . . . . . 16 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> N e. RR+ )
104	103	ad3antrrr 492	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ k e. NN ) -> N e. RR+ )
105	101, 102, 104	ltmul2d 9726	. . . . . . . . . . . . . 14 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ k e. NN ) -> ( k < 1 <-> ( N x. k ) < ( N x. 1 ) ) )
106	99, 105	mpbird 167	. . . . . . . . . . . . 13 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ k e. NN ) -> k < 1 )
107		simpr 110	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ k e. NN ) -> k e. NN )
108	107	nnge1d 8951	. . . . . . . . . . . . . 14 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ k e. NN ) -> 1 <_ k )
109	102, 101, 108	lensymd 8069	. . . . . . . . . . . . 13 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ k e. NN ) -> -. k < 1 )
110	106, 109	pm2.21dd 620	. . . . . . . . . . . 12 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ k e. NN ) -> I = J )
111	93	ad3antrrr 492	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> ( -u N < ( I - J ) /\ ( I - J ) < N ) )
112	111	simpld 112	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> -u N < ( I - J ) )
113		simplr 528	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> ( N x. k ) = ( I - J ) )
114	112, 113	breqtrrd 4028	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> -u N < ( N x. k ) )
115	11	nnzd 9363	. . . . . . . . . . . . . . . . . . . 20 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> N e. ZZ )
116	115	adantr 276	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) -> N e. ZZ )
117		simpr 110	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) -> k e. ZZ )
118	116, 117	zmulcld 9370	. . . . . . . . . . . . . . . . . 18 |- ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) -> ( N x. k ) e. ZZ )
119	118	zred 9364	. . . . . . . . . . . . . . . . 17 |- ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) -> ( N x. k ) e. RR )
120	119	ad2antrr 488	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> ( N x. k ) e. RR )
121	11	nnred 8921	. . . . . . . . . . . . . . . . 17 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> N e. RR )
122	121	ad3antrrr 492	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> N e. RR )
123	120, 122	possumd 8516	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> ( 0 < ( ( N x. k ) + N ) <-> -u N < ( N x. k ) ) )
124	114, 123	mpbird 167	. . . . . . . . . . . . . 14 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> 0 < ( ( N x. k ) + N ) )
125	97	eqcomd 2183	. . . . . . . . . . . . . . . . 17 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> N = ( N x. 1 ) )
126	125	oveq2d 5885	. . . . . . . . . . . . . . . 16 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( N x. k ) + N ) = ( ( N x. k ) + ( N x. 1 ) ) )
127	126	ad3antrrr 492	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> ( ( N x. k ) + N ) = ( ( N x. k ) + ( N x. 1 ) ) )
128	71	ad3antrrr 492	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> N e. CC )
129	117	zcnd 9365	. . . . . . . . . . . . . . . . 17 |- ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) -> k e. CC )
130	129	ad2antrr 488	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> k e. CC )
131		1cnd 7964	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> 1 e. CC )
132	128, 130, 131	adddid 7972	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> ( N x. ( k + 1 ) ) = ( ( N x. k ) + ( N x. 1 ) ) )
133	127, 132	eqtr4d 2213	. . . . . . . . . . . . . 14 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> ( ( N x. k ) + N ) = ( N x. ( k + 1 ) ) )
134	124, 133	breqtrd 4026	. . . . . . . . . . . . 13 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> 0 < ( N x. ( k + 1 ) ) )
135	117	peano2zd 9367	. . . . . . . . . . . . . . . . 17 |- ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) -> ( k + 1 ) e. ZZ )
136	116, 135	zmulcld 9370	. . . . . . . . . . . . . . . 16 |- ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) -> ( N x. ( k + 1 ) ) e. ZZ )
137	136	zred 9364	. . . . . . . . . . . . . . 15 |- ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) -> ( N x. ( k + 1 ) ) e. RR )
138	137	ad2antrr 488	. . . . . . . . . . . . . 14 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> ( N x. ( k + 1 ) ) e. RR )
139		0red 7949	. . . . . . . . . . . . . 14 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> 0 e. RR )
140	71	adantr 276	. . . . . . . . . . . . . . . . 17 |- ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) -> N e. CC )
141	135	zcnd 9365	. . . . . . . . . . . . . . . . 17 |- ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) -> ( k + 1 ) e. CC )
142	140, 141	mulcomd 7969	. . . . . . . . . . . . . . . 16 |- ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) -> ( N x. ( k + 1 ) ) = ( ( k + 1 ) x. N ) )
143	142	ad2antrr 488	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> ( N x. ( k + 1 ) ) = ( ( k + 1 ) x. N ) )
144	135	zred 9364	. . . . . . . . . . . . . . . . 17 |- ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) -> ( k + 1 ) e. RR )
145	144	ad2antrr 488	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> ( k + 1 ) e. RR )
146		zcn 9247	. . . . . . . . . . . . . . . . . . . 20 |- ( k e. ZZ -> k e. CC )
147		1cnd 7964	. . . . . . . . . . . . . . . . . . . 20 |- ( k e. ZZ -> 1 e. CC )
148	146, 147	addcomd 8098	. . . . . . . . . . . . . . . . . . 19 |- ( k e. ZZ -> ( k + 1 ) = ( 1 + k ) )
149	147, 146	subnegd 8265	. . . . . . . . . . . . . . . . . . 19 |- ( k e. ZZ -> ( 1 - -u k ) = ( 1 + k ) )
150	148, 149	eqtr4d 2213	. . . . . . . . . . . . . . . . . 18 |- ( k e. ZZ -> ( k + 1 ) = ( 1 - -u k ) )
151	150	ad3antlr 493	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> ( k + 1 ) = ( 1 - -u k ) )
152		simpr 110	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> -u k e. NN )
153	152	nnge1d 8951	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> 1 <_ -u k )
154		1red 7963	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> 1 e. RR )
155	152	nnred 8921	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> -u k e. RR )
156	154, 155	suble0d 8483	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> ( ( 1 - -u k ) <_ 0 <-> 1 <_ -u k ) )
157	153, 156	mpbird 167	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> ( 1 - -u k ) <_ 0 )
158	151, 157	eqbrtrd 4022	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> ( k + 1 ) <_ 0 )
159	11	nnnn0d 9218	. . . . . . . . . . . . . . . . . 18 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> N e. NN0 )
160	159	nn0ge0d 9221	. . . . . . . . . . . . . . . . 17 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> 0 <_ N )
161	160	ad3antrrr 492	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> 0 <_ N )
162		mulle0r 8890	. . . . . . . . . . . . . . . 16 |- ( ( ( ( k + 1 ) e. RR /\ N e. RR ) /\ ( ( k + 1 ) <_ 0 /\ 0 <_ N ) ) -> ( ( k + 1 ) x. N ) <_ 0 )
163	145, 122, 158, 161, 162	syl22anc 1239	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> ( ( k + 1 ) x. N ) <_ 0 )
164	143, 163	eqbrtrd 4022	. . . . . . . . . . . . . 14 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> ( N x. ( k + 1 ) ) <_ 0 )
165	138, 139, 164	lensymd 8069	. . . . . . . . . . . . 13 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> -. 0 < ( N x. ( k + 1 ) ) )
166	134, 165	pm2.21dd 620	. . . . . . . . . . . 12 |- ( ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) /\ -u k e. NN ) -> I = J )
167		elz 9244	. . . . . . . . . . . . . 14 |- ( k e. ZZ <-> ( k e. RR /\ ( k = 0 \/ k e. NN \/ -u k e. NN ) ) )
168	167	simprbi 275	. . . . . . . . . . . . 13 |- ( k e. ZZ -> ( k = 0 \/ k e. NN \/ -u k e. NN ) )
169	168	ad2antlr 489	. . . . . . . . . . . 12 |- ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) -> ( k = 0 \/ k e. NN \/ -u k e. NN ) )
170	91, 110, 166, 169	mpjao3dan 1307	. . . . . . . . . . 11 |- ( ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) /\ ( N x. k ) = ( I - J ) ) -> I = J )
171	170	ex 115	. . . . . . . . . 10 |- ( ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) /\ k e. ZZ ) -> ( ( N x. k ) = ( I - J ) -> I = J ) )
172	171	rexlimdva 2594	. . . . . . . . 9 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( E. k e. ZZ ( N x. k ) = ( I - J ) -> I = J ) )
173	68, 172	sylbird 170	. . . . . . . 8 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( ( I - J ) / N ) e. ZZ -> I = J ) )
174	65, 173	sylbid 150	. . . . . . 7 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( ( I - J ) mod N ) = 0 -> I = J ) )
175	61, 174	sylbid 150	. . . . . 6 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( ( ( I mod N ) - ( J mod N ) ) mod N ) = 0 -> I = J ) )
176	54, 175	sylbid 150	. . . . 5 |- ( ( 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 ) )
177	37, 176	syl5 32	. . . 4 |- ( ( 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 ) )
178	36, 177	sylbird 170	. . 3 |- ( ( 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 ) )
179	25, 178	sylbid 150	. 2 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( ( I + S ) mod N ) = ( ( J + S ) mod N ) -> I = J ) )
180		oveq1 5876	. . 3 |- ( I = J -> ( I + S ) = ( J + S ) )
181	180	oveq1d 5884	. 2 |- ( I = J -> ( ( I + S ) mod N ) = ( ( J + S ) mod N ) )
182	179, 181	impbid1 142	1 |- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( ( I + S ) mod N ) = ( ( J + S ) mod N ) <-> I = J ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   \/ w3o 977   /\ w3a 978   = wceq 1353   e. wcel 2148   E.wrex 2456   class class class wbr 4000  (class class class)co 5869   CCcc 7800   RRcr 7801   0cc0 7802   1c1 7803   + caddc 7805   x. cmul 7807   < clt 7982   <_ cle 7983   - cmin 8118   -ucneg 8119   / cdiv 8618   NNcn 8908   NN0cn0 9165   ZZcz 9242   QQcq 9608   RR+crp 9640  ..^cfzo 10128   mod cmo 10308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-cnex 7893  ax-resscn 7894  ax-1cn 7895  ax-1re 7896  ax-icn 7897  ax-addcl 7898  ax-addrcl 7899  ax-mulcl 7900  ax-mulrcl 7901  ax-addcom 7902  ax-mulcom 7903  ax-addass 7904  ax-mulass 7905  ax-distr 7906  ax-i2m1 7907  ax-0lt1 7908  ax-1rid 7909  ax-0id 7910  ax-rnegex 7911  ax-precex 7912  ax-cnre 7913  ax-pre-ltirr 7914  ax-pre-ltwlin 7915  ax-pre-lttrn 7916  ax-pre-apti 7917  ax-pre-ltadd 7918  ax-pre-mulgt0 7919  ax-pre-mulext 7920  ax-arch 7921

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-id 4290  df-po 4293  df-iso 4294  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-fv 5220  df-riota 5825  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1st 6135  df-2nd 6136  df-pnf 7984  df-mnf 7985  df-xr 7986  df-ltxr 7987  df-le 7988  df-sub 8120  df-neg 8121  df-reap 8522  df-ap 8529  df-div 8619  df-inn 8909  df-n0 9166  df-z 9243  df-uz 9518  df-q 9609  df-rp 9641  df-fz 9996  df-fzo 10129  df-fl 10256  df-mod 10309

This theorem is referenced by: (None)