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

Metamath Proof Explorer

Theorem modvalr

Description: The value of the modulo operation (multiplication in reversed order). (Contributed by Alexander van der Vekens, 14-Apr-2018)

Ref Expression
Assertion modvalr 
|- ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) = ( A - ( ( |_ ` ( A / B ) ) x. B ) ) )

Proof

Step Hyp Ref Expression
1 modval 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) = ( A - ( B x. ( |_ ` ( A / B ) ) ) ) )
2 rpcn 
 |-  ( B e. RR+ -> B e. CC )
3 2 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> B e. CC )
4 rerpdivcl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A / B ) e. RR )
5 reflcl 
 |-  ( ( A / B ) e. RR -> ( |_ ` ( A / B ) ) e. RR )
6 5 recnd 
 |-  ( ( A / B ) e. RR -> ( |_ ` ( A / B ) ) e. CC )
7 4 6 syl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) e. CC )
8 3 7 mulcomd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( B x. ( |_ ` ( A / B ) ) ) = ( ( |_ ` ( A / B ) ) x. B ) )
9 8 oveq2d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A - ( B x. ( |_ ` ( A / B ) ) ) ) = ( A - ( ( |_ ` ( A / B ) ) x. B ) ) )
10 1 9 eqtrd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) = ( A - ( ( |_ ` ( A / B ) ) x. B ) ) )