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