Theorem modcl

Description: Closure law for the modulo operation. (Contributed by NM, 10-Nov-2008)

	Ref	Expression
Assertion	modcl	|- ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		modval	|- ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) = ( A - ( B x. ( |_ ` ( A / B ) ) ) ) )
2		rpre	|- ( B e. RR+ -> B e. RR )
3	2	adantl	|- ( ( A e. RR /\ B e. RR+ ) -> B e. RR )
4		refldivcl	|- ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) e. RR )
5	3 4	remulcld	|- ( ( A e. RR /\ B e. RR+ ) -> ( B x. ( |_ ` ( A / B ) ) ) e. RR )
6		resubcl	|- ( ( A e. RR /\ ( B x. ( |_ ` ( A / B ) ) ) e. RR ) -> ( A - ( B x. ( |_ ` ( A / B ) ) ) ) e. RR )
7	5 6	syldan	|- ( ( A e. RR /\ B e. RR+ ) -> ( A - ( B x. ( |_ ` ( A / B ) ) ) ) e. RR )
8	1 7	eqeltrd	|- ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) e. RR )