Metamath Proof Explorer

Theorem modadd1

Description: Addition property of the modulo operation. (Contributed by NM, 12-Nov-2008)

Ref Expression
Assertion 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 ) )

Proof

Step Hyp Ref Expression
1 modval 
 |-  ( ( A e. RR /\ D e. RR+ ) -> ( A mod D ) = ( A - ( D x. ( |_ ` ( A / D ) ) ) ) )
2 modval 
 |-  ( ( B e. RR /\ D e. RR+ ) -> ( B mod D ) = ( B - ( D x. ( |_ ` ( B / D ) ) ) ) )
3 1 2 eqeqan12d 
 |-  ( ( ( A e. RR /\ D e. RR+ ) /\ ( B e. RR /\ D e. RR+ ) ) -> ( ( A mod D ) = ( B mod D ) <-> ( A - ( D x. ( |_ ` ( A / D ) ) ) ) = ( B - ( D x. ( |_ ` ( B / D ) ) ) ) ) )
4 3 anandirs 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ D e. RR+ ) -> ( ( A mod D ) = ( B mod D ) <-> ( A - ( D x. ( |_ ` ( A / D ) ) ) ) = ( B - ( D x. ( |_ ` ( B / D ) ) ) ) ) )
5 4 adantrl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( ( A mod D ) = ( B mod D ) <-> ( A - ( D x. ( |_ ` ( A / D ) ) ) ) = ( B - ( D x. ( |_ ` ( B / D ) ) ) ) ) )
6 oveq1 
 |-  ( ( A - ( D x. ( |_ ` ( A / D ) ) ) ) = ( B - ( D x. ( |_ ` ( B / D ) ) ) ) -> ( ( A - ( D x. ( |_ ` ( A / D ) ) ) ) + C ) = ( ( B - ( D x. ( |_ ` ( B / D ) ) ) ) + C ) )
7 5 6 biimtrdi 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( ( A mod D ) = ( B mod D ) -> ( ( A - ( D x. ( |_ ` ( A / D ) ) ) ) + C ) = ( ( B - ( D x. ( |_ ` ( B / D ) ) ) ) + C ) ) )
8 recn 
 |-  ( A e. RR -> A e. CC )
9 8 adantr 
 |-  ( ( A e. RR /\ ( C e. RR /\ D e. RR+ ) ) -> A e. CC )
10 recn 
 |-  ( C e. RR -> C e. CC )
11 10 ad2antrl 
 |-  ( ( A e. RR /\ ( C e. RR /\ D e. RR+ ) ) -> C e. CC )
12 rpcn 
 |-  ( D e. RR+ -> D e. CC )
13 12 adantl 
 |-  ( ( A e. RR /\ D e. RR+ ) -> D e. CC )
14 rerpdivcl 
 |-  ( ( A e. RR /\ D e. RR+ ) -> ( A / D ) e. RR )
15 reflcl 
 |-  ( ( A / D ) e. RR -> ( |_ ` ( A / D ) ) e. RR )
16 15 recnd 
 |-  ( ( A / D ) e. RR -> ( |_ ` ( A / D ) ) e. CC )
17 14 16 syl 
 |-  ( ( A e. RR /\ D e. RR+ ) -> ( |_ ` ( A / D ) ) e. CC )
18 13 17 mulcld 
 |-  ( ( A e. RR /\ D e. RR+ ) -> ( D x. ( |_ ` ( A / D ) ) ) e. CC )
19 18 adantrl 
 |-  ( ( A e. RR /\ ( C e. RR /\ D e. RR+ ) ) -> ( D x. ( |_ ` ( A / D ) ) ) e. CC )
20 9 11 19 addsubd 
 |-  ( ( A e. RR /\ ( C e. RR /\ D e. RR+ ) ) -> ( ( A + C ) - ( D x. ( |_ ` ( A / D ) ) ) ) = ( ( A - ( D x. ( |_ ` ( A / D ) ) ) ) + C ) )
21 20 adantlr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( ( A + C ) - ( D x. ( |_ ` ( A / D ) ) ) ) = ( ( A - ( D x. ( |_ ` ( A / D ) ) ) ) + C ) )
22 recn 
 |-  ( B e. RR -> B e. CC )
23 22 adantr 
 |-  ( ( B e. RR /\ ( C e. RR /\ D e. RR+ ) ) -> B e. CC )
24 10 ad2antrl 
 |-  ( ( B e. RR /\ ( C e. RR /\ D e. RR+ ) ) -> C e. CC )
25 12 adantl 
 |-  ( ( B e. RR /\ D e. RR+ ) -> D e. CC )
26 rerpdivcl 
 |-  ( ( B e. RR /\ D e. RR+ ) -> ( B / D ) e. RR )
27 reflcl 
 |-  ( ( B / D ) e. RR -> ( |_ ` ( B / D ) ) e. RR )
28 27 recnd 
 |-  ( ( B / D ) e. RR -> ( |_ ` ( B / D ) ) e. CC )
29 26 28 syl 
 |-  ( ( B e. RR /\ D e. RR+ ) -> ( |_ ` ( B / D ) ) e. CC )
30 25 29 mulcld 
 |-  ( ( B e. RR /\ D e. RR+ ) -> ( D x. ( |_ ` ( B / D ) ) ) e. CC )
31 30 adantrl 
 |-  ( ( B e. RR /\ ( C e. RR /\ D e. RR+ ) ) -> ( D x. ( |_ ` ( B / D ) ) ) e. CC )
32 23 24 31 addsubd 
 |-  ( ( B e. RR /\ ( C e. RR /\ D e. RR+ ) ) -> ( ( B + C ) - ( D x. ( |_ ` ( B / D ) ) ) ) = ( ( B - ( D x. ( |_ ` ( B / D ) ) ) ) + C ) )
33 32 adantll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( ( B + C ) - ( D x. ( |_ ` ( B / D ) ) ) ) = ( ( B - ( D x. ( |_ ` ( B / D ) ) ) ) + C ) )
34 21 33 eqeq12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( ( ( A + C ) - ( D x. ( |_ ` ( A / D ) ) ) ) = ( ( B + C ) - ( D x. ( |_ ` ( B / D ) ) ) ) <-> ( ( A - ( D x. ( |_ ` ( A / D ) ) ) ) + C ) = ( ( B - ( D x. ( |_ ` ( B / D ) ) ) ) + C ) ) )
35 7 34 sylibrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( ( A mod D ) = ( B mod D ) -> ( ( A + C ) - ( D x. ( |_ ` ( A / D ) ) ) ) = ( ( B + C ) - ( D x. ( |_ ` ( B / D ) ) ) ) ) )
36 oveq1 
 |-  ( ( ( A + C ) - ( D x. ( |_ ` ( A / D ) ) ) ) = ( ( B + C ) - ( D x. ( |_ ` ( B / D ) ) ) ) -> ( ( ( A + C ) - ( D x. ( |_ ` ( A / D ) ) ) ) mod D ) = ( ( ( B + C ) - ( D x. ( |_ ` ( B / D ) ) ) ) mod D ) )
