Metamath Proof Explorer


Theorem modsumfzodifsn

Description: The sum of a number within a half-open range of positive integers is an element of the corresponding open range of nonnegative integers with one excluded integer modulo the excluded integer. (Contributed by AV, 19-Mar-2021)

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

Proof

Step Hyp Ref Expression
1 elfzo0
 |-  ( J e. ( 0 ..^ N ) <-> ( J e. NN0 /\ N e. NN /\ J < N ) )
2 elfzoelz
 |-  ( K e. ( 1 ..^ N ) -> K e. ZZ )
3 2 zred
 |-  ( K e. ( 1 ..^ N ) -> K e. RR )
4 nn0re
 |-  ( J e. NN0 -> J e. RR )
5 4 3ad2ant1
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> J e. RR )
6 readdcl
 |-  ( ( K e. RR /\ J e. RR ) -> ( K + J ) e. RR )
7 3 5 6 syl2anr
 |-  ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ K e. ( 1 ..^ N ) ) -> ( K + J ) e. RR )
8 nnrp
 |-  ( N e. NN -> N e. RR+ )
9 8 3ad2ant2
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> N e. RR+ )
10 9 adantr
 |-  ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ K e. ( 1 ..^ N ) ) -> N e. RR+ )
11 7 10 jca
 |-  ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ K e. ( 1 ..^ N ) ) -> ( ( K + J ) e. RR /\ N e. RR+ ) )
12 1 11 sylanb
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> ( ( K + J ) e. RR /\ N e. RR+ ) )
13 12 adantl
 |-  ( ( ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( K + J ) e. RR /\ N e. RR+ ) )
14 elfzo1
 |-  ( K e. ( 1 ..^ N ) <-> ( K e. NN /\ N e. NN /\ K < N ) )
15 nnnn0
 |-  ( K e. NN -> K e. NN0 )
16 15 3ad2ant1
 |-  ( ( K e. NN /\ N e. NN /\ K < N ) -> K e. NN0 )
17 14 16 sylbi
 |-  ( K e. ( 1 ..^ N ) -> K e. NN0 )
18 elfzonn0
 |-  ( J e. ( 0 ..^ N ) -> J e. NN0 )
19 nn0addcl
 |-  ( ( K e. NN0 /\ J e. NN0 ) -> ( K + J ) e. NN0 )
20 17 18 19 syl2anr
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> ( K + J ) e. NN0 )
21 20 adantl
 |-  ( ( ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( K + J ) e. NN0 )
22 21 nn0ge0d
 |-  ( ( ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> 0 <_ ( K + J ) )
23 simpl
 |-  ( ( ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( K + J ) < N )
24 modid
 |-  ( ( ( ( K + J ) e. RR /\ N e. RR+ ) /\ ( 0 <_ ( K + J ) /\ ( K + J ) < N ) ) -> ( ( K + J ) mod N ) = ( K + J ) )
25 13 22 23 24 syl12anc
 |-  ( ( ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( K + J ) mod N ) = ( K + J ) )
26 simp2
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> N e. NN )
27 1 26 sylbi
 |-  ( J e. ( 0 ..^ N ) -> N e. NN )
28 27 adantr
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> N e. NN )
29 28 adantl
 |-  ( ( ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> N e. NN )
30 elfzo0
 |-  ( ( K + J ) e. ( 0 ..^ N ) <-> ( ( K + J ) e. NN0 /\ N e. NN /\ ( K + J ) < N ) )
31 21 29 23 30 syl3anbrc
 |-  ( ( ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( K + J ) e. ( 0 ..^ N ) )
32 2 zcnd
 |-  ( K e. ( 1 ..^ N ) -> K e. CC )
33 32 adantl
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> K e. CC )
34 0cnd
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> 0 e. CC )
35 elfzoelz
 |-  ( J e. ( 0 ..^ N ) -> J e. ZZ )
36 35 zcnd
 |-  ( J e. ( 0 ..^ N ) -> J e. CC )
37 36 adantr
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> J e. CC )
38 nnne0
 |-  ( K e. NN -> K =/= 0 )
39 38 3ad2ant1
 |-  ( ( K e. NN /\ N e. NN /\ K < N ) -> K =/= 0 )
