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 AB+ABB+AmodB=A

Proof

Step Hyp Ref Expression
1 modvalr AB+AmodB=AABB
2 1 eqcomd AB+AABB=AmodB
3 recn AA
4 3 adantr AB+A
5 rerpdivcl AB+AB
6 flcl ABAB
7 6 zcnd ABAB
8 5 7 syl AB+AB
9 rpcn B+B
10 9 adantl AB+B
11 8 10 mulcld AB+ABB
12 modcl AB+AmodB
13 12 recnd AB+AmodB
14 4 11 13 subaddd AB+AABB=AmodBABB+AmodB=A
15 2 14 mpbid AB+ABB+AmodB=A