Theorem modvalp1

Description: The value of the modulo operation (expressed with sum of denominator and nominator). (Contributed by Alexander van der Vekens, 14-Apr-2018)

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

Proof

Step	Hyp	Ref	Expression
1		recn	|- ( A e. RR -> A e. CC )
2	1	adantr	|- ( ( A e. RR /\ B e. RR+ ) -> A e. CC )
3		refldivcl	|- ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) e. RR )
4	3	recnd	|- ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) e. CC )
5		rpcn	|- ( B e. RR+ -> B e. CC )
6	5	adantl	|- ( ( A e. RR /\ B e. RR+ ) -> B e. CC )
7	4 6	mulcld	|- ( ( A e. RR /\ B e. RR+ ) -> ( ( |_ ` ( A / B ) ) x. B ) e. CC )
8	2 7 6	pnpcan2d	|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A + B ) - ( ( ( |_ ` ( A / B ) ) x. B ) + B ) ) = ( A - ( ( |_ ` ( A / B ) ) x. B ) ) )
9	4 6	adddirp1d	|- ( ( A e. RR /\ B e. RR+ ) -> ( ( ( |_ ` ( A / B ) ) + 1 ) x. B ) = ( ( ( |_ ` ( A / B ) ) x. B ) + B ) )
10	9	oveq2d	|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A + B ) - ( ( ( |_ ` ( A / B ) ) + 1 ) x. B ) ) = ( ( A + B ) - ( ( ( |_ ` ( A / B ) ) x. B ) + B ) ) )
11		modvalr	|- ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) = ( A - ( ( |_ ` ( A / B ) ) x. B ) ) )
12	8 10 11	3eqtr4d	|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A + B ) - ( ( ( |_ ` ( A / B ) ) + 1 ) x. B ) ) = ( A mod B ) )