Theorem moddifz

Description: The modulo operation differs from A by an integer multiple of B . (Contributed by Mario Carneiro, 15-Jul-2014)

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

Proof

Step	Hyp	Ref	Expression
1		moddiffl	|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A - ( A mod B ) ) / B ) = ( |_ ` ( A / B ) ) )
2		rerpdivcl	|- ( ( A e. RR /\ B e. RR+ ) -> ( A / B ) e. RR )
3	2	flcld	|- ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) e. ZZ )
4	1 3	eqeltrd	|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A - ( A mod B ) ) / B ) e. ZZ )