Metamath Proof Explorer

Theorem minusmod5ne

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

Ref Expression
Assertion minusmod5ne ( ( 𝐴 ∈ ( 0 ..^ 5 ) ∧ 𝐾 ∈ ( 1 ..^ 5 ) ) → ( ( 𝐴 − 𝐾 ) mod 5 ) ≠ 𝐴 )

Proof

Step Hyp Ref Expression
1 5nn ⊢ 5 ∈ ℕ
2 1 a1i ⊢ ( ( 𝐴 ∈ ( 0 ..^ 5 ) ∧ 𝐾 ∈ ( 1 ..^ 5 ) ) → 5 ∈ ℕ )
3 elfzoelz ⊢ ( 𝐴 ∈ ( 0 ..^ 5 ) → 𝐴 ∈ ℤ )
4 3 adantr ⊢ ( ( 𝐴 ∈ ( 0 ..^ 5 ) ∧ 𝐾 ∈ ( 1 ..^ 5 ) ) → 𝐴 ∈ ℤ )
5 elfzoelz ⊢ ( 𝐾 ∈ ( 1 ..^ 5 ) → 𝐾 ∈ ℤ )
6 5 adantl ⊢ ( ( 𝐴 ∈ ( 0 ..^ 5 ) ∧ 𝐾 ∈ ( 1 ..^ 5 ) ) → 𝐾 ∈ ℤ )
7 4 6 zsubcld ⊢ ( ( 𝐴 ∈ ( 0 ..^ 5 ) ∧ 𝐾 ∈ ( 1 ..^ 5 ) ) → ( 𝐴 − 𝐾 ) ∈ ℤ )
8 3 zcnd ⊢ ( 𝐴 ∈ ( 0 ..^ 5 ) → 𝐴 ∈ ℂ )
9 5 zcnd ⊢ ( 𝐾 ∈ ( 1 ..^ 5 ) → 𝐾 ∈ ℂ )
10 nncan ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( 𝐴 − ( 𝐴 − 𝐾 ) ) = 𝐾 )
11 8 9 10 syl2an ⊢ ( ( 𝐴 ∈ ( 0 ..^ 5 ) ∧ 𝐾 ∈ ( 1 ..^ 5 ) ) → ( 𝐴 − ( 𝐴 − 𝐾 ) ) = 𝐾 )
12 elfzo1 ⊢ ( 𝐾 ∈ ( 1 ..^ 5 ) ↔ ( 𝐾 ∈ ℕ ∧ 5 ∈ ℕ ∧ 𝐾 < 5 ) )
13 nnge1 ⊢ ( 𝐾 ∈ ℕ → 1 ≤ 𝐾 )
14 13 anim1i ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐾 < 5 ) → ( 1 ≤ 𝐾 ∧ 𝐾 < 5 ) )
15 14 3adant2 ⊢ ( ( 𝐾 ∈ ℕ ∧ 5 ∈ ℕ ∧ 𝐾 < 5 ) → ( 1 ≤ 𝐾 ∧ 𝐾 < 5 ) )
16 12 15 sylbi ⊢ ( 𝐾 ∈ ( 1 ..^ 5 ) → ( 1 ≤ 𝐾 ∧ 𝐾 < 5 ) )
17 16 adantl ⊢ ( ( 𝐴 ∈ ( 0 ..^ 5 ) ∧ 𝐾 ∈ ( 1 ..^ 5 ) ) → ( 1 ≤ 𝐾 ∧ 𝐾 < 5 ) )
18 breq2 ⊢ ( ( 𝐴 − ( 𝐴 − 𝐾 ) ) = 𝐾 → ( 1 ≤ ( 𝐴 − ( 𝐴 − 𝐾 ) ) ↔ 1 ≤ 𝐾 ) )
19 breq1 ⊢ ( ( 𝐴 − ( 𝐴 − 𝐾 ) ) = 𝐾 → ( ( 𝐴 − ( 𝐴 − 𝐾 ) ) < 5 ↔ 𝐾 < 5 ) )
20 18 19 anbi12d ⊢ ( ( 𝐴 − ( 𝐴 − 𝐾 ) ) = 𝐾 → ( ( 1 ≤ ( 𝐴 − ( 𝐴 − 𝐾 ) ) ∧ ( 𝐴 − ( 𝐴 − 𝐾 ) ) < 5 ) ↔ ( 1 ≤ 𝐾 ∧ 𝐾 < 5 ) ) )
21 17 20 syl5ibrcom ⊢ ( ( 𝐴 ∈ ( 0 ..^ 5 ) ∧ 𝐾 ∈ ( 1 ..^ 5 ) ) → ( ( 𝐴 − ( 𝐴 − 𝐾 ) ) = 𝐾 → ( 1 ≤ ( 𝐴 − ( 𝐴 − 𝐾 ) ) ∧ ( 𝐴 − ( 𝐴 − 𝐾 ) ) < 5 ) ) )
22 11 21 mpd ⊢ ( ( 𝐴 ∈ ( 0 ..^ 5 ) ∧ 𝐾 ∈ ( 1 ..^ 5 ) ) → ( 1 ≤ ( 𝐴 − ( 𝐴 − 𝐾 ) ) ∧ ( 𝐴 − ( 𝐴 − 𝐾 ) ) < 5 ) )
23 difltmodne ⊢ ( ( 5 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ ( 𝐴 − 𝐾 ) ∈ ℤ ) ∧ ( 1 ≤ ( 𝐴 − ( 𝐴 − 𝐾 ) ) ∧ ( 𝐴 − ( 𝐴 − 𝐾 ) ) < 5 ) ) → ( 𝐴 mod 5 ) ≠ ( ( 𝐴 − 𝐾 ) mod 5 ) )
24 2 4 7 22 23 syl121anc ⊢ ( ( 𝐴 ∈ ( 0 ..^ 5 ) ∧ 𝐾 ∈ ( 1 ..^ 5 ) ) → ( 𝐴 mod 5 ) ≠ ( ( 𝐴 − 𝐾 ) mod 5 ) )
25 24 necomd ⊢ ( ( 𝐴 ∈ ( 0 ..^ 5 ) ∧ 𝐾 ∈ ( 1 ..^ 5 ) ) → ( ( 𝐴 − 𝐾 ) mod 5 ) ≠ ( 𝐴 mod 5 ) )
26 zmodidfzoimp ⊢ ( 𝐴 ∈ ( 0 ..^ 5 ) → ( 𝐴 mod 5 ) = 𝐴 )
27 26 adantr ⊢ ( ( 𝐴 ∈ ( 0 ..^ 5 ) ∧ 𝐾 ∈ ( 1 ..^ 5 ) ) → ( 𝐴 mod 5 ) = 𝐴 )
28 25 27 neeqtrd ⊢ ( ( 𝐴 ∈ ( 0 ..^ 5 ) ∧ 𝐾 ∈ ( 1 ..^ 5 ) ) → ( ( 𝐴 − 𝐾 ) mod 5 ) ≠ 𝐴 )