Theorem 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	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ↔ ( ( 𝐴 + 𝐶 ) mod 𝐷 ) = ( ( 𝐵 + 𝐶 ) mod 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		modadd1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( 𝐴 + 𝐶 ) mod 𝐷 ) = ( ( 𝐵 + 𝐶 ) mod 𝐷 ) )
2	1	3expa	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( 𝐴 + 𝐶 ) mod 𝐷 ) = ( ( 𝐵 + 𝐶 ) mod 𝐷 ) )
3		simpll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐴 ∈ ℝ )
4		simprl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐶 ∈ ℝ )
5	3 4	readdcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( 𝐴 + 𝐶 ) ∈ ℝ )
6		simplr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐵 ∈ ℝ )
7	6 4	readdcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
8	5 7	jca	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 + 𝐶 ) ∈ ℝ ∧ ( 𝐵 + 𝐶 ) ∈ ℝ ) )
9	8	adantr	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) ∧ ( ( 𝐴 + 𝐶 ) mod 𝐷 ) = ( ( 𝐵 + 𝐶 ) mod 𝐷 ) ) → ( ( 𝐴 + 𝐶 ) ∈ ℝ ∧ ( 𝐵 + 𝐶 ) ∈ ℝ ) )
10		renegcl	⊢ ( 𝐶 ∈ ℝ → - 𝐶 ∈ ℝ )
11	10	anim1i	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( - 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) )
12	11	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( - 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) )
13	12	adantr	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) ∧ ( ( 𝐴 + 𝐶 ) mod 𝐷 ) = ( ( 𝐵 + 𝐶 ) mod 𝐷 ) ) → ( - 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) )
14		simpr	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) ∧ ( ( 𝐴 + 𝐶 ) mod 𝐷 ) = ( ( 𝐵 + 𝐶 ) mod 𝐷 ) ) → ( ( 𝐴 + 𝐶 ) mod 𝐷 ) = ( ( 𝐵 + 𝐶 ) mod 𝐷 ) )
15		modadd1	⊢ ( ( ( ( 𝐴 + 𝐶 ) ∈ ℝ ∧ ( 𝐵 + 𝐶 ) ∈ ℝ ) ∧ ( - 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ∧ ( ( 𝐴 + 𝐶 ) mod 𝐷 ) = ( ( 𝐵 + 𝐶 ) mod 𝐷 ) ) → ( ( ( 𝐴 + 𝐶 ) + - 𝐶 ) mod 𝐷 ) = ( ( ( 𝐵 + 𝐶 ) + - 𝐶 ) mod 𝐷 ) )
16	9 13 14 15	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) ∧ ( ( 𝐴 + 𝐶 ) mod 𝐷 ) = ( ( 𝐵 + 𝐶 ) mod 𝐷 ) ) → ( ( ( 𝐴 + 𝐶 ) + - 𝐶 ) mod 𝐷 ) = ( ( ( 𝐵 + 𝐶 ) + - 𝐶 ) mod 𝐷 ) )
17		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ )
18	17	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℂ )
19	18	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐴 ∈ ℂ )
20		simpl	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → 𝐶 ∈ ℝ )
21	20	recnd	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → 𝐶 ∈ ℂ )
22	21	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐶 ∈ ℂ )
23	19 22	addcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( 𝐴 + 𝐶 ) ∈ ℂ )
24	23 22	negsubd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 + 𝐶 ) + - 𝐶 ) = ( ( 𝐴 + 𝐶 ) − 𝐶 ) )
25	19 22	pncand	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 + 𝐶 ) − 𝐶 ) = 𝐴 )
26	24 25	eqtr2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐴 = ( ( 𝐴 + 𝐶 ) + - 𝐶 ) )
27	26	oveq1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( 𝐴 mod 𝐷 ) = ( ( ( 𝐴 + 𝐶 ) + - 𝐶 ) mod 𝐷 ) )
28		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
29	28	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℂ )
30	29	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐵 ∈ ℂ )
31	30 22	addcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( 𝐵 + 𝐶 ) ∈ ℂ )
32	31 22	negsubd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐵 + 𝐶 ) + - 𝐶 ) = ( ( 𝐵 + 𝐶 ) − 𝐶 ) )
33	30 22	pncand	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐵 + 𝐶 ) − 𝐶 ) = 𝐵 )
34	32 33	eqtr2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐵 = ( ( 𝐵 + 𝐶 ) + - 𝐶 ) )
35	34	oveq1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( 𝐵 mod 𝐷 ) = ( ( ( 𝐵 + 𝐶 ) + - 𝐶 ) mod 𝐷 ) )
36	27 35	eqeq12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ↔ ( ( ( 𝐴 + 𝐶 ) + - 𝐶 ) mod 𝐷 ) = ( ( ( 𝐵 + 𝐶 ) + - 𝐶 ) mod 𝐷 ) ) )
37	36	adantr	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) ∧ ( ( 𝐴 + 𝐶 ) mod 𝐷 ) = ( ( 𝐵 + 𝐶 ) mod 𝐷 ) ) → ( ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ↔ ( ( ( 𝐴 + 𝐶 ) + - 𝐶 ) mod 𝐷 ) = ( ( ( 𝐵 + 𝐶 ) + - 𝐶 ) mod 𝐷 ) ) )
38	16 37	mpbird	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) ∧ ( ( 𝐴 + 𝐶 ) mod 𝐷 ) = ( ( 𝐵 + 𝐶 ) mod 𝐷 ) ) → ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) )
39	2 38	impbida	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ↔ ( ( 𝐴 + 𝐶 ) mod 𝐷 ) = ( ( 𝐵 + 𝐶 ) mod 𝐷 ) ) )