Theorem modmulmodr

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

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

Proof

Step	Hyp	Ref	Expression
1		zcn	|- ( A e. ZZ -> A e. CC )
2	1	3ad2ant1	|- ( ( A e. ZZ /\ B e. RR /\ M e. RR+ ) -> A e. CC )
3		simp2	|- ( ( A e. ZZ /\ B e. RR /\ M e. RR+ ) -> B e. RR )
4		simp3	|- ( ( A e. ZZ /\ B e. RR /\ M e. RR+ ) -> M e. RR+ )
5	3 4	modcld	|- ( ( A e. ZZ /\ B e. RR /\ M e. RR+ ) -> ( B mod M ) e. RR )
6	5	recnd	|- ( ( A e. ZZ /\ B e. RR /\ M e. RR+ ) -> ( B mod M ) e. CC )
7	2 6	mulcomd	|- ( ( A e. ZZ /\ B e. RR /\ M e. RR+ ) -> ( A x. ( B mod M ) ) = ( ( B mod M ) x. A ) )
8	7	oveq1d	|- ( ( A e. ZZ /\ B e. RR /\ M e. RR+ ) -> ( ( A x. ( B mod M ) ) mod M ) = ( ( ( B mod M ) x. A ) mod M ) )
9		modmulmod	|- ( ( B e. RR /\ A e. ZZ /\ M e. RR+ ) -> ( ( ( B mod M ) x. A ) mod M ) = ( ( B x. A ) mod M ) )
10	9	3com12	|- ( ( A e. ZZ /\ B e. RR /\ M e. RR+ ) -> ( ( ( B mod M ) x. A ) mod M ) = ( ( B x. A ) mod M ) )
11		recn	|- ( B e. RR -> B e. CC )
12	1 11	anim12ci	|- ( ( A e. ZZ /\ B e. RR ) -> ( B e. CC /\ A e. CC ) )
13	12	3adant3	|- ( ( A e. ZZ /\ B e. RR /\ M e. RR+ ) -> ( B e. CC /\ A e. CC ) )
14		mulcom	|- ( ( B e. CC /\ A e. CC ) -> ( B x. A ) = ( A x. B ) )
15	13 14	syl	|- ( ( A e. ZZ /\ B e. RR /\ M e. RR+ ) -> ( B x. A ) = ( A x. B ) )
16	15	oveq1d	|- ( ( A e. ZZ /\ B e. RR /\ M e. RR+ ) -> ( ( B x. A ) mod M ) = ( ( A x. B ) mod M ) )
17	8 10 16	3eqtrd	|- ( ( A e. ZZ /\ B e. RR /\ M e. RR+ ) -> ( ( A x. ( B mod M ) ) mod M ) = ( ( A x. B ) mod M ) )