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	⊢ ( ( 𝐴 ∈ ( 0 ..^ 5 ) ∧ 𝐾 ∈ ( 1 ..^ 5 ) ) → ( ( 𝐴 + 𝐾 ) mod 5 ) ≠ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		5nn	⊢ 5 ∈ ℕ
2		elfzo0	⊢ ( 𝐴 ∈ ( 0 ..^ 5 ) ↔ ( 𝐴 ∈ ℕ0 ∧ 5 ∈ ℕ ∧ 𝐴 < 5 ) )
3		3simpb	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 5 ∈ ℕ ∧ 𝐴 < 5 ) → ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 5 ) )
4	2 3	sylbi	⊢ ( 𝐴 ∈ ( 0 ..^ 5 ) → ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 5 ) )
5		elfzo1	⊢ ( 𝐾 ∈ ( 1 ..^ 5 ) ↔ ( 𝐾 ∈ ℕ ∧ 5 ∈ ℕ ∧ 𝐾 < 5 ) )
6		3simpb	⊢ ( ( 𝐾 ∈ ℕ ∧ 5 ∈ ℕ ∧ 𝐾 < 5 ) → ( 𝐾 ∈ ℕ ∧ 𝐾 < 5 ) )
7	5 6	sylbi	⊢ ( 𝐾 ∈ ( 1 ..^ 5 ) → ( 𝐾 ∈ ℕ ∧ 𝐾 < 5 ) )
8		addmodne	⊢ ( ( 5 ∈ ℕ ∧ ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 5 ) ∧ ( 𝐾 ∈ ℕ ∧ 𝐾 < 5 ) ) → ( ( 𝐴 + 𝐾 ) mod 5 ) ≠ 𝐴 )
9	1 4 7 8	mp3an3an	⊢ ( ( 𝐴 ∈ ( 0 ..^ 5 ) ∧ 𝐾 ∈ ( 1 ..^ 5 ) ) → ( ( 𝐴 + 𝐾 ) mod 5 ) ≠ 𝐴 )