Metamath Proof Explorer


Theorem mulmod0

Description: The product of an integer and a positive real number is 0 modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018) (Revised by AV, 5-Jul-2020)

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

Proof

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 )