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 )