Metamath Proof Explorer

Theorem modfzo0difsn

Description: For a number within a half-open range of nonnegative integers with one excluded integer there is a positive integer so that the number is equal to the sum of the positive integer and the excluded integer modulo the upper bound of the range. (Contributed by AV, 19-Mar-2021)

Ref Expression
Assertion modfzo0difsn 
|- ( ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) -> E. i e. ( 1 ..^ N ) K = ( ( i + J ) mod N ) )

Proof

Step Hyp Ref Expression
1 eldifi 
 |-  ( K e. ( ( 0 ..^ N ) \ { J } ) -> K e. ( 0 ..^ N ) )
2 elfzoelz 
 |-  ( K e. ( 0 ..^ N ) -> K e. ZZ )
3 2 zred 
 |-  ( K e. ( 0 ..^ N ) -> K e. RR )
4 1 3 syl 
 |-  ( K e. ( ( 0 ..^ N ) \ { J } ) -> K e. RR )
5 elfzoelz 
 |-  ( J e. ( 0 ..^ N ) -> J e. ZZ )
6 5 zred 
 |-  ( J e. ( 0 ..^ N ) -> J e. RR )
7 leloe 
 |-  ( ( K e. RR /\ J e. RR ) -> ( K <_ J <-> ( K < J \/ K = J ) ) )
8 4 6 7 syl2anr 
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) -> ( K <_ J <-> ( K < J \/ K = J ) ) )
9 elfzo0 
 |-  ( K e. ( 0 ..^ N ) <-> ( K e. NN0 /\ N e. NN /\ K < N ) )
10 elfzo0 
 |-  ( J e. ( 0 ..^ N ) <-> ( J e. NN0 /\ N e. NN /\ J < N ) )
11 nn0cn 
 |-  ( K e. NN0 -> K e. CC )
12 11 adantr 
 |-  ( ( K e. NN0 /\ K < N ) -> K e. CC )
13 12 adantl 
 |-  ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ ( K e. NN0 /\ K < N ) ) -> K e. CC )
14 nn0cn 
 |-  ( J e. NN0 -> J e. CC )
15 14 3ad2ant1 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> J e. CC )
16 15 adantr 
 |-  ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ ( K e. NN0 /\ K < N ) ) -> J e. CC )
17 nncn 
 |-  ( N e. NN -> N e. CC )
18 17 3ad2ant2 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> N e. CC )
19 18 adantr 
 |-  ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ ( K e. NN0 /\ K < N ) ) -> N e. CC )
20 13 16 19 subadd23d 
 |-  ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ ( K e. NN0 /\ K < N ) ) -> ( ( K - J ) + N ) = ( K + ( N - J ) ) )
21 simpl 
 |-  ( ( K e. NN0 /\ K < N ) -> K e. NN0 )
22 nn0z 
 |-  ( J e. NN0 -> J e. ZZ )
23 nnz 
 |-  ( N e. NN -> N e. ZZ )
24 znnsub 
 |-  ( ( J e. ZZ /\ N e. ZZ ) -> ( J < N <-> ( N - J ) e. NN ) )
25 22 23 24 syl2an 
 |-  ( ( J e. NN0 /\ N e. NN ) -> ( J < N <-> ( N - J ) e. NN ) )
26 25 biimp3a 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( N - J ) e. NN )
27 nn0nnaddcl 
 |-  ( ( K e. NN0 /\ ( N - J ) e. NN ) -> ( K + ( N - J ) ) e. NN )
28 21 26 27 syl2anr 
 |-  ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ ( K e. NN0 /\ K < N ) ) -> ( K + ( N - J ) ) e. NN )
29 20 28 eqeltrd 
 |-  ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ ( K e. NN0 /\ K < N ) ) -> ( ( K - J ) + N ) e. NN )
30 29 adantr 
 |-  ( ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ ( K e. NN0 /\ K < N ) ) /\ K < J ) -> ( ( K - J ) + N ) e. NN )
31 simp2 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> N e. NN )
32 31 adantr 
 |-  ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ ( K e. NN0 /\ K < N ) ) -> N e. NN )
33 32 adantr 
 |-  ( ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ ( K e. NN0 /\ K < N ) ) /\ K < J ) -> N e. NN )
34 nn0re 
 |-  ( K e. NN0 -> K e. RR )
35 34 adantr 
 |-  ( ( K e. NN0 /\ K < N ) -> K e. RR )
36 35 adantl 
 |-  ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ ( K e. NN0 /\ K < N ) ) -> K e. RR )
37 nn0re 
 |-  ( J e. NN0 -> J e. RR )
38 37 3ad2ant1 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> J e. RR )
39 38 adantr 
 |-  ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ ( K e. NN0 /\ K < N ) ) -> J e. RR )
40 36 39 sublt0d 
 |-  ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ ( K e. NN0 /\ K < N ) ) -> ( ( K - J ) < 0 <-> K < J ) )
41 40 bicomd 
 |-  ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ ( K e. NN0 /\ K < N ) ) -> ( K < J <-> ( K - J ) < 0 ) )
42 41 biimpa 
 |-  ( ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ ( K e. NN0 /\ K < N ) ) /\ K < J ) -> ( K - J ) < 0 )
43 resubcl 
 |-  ( ( K e. RR /\ J e. RR ) -> ( K - J ) e. RR )
44 35 38 43 syl2anr 
 |-  ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ ( K e. NN0 /\ K < N ) ) -> ( K - J ) e. RR )
45 nnre 
 |-  ( N e. NN -> N e. RR )
46 45 3ad2ant2 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> N e. RR )
47 46 adantr 
 |-  ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ ( K e. NN0 /\ K < N ) ) -> N e. RR )
48 44 47 jca 
 |-  ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ ( K e. NN0 /\ K < N ) ) -> ( ( K - J ) e. RR /\ N e. RR ) )
49 48 adantr 
 |-  ( ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ ( K e. NN0 /\ K < N ) ) /\ K < J ) -> ( ( K - J ) e. RR /\ N e. RR ) )
50 ltaddnegr 
 |-  ( ( ( K - J ) e. RR /\ N e. RR ) -> ( ( K - J ) < 0 <-> ( ( K - J ) + N ) < N ) )
51 49 50 syl 
 |-  ( ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ ( K e. NN0 /\ K < N ) ) /\ K < J ) -> ( ( K - J ) < 0 <-> ( ( K - J ) + N ) < N ) )
52 42 51 mpbid 
 |-  ( ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ ( K e. NN0 /\ K < N ) ) /\ K < J ) -> ( ( K - J ) + N ) < N )
53 elfzo1 
 |-  ( ( ( K - J ) + N ) e. ( 1 ..^ N ) <-> ( ( ( K - J ) + N ) e. NN /\ N e. NN /\ ( ( K - J ) + N ) < N ) )
54 30 33 52 53 syl3anbrc 
 |-  ( ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ ( K e. NN0 /\ K < N ) ) /\ K < J ) -> ( ( K - J ) + N ) e. ( 1 ..^ N ) )
55 54 exp31 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( ( K e. NN0 /\ K < N ) -> ( K < J -> ( ( K - J ) + N ) e. ( 1 ..^ N ) ) ) )
56 10 55 sylbi 
 |-  ( J e. ( 0 ..^ N ) -> ( ( K e. NN0 /\ K < N ) -> ( K < J -> ( ( K - J ) + N ) e. ( 1 ..^ N ) ) ) )
57 56 com12 
 |-  ( ( K e. NN0 /\ K < N ) -> ( J e. ( 0 ..^ N ) -> ( K < J -> ( ( K - J ) + N ) e. ( 1 ..^ N ) ) ) )
58 57 3adant2 
 |-  ( ( K e. NN0 /\ N e. NN /\ K < N ) -> ( J e. ( 0 ..^ N ) -> ( K < J -> ( ( K - J ) + N ) e. ( 1 ..^ N ) ) ) )
59 9 58 sylbi 
 |-  ( K e. ( 0 ..^ N ) -> ( J e. ( 0 ..^ N ) -> ( K < J -> ( ( K - J ) + N ) e. ( 1 ..^ N ) ) ) )
