Theorem modmknepk

Description: A nonnegative integer less than the modulus plus/minus a positive integer less than (the ceiling of) half of the modulus are not equal modulo the modulus. For this theorem, it is essential that K < ( N / 2 ) ! (Contributed by AV, 3-Sep-2025) (Revised by AV, 15-Nov-2025)

	Ref	Expression
Hypotheses	modmknepk.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
	modmknepk.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
Assertion	modmknepk	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑌 ∈ 𝐼 ∧ 𝐾 ∈ 𝐽 ) → ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ≠ ( ( 𝑌 + 𝐾 ) mod 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		modmknepk.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
2		modmknepk.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
3		eluz3nn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
4	3	3ad2ant1	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑌 ∈ 𝐼 ∧ 𝐾 ∈ 𝐽 ) → 𝑁 ∈ ℕ )
5		elfzoelz	⊢ ( 𝑌 ∈ ( 0 ..^ 𝑁 ) → 𝑌 ∈ ℤ )
6	5 2	eleq2s	⊢ ( 𝑌 ∈ 𝐼 → 𝑌 ∈ ℤ )
7	6	3ad2ant2	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑌 ∈ 𝐼 ∧ 𝐾 ∈ 𝐽 ) → 𝑌 ∈ ℤ )
8		elfzoelz	⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 𝐾 ∈ ℤ )
9	8 1	eleq2s	⊢ ( 𝐾 ∈ 𝐽 → 𝐾 ∈ ℤ )
10	9	3ad2ant3	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑌 ∈ 𝐼 ∧ 𝐾 ∈ 𝐽 ) → 𝐾 ∈ ℤ )
11	9	zcnd	⊢ ( 𝐾 ∈ 𝐽 → 𝐾 ∈ ℂ )
12	11	2timesd	⊢ ( 𝐾 ∈ 𝐽 → ( 2 · 𝐾 ) = ( 𝐾 + 𝐾 ) )
13	12	eqcomd	⊢ ( 𝐾 ∈ 𝐽 → ( 𝐾 + 𝐾 ) = ( 2 · 𝐾 ) )
14	13	adantl	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝐾 + 𝐾 ) = ( 2 · 𝐾 ) )
15		1red	⊢ ( 𝐾 ∈ 𝐽 → 1 ∈ ℝ )
16	9	zred	⊢ ( 𝐾 ∈ 𝐽 → 𝐾 ∈ ℝ )
17		2z	⊢ 2 ∈ ℤ
18	17	a1i	⊢ ( 𝐾 ∈ 𝐽 → 2 ∈ ℤ )
19	18 9	zmulcld	⊢ ( 𝐾 ∈ 𝐽 → ( 2 · 𝐾 ) ∈ ℤ )
20	19	zred	⊢ ( 𝐾 ∈ 𝐽 → ( 2 · 𝐾 ) ∈ ℝ )
21		elfzole1	⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 1 ≤ 𝐾 )
22	21 1	eleq2s	⊢ ( 𝐾 ∈ 𝐽 → 1 ≤ 𝐾 )
23		elfzo1	⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ↔ ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝐾 < ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
24	23	simp1bi	⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 𝐾 ∈ ℕ )
25	24 1	eleq2s	⊢ ( 𝐾 ∈ 𝐽 → 𝐾 ∈ ℕ )
26	25	nnnn0d	⊢ ( 𝐾 ∈ 𝐽 → 𝐾 ∈ ℕ0 )
27		nn0le2x	⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ≤ ( 2 · 𝐾 ) )
28	26 27	syl	⊢ ( 𝐾 ∈ 𝐽 → 𝐾 ≤ ( 2 · 𝐾 ) )
29	15 16 20 22 28	letrd	⊢ ( 𝐾 ∈ 𝐽 → 1 ≤ ( 2 · 𝐾 ) )
30	29	adantl	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → 1 ≤ ( 2 · 𝐾 ) )
31	1	eleq2i	⊢ ( 𝐾 ∈ 𝐽 ↔ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
32		2tceilhalfelfzo1	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( 2 · 𝐾 ) < 𝑁 )
33	31 32	sylan2b	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 2 · 𝐾 ) < 𝑁 )
34	30 33	jca	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 1 ≤ ( 2 · 𝐾 ) ∧ ( 2 · 𝐾 ) < 𝑁 ) )
35		breq2	⊢ ( ( 𝐾 + 𝐾 ) = ( 2 · 𝐾 ) → ( 1 ≤ ( 𝐾 + 𝐾 ) ↔ 1 ≤ ( 2 · 𝐾 ) ) )
36		breq1	⊢ ( ( 𝐾 + 𝐾 ) = ( 2 · 𝐾 ) → ( ( 𝐾 + 𝐾 ) < 𝑁 ↔ ( 2 · 𝐾 ) < 𝑁 ) )
37	35 36	anbi12d	⊢ ( ( 𝐾 + 𝐾 ) = ( 2 · 𝐾 ) → ( ( 1 ≤ ( 𝐾 + 𝐾 ) ∧ ( 𝐾 + 𝐾 ) < 𝑁 ) ↔ ( 1 ≤ ( 2 · 𝐾 ) ∧ ( 2 · 𝐾 ) < 𝑁 ) ) )
38	34 37	syl5ibrcom	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ( 𝐾 + 𝐾 ) = ( 2 · 𝐾 ) → ( 1 ≤ ( 𝐾 + 𝐾 ) ∧ ( 𝐾 + 𝐾 ) < 𝑁 ) ) )
39	14 38	mpd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 1 ≤ ( 𝐾 + 𝐾 ) ∧ ( 𝐾 + 𝐾 ) < 𝑁 ) )
40	39	3adant2	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑌 ∈ 𝐼 ∧ 𝐾 ∈ 𝐽 ) → ( 1 ≤ ( 𝐾 + 𝐾 ) ∧ ( 𝐾 + 𝐾 ) < 𝑁 ) )
41		submodneaddmod	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑌 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 1 ≤ ( 𝐾 + 𝐾 ) ∧ ( 𝐾 + 𝐾 ) < 𝑁 ) ) → ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ≠ ( ( 𝑌 − 𝐾 ) mod 𝑁 ) )
42	41	necomd	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑌 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 1 ≤ ( 𝐾 + 𝐾 ) ∧ ( 𝐾 + 𝐾 ) < 𝑁 ) ) → ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ≠ ( ( 𝑌 + 𝐾 ) mod 𝑁 ) )
43	4 7 10 10 40 42	syl131anc	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑌 ∈ 𝐼 ∧ 𝐾 ∈ 𝐽 ) → ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ≠ ( ( 𝑌 + 𝐾 ) mod 𝑁 ) )