Theorem zp1modne

Description: An integer is not itself plus 1 modulo an integer greater than 1. (Contributed by AV, 6-Sep-2025)

	Ref	Expression
Assertion	zp1modne	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 + 1 ) mod 𝑁 ) ≠ ( 𝐴 mod 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		fzo1lb	⊢ ( 1 ∈ ( 1 ..^ 𝑁 ) ↔ 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
2	1	biimpri	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 ∈ ( 1 ..^ 𝑁 ) )
3	2	adantr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ) → 1 ∈ ( 1 ..^ 𝑁 ) )
4		zplusmodne	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 1 ∈ ( 1 ..^ 𝑁 ) ) → ( ( 𝐴 + 1 ) mod 𝑁 ) ≠ ( 𝐴 mod 𝑁 ) )
5	3 4	mpd3an3	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 + 1 ) mod 𝑁 ) ≠ ( 𝐴 mod 𝑁 ) )