Theorem p1modne

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

	Ref	Expression
Assertion	p1modne	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐴 + 1 ) mod 𝑁 ) ≠ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elfzoelz	⊢ ( 𝐴 ∈ ( 0 ..^ 𝑁 ) → 𝐴 ∈ ℤ )
2		zp1modne	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 + 1 ) mod 𝑁 ) ≠ ( 𝐴 mod 𝑁 ) )
3	1 2	sylan2	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐴 + 1 ) mod 𝑁 ) ≠ ( 𝐴 mod 𝑁 ) )
4		zmodidfzoimp	⊢ ( 𝐴 ∈ ( 0 ..^ 𝑁 ) → ( 𝐴 mod 𝑁 ) = 𝐴 )
5	4	adantl	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 mod 𝑁 ) = 𝐴 )
6	3 5	neeqtrd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐴 + 1 ) mod 𝑁 ) ≠ 𝐴 )