Step |
Hyp |
Ref |
Expression |
1 |
|
zcn |
|- ( A e. ZZ -> A e. CC ) |
2 |
1
|
adantr |
|- ( ( A e. ZZ /\ M e. RR+ ) -> A e. CC ) |
3 |
|
rpcn |
|- ( M e. RR+ -> M e. CC ) |
4 |
3
|
adantl |
|- ( ( A e. ZZ /\ M e. RR+ ) -> M e. CC ) |
5 |
|
rpne0 |
|- ( M e. RR+ -> M =/= 0 ) |
6 |
5
|
adantl |
|- ( ( A e. ZZ /\ M e. RR+ ) -> M =/= 0 ) |
7 |
2 4 6
|
divcan4d |
|- ( ( A e. ZZ /\ M e. RR+ ) -> ( ( A x. M ) / M ) = A ) |
8 |
|
simpl |
|- ( ( A e. ZZ /\ M e. RR+ ) -> A e. ZZ ) |
9 |
7 8
|
eqeltrd |
|- ( ( A e. ZZ /\ M e. RR+ ) -> ( ( A x. M ) / M ) e. ZZ ) |
10 |
|
zre |
|- ( A e. ZZ -> A e. RR ) |
11 |
|
rpre |
|- ( M e. RR+ -> M e. RR ) |
12 |
|
remulcl |
|- ( ( A e. RR /\ M e. RR ) -> ( A x. M ) e. RR ) |
13 |
10 11 12
|
syl2an |
|- ( ( A e. ZZ /\ M e. RR+ ) -> ( A x. M ) e. RR ) |
14 |
|
mod0 |
|- ( ( ( A x. M ) e. RR /\ M e. RR+ ) -> ( ( ( A x. M ) mod M ) = 0 <-> ( ( A x. M ) / M ) e. ZZ ) ) |
15 |
13 14
|
sylancom |
|- ( ( A e. ZZ /\ M e. RR+ ) -> ( ( ( A x. M ) mod M ) = 0 <-> ( ( A x. M ) / M ) e. ZZ ) ) |
16 |
9 15
|
mpbird |
|- ( ( A e. ZZ /\ M e. RR+ ) -> ( ( A x. M ) mod M ) = 0 ) |