modm1p1ne

Description: If an integer minus one equals another integer plus one modulo an integer greater than 4, then the first integer plus one is not equal to the second integer minus one modulo the same modulus. (Contributed by AV, 15-Nov-2025)

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

Proof

Step	Hyp	Ref	Expression
1		modm1nep1.i	$⊢ I = (0 ..^N)$
2		eluz2	$⊢ N \in ℤ_{\geq 5} \leftrightarrow (5 \in ℤ \land N \in ℤ \land 5 \leq N)$
3		4nn0	$⊢ 4 \in ℕ_{0}$
4	3	a1i	$⊢ (5 \in ℤ \land N \in ℤ \land 5 \leq N) \to 4 \in ℕ_{0}$
5		simp2	$⊢ (5 \in ℤ \land N \in ℤ \land 5 \leq N) \to N \in ℤ$
6		0red	$⊢ (5 \in ℤ \land N \in ℤ \land 5 \leq N) \to 0 \in ℝ$
7		5re	$⊢ 5 \in ℝ$
8	7	a1i	$⊢ (5 \in ℤ \land N \in ℤ \land 5 \leq N) \to 5 \in ℝ$
9		zre	$⊢ N \in ℤ \to N \in ℝ$
10	9	3ad2ant2	$⊢ (5 \in ℤ \land N \in ℤ \land 5 \leq N) \to N \in ℝ$
11		5pos	$⊢ 0 < 5$
12	11	a1i	$⊢ (5 \in ℤ \land N \in ℤ \land 5 \leq N) \to 0 < 5$
13		simp3	$⊢ (5 \in ℤ \land N \in ℤ \land 5 \leq N) \to 5 \leq N$
14	6 8 10 12 13	ltletrd	$⊢ (5 \in ℤ \land N \in ℤ \land 5 \leq N) \to 0 < N$
15		elnnz	$⊢ N \in ℕ \leftrightarrow (N \in ℤ \land 0 < N)$
16	5 14 15	sylanbrc	$⊢ (5 \in ℤ \land N \in ℤ \land 5 \leq N) \to N \in ℕ$
17		4re	$⊢ 4 \in ℝ$
18	17	a1i	$⊢ (5 \in ℤ \land N \in ℤ \land 5 \leq N) \to 4 \in ℝ$
19		4lt5	$⊢ 4 < 5$
20	19	a1i	$⊢ (5 \in ℤ \land N \in ℤ \land 5 \leq N) \to 4 < 5$
21	18 8 10 20 13	ltletrd	$⊢ (5 \in ℤ \land N \in ℤ \land 5 \leq N) \to 4 < N$
22		elfzo0	$⊢ 4 \in (0 ..^N) \leftrightarrow (4 \in ℕ_{0} \land N \in ℕ \land 4 < N)$
23	4 16 21 22	syl3anbrc	$⊢ (5 \in ℤ \land N \in ℤ \land 5 \leq N) \to 4 \in (0 ..^N)$
24	2 23	sylbi	$⊢ N \in ℤ_{\geq 5} \to 4 \in (0 ..^N)$
25		zmodidfzoimp	$⊢ 4 \in (0 ..^N) \to 4 \mod N = 4$
26	24 25	syl	$⊢ N \in ℤ_{\geq 5} \to 4 \mod N = 4$
27		4ne0	$⊢ 4 \neq 0$
28	27	a1i	$⊢ N \in ℤ_{\geq 5} \to 4 \neq 0$
29	26 28	eqnetrd	$⊢ N \in ℤ_{\geq 5} \to 4 \mod N \neq 0$
30		df-ne	$⊢ 4 \cdot 1 \mod N \neq 0 \leftrightarrow \neg 4 \cdot 1 \mod N = 0$
31		4cn	$⊢ 4 \in ℂ$
32	31	mulridi	$⊢ 4 \cdot 1 = 4$
33	32	oveq1i	$⊢ 4 \cdot 1 \mod N = 4 \mod N$
34	33	neeq1i	$⊢ 4 \cdot 1 \mod N \neq 0 \leftrightarrow 4 \mod N \neq 0$
35	30 34	bitr3i	$⊢ \neg 4 \cdot 1 \mod N = 0 \leftrightarrow 4 \mod N \neq 0$
36	29 35	sylibr	$⊢ N \in ℤ_{\geq 5} \to \neg 4 \cdot 1 \mod N = 0$
37	36	3ad2ant1	$⊢ (N \in ℤ_{\geq 5} \land X \in I \land Y \in I) \to \neg 4 \cdot 1 \mod N = 0$
38	37	adantr	$⊢ ((N \in ℤ_{\geq 5} \land X \in I \land Y \in I) \land (Y - 1) \mod N = (X + 1) \mod N) \to \neg 4 \cdot 1 \mod N = 0$
39		uzuzle35	$⊢ N \in ℤ_{\geq 5} \to N \in ℤ_{\geq 3}$
40		eluz3nn	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ$
41	39 40	syl	$⊢ N \in ℤ_{\geq 5} \to N \in ℕ$
42	41	3ad2ant1	$⊢ (N \in ℤ_{\geq 5} \land X \in I \land Y \in I) \to N \in ℕ$
43		elfzoelz	$⊢ X \in (0 ..^N) \to X \in ℤ$
44	43 1	eleq2s	$⊢ X \in I \to X \in ℤ$
45	44	3ad2ant2	$⊢ (N \in ℤ_{\geq 5} \land X \in I \land Y \in I) \to X \in ℤ$
46		elfzoelz	$⊢ Y \in (0 ..^N) \to Y \in ℤ$
47	46 1	eleq2s	$⊢ Y \in I \to Y \in ℤ$
48	47	3ad2ant3	$⊢ (N \in ℤ_{\geq 5} \land X \in I \land Y \in I) \to Y \in ℤ$
49		1zzd	$⊢ (N \in ℤ_{\geq 5} \land X \in I \land Y \in I) \to 1 \in ℤ$
50		modmkpkne	$⊢ (N \in ℕ \land (X \in ℤ \land Y \in ℤ \land 1 \in ℤ)) \to ((Y - 1) \mod N = (X + 1) \mod N \to ((Y + 1) \mod N = (X - 1) \mod N \leftrightarrow 4 \cdot 1 \mod N = 0))$
51	42 45 48 49 50	syl13anc	$⊢ (N \in ℤ_{\geq 5} \land X \in I \land Y \in I) \to ((Y - 1) \mod N = (X + 1) \mod N \to ((Y + 1) \mod N = (X - 1) \mod N \leftrightarrow 4 \cdot 1 \mod N = 0))$
52	51	imp	$⊢ ((N \in ℤ_{\geq 5} \land X \in I \land Y \in I) \land (Y - 1) \mod N = (X + 1) \mod N) \to ((Y + 1) \mod N = (X - 1) \mod N \leftrightarrow 4 \cdot 1 \mod N = 0)$
53	38 52	mtbird	$⊢ ((N \in ℤ_{\geq 5} \land X \in I \land Y \in I) \land (Y - 1) \mod N = (X + 1) \mod N) \to \neg (Y + 1) \mod N = (X - 1) \mod N$
54	53	neqned	$⊢ ((N \in ℤ_{\geq 5} \land X \in I \land Y \in I) \land (Y - 1) \mod N = (X + 1) \mod N) \to (Y + 1) \mod N \neq (X - 1) \mod N$
55	54	ex	$⊢ (N \in ℤ_{\geq 5} \land X \in I \land Y \in I) \to ((Y - 1) \mod N = (X + 1) \mod N \to (Y + 1) \mod N \neq (X - 1) \mod N)$

Metamath Proof Explorer

Theorem modm1p1ne

Proof