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