40 14 39 sylbi
 |-  ( K e. ( 1 ..^ N ) -> K =/= 0 )
41 40 adantl
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> K =/= 0 )
42 33 34 37 41 addneintr2d
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> ( K + J ) =/= ( 0 + J ) )
43 42 adantl
 |-  ( ( ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( K + J ) =/= ( 0 + J ) )
44 37 adantl
 |-  ( ( ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> J e. CC )
45 addid2
 |-  ( J e. CC -> ( 0 + J ) = J )
46 45 eqcomd
 |-  ( J e. CC -> J = ( 0 + J ) )
47 44 46 syl
 |-  ( ( ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> J = ( 0 + J ) )
48 43 47 neeqtrrd
 |-  ( ( ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( K + J ) =/= J )
49 eldifsn
 |-  ( ( K + J ) e. ( ( 0 ..^ N ) \ { J } ) <-> ( ( K + J ) e. ( 0 ..^ N ) /\ ( K + J ) =/= J ) )
50 31 48 49 sylanbrc
 |-  ( ( ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( K + J ) e. ( ( 0 ..^ N ) \ { J } ) )
51 25 50 eqeltrd
 |-  ( ( ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( K + J ) mod N ) e. ( ( 0 ..^ N ) \ { J } ) )
52 elfzoel2
 |-  ( J e. ( 0 ..^ N ) -> N e. ZZ )
53 52 zcnd
 |-  ( J e. ( 0 ..^ N ) -> N e. CC )
54 53 adantr
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> N e. CC )
55 54 adantl
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> N e. CC )
56 55 mulm1d
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( -u 1 x. N ) = -u N )
57 56 oveq2d
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( K + J ) + ( -u 1 x. N ) ) = ( ( K + J ) + -u N ) )
58 zaddcl
 |-  ( ( K e. ZZ /\ J e. ZZ ) -> ( K + J ) e. ZZ )
59 2 35 58 syl2anr
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> ( K + J ) e. ZZ )
60 59 zcnd
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> ( K + J ) e. CC )
61 60 54 jca
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> ( ( K + J ) e. CC /\ N e. CC ) )
62 61 adantl
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( K + J ) e. CC /\ N e. CC ) )
63 negsub
 |-  ( ( ( K + J ) e. CC /\ N e. CC ) -> ( ( K + J ) + -u N ) = ( ( K + J ) - N ) )
64 62 63 syl
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( K + J ) + -u N ) = ( ( K + J ) - N ) )
65 57 64 eqtrd
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( K + J ) + ( -u 1 x. N ) ) = ( ( K + J ) - N ) )
66 65 oveq1d
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( ( K + J ) + ( -u 1 x. N ) ) mod N ) = ( ( ( K + J ) - N ) mod N ) )
67 2 35 58 syl2an
 |-  ( ( K e. ( 1 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( K + J ) e. ZZ )
68 67 zred
 |-  ( ( K e. ( 1 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( K + J ) e. RR )
69 68 ancoms
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> ( K + J ) e. RR )
70 52 zred
 |-  ( J e. ( 0 ..^ N ) -> N e. RR )
71 70 adantr
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> N e. RR )
72 69 71 resubcld
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> ( ( K + J ) - N ) e. RR )
73 72 adantl
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( K + J ) - N ) e. RR )
74 26 nnrpd
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> N e. RR+ )
75 1 74 sylbi
 |-  ( J e. ( 0 ..^ N ) -> N e. RR+ )
76 75 adantr
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> N e. RR+ )
77 76 adantl
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> N e. RR+ )
78 nnre
 |-  ( K e. NN -> K e. RR )
79 78 3ad2ant1
 |-  ( ( K e. NN /\ N e. NN /\ K < N ) -> K e. RR )
80 79 adantl
 |-  ( ( ( J e. NN0 /\ J < N ) /\ ( K e. NN /\ N e. NN /\ K < N ) ) -> K e. RR )
81 4 adantr
 |-  ( ( J e. NN0 /\ J < N ) -> J e. RR )
