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