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

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 )