modaddb

Description: Addition property of the modulo operation. Biconditional version of modadd1 by applying modadd1 twice. (Contributed by AV, 14-Nov-2025)

		Ref	Expression
	Assertion	modaddb	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to (A \mod D = B \mod D \leftrightarrow (A + C) \mod D = (B + C) \mod D)$

Proof

Step	Hyp	Ref	Expression
1		modadd1	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+}) \land A \mod D = B \mod D) \to (A + C) \mod D = (B + C) \mod D$
2	1	3expa	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \land A \mod D = B \mod D) \to (A + C) \mod D = (B + C) \mod D$
3		simpll	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to A \in ℝ$
4		simprl	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to C \in ℝ$
5	3 4	readdcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to A + C \in ℝ$
6		simplr	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to B \in ℝ$
7	6 4	readdcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to B + C \in ℝ$
8	5 7	jca	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to (A + C \in ℝ \land B + C \in ℝ)$
9	8	adantr	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \land (A + C) \mod D = (B + C) \mod D) \to (A + C \in ℝ \land B + C \in ℝ)$
10		renegcl	$⊢ C \in ℝ \to - C \in ℝ$
11	10	anim1i	$⊢ (C \in ℝ \land D \in ℝ^{+}) \to (- C \in ℝ \land D \in ℝ^{+})$
12	11	adantl	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to (- C \in ℝ \land D \in ℝ^{+})$
13	12	adantr	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \land (A + C) \mod D = (B + C) \mod D) \to (- C \in ℝ \land D \in ℝ^{+})$
14		simpr	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \land (A + C) \mod D = (B + C) \mod D) \to (A + C) \mod D = (B + C) \mod D$
15		modadd1	$⊢ ((A + C \in ℝ \land B + C \in ℝ) \land (- C \in ℝ \land D \in ℝ^{+}) \land (A + C) \mod D = (B + C) \mod D) \to (A + C + (- C)) \mod D = (B + C + (- C)) \mod D$
16	9 13 14 15	syl3anc	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \land (A + C) \mod D = (B + C) \mod D) \to (A + C + (- C)) \mod D = (B + C + (- C)) \mod D$
17		simpl	$⊢ (A \in ℝ \land B \in ℝ) \to A \in ℝ$
18	17	recnd	$⊢ (A \in ℝ \land B \in ℝ) \to A \in ℂ$
19	18	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to A \in ℂ$
20		simpl	$⊢ (C \in ℝ \land D \in ℝ^{+}) \to C \in ℝ$
21	20	recnd	$⊢ (C \in ℝ \land D \in ℝ^{+}) \to C \in ℂ$
22	21	adantl	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to C \in ℂ$
23	19 22	addcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to A + C \in ℂ$
24	23 22	negsubd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to A + C + (- C) = A + C - C$
25	19 22	pncand	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to A + C - C = A$
26	24 25	eqtr2d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to A = A + C + (- C)$
27	26	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to A \mod D = (A + C + (- C)) \mod D$
28		simpr	$⊢ (A \in ℝ \land B \in ℝ) \to B \in ℝ$
29	28	recnd	$⊢ (A \in ℝ \land B \in ℝ) \to B \in ℂ$
30	29	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to B \in ℂ$
31	30 22	addcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to B + C \in ℂ$
32	31 22	negsubd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to B + C + (- C) = B + C - C$
33	30 22	pncand	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to B + C - C = B$
34	32 33	eqtr2d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to B = B + C + (- C)$
35	34	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to B \mod D = (B + C + (- C)) \mod D$
36	27 35	eqeq12d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to (A \mod D = B \mod D \leftrightarrow (A + C + (- C)) \mod D = (B + C + (- C)) \mod D)$
37	36	adantr	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \land (A + C) \mod D = (B + C) \mod D) \to (A \mod D = B \mod D \leftrightarrow (A + C + (- C)) \mod D = (B + C + (- C)) \mod D)$
38	16 37	mpbird	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \land (A + C) \mod D = (B + C) \mod D) \to A \mod D = B \mod D$
39	2 38	impbida	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ^{+})) \to (A \mod D = B \mod D \leftrightarrow (A + C) \mod D = (B + C) \mod D)$

Metamath Proof Explorer

Theorem modaddb

Proof