Metamath Proof Explorer

Theorem fldivmod

Description: Expressing the floor of a division by the modulo operator. (Contributed by AV, 6-Jun-2020)

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

Proof

Step Hyp Ref Expression
1 rerpdivcl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A / B ) e. RR )
2 1 flcld 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) e. ZZ )
3 2 zcnd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) e. CC )
4 rpcn 
 |-  ( B e. RR+ -> B e. CC )
5 4 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> B e. CC )
6 3 5 mulcld 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( |_ ` ( A / B ) ) x. B ) e. CC )
7 modcl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) e. RR )
8 7 recnd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) e. CC )
9 6 8 pncand 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( ( ( |_ ` ( A / B ) ) x. B ) + ( A mod B ) ) - ( A mod B ) ) = ( ( |_ ` ( A / B ) ) x. B ) )
10 6 8 addcld 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( ( |_ ` ( A / B ) ) x. B ) + ( A mod B ) ) e. CC )
11 10 8 subcld 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( ( ( |_ ` ( A / B ) ) x. B ) + ( A mod B ) ) - ( A mod B ) ) e. CC )
12 rpne0 
 |-  ( B e. RR+ -> B =/= 0 )
13 12 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> B =/= 0 )
14 11 3 5 13 divmul3d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( ( ( ( ( |_ ` ( A / B ) ) x. B ) + ( A mod B ) ) - ( A mod B ) ) / B ) = ( |_ ` ( A / B ) ) <-> ( ( ( ( |_ ` ( A / B ) ) x. B ) + ( A mod B ) ) - ( A mod B ) ) = ( ( |_ ` ( A / B ) ) x. B ) ) )
15 9 14 mpbird 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( ( ( ( |_ ` ( A / B ) ) x. B ) + ( A mod B ) ) - ( A mod B ) ) / B ) = ( |_ ` ( A / B ) ) )
16 flpmodeq 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( ( |_ ` ( A / B ) ) x. B ) + ( A mod B ) ) = A )
17 16 oveq1d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( ( ( |_ ` ( A / B ) ) x. B ) + ( A mod B ) ) - ( A mod B ) ) = ( A - ( A mod B ) ) )
18 17 oveq1d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( ( ( ( |_ ` ( A / B ) ) x. B ) + ( A mod B ) ) - ( A mod B ) ) / B ) = ( ( A - ( A mod B ) ) / B ) )
19 15 18 eqtr3d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) = ( ( A - ( A mod B ) ) / B ) )