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 
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( ( A mod D ) = ( B mod D ) <-> ( ( A + C ) mod D ) = ( ( B + C ) mod D ) ) )

Proof

Step Hyp Ref Expression
1 modadd1 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) /\ ( A mod D ) = ( B mod D ) ) -> ( ( A + C ) mod D ) = ( ( B + C ) mod D ) )
2 1 3expa 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) /\ ( A mod D ) = ( B mod D ) ) -> ( ( A + C ) mod D ) = ( ( B + C ) mod D ) )
3 simpll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> A e. RR )
4 simprl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> C e. RR )
5 3 4 readdcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( A + C ) e. RR )
6 simplr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> B e. RR )
7 6 4 readdcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( B + C ) e. RR )
8 5 7 jca 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( ( A + C ) e. RR /\ ( B + C ) e. RR ) )
9 8 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) /\ ( ( A + C ) mod D ) = ( ( B + C ) mod D ) ) -> ( ( A + C ) e. RR /\ ( B + C ) e. RR ) )
10 renegcl 
 |-  ( C e. RR -> -u C e. RR )
11 10 anim1i 
 |-  ( ( C e. RR /\ D e. RR+ ) -> ( -u C e. RR /\ D e. RR+ ) )
12 11 adantl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( -u C e. RR /\ D e. RR+ ) )
13 12 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) /\ ( ( A + C ) mod D ) = ( ( B + C ) mod D ) ) -> ( -u C e. RR /\ D e. RR+ ) )
14 simpr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) /\ ( ( A + C ) mod D ) = ( ( B + C ) mod D ) ) -> ( ( A + C ) mod D ) = ( ( B + C ) mod D ) )
15 modadd1 
 |-  ( ( ( ( A + C ) e. RR /\ ( B + C ) e. RR ) /\ ( -u C e. RR /\ D e. RR+ ) /\ ( ( A + C ) mod D ) = ( ( B + C ) mod D ) ) -> ( ( ( A + C ) + -u C ) mod D ) = ( ( ( B + C ) + -u C ) mod D ) )
16 9 13 14 15 syl3anc 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) /\ ( ( A + C ) mod D ) = ( ( B + C ) mod D ) ) -> ( ( ( A + C ) + -u C ) mod D ) = ( ( ( B + C ) + -u C ) mod D ) )
17 simpl 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR )
18 17 recnd 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. CC )
19 18 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> A e. CC )
20 simpl 
 |-  ( ( C e. RR /\ D e. RR+ ) -> C e. RR )
21 20 recnd 
 |-  ( ( C e. RR /\ D e. RR+ ) -> C e. CC )
22 21 adantl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> C e. CC )
23 19 22 addcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( A + C ) e. CC )
24 23 22 negsubd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( ( A + C ) + -u C ) = ( ( A + C ) - C ) )
25 19 22 pncand 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( ( A + C ) - C ) = A )
26 24 25 eqtr2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> A = ( ( A + C ) + -u C ) )
27 26 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( A mod D ) = ( ( ( A + C ) + -u C ) mod D ) )
28 simpr 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. RR )
29 28 recnd 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. CC )
30 29 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> B e. CC )
31 30 22 addcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( B + C ) e. CC )
32 31 22 negsubd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( ( B + C ) + -u C ) = ( ( B + C ) - C ) )
33 30 22 pncand 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( ( B + C ) - C ) = B )
34 32 33 eqtr2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> B = ( ( B + C ) + -u C ) )
35 34 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( B mod D ) = ( ( ( B + C ) + -u C ) mod D ) )
36 27 35 eqeq12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( ( A mod D ) = ( B mod D ) <-> ( ( ( A + C ) + -u C ) mod D ) = ( ( ( B + C ) + -u C ) mod D ) ) )
37 36 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) /\ ( ( A + C ) mod D ) = ( ( B + C ) mod D ) ) -> ( ( A mod D ) = ( B mod D ) <-> ( ( ( A + C ) + -u C ) mod D ) = ( ( ( B + C ) + -u C ) mod D ) ) )
38 16 37 mpbird 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) /\ ( ( A + C ) mod D ) = ( ( B + C ) mod D ) ) -> ( A mod D ) = ( B mod D ) )
39 2 38 impbida 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( ( A mod D ) = ( B mod D ) <-> ( ( A + C ) mod D ) = ( ( B + C ) mod D ) ) )