m1modnep2mod

Description: A nonnegative integer minus 1 is not itself plus 2 modulo an integer greater than 3 and the nonnegative integer. (Contributed by AV, 6-Sep-2025)

		Ref	Expression
	Assertion	m1modnep2mod	$⊢ (N \in ℤ_{\geq 4} \land A \in ℤ) \to (A - 1) \mod N \neq (A + 2) \mod N$

Proof

Step	Hyp	Ref	Expression
1		eluz4nn	$⊢ N \in ℤ_{\geq 4} \to N \in ℕ$
2	1	adantr	$⊢ (N \in ℤ_{\geq 4} \land A \in ℤ) \to N \in ℕ$
3		simpr	$⊢ (N \in ℤ_{\geq 4} \land A \in ℤ) \to A \in ℤ$
4		2z	$⊢ 2 \in ℤ$
5	4	a1i	$⊢ (N \in ℤ_{\geq 4} \land A \in ℤ) \to 2 \in ℤ$
6		1zzd	$⊢ (N \in ℤ_{\geq 4} \land A \in ℤ) \to 1 \in ℤ$
7		1le3	$⊢ 1 \leq 3$
8		2p1e3	$⊢ 2 + 1 = 3$
9	7 8	breqtrri	$⊢ 1 \leq 2 + 1$
10	9	a1i	$⊢ (N \in ℤ_{\geq 4} \land A \in ℤ) \to 1 \leq 2 + 1$
11		eluz2	$⊢ N \in ℤ_{\geq 4} \leftrightarrow (4 \in ℤ \land N \in ℤ \land 4 \leq N)$
12		df-4	$⊢ 4 = 3 + 1$
13	12	breq1i	$⊢ 4 \leq N \leftrightarrow 3 + 1 \leq N$
14		3z	$⊢ 3 \in ℤ$
15	14	a1i	$⊢ 4 \in ℤ \to 3 \in ℤ$
16		zltp1le	$⊢ (3 \in ℤ \land N \in ℤ) \to (3 < N \leftrightarrow 3 + 1 \leq N)$
17	15 16	sylan	$⊢ (4 \in ℤ \land N \in ℤ) \to (3 < N \leftrightarrow 3 + 1 \leq N)$
18	17	biimprd	$⊢ (4 \in ℤ \land N \in ℤ) \to (3 + 1 \leq N \to 3 < N)$
19	13 18	biimtrid	$⊢ (4 \in ℤ \land N \in ℤ) \to (4 \leq N \to 3 < N)$
20	19	3impia	$⊢ (4 \in ℤ \land N \in ℤ \land 4 \leq N) \to 3 < N$
21	11 20	sylbi	$⊢ N \in ℤ_{\geq 4} \to 3 < N$
22	8 21	eqbrtrid	$⊢ N \in ℤ_{\geq 4} \to 2 + 1 < N$
23	22	adantr	$⊢ (N \in ℤ_{\geq 4} \land A \in ℤ) \to 2 + 1 < N$
24		submodneaddmod	$⊢ (N \in ℕ \land (A \in ℤ \land 2 \in ℤ \land 1 \in ℤ) \land (1 \leq 2 + 1 \land 2 + 1 < N)) \to (A + 2) \mod N \neq (A - 1) \mod N$
25	2 3 5 6 10 23 24	syl132anc	$⊢ (N \in ℤ_{\geq 4} \land A \in ℤ) \to (A + 2) \mod N \neq (A - 1) \mod N$
26	25	necomd	$⊢ (N \in ℤ_{\geq 4} \land A \in ℤ) \to (A - 1) \mod N \neq (A + 2) \mod N$

Metamath Proof Explorer

Theorem m1modnep2mod

Proof