Theorem modmulmod

Description: The product of a real number modulo a positive real number and an integer equals the product of the real number and the integer modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018)

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

Proof

Step	Hyp	Ref	Expression
1		modcl	|- ( ( A e. RR /\ M e. RR+ ) -> ( A mod M ) e. RR )
2		simpl	|- ( ( A e. RR /\ M e. RR+ ) -> A e. RR )
3	1 2	jca	|- ( ( A e. RR /\ M e. RR+ ) -> ( ( A mod M ) e. RR /\ A e. RR ) )
4	3	3adant2	|- ( ( A e. RR /\ B e. ZZ /\ M e. RR+ ) -> ( ( A mod M ) e. RR /\ A e. RR ) )
5		3simpc	|- ( ( A e. RR /\ B e. ZZ /\ M e. RR+ ) -> ( B e. ZZ /\ M e. RR+ ) )
6		modabs2	|- ( ( A e. RR /\ M e. RR+ ) -> ( ( A mod M ) mod M ) = ( A mod M ) )
7	6	3adant2	|- ( ( A e. RR /\ B e. ZZ /\ M e. RR+ ) -> ( ( A mod M ) mod M ) = ( A mod M ) )
8		modmul1	|- ( ( ( ( A mod M ) e. RR /\ A e. RR ) /\ ( B e. ZZ /\ M e. RR+ ) /\ ( ( A mod M ) mod M ) = ( A mod M ) ) -> ( ( ( A mod M ) x. B ) mod M ) = ( ( A x. B ) mod M ) )
9	4 5 7 8	syl3anc	|- ( ( A e. RR /\ B e. ZZ /\ M e. RR+ ) -> ( ( ( A mod M ) x. B ) mod M ) = ( ( A x. B ) mod M ) )