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 \in (0 ..^5) \land K \in (1 ..^5)) \to (A + K) \mod 5 \neq A$

Step	Hyp	Ref	Expression
1		5nn	$⊢ 5 \in ℕ$
2		elfzo0	$⊢ A \in (0 ..^5) \leftrightarrow (A \in ℕ_{0} \land 5 \in ℕ \land A < 5)$
3		3simpb	$⊢ (A \in ℕ_{0} \land 5 \in ℕ \land A < 5) \to (A \in ℕ_{0} \land A < 5)$
4	2 3	sylbi	$⊢ A \in (0 ..^5) \to (A \in ℕ_{0} \land A < 5)$
5		elfzo1	$⊢ K \in (1 ..^5) \leftrightarrow (K \in ℕ \land 5 \in ℕ \land K < 5)$
6		3simpb	$⊢ (K \in ℕ \land 5 \in ℕ \land K < 5) \to (K \in ℕ \land K < 5)$
7	5 6	sylbi	$⊢ K \in (1 ..^5) \to (K \in ℕ \land K < 5)$
8		addmodne	$⊢ (5 \in ℕ \land (A \in ℕ_{0} \land A < 5) \land (K \in ℕ \land K < 5)) \to (A + K) \mod 5 \neq A$
9	1 4 7 8	mp3an3an	$⊢ (A \in (0 ..^5) \land K \in (1 ..^5)) \to (A + K) \mod 5 \neq A$

Metamath Proof Explorer