Theorem 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	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 − 1 ) mod 𝑁 ) ≠ ( ( 𝐴 + 2 ) mod 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		eluz4nn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 𝑁 ∈ ℕ )
2	1	adantr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝐴 ∈ ℤ ) → 𝑁 ∈ ℕ )
3		simpr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝐴 ∈ ℤ ) → 𝐴 ∈ ℤ )
4		2z	⊢ 2 ∈ ℤ
5	4	a1i	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝐴 ∈ ℤ ) → 2 ∈ ℤ )
6		1zzd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝐴 ∈ ℤ ) → 1 ∈ ℤ )
7		1le3	⊢ 1 ≤ 3
8		2p1e3	⊢ ( 2 + 1 ) = 3
9	7 8	breqtrri	⊢ 1 ≤ ( 2 + 1 )
10	9	a1i	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝐴 ∈ ℤ ) → 1 ≤ ( 2 + 1 ) )
11		eluz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ↔ ( 4 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 4 ≤ 𝑁 ) )
12		df-4	⊢ 4 = ( 3 + 1 )
13	12	breq1i	⊢ ( 4 ≤ 𝑁 ↔ ( 3 + 1 ) ≤ 𝑁 )
14		3z	⊢ 3 ∈ ℤ
15	14	a1i	⊢ ( 4 ∈ ℤ → 3 ∈ ℤ )
16		zltp1le	⊢ ( ( 3 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 3 < 𝑁 ↔ ( 3 + 1 ) ≤ 𝑁 ) )
17	15 16	sylan	⊢ ( ( 4 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 3 < 𝑁 ↔ ( 3 + 1 ) ≤ 𝑁 ) )
18	17	biimprd	⊢ ( ( 4 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 3 + 1 ) ≤ 𝑁 → 3 < 𝑁 ) )
19	13 18	biimtrid	⊢ ( ( 4 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 4 ≤ 𝑁 → 3 < 𝑁 ) )
20	19	3impia	⊢ ( ( 4 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 4 ≤ 𝑁 ) → 3 < 𝑁 )
21	11 20	sylbi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 3 < 𝑁 )
22	8 21	eqbrtrid	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 2 + 1 ) < 𝑁 )
23	22	adantr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝐴 ∈ ℤ ) → ( 2 + 1 ) < 𝑁 )
24		submodneaddmod	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 2 ∈ ℤ ∧ 1 ∈ ℤ ) ∧ ( 1 ≤ ( 2 + 1 ) ∧ ( 2 + 1 ) < 𝑁 ) ) → ( ( 𝐴 + 2 ) mod 𝑁 ) ≠ ( ( 𝐴 − 1 ) mod 𝑁 ) )
25	2 3 5 6 10 23 24	syl132anc	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 + 2 ) mod 𝑁 ) ≠ ( ( 𝐴 − 1 ) mod 𝑁 ) )
26	25	necomd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 − 1 ) mod 𝑁 ) ≠ ( ( 𝐴 + 2 ) mod 𝑁 ) )