60 1 59 syl 
 |-  ( K e. ( ( 0 ..^ N ) \ { J } ) -> ( J e. ( 0 ..^ N ) -> ( K < J -> ( ( K - J ) + N ) e. ( 1 ..^ N ) ) ) )
61 60 impcom 
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) -> ( K < J -> ( ( K - J ) + N ) e. ( 1 ..^ N ) ) )
62 61 impcom 
 |-  ( ( K < J /\ ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) ) -> ( ( K - J ) + N ) e. ( 1 ..^ N ) )
63 oveq1 
 |-  ( i = ( ( K - J ) + N ) -> ( i + J ) = ( ( ( K - J ) + N ) + J ) )
64 2 zcnd 
 |-  ( K e. ( 0 ..^ N ) -> K e. CC )
65 64 adantr 
 |-  ( ( K e. ( 0 ..^ N ) /\ ( J e. NN0 /\ N e. NN ) ) -> K e. CC )
66 14 adantr 
 |-  ( ( J e. NN0 /\ N e. NN ) -> J e. CC )
67 66 adantl 
 |-  ( ( K e. ( 0 ..^ N ) /\ ( J e. NN0 /\ N e. NN ) ) -> J e. CC )
68 17 adantl 
 |-  ( ( J e. NN0 /\ N e. NN ) -> N e. CC )
69 68 adantl 
 |-  ( ( K e. ( 0 ..^ N ) /\ ( J e. NN0 /\ N e. NN ) ) -> N e. CC )
70 65 67 69 3jca 
 |-  ( ( K e. ( 0 ..^ N ) /\ ( J e. NN0 /\ N e. NN ) ) -> ( K e. CC /\ J e. CC /\ N e. CC ) )
71 70 ex 
 |-  ( K e. ( 0 ..^ N ) -> ( ( J e. NN0 /\ N e. NN ) -> ( K e. CC /\ J e. CC /\ N e. CC ) ) )
72 1 71 syl 
 |-  ( K e. ( ( 0 ..^ N ) \ { J } ) -> ( ( J e. NN0 /\ N e. NN ) -> ( K e. CC /\ J e. CC /\ N e. CC ) ) )
73 72 com12 
 |-  ( ( J e. NN0 /\ N e. NN ) -> ( K e. ( ( 0 ..^ N ) \ { J } ) -> ( K e. CC /\ J e. CC /\ N e. CC ) ) )
74 73 3adant3 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( K e. ( ( 0 ..^ N ) \ { J } ) -> ( K e. CC /\ J e. CC /\ N e. CC ) ) )
75 10 74 sylbi 
 |-  ( J e. ( 0 ..^ N ) -> ( K e. ( ( 0 ..^ N ) \ { J } ) -> ( K e. CC /\ J e. CC /\ N e. CC ) ) )
76 75 imp 
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) -> ( K e. CC /\ J e. CC /\ N e. CC ) )
77 76 adantl 
 |-  ( ( K < J /\ ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) ) -> ( K e. CC /\ J e. CC /\ N e. CC ) )
78 nppcan 
 |-  ( ( K e. CC /\ J e. CC /\ N e. CC ) -> ( ( ( K - J ) + N ) + J ) = ( K + N ) )
79 77 78 syl 
 |-  ( ( K < J /\ ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) ) -> ( ( ( K - J ) + N ) + J ) = ( K + N ) )
80 63 79 sylan9eqr 
 |-  ( ( ( K < J /\ ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) ) /\ i = ( ( K - J ) + N ) ) -> ( i + J ) = ( K + N ) )
81 80 oveq1d 
 |-  ( ( ( K < J /\ ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) ) /\ i = ( ( K - J ) + N ) ) -> ( ( i + J ) mod N ) = ( ( K + N ) mod N ) )
82 81 eqeq2d 
 |-  ( ( ( K < J /\ ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) ) /\ i = ( ( K - J ) + N ) ) -> ( K = ( ( i + J ) mod N ) <-> K = ( ( K + N ) mod N ) ) )
83 9 biimpi 
 |-  ( K e. ( 0 ..^ N ) -> ( K e. NN0 /\ N e. NN /\ K < N ) )
