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