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

Metamath Proof Explorer

Theorem moddiffl

Description: Value of the modulo operation rewritten to give two ways of expressing the quotient when " A is divided by B using Euclidean division." Multiplying both sides by B , this implies that A mod B differs from A by an integer multiple of B . (Contributed by Jeff Madsen, 17-Jun-2010) (Revised by Mario Carneiro, 6-Sep-2016)

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

Proof

Step Hyp Ref Expression
1 modval 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) = ( A - ( B x. ( |_ ` ( A / B ) ) ) ) )
2 1 oveq2d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A - ( A mod B ) ) = ( A - ( A - ( B x. ( |_ ` ( A / B ) ) ) ) ) )
3 simpl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> A e. RR )
4 3 recnd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> A e. CC )
5 rpcn 
 |-  ( B e. RR+ -> B e. CC )
6 5 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> B e. CC )
7 rerpdivcl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A / B ) e. RR )
8 7 flcld 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) e. ZZ )
9 8 zcnd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) e. CC )
10 6 9 mulcld 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( B x. ( |_ ` ( A / B ) ) ) e. CC )
11 4 10 nncand 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A - ( A - ( B x. ( |_ ` ( A / B ) ) ) ) ) = ( B x. ( |_ ` ( A / B ) ) ) )
12 2 11 eqtrd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A - ( A mod B ) ) = ( B x. ( |_ ` ( A / B ) ) ) )
13 12 oveq1d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A - ( A mod B ) ) / B ) = ( ( B x. ( |_ ` ( A / B ) ) ) / B ) )
14 rpne0 
 |-  ( B e. RR+ -> B =/= 0 )
15 14 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> B =/= 0 )
16 9 6 15 divcan3d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( B x. ( |_ ` ( A / B ) ) ) / B ) = ( |_ ` ( A / B ) ) )
17 13 16 eqtrd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A - ( A mod B ) ) / B ) = ( |_ ` ( A / B ) ) )