37 readdcl 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A + C ) e. RR )
38 37 adantrr 
 |-  ( ( A e. RR /\ ( C e. RR /\ D e. RR+ ) ) -> ( A + C ) e. RR )
39 simprr 
 |-  ( ( A e. RR /\ ( C e. RR /\ D e. RR+ ) ) -> D e. RR+ )
40 14 flcld 
 |-  ( ( A e. RR /\ D e. RR+ ) -> ( |_ ` ( A / D ) ) e. ZZ )
41 40 adantrl 
 |-  ( ( A e. RR /\ ( C e. RR /\ D e. RR+ ) ) -> ( |_ ` ( A / D ) ) e. ZZ )
42 modcyc2 
 |-  ( ( ( A + C ) e. RR /\ D e. RR+ /\ ( |_ ` ( A / D ) ) e. ZZ ) -> ( ( ( A + C ) - ( D x. ( |_ ` ( A / D ) ) ) ) mod D ) = ( ( A + C ) mod D ) )
43 38 39 41 42 syl3anc 
 |-  ( ( A e. RR /\ ( C e. RR /\ D e. RR+ ) ) -> ( ( ( A + C ) - ( D x. ( |_ ` ( A / D ) ) ) ) mod D ) = ( ( A + C ) mod D ) )
44 43 adantlr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( ( ( A + C ) - ( D x. ( |_ ` ( A / D ) ) ) ) mod D ) = ( ( A + C ) mod D ) )
45 readdcl 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B + C ) e. RR )
46 45 adantrr 
 |-  ( ( B e. RR /\ ( C e. RR /\ D e. RR+ ) ) -> ( B + C ) e. RR )
47 simprr 
 |-  ( ( B e. RR /\ ( C e. RR /\ D e. RR+ ) ) -> D e. RR+ )
48 26 flcld 
 |-  ( ( B e. RR /\ D e. RR+ ) -> ( |_ ` ( B / D ) ) e. ZZ )
49 48 adantrl 
 |-  ( ( B e. RR /\ ( C e. RR /\ D e. RR+ ) ) -> ( |_ ` ( B / D ) ) e. ZZ )
50 modcyc2 
 |-  ( ( ( B + C ) e. RR /\ D e. RR+ /\ ( |_ ` ( B / D ) ) e. ZZ ) -> ( ( ( B + C ) - ( D x. ( |_ ` ( B / D ) ) ) ) mod D ) = ( ( B + C ) mod D ) )
51 46 47 49 50 syl3anc 
 |-  ( ( B e. RR /\ ( C e. RR /\ D e. RR+ ) ) -> ( ( ( B + C ) - ( D x. ( |_ ` ( B / D ) ) ) ) mod D ) = ( ( B + C ) mod D ) )
52 51 adantll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( ( ( B + C ) - ( D x. ( |_ ` ( B / D ) ) ) ) mod D ) = ( ( B + C ) mod D ) )
53 44 52 eqeq12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( ( ( ( A + C ) - ( D x. ( |_ ` ( A / D ) ) ) ) mod D ) = ( ( ( B + C ) - ( D x. ( |_ ` ( B / D ) ) ) ) mod D ) <-> ( ( A + C ) mod D ) = ( ( B + C ) mod D ) ) )
54 36 53 imbitrid 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR+ ) ) -> ( ( ( A + C ) - ( D x. ( |_ ` ( A / D ) ) ) ) = ( ( B + C ) - ( D x. ( |_ ` ( B / D ) ) ) ) -> ( ( A + C ) mod D ) = ( ( B + C ) mod D ) ) )
55 35 54 syld 
 |-  ( ( ( 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 ) ) )
56 55 3impia 
 |-  ( ( ( 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 ) )