82 81 adantr
 |-  ( ( ( J e. NN0 /\ J < N ) /\ ( K e. NN /\ N e. NN /\ K < N ) ) -> J e. RR )
83 nnre
 |-  ( N e. NN -> N e. RR )
84 83 3ad2ant2
 |-  ( ( K e. NN /\ N e. NN /\ K < N ) -> N e. RR )
85 84 adantl
 |-  ( ( ( J e. NN0 /\ J < N ) /\ ( K e. NN /\ N e. NN /\ K < N ) ) -> N e. RR )
86 simp3
 |-  ( ( K e. RR /\ J e. RR /\ N e. RR ) -> N e. RR )
87 6 3adant3
 |-  ( ( K e. RR /\ J e. RR /\ N e. RR ) -> ( K + J ) e. RR )
88 86 87 lenltd
 |-  ( ( K e. RR /\ J e. RR /\ N e. RR ) -> ( N <_ ( K + J ) <-> -. ( K + J ) < N ) )
89 88 biimprd
 |-  ( ( K e. RR /\ J e. RR /\ N e. RR ) -> ( -. ( K + J ) < N -> N <_ ( K + J ) ) )
90 87 86 subge0d
 |-  ( ( K e. RR /\ J e. RR /\ N e. RR ) -> ( 0 <_ ( ( K + J ) - N ) <-> N <_ ( K + J ) ) )
91 89 90 sylibrd
 |-  ( ( K e. RR /\ J e. RR /\ N e. RR ) -> ( -. ( K + J ) < N -> 0 <_ ( ( K + J ) - N ) ) )
92 80 82 85 91 syl3anc
 |-  ( ( ( J e. NN0 /\ J < N ) /\ ( K e. NN /\ N e. NN /\ K < N ) ) -> ( -. ( K + J ) < N -> 0 <_ ( ( K + J ) - N ) ) )
93 81 79 anim12ci
 |-  ( ( ( J e. NN0 /\ J < N ) /\ ( K e. NN /\ N e. NN /\ K < N ) ) -> ( K e. RR /\ J e. RR ) )
94 83 83 jca
 |-  ( N e. NN -> ( N e. RR /\ N e. RR ) )
95 94 3ad2ant2
 |-  ( ( K e. NN /\ N e. NN /\ K < N ) -> ( N e. RR /\ N e. RR ) )
96 95 adantl
 |-  ( ( ( J e. NN0 /\ J < N ) /\ ( K e. NN /\ N e. NN /\ K < N ) ) -> ( N e. RR /\ N e. RR ) )
97 simpr
 |-  ( ( J e. NN0 /\ J < N ) -> J < N )
98 simp3
 |-  ( ( K e. NN /\ N e. NN /\ K < N ) -> K < N )
99 97 98 anim12ci
 |-  ( ( ( J e. NN0 /\ J < N ) /\ ( K e. NN /\ N e. NN /\ K < N ) ) -> ( K < N /\ J < N ) )
100 93 96 99 jca31
 |-  ( ( ( J e. NN0 /\ J < N ) /\ ( K e. NN /\ N e. NN /\ K < N ) ) -> ( ( ( K e. RR /\ J e. RR ) /\ ( N e. RR /\ N e. RR ) ) /\ ( K < N /\ J < N ) ) )
101 lt2add
 |-  ( ( ( K e. RR /\ J e. RR ) /\ ( N e. RR /\ N e. RR ) ) -> ( ( K < N /\ J < N ) -> ( K + J ) < ( N + N ) ) )
102 101 imp
 |-  ( ( ( ( K e. RR /\ J e. RR ) /\ ( N e. RR /\ N e. RR ) ) /\ ( K < N /\ J < N ) ) -> ( K + J ) < ( N + N ) )
103 100 102 syl
 |-  ( ( ( J e. NN0 /\ J < N ) /\ ( K e. NN /\ N e. NN /\ K < N ) ) -> ( K + J ) < ( N + N ) )
104 79 81 6 syl2anr
 |-  ( ( ( J e. NN0 /\ J < N ) /\ ( K e. NN /\ N e. NN /\ K < N ) ) -> ( K + J ) e. RR )
