Metamath Proof Explorer


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 )