modm1nep2

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

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

Proof

Step	Hyp	Ref	Expression
1		modm1nep1.i	$⊢ I = (0 ..^N)$
2		elfzoelz	$⊢ Y \in (0 ..^N) \to Y \in ℤ$
3	2 1	eleq2s	$⊢ Y \in I \to Y \in ℤ$
4	3	zcnd	$⊢ Y \in I \to Y \in ℂ$
5		1cnd	$⊢ Y \in I \to 1 \in ℂ$
6	4 5	negsubd	$⊢ Y \in I \to Y + -1 = Y - 1$
7	6	eqcomd	$⊢ Y \in I \to Y - 1 = Y + -1$
8	7	oveq1d	$⊢ Y \in I \to (Y - 1) \mod N = (Y + -1) \mod N$
9	8	adantl	$⊢ (N \in ℤ_{\geq 5} \land Y \in I) \to (Y - 1) \mod N = (Y + -1) \mod N$
10		eluz5nn	$⊢ N \in ℤ_{\geq 5} \to N \in ℕ$
11	10	adantr	$⊢ (N \in ℤ_{\geq 5} \land Y \in I) \to N \in ℕ$
12		simpr	$⊢ (N \in ℤ_{\geq 5} \land Y \in I) \to Y \in I$
13		2z	$⊢ 2 \in ℤ$
14	13	a1i	$⊢ (N \in ℤ_{\geq 5} \land Y \in I) \to 2 \in ℤ$
15		1zzd	$⊢ (N \in ℤ_{\geq 5} \land Y \in I) \to 1 \in ℤ$
16	15	znegcld	$⊢ (N \in ℤ_{\geq 5} \land Y \in I) \to - 1 \in ℤ$
17		2cn	$⊢ 2 \in ℂ$
18		ax-1cn	$⊢ 1 \in ℂ$
19	17 18	subnegi	$⊢ 2 - -1 = 2 + 1$
20		2p1e3	$⊢ 2 + 1 = 3$
21	19 20	eqtri	$⊢ 2 - -1 = 3$
22	21	fveq2i	$⊢ \|2 - -1\| = \|3\|$
23		3nn0	$⊢ 3 \in ℕ_{0}$
24	23	nn0absidi	$⊢ \|3\| = 3$
25	22 24	eqtri	$⊢ \|2 - -1\| = 3$
26		3nn	$⊢ 3 \in ℕ$
27	26	a1i	$⊢ N \in ℤ_{\geq 5} \to 3 \in ℕ$
28		eluz2	$⊢ N \in ℤ_{\geq 5} \leftrightarrow (5 \in ℤ \land N \in ℤ \land 5 \leq N)$
29		3re	$⊢ 3 \in ℝ$
30	29	a1i	$⊢ (N \in ℤ \land 5 \leq N) \to 3 \in ℝ$
31		5re	$⊢ 5 \in ℝ$
32	31	a1i	$⊢ (N \in ℤ \land 5 \leq N) \to 5 \in ℝ$
33		zre	$⊢ N \in ℤ \to N \in ℝ$
34	33	adantr	$⊢ (N \in ℤ \land 5 \leq N) \to N \in ℝ$
35		3lt5	$⊢ 3 < 5$
36	35	a1i	$⊢ (N \in ℤ \land 5 \leq N) \to 3 < 5$
37		simpr	$⊢ (N \in ℤ \land 5 \leq N) \to 5 \leq N$
38	30 32 34 36 37	ltletrd	$⊢ (N \in ℤ \land 5 \leq N) \to 3 < N$
39	38	3adant1	$⊢ (5 \in ℤ \land N \in ℤ \land 5 \leq N) \to 3 < N$
40	28 39	sylbi	$⊢ N \in ℤ_{\geq 5} \to 3 < N$
41		elfzo1	$⊢ 3 \in (1 ..^N) \leftrightarrow (3 \in ℕ \land N \in ℕ \land 3 < N)$
42	27 10 40 41	syl3anbrc	$⊢ N \in ℤ_{\geq 5} \to 3 \in (1 ..^N)$
43	42	adantr	$⊢ (N \in ℤ_{\geq 5} \land Y \in I) \to 3 \in (1 ..^N)$
44	25 43	eqeltrid	$⊢ (N \in ℤ_{\geq 5} \land Y \in I) \to \|2 - -1\| \in (1 ..^N)$
45	1	mod2addne	$⊢ (N \in ℕ \land (Y \in I \land 2 \in ℤ \land - 1 \in ℤ) \land \|2 - -1\| \in (1 ..^N)) \to (Y + 2) \mod N \neq (Y + -1) \mod N$
46	11 12 14 16 44 45	syl131anc	$⊢ (N \in ℤ_{\geq 5} \land Y \in I) \to (Y + 2) \mod N \neq (Y + -1) \mod N$
47	46	necomd	$⊢ (N \in ℤ_{\geq 5} \land Y \in I) \to (Y + -1) \mod N \neq (Y + 2) \mod N$
48	9 47	eqnetrd	$⊢ (N \in ℤ_{\geq 5} \land Y \in I) \to (Y - 1) \mod N \neq (Y + 2) \mod N$

Metamath Proof Explorer

Theorem modm1nep2

Proof