105 ltsubadd
 |-  ( ( ( K + J ) e. RR /\ N e. RR /\ N e. RR ) -> ( ( ( K + J ) - N ) < N <-> ( K + J ) < ( N + N ) ) )
106 104 85 85 105 syl3anc
 |-  ( ( ( J e. NN0 /\ J < N ) /\ ( K e. NN /\ N e. NN /\ K < N ) ) -> ( ( ( K + J ) - N ) < N <-> ( K + J ) < ( N + N ) ) )
107 103 106 mpbird
 |-  ( ( ( J e. NN0 /\ J < N ) /\ ( K e. NN /\ N e. NN /\ K < N ) ) -> ( ( K + J ) - N ) < N )
108 92 107 jctird
 |-  ( ( ( J e. NN0 /\ J < N ) /\ ( K e. NN /\ N e. NN /\ K < N ) ) -> ( -. ( K + J ) < N -> ( 0 <_ ( ( K + J ) - N ) /\ ( ( K + J ) - N ) < N ) ) )
109 108 ex
 |-  ( ( J e. NN0 /\ J < N ) -> ( ( K e. NN /\ N e. NN /\ K < N ) -> ( -. ( K + J ) < N -> ( 0 <_ ( ( K + J ) - N ) /\ ( ( K + J ) - N ) < N ) ) ) )
110 14 109 syl5bi
 |-  ( ( J e. NN0 /\ J < N ) -> ( K e. ( 1 ..^ N ) -> ( -. ( K + J ) < N -> ( 0 <_ ( ( K + J ) - N ) /\ ( ( K + J ) - N ) < N ) ) ) )
111 110 3adant2
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( K e. ( 1 ..^ N ) -> ( -. ( K + J ) < N -> ( 0 <_ ( ( K + J ) - N ) /\ ( ( K + J ) - N ) < N ) ) ) )
112 1 111 sylbi
 |-  ( J e. ( 0 ..^ N ) -> ( K e. ( 1 ..^ N ) -> ( -. ( K + J ) < N -> ( 0 <_ ( ( K + J ) - N ) /\ ( ( K + J ) - N ) < N ) ) ) )
113 112 imp
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> ( -. ( K + J ) < N -> ( 0 <_ ( ( K + J ) - N ) /\ ( ( K + J ) - N ) < N ) ) )
114 113 impcom
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( 0 <_ ( ( K + J ) - N ) /\ ( ( K + J ) - N ) < N ) )
115 73 77 114 jca31
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( ( ( K + J ) - N ) e. RR /\ N e. RR+ ) /\ ( 0 <_ ( ( K + J ) - N ) /\ ( ( K + J ) - N ) < N ) ) )
116 modid
 |-  ( ( ( ( ( K + J ) - N ) e. RR /\ N e. RR+ ) /\ ( 0 <_ ( ( K + J ) - N ) /\ ( ( K + J ) - N ) < N ) ) -> ( ( ( K + J ) - N ) mod N ) = ( ( K + J ) - N ) )
117 115 116 syl
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( ( K + J ) - N ) mod N ) = ( ( K + J ) - N ) )
118 66 117 eqtrd
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( ( K + J ) + ( -u 1 x. N ) ) mod N ) = ( ( K + J ) - N ) )
119 118 eqcomd
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( K + J ) - N ) = ( ( ( K + J ) + ( -u 1 x. N ) ) mod N ) )
120 1 9 sylbi
 |-  ( J e. ( 0 ..^ N ) -> N e. RR+ )
121 120 adantr
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> N e. RR+ )
122 neg1z
 |-  -u 1 e. ZZ
123 122 a1i
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> -u 1 e. ZZ )
124 modcyc
 |-  ( ( ( K + J ) e. RR /\ N e. RR+ /\ -u 1 e. ZZ ) -> ( ( ( K + J ) + ( -u 1 x. N ) ) mod N ) = ( ( K + J ) mod N ) )
