modm1nem2

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

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

Metamath Proof Explorer

Theorem modm1nem2

Proof