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 syl6bi
 |-  ( ( ( 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 syl5ib
 |-  ( ( ( 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 ) )