84 83 a1d 
 |-  ( K e. ( 0 ..^ N ) -> ( J e. ( 0 ..^ N ) -> ( K e. NN0 /\ N e. NN /\ K < N ) ) )
85 1 84 syl 
 |-  ( K e. ( ( 0 ..^ N ) \ { J } ) -> ( J e. ( 0 ..^ N ) -> ( K e. NN0 /\ N e. NN /\ K < N ) ) )
86 85 impcom 
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) -> ( K e. NN0 /\ N e. NN /\ K < N ) )
87 86 adantl 
 |-  ( ( K < J /\ ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) ) -> ( K e. NN0 /\ N e. NN /\ K < N ) )
88 addmodidr 
 |-  ( ( K e. NN0 /\ N e. NN /\ K < N ) -> ( ( K + N ) mod N ) = K )
89 88 eqcomd 
 |-  ( ( K e. NN0 /\ N e. NN /\ K < N ) -> K = ( ( K + N ) mod N ) )
90 87 89 syl 
 |-  ( ( K < J /\ ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) ) -> K = ( ( K + N ) mod N ) )
91 62 82 90 rspcedvd 
 |-  ( ( K < J /\ ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) ) -> E. i e. ( 1 ..^ N ) K = ( ( i + J ) mod N ) )
92 91 ex 
 |-  ( K < J -> ( ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) -> E. i e. ( 1 ..^ N ) K = ( ( i + J ) mod N ) ) )
93 eldifsn 
 |-  ( K e. ( ( 0 ..^ N ) \ { J } ) <-> ( K e. ( 0 ..^ N ) /\ K =/= J ) )
94 eqneqall 
 |-  ( K = J -> ( K =/= J -> E. i e. ( 1 ..^ N ) K = ( ( i + J ) mod N ) ) )
95 94 com12 
 |-  ( K =/= J -> ( K = J -> E. i e. ( 1 ..^ N ) K = ( ( i + J ) mod N ) ) )
96 95 adantl 
 |-  ( ( K e. ( 0 ..^ N ) /\ K =/= J ) -> ( K = J -> E. i e. ( 1 ..^ N ) K = ( ( i + J ) mod N ) ) )
97 93 96 sylbi 
 |-  ( K e. ( ( 0 ..^ N ) \ { J } ) -> ( K = J -> E. i e. ( 1 ..^ N ) K = ( ( i + J ) mod N ) ) )
98 97 adantl 
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) -> ( K = J -> E. i e. ( 1 ..^ N ) K = ( ( i + J ) mod N ) ) )
99 98 com12 
 |-  ( K = J -> ( ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) -> E. i e. ( 1 ..^ N ) K = ( ( i + J ) mod N ) ) )
100 92 99 jaoi 
 |-  ( ( K < J \/ K = J ) -> ( ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) -> E. i e. ( 1 ..^ N ) K = ( ( i + J ) mod N ) ) )
101 100 com12 
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) -> ( ( K < J \/ K = J ) -> E. i e. ( 1 ..^ N ) K = ( ( i + J ) mod N ) ) )
102 8 101 sylbid 
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) -> ( K <_ J -> E. i e. ( 1 ..^ N ) K = ( ( i + J ) mod N ) ) )
103 102 com12 
 |-  ( K <_ J -> ( ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) -> E. i e. ( 1 ..^ N ) K = ( ( i + J ) mod N ) ) )
104 ltnle 
 |-  ( ( J e. RR /\ K e. RR ) -> ( J < K <-> -. K <_ J ) )
105 6 4 104 syl2an 
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) -> ( J < K <-> -. K <_ J ) )
106 105 bicomd 
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) -> ( -. K <_ J <-> J < K ) )
107 22 3ad2ant1 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> J e. ZZ )
108 nn0z 
 |-  ( K e. NN0 -> K e. ZZ )
109 108 adantr 
 |-  ( ( K e. NN0 /\ K < N ) -> K e. ZZ )
110 znnsub 
 |-  ( ( J e. ZZ /\ K e. ZZ ) -> ( J < K <-> ( K - J ) e. NN ) )