125 69 121 123 124 syl2an23an
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( ( K + J ) + ( -u 1 x. N ) ) mod N ) = ( ( K + J ) mod N ) )
126 119 125 eqtrd
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( K + J ) - N ) = ( ( K + J ) mod N ) )
127 126 eqcomd
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( K + J ) mod N ) = ( ( K + J ) - N ) )
128 52 adantr
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> N e. ZZ )
129 59 128 zsubcld
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> ( ( K + J ) - N ) e. ZZ )
130 129 adantl
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( K + J ) - N ) e. ZZ )
131 3 adantl
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> K e. RR )
132 35 zred
 |-  ( J e. ( 0 ..^ N ) -> J e. RR )
133 132 adantr
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> J e. RR )
134 90 biimprd
 |-  ( ( K e. RR /\ J e. RR /\ N e. RR ) -> ( N <_ ( K + J ) -> 0 <_ ( ( K + J ) - N ) ) )
135 88 134 sylbird
 |-  ( ( K e. RR /\ J e. RR /\ N e. RR ) -> ( -. ( K + J ) < N -> 0 <_ ( ( K + J ) - N ) ) )
136 131 133 71 135 syl3anc
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> ( -. ( K + J ) < N -> 0 <_ ( ( K + J ) - N ) ) )
137 136 impcom
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> 0 <_ ( ( K + J ) - N ) )
138 elnn0z
 |-  ( ( ( K + J ) - N ) e. NN0 <-> ( ( ( K + J ) - N ) e. ZZ /\ 0 <_ ( ( K + J ) - N ) ) )
139 130 137 138 sylanbrc
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( K + J ) - N ) e. NN0 )
140 28 adantl
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> N e. NN )
141 100 expcom
 |-  ( ( K e. NN /\ N e. NN /\ K < N ) -> ( ( J e. NN0 /\ J < N ) -> ( ( ( K e. RR /\ J e. RR ) /\ ( N e. RR /\ N e. RR ) ) /\ ( K < N /\ J < N ) ) ) )
142 14 141 sylbi
 |-  ( K e. ( 1 ..^ N ) -> ( ( J e. NN0 /\ J < N ) -> ( ( ( K e. RR /\ J e. RR ) /\ ( N e. RR /\ N e. RR ) ) /\ ( K < N /\ J < N ) ) ) )
143 142 com12
 |-  ( ( J e. NN0 /\ J < N ) -> ( K e. ( 1 ..^ N ) -> ( ( ( K e. RR /\ J e. RR ) /\ ( N e. RR /\ N e. RR ) ) /\ ( K < N /\ J < N ) ) ) )
144 143 3adant2
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( K e. ( 1 ..^ N ) -> ( ( ( K e. RR /\ J e. RR ) /\ ( N e. RR /\ N e. RR ) ) /\ ( K < N /\ J < N ) ) ) )
145 1 144 sylbi
 |-  ( J e. ( 0 ..^ N ) -> ( K e. ( 1 ..^ N ) -> ( ( ( K e. RR /\ J e. RR ) /\ ( N e. RR /\ N e. RR ) ) /\ ( K < N /\ J < N ) ) ) )
146 145 imp
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> ( ( ( K e. RR /\ J e. RR ) /\ ( N e. RR /\ N e. RR ) ) /\ ( K < N /\ J < N ) ) )
147 146 102 syl
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> ( K + J ) < ( N + N ) )
148 4 adantr
 |-  ( ( J e. NN0 /\ N e. NN ) -> J e. RR )
149 3 148 6 syl2anr
 |-  ( ( ( J e. NN0 /\ N e. NN ) /\ K e. ( 1 ..^ N ) ) -> ( K + J ) e. RR )
150 83 adantl
 |-  ( ( J e. NN0 /\ N e. NN ) -> N e. RR )
151 150 adantr
 |-  ( ( ( J e. NN0 /\ N e. NN ) /\ K e. ( 1 ..^ N ) ) -> N e. RR )
152 149 151 151 3jca
 |-  ( ( ( J e. NN0 /\ N e. NN ) /\ K e. ( 1 ..^ N ) ) -> ( ( K + J ) e. RR /\ N e. RR /\ N e. RR ) )
153 152 ex
 |-  ( ( J e. NN0 /\ N e. NN ) -> ( K e. ( 1 ..^ N ) -> ( ( K + J ) e. RR /\ N e. RR /\ N e. RR ) ) )
