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 ( ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) → ( ( 𝐾 + 𝐽 ) mod 𝑁 ) ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) )

Proof

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