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