154 153 3adant3
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( K e. ( 1 ..^ N ) -> ( ( K + J ) e. RR /\ N e. RR /\ N e. RR ) ) )
155 1 154 sylbi
 |-  ( J e. ( 0 ..^ N ) -> ( K e. ( 1 ..^ N ) -> ( ( K + J ) e. RR /\ N e. RR /\ N e. RR ) ) )
156 155 imp
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> ( ( K + J ) e. RR /\ N e. RR /\ N e. RR ) )
157 156 105 syl
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> ( ( ( K + J ) - N ) < N <-> ( K + J ) < ( N + N ) ) )
158 147 157 mpbird
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> ( ( K + J ) - N ) < N )
159 158 adantl
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( K + J ) - N ) < N )
160 elfzo0
 |-  ( ( ( K + J ) - N ) e. ( 0 ..^ N ) <-> ( ( ( K + J ) - N ) e. NN0 /\ N e. NN /\ ( ( K + J ) - N ) < N ) )
161 139 140 159 160 syl3anbrc
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( K + J ) - N ) e. ( 0 ..^ N ) )
162 nncn
 |-  ( K e. NN -> K e. CC )
163 nncn
 |-  ( N e. NN -> N e. CC )
164 subcl
 |-  ( ( K e. CC /\ N e. CC ) -> ( K - N ) e. CC )
165 162 163 164 syl2an
 |-  ( ( K e. NN /\ N e. NN ) -> ( K - N ) e. CC )
166 165 3adant3
 |-  ( ( K e. NN /\ N e. NN /\ K < N ) -> ( K - N ) e. CC )
167 14 166 sylbi
 |-  ( K e. ( 1 ..^ N ) -> ( K - N ) e. CC )
168 167 adantl
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> ( K - N ) e. CC )
169 168 adantl
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( K - N ) e. CC )
170 0cnd
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> 0 e. CC )
171 37 adantl
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> J e. CC )
172 elfzoel2
 |-  ( K e. ( 1 ..^ N ) -> N e. ZZ )
173 172 zcnd
 |-  ( K e. ( 1 ..^ N ) -> N e. CC )
174 79 98 ltned
 |-  ( ( K e. NN /\ N e. NN /\ K < N ) -> K =/= N )
175 14 174 sylbi
 |-  ( K e. ( 1 ..^ N ) -> K =/= N )
176 32 173 175 subne0d
 |-  ( K e. ( 1 ..^ N ) -> ( K - N ) =/= 0 )
177 176 adantl
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> ( K - N ) =/= 0 )
178 177 adantl
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( K - N ) =/= 0 )
179 169 170 171 178 addneintr2d
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( K - N ) + J ) =/= ( 0 + J ) )
180 33 37 54 3jca
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> ( K e. CC /\ J e. CC /\ N e. CC ) )
181 180 adantl
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( K e. CC /\ J e. CC /\ N e. CC ) )
182 addsub
 |-  ( ( K e. CC /\ J e. CC /\ N e. CC ) -> ( ( K + J ) - N ) = ( ( K - N ) + J ) )
183 181 182 syl
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( K + J ) - N ) = ( ( K - N ) + J ) )
184 171 45 syl
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( 0 + J ) = J )
185 184 eqcomd
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> J = ( 0 + J ) )
186 179 183 185 3netr4d
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( K + J ) - N ) =/= J )
187 eldifsn
 |-  ( ( ( K + J ) - N ) e. ( ( 0 ..^ N ) \ { J } ) <-> ( ( ( K + J ) - N ) e. ( 0 ..^ N ) /\ ( ( K + J ) - N ) =/= J ) )
188 161 186 187 sylanbrc
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( K + J ) - N ) e. ( ( 0 ..^ N ) \ { J } ) )
189 127 188 eqeltrd
 |-  ( ( -. ( K + J ) < N /\ ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) ) -> ( ( K + J ) mod N ) e. ( ( 0 ..^ N ) \ { J } ) )
190 51 189 pm2.61ian
 |-  ( ( J e. ( 0 ..^ N ) /\ K e. ( 1 ..^ N ) ) -> ( ( K + J ) mod N ) e. ( ( 0 ..^ N ) \ { J } ) )