This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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