This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )