# 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 ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{B}}⌋{B}+\left({A}\mathrm{mod}{B}\right)={A}$

### Proof

Step Hyp Ref Expression
1 modvalr ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{B}={A}-⌊\frac{{A}}{{B}}⌋{B}$
2 1 eqcomd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}-⌊\frac{{A}}{{B}}⌋{B}={A}\mathrm{mod}{B}$
3 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
4 3 adantr ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\in ℂ$
5 rerpdivcl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \frac{{A}}{{B}}\in ℝ$
6 flcl ${⊢}\frac{{A}}{{B}}\in ℝ\to ⌊\frac{{A}}{{B}}⌋\in ℤ$
7 6 zcnd ${⊢}\frac{{A}}{{B}}\in ℝ\to ⌊\frac{{A}}{{B}}⌋\in ℂ$
8 5 7 syl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{B}}⌋\in ℂ$
9 rpcn ${⊢}{B}\in {ℝ}^{+}\to {B}\in ℂ$
10 9 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}\in ℂ$
11 8 10 mulcld ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{B}}⌋{B}\in ℂ$
12 modcl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{B}\in ℝ$
13 12 recnd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{B}\in ℂ$
14 4 11 13 subaddd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({A}-⌊\frac{{A}}{{B}}⌋{B}={A}\mathrm{mod}{B}↔⌊\frac{{A}}{{B}}⌋{B}+\left({A}\mathrm{mod}{B}\right)={A}\right)$
15 2 14 mpbid ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{B}}⌋{B}+\left({A}\mathrm{mod}{B}\right)={A}$