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 ..^ 𝑁 ) ∖ { 𝐽 } ) )