modm2nep1

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	modm2nep1	$⊢ (N \in ℤ_{\geq 5} \land Y \in I) \to (Y - 2) \mod N \neq (Y + 1) \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		2cnd	$⊢ Y \in I \to 2 \in ℂ$
6	4 5	negsubd	$⊢ Y \in I \to Y + -2 = Y - 2$
7	6	adantl	$⊢ (N \in ℤ_{\geq 5} \land Y \in I) \to Y + -2 = Y - 2$
8	7	eqcomd	$⊢ (N \in ℤ_{\geq 5} \land Y \in I) \to Y - 2 = Y + -2$
9	8	oveq1d	$⊢ (N \in ℤ_{\geq 5} \land Y \in I) \to (Y - 2) \mod N = (Y + -2) \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		1zzd	$⊢ (N \in ℤ_{\geq 5} \land Y \in I) \to 1 \in ℤ$
14		2z	$⊢ 2 \in ℤ$
15	14	a1i	$⊢ (N \in ℤ_{\geq 5} \land Y \in I) \to 2 \in ℤ$
16	15	znegcld	$⊢ (N \in ℤ_{\geq 5} \land Y \in I) \to - 2 \in ℤ$
17		ax-1cn	$⊢ 1 \in ℂ$
18		2cn	$⊢ 2 \in ℂ$
19	17 18	subnegi	$⊢ 1 - -2 = 1 + 2$
20		1p2e3	$⊢ 1 + 2 = 3$
21	19 20	eqtri	$⊢ 1 - -2 = 3$
22	21	fveq2i	$⊢ \|1 - -2\| = \|3\|$
23		3nn0	$⊢ 3 \in ℕ_{0}$
24	23	nn0absidi	$⊢ \|3\| = 3$
25	22 24	eqtri	$⊢ \|1 - -2\| = 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 \|1 - -2\| \in (1 ..^N)$
45	1	mod2addne	$⊢ (N \in ℕ \land (Y \in I \land 1 \in ℤ \land - 2 \in ℤ) \land \|1 - -2\| \in (1 ..^N)) \to (Y + 1) \mod N \neq (Y + -2) \mod N$
46	11 12 13 16 44 45	syl131anc	$⊢ (N \in ℤ_{\geq 5} \land Y \in I) \to (Y + 1) \mod N \neq (Y + -2) \mod N$
47	46	necomd	$⊢ (N \in ℤ_{\geq 5} \land Y \in I) \to (Y + -2) \mod N \neq (Y + 1) \mod N$
48	9 47	eqnetrd	$⊢ (N \in ℤ_{\geq 5} \land Y \in I) \to (Y - 2) \mod N \neq (Y + 1) \mod N$

Metamath Proof Explorer

Theorem modm2nep1

Proof