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	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
	modmknepk.i	$⊢ I = (0 ..^N)$
Assertion	modmknepk	$⊢ (N \in ℤ_{\geq 3} \land Y \in I \land K \in J) \to (Y - K) \mod N \neq (Y + K) \mod N$

Proof

Step	Hyp	Ref	Expression
1		modmknepk.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
2		modmknepk.i	$⊢ I = (0 ..^N)$
3		eluz3nn	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ$
4	3	3ad2ant1	$⊢ (N \in ℤ_{\geq 3} \land Y \in I \land K \in J) \to N \in ℕ$
5		elfzoelz	$⊢ Y \in (0 ..^N) \to Y \in ℤ$
6	5 2	eleq2s	$⊢ Y \in I \to Y \in ℤ$
7	6	3ad2ant2	$⊢ (N \in ℤ_{\geq 3} \land Y \in I \land K \in J) \to Y \in ℤ$
8		elfzoelz	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K \in ℤ$
9	8 1	eleq2s	$⊢ K \in J \to K \in ℤ$
10	9	3ad2ant3	$⊢ (N \in ℤ_{\geq 3} \land Y \in I \land K \in J) \to K \in ℤ$
11	9	zcnd	$⊢ K \in J \to K \in ℂ$
12	11	2timesd	$⊢ K \in J \to 2 K = K + K$
13	12	eqcomd	$⊢ K \in J \to K + K = 2 K$
14	13	adantl	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to K + K = 2 K$
15		1red	$⊢ K \in J \to 1 \in ℝ$
16	9	zred	$⊢ K \in J \to K \in ℝ$
17		2z	$⊢ 2 \in ℤ$
18	17	a1i	$⊢ K \in J \to 2 \in ℤ$
19	18 9	zmulcld	$⊢ K \in J \to 2 K \in ℤ$
20	19	zred	$⊢ K \in J \to 2 K \in ℝ$
21		elfzole1	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to 1 \leq K$
22	21 1	eleq2s	$⊢ K \in J \to 1 \leq K$
23		elfzo1	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \leftrightarrow (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land K < ⌈\frac{N}{2}⌉)$
24	23	simp1bi	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K \in ℕ$
25	24 1	eleq2s	$⊢ K \in J \to K \in ℕ$
26	25	nnnn0d	$⊢ K \in J \to K \in ℕ_{0}$
27		nn0le2x	$⊢ K \in ℕ_{0} \to K \leq 2 K$
28	26 27	syl	$⊢ K \in J \to K \leq 2 K$
29	15 16 20 22 28	letrd	$⊢ K \in J \to 1 \leq 2 K$
30	29	adantl	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to 1 \leq 2 K$
31	1	eleq2i	$⊢ K \in J \leftrightarrow K \in (1 ..^⌈\frac{N}{2}⌉)$
32		2tceilhalfelfzo1	$⊢ (N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉)) \to 2 K < N$
33	31 32	sylan2b	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to 2 K < N$
34	30 33	jca	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (1 \leq 2 K \land 2 K < N)$
35		breq2	$⊢ K + K = 2 K \to (1 \leq K + K \leftrightarrow 1 \leq 2 K)$
36		breq1	$⊢ K + K = 2 K \to (K + K < N \leftrightarrow 2 K < N)$
37	35 36	anbi12d	$⊢ K + K = 2 K \to ((1 \leq K + K \land K + K < N) \leftrightarrow (1 \leq 2 K \land 2 K < N))$
38	34 37	syl5ibrcom	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (K + K = 2 K \to (1 \leq K + K \land K + K < N))$
39	14 38	mpd	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (1 \leq K + K \land K + K < N)$
40	39	3adant2	$⊢ (N \in ℤ_{\geq 3} \land Y \in I \land K \in J) \to (1 \leq K + K \land K + K < N)$
41		submodneaddmod	$⊢ (N \in ℕ \land (Y \in ℤ \land K \in ℤ \land K \in ℤ) \land (1 \leq K + K \land K + K < N)) \to (Y + K) \mod N \neq (Y - K) \mod N$
42	41	necomd	$⊢ (N \in ℕ \land (Y \in ℤ \land K \in ℤ \land K \in ℤ) \land (1 \leq K + K \land K + K < N)) \to (Y - K) \mod N \neq (Y + K) \mod N$
43	4 7 10 10 40 42	syl131anc	$⊢ (N \in ℤ_{\geq 3} \land Y \in I \land K \in J) \to (Y - K) \mod N \neq (Y + K) \mod N$

Metamath Proof Explorer

Theorem modmknepk

Proof