Metamath Proof Explorer

Theorem modaddmulmod

Description: The sum of a real number and the product of a second real number modulo a positive real number and an integer equals the sum of the real number and the product of the other real number and the integer modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018)

Ref Expression
Assertion modaddmulmod 
|- ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> ( ( A + ( ( B mod M ) x. C ) ) mod M ) = ( ( A + ( B x. C ) ) mod M ) )

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 1 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. ZZ ) -> A e. CC )
3 2 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> A e. CC )
4 simpl2 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> B e. RR )
5 simpr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> M e. RR+ )
6 4 5 modcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> ( B mod M ) e. RR )
7 6 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> ( B mod M ) e. CC )
8 zcn 
 |-  ( C e. ZZ -> C e. CC )
9 8 3ad2ant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. ZZ ) -> C e. CC )
10 9 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> C e. CC )
11 7 10 mulcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> ( ( B mod M ) x. C ) e. CC )
12 3 11 addcomd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> ( A + ( ( B mod M ) x. C ) ) = ( ( ( B mod M ) x. C ) + A ) )
13 12 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> ( ( A + ( ( B mod M ) x. C ) ) mod M ) = ( ( ( ( B mod M ) x. C ) + A ) mod M ) )
14 zre 
 |-  ( C e. ZZ -> C e. RR )
15 14 3ad2ant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. ZZ ) -> C e. RR )
16 15 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> C e. RR )
17 6 16 remulcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> ( ( B mod M ) x. C ) e. RR )
18 simpl 
 |-  ( ( B e. RR /\ C e. ZZ ) -> B e. RR )
19 14 adantl 
 |-  ( ( B e. RR /\ C e. ZZ ) -> C e. RR )
20 18 19 remulcld 
 |-  ( ( B e. RR /\ C e. ZZ ) -> ( B x. C ) e. RR )
21 20 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. ZZ ) -> ( B x. C ) e. RR )
22 21 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> ( B x. C ) e. RR )
23 22 5 modcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> ( ( B x. C ) mod M ) e. RR )
24 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. ZZ ) -> A e. RR )
25 24 anim1i 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> ( A e. RR /\ M e. RR+ ) )
26 simpl3 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> C e. ZZ )
27 modmulmod 
 |-  ( ( B e. RR /\ C e. ZZ /\ M e. RR+ ) -> ( ( ( B mod M ) x. C ) mod M ) = ( ( B x. C ) mod M ) )
28 4 26 5 27 syl3anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> ( ( ( B mod M ) x. C ) mod M ) = ( ( B x. C ) mod M ) )
29 remulcl 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B x. C ) e. RR )
30 14 29 sylan2 
 |-  ( ( B e. RR /\ C e. ZZ ) -> ( B x. C ) e. RR )
31 30 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. ZZ ) -> ( B x. C ) e. RR )
32 modabs2 
 |-  ( ( ( B x. C ) e. RR /\ M e. RR+ ) -> ( ( ( B x. C ) mod M ) mod M ) = ( ( B x. C ) mod M ) )
33 31 32 sylan 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> ( ( ( B x. C ) mod M ) mod M ) = ( ( B x. C ) mod M ) )
34 28 33 eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> ( ( ( B mod M ) x. C ) mod M ) = ( ( ( B x. C ) mod M ) mod M ) )
35 modadd1 
 |-  ( ( ( ( ( B mod M ) x. C ) e. RR /\ ( ( B x. C ) mod M ) e. RR ) /\ ( A e. RR /\ M e. RR+ ) /\ ( ( ( B mod M ) x. C ) mod M ) = ( ( ( B x. C ) mod M ) mod M ) ) -> ( ( ( ( B mod M ) x. C ) + A ) mod M ) = ( ( ( ( B x. C ) mod M ) + A ) mod M ) )
36 17 23 25 34 35 syl211anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> ( ( ( ( B mod M ) x. C ) + A ) mod M ) = ( ( ( ( B x. C ) mod M ) + A ) mod M ) )
37 31 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> ( B x. C ) e. RR )
38 24 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> A e. RR )
39 modaddmod 
 |-  ( ( ( B x. C ) e. RR /\ A e. RR /\ M e. RR+ ) -> ( ( ( ( B x. C ) mod M ) + A ) mod M ) = ( ( ( B x. C ) + A ) mod M ) )
40 37 38 5 39 syl3anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> ( ( ( ( B x. C ) mod M ) + A ) mod M ) = ( ( ( B x. C ) + A ) mod M ) )
41 recn 
 |-  ( B e. RR -> B e. CC )
42 mulcl 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B x. C ) e. CC )
43 41 8 42 syl2an 
 |-  ( ( B e. RR /\ C e. ZZ ) -> ( B x. C ) e. CC )
44 43 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. ZZ ) -> ( B x. C ) e. CC )
45 44 2 addcomd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. ZZ ) -> ( ( B x. C ) + A ) = ( A + ( B x. C ) ) )
46 45 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> ( ( B x. C ) + A ) = ( A + ( B x. C ) ) )
47 46 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> ( ( ( B x. C ) + A ) mod M ) = ( ( A + ( B x. C ) ) mod M ) )
48 40 47 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> ( ( ( ( B x. C ) mod M ) + A ) mod M ) = ( ( A + ( B x. C ) ) mod M ) )
49 13 36 48 3eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. ZZ ) /\ M e. RR+ ) -> ( ( A + ( ( B mod M ) x. C ) ) mod M ) = ( ( A + ( B x. C ) ) mod M ) )