111 107 109 110 syl2anr 
 |-  ( ( ( K e. NN0 /\ K < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> ( J < K <-> ( K - J ) e. NN ) )
112 111 biimpa 
 |-  ( ( ( ( K e. NN0 /\ K < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) /\ J < K ) -> ( K - J ) e. NN )
113 31 adantl 
 |-  ( ( ( K e. NN0 /\ K < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> N e. NN )
114 113 adantr 
 |-  ( ( ( ( K e. NN0 /\ K < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) /\ J < K ) -> N e. NN )
115 nn0ge0 
 |-  ( J e. NN0 -> 0 <_ J )
116 115 3ad2ant1 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> 0 <_ J )
117 116 adantl 
 |-  ( ( K e. NN0 /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> 0 <_ J )
118 subge02 
 |-  ( ( K e. RR /\ J e. RR ) -> ( 0 <_ J <-> ( K - J ) <_ K ) )
119 34 38 118 syl2an 
 |-  ( ( K e. NN0 /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> ( 0 <_ J <-> ( K - J ) <_ K ) )
120 117 119 mpbid 
 |-  ( ( K e. NN0 /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> ( K - J ) <_ K )
121 38 adantl 
 |-  ( ( K e. NN0 /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> J e. RR )
122 34 adantr 
 |-  ( ( K e. NN0 /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> K e. RR )
123 46 adantl 
 |-  ( ( K e. NN0 /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> N e. RR )
124 121 122 123 3jca 
 |-  ( ( K e. NN0 /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> ( J e. RR /\ K e. RR /\ N e. RR ) )
125 43 ancoms 
 |-  ( ( J e. RR /\ K e. RR ) -> ( K - J ) e. RR )
126 125 3adant3 
 |-  ( ( J e. RR /\ K e. RR /\ N e. RR ) -> ( K - J ) e. RR )
127 simp2 
 |-  ( ( J e. RR /\ K e. RR /\ N e. RR ) -> K e. RR )
128 simp3 
 |-  ( ( J e. RR /\ K e. RR /\ N e. RR ) -> N e. RR )
129 126 127 128 3jca 
 |-  ( ( J e. RR /\ K e. RR /\ N e. RR ) -> ( ( K - J ) e. RR /\ K e. RR /\ N e. RR ) )
130 124 129 syl 
 |-  ( ( K e. NN0 /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> ( ( K - J ) e. RR /\ K e. RR /\ N e. RR ) )
131 lelttr 
 |-  ( ( ( K - J ) e. RR /\ K e. RR /\ N e. RR ) -> ( ( ( K - J ) <_ K /\ K < N ) -> ( K - J ) < N ) )
132 130 131 syl 
 |-  ( ( K e. NN0 /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> ( ( ( K - J ) <_ K /\ K < N ) -> ( K - J ) < N ) )
133 120 132 mpand 
 |-  ( ( K e. NN0 /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> ( K < N -> ( K - J ) < N ) )
134 133 impancom 
 |-  ( ( K e. NN0 /\ K < N ) -> ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( K - J ) < N ) )
135 134 imp 
 |-  ( ( ( K e. NN0 /\ K < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) -> ( K - J ) < N )
136 135 adantr 
 |-  ( ( ( ( K e. NN0 /\ K < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) /\ J < K ) -> ( K - J ) < N )
137 112 114 136 3jca 
 |-  ( ( ( ( K e. NN0 /\ K < N ) /\ ( J e. NN0 /\ N e. NN /\ J < N ) ) /\ J < K ) -> ( ( K - J ) e. NN /\ N e. NN /\ ( K - J ) < N ) )
138 137 exp31 
 |-  ( ( K e. NN0 /\ K < N ) -> ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( J < K -> ( ( K - J ) e. NN /\ N e. NN /\ ( K - J ) < N ) ) ) )
139 138 3adant2 
 |-  ( ( K e. NN0 /\ N e. NN /\ K < N ) -> ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( J < K -> ( ( K - J ) e. NN /\ N e. NN /\ ( K - J ) < N ) ) ) )
140 9 139 sylbi 
 |-  ( K e. ( 0 ..^ N ) -> ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( J < K -> ( ( K - J ) e. NN /\ N e. NN /\ ( K - J ) < N ) ) ) )
141 1 140 syl 
 |-  ( K e. ( ( 0 ..^ N ) \ { J } ) -> ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( J < K -> ( ( K - J ) e. NN /\ N e. NN /\ ( K - J ) < N ) ) ) )
142 141 com12 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( K e. ( ( 0 ..^ N ) \ { J } ) -> ( J < K -> ( ( K - J ) e. NN /\ N e. NN /\ ( K - J ) < N ) ) ) )
143 10 142 sylbi 
 |-  ( J e. ( 0 ..^ N ) -> ( K e. ( ( 0 ..^ N ) \ { J } ) -> ( J < K -> ( ( K - J ) e. NN /\ N e. NN /\ ( K - J ) < N ) ) ) )
144 143 imp 
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) -> ( J < K -> ( ( K - J ) e. NN /\ N e. NN /\ ( K - J ) < N ) ) )
145 106 144 sylbid 
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) -> ( -. K <_ J -> ( ( K - J ) e. NN /\ N e. NN /\ ( K - J ) < N ) ) )
146 145 impcom 
 |-  ( ( -. K <_ J /\ ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) ) -> ( ( K - J ) e. NN /\ N e. NN /\ ( K - J ) < N ) )
147 elfzo1 
 |-  ( ( K - J ) e. ( 1 ..^ N ) <-> ( ( K - J ) e. NN /\ N e. NN /\ ( K - J ) < N ) )
148 146 147 sylibr 
 |-  ( ( -. K <_ J /\ ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) ) -> ( K - J ) e. ( 1 ..^ N ) )
149 oveq1 
 |-  ( i = ( K - J ) -> ( i + J ) = ( ( K - J ) + J ) )
150 1 64 syl 
 |-  ( K e. ( ( 0 ..^ N ) \ { J } ) -> K e. CC )
151 5 zcnd 
 |-  ( J e. ( 0 ..^ N ) -> J e. CC )
152 npcan 
 |-  ( ( K e. CC /\ J e. CC ) -> ( ( K - J ) + J ) = K )
153 150 151 152 syl2anr 
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) -> ( ( K - J ) + J ) = K )
154 153 adantl 
 |-  ( ( -. K <_ J /\ ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) ) -> ( ( K - J ) + J ) = K )
155 149 154 sylan9eqr 
 |-  ( ( ( -. K <_ J /\ ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) ) /\ i = ( K - J ) ) -> ( i + J ) = K )
156 155 oveq1d 
 |-  ( ( ( -. K <_ J /\ ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) ) /\ i = ( K - J ) ) -> ( ( i + J ) mod N ) = ( K mod N ) )
