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

Metamath Proof Explorer

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 ) )