Metamath Proof Explorer

Theorem submodneaddmod

Description: An integer minus B is not itself plus C modulo an integer greater than the sum of B and C . (Contributed by AV, 6-Sep-2025)

Ref Expression
Assertion submodneaddmod ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 1 ≤ ( 𝐵 + 𝐶 ) ∧ ( 𝐵 + 𝐶 ) < 𝑁 ) ) → ( ( 𝐴 + 𝐵 ) mod 𝑁 ) ≠ ( ( 𝐴 − 𝐶 ) mod 𝑁 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 1 ≤ ( 𝐵 + 𝐶 ) ∧ ( 𝐵 + 𝐶 ) < 𝑁 ) ) → 𝑁 ∈ ℕ )
2 zaddcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 + 𝐵 ) ∈ ℤ )
3 2 3adant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 + 𝐵 ) ∈ ℤ )
4 zsubcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 − 𝐶 ) ∈ ℤ )
5 4 3adant2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 − 𝐶 ) ∈ ℤ )
6 3 5 jca ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( 𝐴 + 𝐵 ) ∈ ℤ ∧ ( 𝐴 − 𝐶 ) ∈ ℤ ) )
7 6 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 1 ≤ ( 𝐵 + 𝐶 ) ∧ ( 𝐵 + 𝐶 ) < 𝑁 ) ) → ( ( 𝐴 + 𝐵 ) ∈ ℤ ∧ ( 𝐴 − 𝐶 ) ∈ ℤ ) )
8 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
9 8 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐴 ∈ ℂ )
10 9 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 1 ≤ ( 𝐵 + 𝐶 ) ∧ ( 𝐵 + 𝐶 ) < 𝑁 ) ) → 𝐴 ∈ ℂ )
11 zcn ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
12 11 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐵 ∈ ℂ )
13 12 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 1 ≤ ( 𝐵 + 𝐶 ) ∧ ( 𝐵 + 𝐶 ) < 𝑁 ) ) → 𝐵 ∈ ℂ )
14 zcn ⊢ ( 𝐶 ∈ ℤ → 𝐶 ∈ ℂ )
15 14 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐶 ∈ ℂ )
16 15 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 1 ≤ ( 𝐵 + 𝐶 ) ∧ ( 𝐵 + 𝐶 ) < 𝑁 ) ) → 𝐶 ∈ ℂ )
17 10 13 16 pnncand ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 1 ≤ ( 𝐵 + 𝐶 ) ∧ ( 𝐵 + 𝐶 ) < 𝑁 ) ) → ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) = ( 𝐵 + 𝐶 ) )
18 simpl3l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 1 ≤ ( 𝐵 + 𝐶 ) ∧ ( 𝐵 + 𝐶 ) < 𝑁 ) ) ∧ ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) = ( 𝐵 + 𝐶 ) ) → 1 ≤ ( 𝐵 + 𝐶 ) )
19 breq2 ⊢ ( ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) = ( 𝐵 + 𝐶 ) → ( 1 ≤ ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) ↔ 1 ≤ ( 𝐵 + 𝐶 ) ) )
20 19 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 1 ≤ ( 𝐵 + 𝐶 ) ∧ ( 𝐵 + 𝐶 ) < 𝑁 ) ) ∧ ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) = ( 𝐵 + 𝐶 ) ) → ( 1 ≤ ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) ↔ 1 ≤ ( 𝐵 + 𝐶 ) ) )
21 18 20 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 1 ≤ ( 𝐵 + 𝐶 ) ∧ ( 𝐵 + 𝐶 ) < 𝑁 ) ) ∧ ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) = ( 𝐵 + 𝐶 ) ) → 1 ≤ ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) )
22 simpl3r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 1 ≤ ( 𝐵 + 𝐶 ) ∧ ( 𝐵 + 𝐶 ) < 𝑁 ) ) ∧ ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) = ( 𝐵 + 𝐶 ) ) → ( 𝐵 + 𝐶 ) < 𝑁 )
23 breq1 ⊢ ( ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) = ( 𝐵 + 𝐶 ) → ( ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) < 𝑁 ↔ ( 𝐵 + 𝐶 ) < 𝑁 ) )
24 23 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 1 ≤ ( 𝐵 + 𝐶 ) ∧ ( 𝐵 + 𝐶 ) < 𝑁 ) ) ∧ ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) = ( 𝐵 + 𝐶 ) ) → ( ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) < 𝑁 ↔ ( 𝐵 + 𝐶 ) < 𝑁 ) )
25 22 24 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 1 ≤ ( 𝐵 + 𝐶 ) ∧ ( 𝐵 + 𝐶 ) < 𝑁 ) ) ∧ ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) = ( 𝐵 + 𝐶 ) ) → ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) < 𝑁 )
26 21 25 jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 1 ≤ ( 𝐵 + 𝐶 ) ∧ ( 𝐵 + 𝐶 ) < 𝑁 ) ) ∧ ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) = ( 𝐵 + 𝐶 ) ) → ( 1 ≤ ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) ∧ ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) < 𝑁 ) )
27 17 26 mpdan ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 1 ≤ ( 𝐵 + 𝐶 ) ∧ ( 𝐵 + 𝐶 ) < 𝑁 ) ) → ( 1 ≤ ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) ∧ ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) < 𝑁 ) )
28 difltmodne ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 + 𝐵 ) ∈ ℤ ∧ ( 𝐴 − 𝐶 ) ∈ ℤ ) ∧ ( 1 ≤ ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) ∧ ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) < 𝑁 ) ) → ( ( 𝐴 + 𝐵 ) mod 𝑁 ) ≠ ( ( 𝐴 − 𝐶 ) mod 𝑁 ) )
29 1 7 27 28 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 1 ≤ ( 𝐵 + 𝐶 ) ∧ ( 𝐵 + 𝐶 ) < 𝑁 ) ) → ( ( 𝐴 + 𝐵 ) mod 𝑁 ) ≠ ( ( 𝐴 − 𝐶 ) mod 𝑁 ) )