submodaddmod

Description: Subtraction and addition modulo a positive integer. (Contributed by AV, 7-Sep-2025)

		Ref	Expression
	Assertion	submodaddmod	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ \land C \in ℤ)) \to ((A + B) \mod N = (A - C) \mod N \leftrightarrow (A + B + C) \mod N = A \mod N)$

Proof

Step	Hyp	Ref	Expression
1		zcn	$⊢ A \in ℤ \to A \in ℂ$
2	1	3ad2ant1	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to A \in ℂ$
3	2	adantl	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ \land C \in ℤ)) \to A \in ℂ$
4		zcn	$⊢ B \in ℤ \to B \in ℂ$
5	4	3ad2ant2	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to B \in ℂ$
6	5	adantl	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ \land C \in ℤ)) \to B \in ℂ$
7		zcn	$⊢ C \in ℤ \to C \in ℂ$
8	7	3ad2ant3	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to C \in ℂ$
9	8	adantl	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ \land C \in ℤ)) \to C \in ℂ$
10	3 6 9	pnncand	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ \land C \in ℤ)) \to A + B - (A - C) = B + C$
11		zaddcl	$⊢ (B \in ℤ \land C \in ℤ) \to B + C \in ℤ$
12	11	zcnd	$⊢ (B \in ℤ \land C \in ℤ) \to B + C \in ℂ$
13	12	3adant1	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to B + C \in ℂ$
14	13	adantl	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ \land C \in ℤ)) \to B + C \in ℂ$
15	3 14	pncan2d	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ \land C \in ℤ)) \to A + (B + C) - A = B + C$
16	10 15	eqtr4d	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ \land C \in ℤ)) \to A + B - (A - C) = A + (B + C) - A$
17	16	breq2d	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ \land C \in ℤ)) \to (N ∥ (A + B - (A - C)) \leftrightarrow N ∥ (A + (B + C) - A))$
18		simpl	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ \land C \in ℤ)) \to N \in ℕ$
19		zaddcl	$⊢ (A \in ℤ \land B \in ℤ) \to A + B \in ℤ$
20	19	3adant3	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to A + B \in ℤ$
21	20	adantl	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ \land C \in ℤ)) \to A + B \in ℤ$
22		zsubcl	$⊢ (A \in ℤ \land C \in ℤ) \to A - C \in ℤ$
23	22	3adant2	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to A - C \in ℤ$
24	23	adantl	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ \land C \in ℤ)) \to A - C \in ℤ$
25		moddvds	$⊢ (N \in ℕ \land A + B \in ℤ \land A - C \in ℤ) \to ((A + B) \mod N = (A - C) \mod N \leftrightarrow N ∥ (A + B - (A - C)))$
26	18 21 24 25	syl3anc	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ \land C \in ℤ)) \to ((A + B) \mod N = (A - C) \mod N \leftrightarrow N ∥ (A + B - (A - C)))$
27		simp1	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to A \in ℤ$
28		simp2	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to B \in ℤ$
29		simp3	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to C \in ℤ$
30	28 29	zaddcld	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to B + C \in ℤ$
31	27 30	zaddcld	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to A + B + C \in ℤ$
32	31	adantl	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ \land C \in ℤ)) \to A + B + C \in ℤ$
33		simpr1	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ \land C \in ℤ)) \to A \in ℤ$
34		moddvds	$⊢ (N \in ℕ \land A + B + C \in ℤ \land A \in ℤ) \to ((A + B + C) \mod N = A \mod N \leftrightarrow N ∥ (A + (B + C) - A))$
35	18 32 33 34	syl3anc	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ \land C \in ℤ)) \to ((A + B + C) \mod N = A \mod N \leftrightarrow N ∥ (A + (B + C) - A))$
36	17 26 35	3bitr4d	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ \land C \in ℤ)) \to ((A + B) \mod N = (A - C) \mod N \leftrightarrow (A + B + C) \mod N = A \mod N)$

Metamath Proof Explorer

Theorem submodaddmod

Proof