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	|- ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ ) -> ( ( A + 1 ) mod N ) =/= ( A mod N ) )

Proof

Step	Hyp	Ref	Expression
1		fzo1lb	|- ( 1 e. ( 1 ..^ N ) <-> N e. ( ZZ>= ` 2 ) )
2	1	biimpri	|- ( N e. ( ZZ>= ` 2 ) -> 1 e. ( 1 ..^ N ) )
3	2	adantr	|- ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ ) -> 1 e. ( 1 ..^ N ) )
4		zplusmodne	|- ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ 1 e. ( 1 ..^ N ) ) -> ( ( A + 1 ) mod N ) =/= ( A mod N ) )
5	3 4	mpd3an3	|- ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ ) -> ( ( A + 1 ) mod N ) =/= ( A mod N ) )