157 156 eqeq2d 
 |-  ( ( ( -. K <_ J /\ ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) ) /\ i = ( K - J ) ) -> ( K = ( ( i + J ) mod N ) <-> K = ( K mod N ) ) )
158 zmodidfzoimp 
 |-  ( K e. ( 0 ..^ N ) -> ( K mod N ) = K )
159 1 158 syl 
 |-  ( K e. ( ( 0 ..^ N ) \ { J } ) -> ( K mod N ) = K )
160 159 adantl 
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) -> ( K mod N ) = K )
161 160 adantl 
 |-  ( ( -. K <_ J /\ ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) ) -> ( K mod N ) = K )
162 161 eqcomd 
 |-  ( ( -. K <_ J /\ ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) ) -> K = ( K mod N ) )
163 148 157 162 rspcedvd 
 |-  ( ( -. K <_ J /\ ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) ) -> E. i e. ( 1 ..^ N ) K = ( ( i + J ) mod N ) )
164 163 ex 
 |-  ( -. K <_ J -> ( ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) -> E. i e. ( 1 ..^ N ) K = ( ( i + J ) mod N ) ) )
165 103 164 pm2.61i 
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( ( 0 ..^ N ) \ { J } ) ) -> E. i e. ( 1 ..^ N ) K = ( ( i + J ) mod N ) )