Theorem flpmodeq

Description: Partition of a division into its integer part and the remainder. (Contributed by Alexander van der Vekens, 14-Apr-2018)

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

Proof

Step	Hyp	Ref	Expression
1		modvalr	|- ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) = ( A - ( ( |_ ` ( A / B ) ) x. B ) ) )
2	1	eqcomd	|- ( ( A e. RR /\ B e. RR+ ) -> ( A - ( ( |_ ` ( A / B ) ) x. B ) ) = ( A mod B ) )
3		recn	|- ( A e. RR -> A e. CC )
4	3	adantr	|- ( ( A e. RR /\ B e. RR+ ) -> A e. CC )
5		rerpdivcl	|- ( ( A e. RR /\ B e. RR+ ) -> ( A / B ) e. RR )
6		flcl	|- ( ( A / B ) e. RR -> ( |_ ` ( A / B ) ) e. ZZ )
7	6	zcnd	|- ( ( A / B ) e. RR -> ( |_ ` ( A / B ) ) e. CC )
8	5 7	syl	|- ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) e. CC )
9		rpcn	|- ( B e. RR+ -> B e. CC )
10	9	adantl	|- ( ( A e. RR /\ B e. RR+ ) -> B e. CC )
11	8 10	mulcld	|- ( ( A e. RR /\ B e. RR+ ) -> ( ( |_ ` ( A / B ) ) x. B ) e. CC )
12		modcl	|- ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) e. RR )
13	12	recnd	|- ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) e. CC )
14	4 11 13	subaddd	|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A - ( ( |_ ` ( A / B ) ) x. B ) ) = ( A mod B ) <-> ( ( ( |_ ` ( A / B ) ) x. B ) + ( A mod B ) ) = A ) )
15	2 14	mpbid	|- ( ( A e. RR /\ B e. RR+ ) -> ( ( ( |_ ` ( A / B ) ) x. B ) + ( A mod B ) ) = A )