modm1nep1

Description: A nonnegative integer less than a modulus greater than 2 plus/minus one are not equal modulo the modulus. (Contributed by AV, 15-Nov-2025)

		Ref	Expression
	Hypothesis	modm1nep1.i	$⊢ I = (0 ..^N)$
	Assertion	modm1nep1	$⊢ (N \in ℤ_{\geq 3} \land Y \in I) \to (Y - 1) \mod N \neq (Y + 1) \mod N$

Proof

Step	Hyp	Ref	Expression
1		modm1nep1.i	$⊢ I = (0 ..^N)$
2		1elfzo1ceilhalf1	$⊢ N \in ℤ_{\geq 3} \to 1 \in (1 ..^⌈\frac{N}{2}⌉)$
3	2	adantr	$⊢ (N \in ℤ_{\geq 3} \land Y \in I) \to 1 \in (1 ..^⌈\frac{N}{2}⌉)$
4		eqid	$⊢ (1 ..^⌈\frac{N}{2}⌉) = (1 ..^⌈\frac{N}{2}⌉)$
5	4 1	modmknepk	$⊢ (N \in ℤ_{\geq 3} \land Y \in I \land 1 \in (1 ..^⌈\frac{N}{2}⌉)) \to (Y - 1) \mod N \neq (Y + 1) \mod N$
6	3 5	mpd3an3	$⊢ (N \in ℤ_{\geq 3} \land Y \in I) \to (Y - 1) \mod N \neq (Y + 1) \mod N$

Metamath Proof Explorer

Theorem modm1nep1

Proof