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 ⊢ A ∈ 0 ..^ 5 ∧ K ∈ 1 ..^ 5 → A − K mod 5 ≠ A

Proof

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