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

Proof

Step Hyp Ref Expression
1 eldifi ⊢ ( 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) → 𝐾 ∈ ( 0 ..^ 𝑁 ) )
2 elfzoelz ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝐾 ∈ ℤ )
3 2 zred ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝐾 ∈ ℝ )
4 1 3 syl ⊢ ( 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) → 𝐾 ∈ ℝ )
5 elfzoelz ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ℤ )
6 5 zred ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ℝ )
7 leloe ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ ) → ( 𝐾 ≤ 𝐽 ↔ ( 𝐾 < 𝐽 ∨ 𝐾 = 𝐽 ) ) )
8 4 6 7 syl2anr ⊢ ( ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ( 𝐾 ≤ 𝐽 ↔ ( 𝐾 < 𝐽 ∨ 𝐾 = 𝐽 ) ) )
9 elfzo0 ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) )
10 elfzo0 ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) )
11 nn0cn ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℂ )
12 11 adantr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) → 𝐾 ∈ ℂ )
13 12 adantl ⊢ ( ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ) → 𝐾 ∈ ℂ )
14 nn0cn ⊢ ( 𝐽 ∈ ℕ0 → 𝐽 ∈ ℂ )
15 14 3ad2ant1 ⊢ ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) → 𝐽 ∈ ℂ )
16 15 adantr ⊢ ( ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ) → 𝐽 ∈ ℂ )
17 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
18 17 3ad2ant2 ⊢ ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) → 𝑁 ∈ ℂ )
19 18 adantr ⊢ ( ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ) → 𝑁 ∈ ℂ )
20 13 16 19 subadd23d ⊢ ( ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ) → ( ( 𝐾 − 𝐽 ) + 𝑁 ) = ( 𝐾 + ( 𝑁 − 𝐽 ) ) )
21 simpl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) → 𝐾 ∈ ℕ0 )
22 nn0z ⊢ ( 𝐽 ∈ ℕ0 → 𝐽 ∈ ℤ )
23 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
24 znnsub ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐽 < 𝑁 ↔ ( 𝑁 − 𝐽 ) ∈ ℕ ) )
25 22 23 24 syl2an ⊢ ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝐽 < 𝑁 ↔ ( 𝑁 − 𝐽 ) ∈ ℕ ) )
26 25 biimp3a ⊢ ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) → ( 𝑁 − 𝐽 ) ∈ ℕ )
27 nn0nnaddcl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 − 𝐽 ) ∈ ℕ ) → ( 𝐾 + ( 𝑁 − 𝐽 ) ) ∈ ℕ )
28 21 26 27 syl2anr ⊢ ( ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ) → ( 𝐾 + ( 𝑁 − 𝐽 ) ) ∈ ℕ )
29 20 28 eqeltrd ⊢ ( ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ) → ( ( 𝐾 − 𝐽 ) + 𝑁 ) ∈ ℕ )
30 29 adantr ⊢ ( ( ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ) ∧ 𝐾 < 𝐽 ) → ( ( 𝐾 − 𝐽 ) + 𝑁 ) ∈ ℕ )
31 simp2 ⊢ ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) → 𝑁 ∈ ℕ )
32 31 adantr ⊢ ( ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ) → 𝑁 ∈ ℕ )
33 32 adantr ⊢ ( ( ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ) ∧ 𝐾 < 𝐽 ) → 𝑁 ∈ ℕ )
34 nn0re ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℝ )
35 34 adantr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) → 𝐾 ∈ ℝ )
36 35 adantl ⊢ ( ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ) → 𝐾 ∈ ℝ )
37 nn0re ⊢ ( 𝐽 ∈ ℕ0 → 𝐽 ∈ ℝ )
38 37 3ad2ant1 ⊢ ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) → 𝐽 ∈ ℝ )
39 38 adantr ⊢ ( ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ) → 𝐽 ∈ ℝ )
40 36 39 sublt0d ⊢ ( ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ) → ( ( 𝐾 − 𝐽 ) < 0 ↔ 𝐾 < 𝐽 ) )
41 40 bicomd ⊢ ( ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ) → ( 𝐾 < 𝐽 ↔ ( 𝐾 − 𝐽 ) < 0 ) )
42 41 biimpa ⊢ ( ( ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ) ∧ 𝐾 < 𝐽 ) → ( 𝐾 − 𝐽 ) < 0 )
43 resubcl ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ ) → ( 𝐾 − 𝐽 ) ∈ ℝ )
44 35 38 43 syl2anr ⊢ ( ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ) → ( 𝐾 − 𝐽 ) ∈ ℝ )
45 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
46 45 3ad2ant2 ⊢ ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) → 𝑁 ∈ ℝ )
47 46 adantr ⊢ ( ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ) → 𝑁 ∈ ℝ )
48 44 47 jca ⊢ ( ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ) → ( ( 𝐾 − 𝐽 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
49 48 adantr ⊢ ( ( ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ) ∧ 𝐾 < 𝐽 ) → ( ( 𝐾 − 𝐽 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
50 ltaddnegr ⊢ ( ( ( 𝐾 − 𝐽 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝐾 − 𝐽 ) < 0 ↔ ( ( 𝐾 − 𝐽 ) + 𝑁 ) < 𝑁 ) )
51 49 50 syl ⊢ ( ( ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ) ∧ 𝐾 < 𝐽 ) → ( ( 𝐾 − 𝐽 ) < 0 ↔ ( ( 𝐾 − 𝐽 ) + 𝑁 ) < 𝑁 ) )
52 42 51 mpbid ⊢ ( ( ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ) ∧ 𝐾 < 𝐽 ) → ( ( 𝐾 − 𝐽 ) + 𝑁 ) < 𝑁 )
53 elfzo1 ⊢ ( ( ( 𝐾 − 𝐽 ) + 𝑁 ) ∈ ( 1 ..^ 𝑁 ) ↔ ( ( ( 𝐾 − 𝐽 ) + 𝑁 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( ( 𝐾 − 𝐽 ) + 𝑁 ) < 𝑁 ) )
54 30 33 52 53 syl3anbrc ⊢ ( ( ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ) ∧ 𝐾 < 𝐽 ) → ( ( 𝐾 − 𝐽 ) + 𝑁 ) ∈ ( 1 ..^ 𝑁 ) )
55 54 exp31 ⊢ ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) → ( ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) → ( 𝐾 < 𝐽 → ( ( 𝐾 − 𝐽 ) + 𝑁 ) ∈ ( 1 ..^ 𝑁 ) ) ) )
56 10 55 sylbi ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) → ( 𝐾 < 𝐽 → ( ( 𝐾 − 𝐽 ) + 𝑁 ) ∈ ( 1 ..^ 𝑁 ) ) ) )
57 56 com12 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) → ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝐾 < 𝐽 → ( ( 𝐾 − 𝐽 ) + 𝑁 ) ∈ ( 1 ..^ 𝑁 ) ) ) )
58 57 3adant2 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝐾 < 𝐽 → ( ( 𝐾 − 𝐽 ) + 𝑁 ) ∈ ( 1 ..^ 𝑁 ) ) ) )
59 9 58 sylbi ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝐾 < 𝐽 → ( ( 𝐾 − 𝐽 ) + 𝑁 ) ∈ ( 1 ..^ 𝑁 ) ) ) )
60 1 59 syl ⊢ ( 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) → ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝐾 < 𝐽 → ( ( 𝐾 − 𝐽 ) + 𝑁 ) ∈ ( 1 ..^ 𝑁 ) ) ) )
61 60 impcom ⊢ ( ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ( 𝐾 < 𝐽 → ( ( 𝐾 − 𝐽 ) + 𝑁 ) ∈ ( 1 ..^ 𝑁 ) ) )
62 61 impcom ⊢ ( ( 𝐾 < 𝐽 ∧ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) ) → ( ( 𝐾 − 𝐽 ) + 𝑁 ) ∈ ( 1 ..^ 𝑁 ) )
63 oveq1 ⊢ ( 𝑖 = ( ( 𝐾 − 𝐽 ) + 𝑁 ) → ( 𝑖 + 𝐽 ) = ( ( ( 𝐾 − 𝐽 ) + 𝑁 ) + 𝐽 ) )
64 2 zcnd ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝐾 ∈ ℂ )
65 64 adantr ⊢ ( ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ) → 𝐾 ∈ ℂ )
66 14 adantr ⊢ ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → 𝐽 ∈ ℂ )
67 66 adantl ⊢ ( ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ) → 𝐽 ∈ ℂ )
68 17 adantl ⊢ ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
69 68 adantl ⊢ ( ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ) → 𝑁 ∈ ℂ )
70 65 67 69 3jca ⊢ ( ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ) → ( 𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ ) )
71 70 ex ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ) )
72 1 71 syl ⊢ ( 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) → ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ) )
73 72 com12 ⊢ ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) → ( 𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ) )
74 73 3adant3 ⊢ ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) → ( 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) → ( 𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ) )
75 10 74 sylbi ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) → ( 𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ) )
76 75 imp ⊢ ( ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ( 𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ ) )
77 76 adantl ⊢ ( ( 𝐾 < 𝐽 ∧ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) ) → ( 𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ ) )
78 nppcan ⊢ ( ( 𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( ( 𝐾 − 𝐽 ) + 𝑁 ) + 𝐽 ) = ( 𝐾 + 𝑁 ) )
79 77 78 syl ⊢ ( ( 𝐾 < 𝐽 ∧ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) ) → ( ( ( 𝐾 − 𝐽 ) + 𝑁 ) + 𝐽 ) = ( 𝐾 + 𝑁 ) )
80 63 79 sylan9eqr ⊢ ( ( ( 𝐾 < 𝐽 ∧ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) ) ∧ 𝑖 = ( ( 𝐾 − 𝐽 ) + 𝑁 ) ) → ( 𝑖 + 𝐽 ) = ( 𝐾 + 𝑁 ) )
81 80 oveq1d ⊢ ( ( ( 𝐾 < 𝐽 ∧ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) ) ∧ 𝑖 = ( ( 𝐾 − 𝐽 ) + 𝑁 ) ) → ( ( 𝑖 + 𝐽 ) mod 𝑁 ) = ( ( 𝐾 + 𝑁 ) mod 𝑁 ) )
82 81 eqeq2d ⊢ ( ( ( 𝐾 < 𝐽 ∧ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) ) ∧ 𝑖 = ( ( 𝐾 − 𝐽 ) + 𝑁 ) ) → ( 𝐾 = ( ( 𝑖 + 𝐽 ) mod 𝑁 ) ↔ 𝐾 = ( ( 𝐾 + 𝑁 ) mod 𝑁 ) ) )
83 9 biimpi ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) )
84 83 a1d ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) ) )
85 1 84 syl ⊢ ( 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) → ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) ) )
86 85 impcom ⊢ ( ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) )
87 86 adantl ⊢ ( ( 𝐾 < 𝐽 ∧ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) ) → ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) )
88 addmodidr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → ( ( 𝐾 + 𝑁 ) mod 𝑁 ) = 𝐾 )
89 88 eqcomd ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → 𝐾 = ( ( 𝐾 + 𝑁 ) mod 𝑁 ) )
90 87 89 syl ⊢ ( ( 𝐾 < 𝐽 ∧ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) ) → 𝐾 = ( ( 𝐾 + 𝑁 ) mod 𝑁 ) )
91 62 82 90 rspcedvd ⊢ ( ( 𝐾 < 𝐽 ∧ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) ) → ∃ 𝑖 ∈ ( 1 ..^ 𝑁 ) 𝐾 = ( ( 𝑖 + 𝐽 ) mod 𝑁 ) )
92 91 ex ⊢ ( 𝐾 < 𝐽 → ( ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ∃ 𝑖 ∈ ( 1 ..^ 𝑁 ) 𝐾 = ( ( 𝑖 + 𝐽 ) mod 𝑁 ) ) )
93 eldifsn ⊢ ( 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ↔ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝐽 ) )
94 eqneqall ⊢ ( 𝐾 = 𝐽 → ( 𝐾 ≠ 𝐽 → ∃ 𝑖 ∈ ( 1 ..^ 𝑁 ) 𝐾 = ( ( 𝑖 + 𝐽 ) mod 𝑁 ) ) )
95 94 com12 ⊢ ( 𝐾 ≠ 𝐽 → ( 𝐾 = 𝐽 → ∃ 𝑖 ∈ ( 1 ..^ 𝑁 ) 𝐾 = ( ( 𝑖 + 𝐽 ) mod 𝑁 ) ) )
96 95 adantl ⊢ ( ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝐽 ) → ( 𝐾 = 𝐽 → ∃ 𝑖 ∈ ( 1 ..^ 𝑁 ) 𝐾 = ( ( 𝑖 + 𝐽 ) mod 𝑁 ) ) )
97 93 96 sylbi ⊢ ( 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) → ( 𝐾 = 𝐽 → ∃ 𝑖 ∈ ( 1 ..^ 𝑁 ) 𝐾 = ( ( 𝑖 + 𝐽 ) mod 𝑁 ) ) )
98 97 adantl ⊢ ( ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ( 𝐾 = 𝐽 → ∃ 𝑖 ∈ ( 1 ..^ 𝑁 ) 𝐾 = ( ( 𝑖 + 𝐽 ) mod 𝑁 ) ) )
99 98 com12 ⊢ ( 𝐾 = 𝐽 → ( ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ∃ 𝑖 ∈ ( 1 ..^ 𝑁 ) 𝐾 = ( ( 𝑖 + 𝐽 ) mod 𝑁 ) ) )
100 92 99 jaoi ⊢ ( ( 𝐾 < 𝐽 ∨ 𝐾 = 𝐽 ) → ( ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ∃ 𝑖 ∈ ( 1 ..^ 𝑁 ) 𝐾 = ( ( 𝑖 + 𝐽 ) mod 𝑁 ) ) )
101 100 com12 ⊢ ( ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ( ( 𝐾 < 𝐽 ∨ 𝐾 = 𝐽 ) → ∃ 𝑖 ∈ ( 1 ..^ 𝑁 ) 𝐾 = ( ( 𝑖 + 𝐽 ) mod 𝑁 ) ) )
102 8 101 sylbid ⊢ ( ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ( 𝐾 ≤ 𝐽 → ∃ 𝑖 ∈ ( 1 ..^ 𝑁 ) 𝐾 = ( ( 𝑖 + 𝐽 ) mod 𝑁 ) ) )
103 102 com12 ⊢ ( 𝐾 ≤ 𝐽 → ( ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ∃ 𝑖 ∈ ( 1 ..^ 𝑁 ) 𝐾 = ( ( 𝑖 + 𝐽 ) mod 𝑁 ) ) )
104 ltnle ⊢ ( ( 𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝐽 < 𝐾 ↔ ¬ 𝐾 ≤ 𝐽 ) )
105 6 4 104 syl2an ⊢ ( ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ( 𝐽 < 𝐾 ↔ ¬ 𝐾 ≤ 𝐽 ) )
106 105 bicomd ⊢ ( ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ( ¬ 𝐾 ≤ 𝐽 ↔ 𝐽 < 𝐾 ) )
107 22 3ad2ant1 ⊢ ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) → 𝐽 ∈ ℤ )
108 nn0z ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℤ )
109 108 adantr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) → 𝐾 ∈ ℤ )
110 znnsub ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐽 < 𝐾 ↔ ( 𝐾 − 𝐽 ) ∈ ℕ ) )
111 107 109 110 syl2anr ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ∧ ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ) → ( 𝐽 < 𝐾 ↔ ( 𝐾 − 𝐽 ) ∈ ℕ ) )
112 111 biimpa ⊢ ( ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ∧ ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ) ∧ 𝐽 < 𝐾 ) → ( 𝐾 − 𝐽 ) ∈ ℕ )
113 31 adantl ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ∧ ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ) → 𝑁 ∈ ℕ )
114 113 adantr ⊢ ( ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ∧ ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ) ∧ 𝐽 < 𝐾 ) → 𝑁 ∈ ℕ )
115 nn0ge0 ⊢ ( 𝐽 ∈ ℕ0 → 0 ≤ 𝐽 )
116 115 3ad2ant1 ⊢ ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) → 0 ≤ 𝐽 )
117 116 adantl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ) → 0 ≤ 𝐽 )
118 subge02 ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ ) → ( 0 ≤ 𝐽 ↔ ( 𝐾 − 𝐽 ) ≤ 𝐾 ) )
119 34 38 118 syl2an ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ) → ( 0 ≤ 𝐽 ↔ ( 𝐾 − 𝐽 ) ≤ 𝐾 ) )
120 117 119 mpbid ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ) → ( 𝐾 − 𝐽 ) ≤ 𝐾 )
121 38 adantl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ) → 𝐽 ∈ ℝ )
122 34 adantr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ) → 𝐾 ∈ ℝ )
123 46 adantl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ) → 𝑁 ∈ ℝ )
124 121 122 123 3jca ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ) → ( 𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
125 43 ancoms ⊢ ( ( 𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝐾 − 𝐽 ) ∈ ℝ )
126 125 3adant3 ⊢ ( ( 𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝐾 − 𝐽 ) ∈ ℝ )
127 simp2 ⊢ ( ( 𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝐾 ∈ ℝ )
128 simp3 ⊢ ( ( 𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑁 ∈ ℝ )
129 126 127 128 3jca ⊢ ( ( 𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝐾 − 𝐽 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
130 124 129 syl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ) → ( ( 𝐾 − 𝐽 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
131 lelttr ⊢ ( ( ( 𝐾 − 𝐽 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( ( 𝐾 − 𝐽 ) ≤ 𝐾 ∧ 𝐾 < 𝑁 ) → ( 𝐾 − 𝐽 ) < 𝑁 ) )
132 130 131 syl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ) → ( ( ( 𝐾 − 𝐽 ) ≤ 𝐾 ∧ 𝐾 < 𝑁 ) → ( 𝐾 − 𝐽 ) < 𝑁 ) )
133 120 132 mpand ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ) → ( 𝐾 < 𝑁 → ( 𝐾 − 𝐽 ) < 𝑁 ) )
134 133 impancom ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) → ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) → ( 𝐾 − 𝐽 ) < 𝑁 ) )
135 134 imp ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ∧ ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ) → ( 𝐾 − 𝐽 ) < 𝑁 )
136 135 adantr ⊢ ( ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ∧ ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ) ∧ 𝐽 < 𝐾 ) → ( 𝐾 − 𝐽 ) < 𝑁 )
137 112 114 136 3jca ⊢ ( ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) ∧ ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) ) ∧ 𝐽 < 𝐾 ) → ( ( 𝐾 − 𝐽 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝐾 − 𝐽 ) < 𝑁 ) )
138 137 exp31 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐾 < 𝑁 ) → ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) → ( 𝐽 < 𝐾 → ( ( 𝐾 − 𝐽 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝐾 − 𝐽 ) < 𝑁 ) ) ) )
139 138 3adant2 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) → ( 𝐽 < 𝐾 → ( ( 𝐾 − 𝐽 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝐾 − 𝐽 ) < 𝑁 ) ) ) )
140 9 139 sylbi ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) → ( 𝐽 < 𝐾 → ( ( 𝐾 − 𝐽 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝐾 − 𝐽 ) < 𝑁 ) ) ) )
141 1 140 syl ⊢ ( 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) → ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) → ( 𝐽 < 𝐾 → ( ( 𝐾 − 𝐽 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝐾 − 𝐽 ) < 𝑁 ) ) ) )
142 141 com12 ⊢ ( ( 𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁 ) → ( 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) → ( 𝐽 < 𝐾 → ( ( 𝐾 − 𝐽 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝐾 − 𝐽 ) < 𝑁 ) ) ) )
143 10 142 sylbi ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) → ( 𝐽 < 𝐾 → ( ( 𝐾 − 𝐽 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝐾 − 𝐽 ) < 𝑁 ) ) ) )
144 143 imp ⊢ ( ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ( 𝐽 < 𝐾 → ( ( 𝐾 − 𝐽 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝐾 − 𝐽 ) < 𝑁 ) ) )
145 106 144 sylbid ⊢ ( ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ( ¬ 𝐾 ≤ 𝐽 → ( ( 𝐾 − 𝐽 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝐾 − 𝐽 ) < 𝑁 ) ) )
146 145 impcom ⊢ ( ( ¬ 𝐾 ≤ 𝐽 ∧ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) ) → ( ( 𝐾 − 𝐽 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝐾 − 𝐽 ) < 𝑁 ) )
147 elfzo1 ⊢ ( ( 𝐾 − 𝐽 ) ∈ ( 1 ..^ 𝑁 ) ↔ ( ( 𝐾 − 𝐽 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝐾 − 𝐽 ) < 𝑁 ) )
148 146 147 sylibr ⊢ ( ( ¬ 𝐾 ≤ 𝐽 ∧ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) ) → ( 𝐾 − 𝐽 ) ∈ ( 1 ..^ 𝑁 ) )
149 oveq1 ⊢ ( 𝑖 = ( 𝐾 − 𝐽 ) → ( 𝑖 + 𝐽 ) = ( ( 𝐾 − 𝐽 ) + 𝐽 ) )
150 1 64 syl ⊢ ( 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) → 𝐾 ∈ ℂ )
151 5 zcnd ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ℂ )
152 npcan ⊢ ( ( 𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ) → ( ( 𝐾 − 𝐽 ) + 𝐽 ) = 𝐾 )
153 150 151 152 syl2anr ⊢ ( ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ( ( 𝐾 − 𝐽 ) + 𝐽 ) = 𝐾 )
154 153 adantl ⊢ ( ( ¬ 𝐾 ≤ 𝐽 ∧ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) ) → ( ( 𝐾 − 𝐽 ) + 𝐽 ) = 𝐾 )
155 149 154 sylan9eqr ⊢ ( ( ( ¬ 𝐾 ≤ 𝐽 ∧ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) ) ∧ 𝑖 = ( 𝐾 − 𝐽 ) ) → ( 𝑖 + 𝐽 ) = 𝐾 )
156 155 oveq1d ⊢ ( ( ( ¬ 𝐾 ≤ 𝐽 ∧ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) ) ∧ 𝑖 = ( 𝐾 − 𝐽 ) ) → ( ( 𝑖 + 𝐽 ) mod 𝑁 ) = ( 𝐾 mod 𝑁 ) )
157 156 eqeq2d ⊢ ( ( ( ¬ 𝐾 ≤ 𝐽 ∧ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) ) ∧ 𝑖 = ( 𝐾 − 𝐽 ) ) → ( 𝐾 = ( ( 𝑖 + 𝐽 ) mod 𝑁 ) ↔ 𝐾 = ( 𝐾 mod 𝑁 ) ) )
158 zmodidfzoimp ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐾 mod 𝑁 ) = 𝐾 )
159 1 158 syl ⊢ ( 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) → ( 𝐾 mod 𝑁 ) = 𝐾 )
160 159 adantl ⊢ ( ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ( 𝐾 mod 𝑁 ) = 𝐾 )
161 160 adantl ⊢ ( ( ¬ 𝐾 ≤ 𝐽 ∧ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) ) → ( 𝐾 mod 𝑁 ) = 𝐾 )
162 161 eqcomd ⊢ ( ( ¬ 𝐾 ≤ 𝐽 ∧ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) ) → 𝐾 = ( 𝐾 mod 𝑁 ) )
163 148 157 162 rspcedvd ⊢ ( ( ¬ 𝐾 ≤ 𝐽 ∧ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) ) → ∃ 𝑖 ∈ ( 1 ..^ 𝑁 ) 𝐾 = ( ( 𝑖 + 𝐽 ) mod 𝑁 ) )
164 163 ex ⊢ ( ¬ 𝐾 ≤ 𝐽 → ( ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ∃ 𝑖 ∈ ( 1 ..^ 𝑁 ) 𝐾 = ( ( 𝑖 + 𝐽 ) mod 𝑁 ) ) )
165 103 164 pm2.61i ⊢ ( ( 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) → ∃ 𝑖 ∈ ( 1 ..^ 𝑁 ) 𝐾 = ( ( 𝑖 + 𝐽 ) mod 𝑁 ) )