Theorem plusmod5ne

Description: A nonnegative integer is not itself plus a positive integer less than 5 modulo 5. (Contributed by AV, 6-Sep-2025)

	Ref	Expression
Assertion	plusmod5ne	|- ( ( A e. ( 0 ..^ 5 ) /\ K e. ( 1 ..^ 5 ) ) -> ( ( A + K ) mod 5 ) =/= A )

Proof

Step	Hyp	Ref	Expression
1		5nn	|- 5 e. NN
2		elfzo0	|- ( A e. ( 0 ..^ 5 ) <-> ( A e. NN0 /\ 5 e. NN /\ A < 5 ) )
3		3simpb	|- ( ( A e. NN0 /\ 5 e. NN /\ A < 5 ) -> ( A e. NN0 /\ A < 5 ) )
4	2 3	sylbi	|- ( A e. ( 0 ..^ 5 ) -> ( A e. NN0 /\ A < 5 ) )
5		elfzo1	|- ( K e. ( 1 ..^ 5 ) <-> ( K e. NN /\ 5 e. NN /\ K < 5 ) )
6		3simpb	|- ( ( K e. NN /\ 5 e. NN /\ K < 5 ) -> ( K e. NN /\ K < 5 ) )
7	5 6	sylbi	|- ( K e. ( 1 ..^ 5 ) -> ( K e. NN /\ K < 5 ) )
8		addmodne	|- ( ( 5 e. NN /\ ( A e. NN0 /\ A < 5 ) /\ ( K e. NN /\ K < 5 ) ) -> ( ( A + K ) mod 5 ) =/= A )
9	1 4 7 8	mp3an3an	|- ( ( A e. ( 0 ..^ 5 ) /\ K e. ( 1 ..^ 5 ) ) -> ( ( A + K ) mod 5 ) =/= A )