This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐷 ) ) )