Metamath Proof Explorer

Theorem minusmodnep2tmod

Description: A nonnegative integer minus a positive integer 1 or 2 is not itself plus 2 times the positive integer modulo 5. (Contributed by AV, 8-Sep-2025)

Ref Expression
Assertion minusmodnep2tmod ⊢ A ∈ ℤ ∧ B ∈ 1 ..^ 3 → A − B mod 5 ≠ A + 2 ⁢ B mod 5

Proof

Step Hyp Ref Expression
1 elpri ⊢ B ∈ 1 2 → B = 1 ∨ B = 2
2 5ndvds3 ⊢ ¬ 5 ∥ 3
3 oveq2 ⊢ B = 1 → 3 ⁢ B = 3 ⋅ 1
4 3t1e3 ⊢ 3 ⋅ 1 = 3
5 3 4 eqtrdi ⊢ B = 1 → 3 ⁢ B = 3
6 5 breq2d ⊢ B = 1 → 5 ∥ 3 ⁢ B ↔ 5 ∥ 3
7 2 6 mtbiri ⊢ B = 1 → ¬ 5 ∥ 3 ⁢ B
8 5ndvds6 ⊢ ¬ 5 ∥ 6
9 oveq2 ⊢ B = 2 → 3 ⁢ B = 3 ⋅ 2
10 3t2e6 ⊢ 3 ⋅ 2 = 6
11 9 10 eqtrdi ⊢ B = 2 → 3 ⁢ B = 6
12 11 breq2d ⊢ B = 2 → 5 ∥ 3 ⁢ B ↔ 5 ∥ 6
13 8 12 mtbiri ⊢ B = 2 → ¬ 5 ∥ 3 ⁢ B
14 7 13 jaoi ⊢ B = 1 ∨ B = 2 → ¬ 5 ∥ 3 ⁢ B
15 1 14 syl ⊢ B ∈ 1 2 → ¬ 5 ∥ 3 ⁢ B
16 fzo13pr ⊢ 1 ..^ 3 = 1 2
17 15 16 eleq2s ⊢ B ∈ 1 ..^ 3 → ¬ 5 ∥ 3 ⁢ B
18 17 adantl ⊢ A ∈ ℤ ∧ B ∈ 1 ..^ 3 → ¬ 5 ∥ 3 ⁢ B
19 5nn ⊢ 5 ∈ ℕ
20 19 a1i ⊢ A ∈ ℤ ∧ B ∈ 1 ..^ 3 → 5 ∈ ℕ
21 simpl ⊢ A ∈ ℤ ∧ B ∈ 1 ..^ 3 → A ∈ ℤ
22 2z ⊢ 2 ∈ ℤ
23 22 a1i ⊢ A ∈ ℤ ∧ B ∈ 1 ..^ 3 → 2 ∈ ℤ
24 elfzoelz ⊢ B ∈ 1 ..^ 3 → B ∈ ℤ
25 24 adantl ⊢ A ∈ ℤ ∧ B ∈ 1 ..^ 3 → B ∈ ℤ
26 23 25 zmulcld ⊢ A ∈ ℤ ∧ B ∈ 1 ..^ 3 → 2 ⁢ B ∈ ℤ
27 submodaddmod ⊢ 5 ∈ ℕ ∧ A ∈ ℤ ∧ 2 ⁢ B ∈ ℤ ∧ B ∈ ℤ → A + 2 ⁢ B mod 5 = A − B mod 5 ↔ A + 2 ⁢ B + B mod 5 = A mod 5
28 20 21 26 25 27 syl13anc ⊢ A ∈ ℤ ∧ B ∈ 1 ..^ 3 → A + 2 ⁢ B mod 5 = A − B mod 5 ↔ A + 2 ⁢ B + B mod 5 = A mod 5
29 2cnd ⊢ B ∈ 1 ..^ 3 → 2 ∈ ℂ
30 24 zcnd ⊢ B ∈ 1 ..^ 3 → B ∈ ℂ
31 29 30 adddirp1d ⊢ B ∈ 1 ..^ 3 → 2 + 1 ⁢ B = 2 ⁢ B + B
32 31 eqcomd ⊢ B ∈ 1 ..^ 3 → 2 ⁢ B + B = 2 + 1 ⁢ B
33 32 adantl ⊢ A ∈ ℤ ∧ B ∈ 1 ..^ 3 → 2 ⁢ B + B = 2 + 1 ⁢ B
34 2p1e3 ⊢ 2 + 1 = 3
35 34 oveq1i ⊢ 2 + 1 ⁢ B = 3 ⁢ B
36 33 35 eqtrdi ⊢ A ∈ ℤ ∧ B ∈ 1 ..^ 3 → 2 ⁢ B + B = 3 ⁢ B
37 36 oveq2d ⊢ A ∈ ℤ ∧ B ∈ 1 ..^ 3 → A + 2 ⁢ B + B = A + 3 ⁢ B
38 37 oveq1d ⊢ A ∈ ℤ ∧ B ∈ 1 ..^ 3 → A + 2 ⁢ B + B mod 5 = A + 3 ⁢ B mod 5
39 38 eqeq1d ⊢ A ∈ ℤ ∧ B ∈ 1 ..^ 3 → A + 2 ⁢ B + B mod 5 = A mod 5 ↔ A + 3 ⁢ B mod 5 = A mod 5
40 28 39 bitrd ⊢ A ∈ ℤ ∧ B ∈ 1 ..^ 3 → A + 2 ⁢ B mod 5 = A − B mod 5 ↔ A + 3 ⁢ B mod 5 = A mod 5
41 eqcom ⊢ A − B mod 5 = A + 2 ⁢ B mod 5 ↔ A + 2 ⁢ B mod 5 = A − B mod 5
42 41 a1i ⊢ A ∈ ℤ ∧ B ∈ 1 ..^ 3 → A − B mod 5 = A + 2 ⁢ B mod 5 ↔ A + 2 ⁢ B mod 5 = A − B mod 5
43 3z ⊢ 3 ∈ ℤ
44 43 a1i ⊢ A ∈ ℤ ∧ B ∈ 1 ..^ 3 → 3 ∈ ℤ
45 addmulmodb ⊢ 5 ∈ ℕ ∧ A ∈ ℤ ∧ 3 ∈ ℤ ∧ B ∈ ℤ → 5 ∥ 3 ⁢ B ↔ A + 3 ⁢ B mod 5 = A mod 5
46 20 21 44 25 45 syl13anc ⊢ A ∈ ℤ ∧ B ∈ 1 ..^ 3 → 5 ∥ 3 ⁢ B ↔ A + 3 ⁢ B mod 5 = A mod 5
47 40 42 46 3bitr4d ⊢ A ∈ ℤ ∧ B ∈ 1 ..^ 3 → A − B mod 5 = A + 2 ⁢ B mod 5 ↔ 5 ∥ 3 ⁢ B
48 18 47 mtbird ⊢ A ∈ ℤ ∧ B ∈ 1 ..^ 3 → ¬ A − B mod 5 = A + 2 ⁢ B mod 5
49 48 neqned ⊢ A ∈ ℤ ∧ B ∈ 1 ..^ 3 → A − B mod 5 ≠ A + 2 ⁢ B mod 5