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 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( 1 ..^ 3 ) ) → ( ( 𝐴 − 𝐵 ) mod 5 ) ≠ ( ( 𝐴 + ( 2 · 𝐵 ) ) mod 5 ) )

Proof

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