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 ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ 1 ≤ B + C ∧ B + C < N → A + B mod N ≠ A − C mod N

Proof

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