# Metamath Proof Explorer

## Theorem moddiffl

Description: Value of the modulo operation rewritten to give two ways of expressing the quotient when " A is divided by B using Euclidean division." Multiplying both sides by B , this implies that A mod B differs from A by an integer multiple of B . (Contributed by Jeff Madsen, 17-Jun-2010) (Revised by Mario Carneiro, 6-Sep-2016)

Ref Expression
Assertion moddiffl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \frac{{A}-\left({A}\mathrm{mod}{B}\right)}{{B}}=⌊\frac{{A}}{{B}}⌋$

### Proof

Step Hyp Ref Expression
1 modval ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{B}={A}-{B}⌊\frac{{A}}{{B}}⌋$
2 1 oveq2d ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}-\left({A}\mathrm{mod}{B}\right)={A}-\left({A}-{B}⌊\frac{{A}}{{B}}⌋\right)$
3 simpl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\in ℝ$
4 3 recnd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\in ℂ$
5 rpcn ${⊢}{B}\in {ℝ}^{+}\to {B}\in ℂ$
6 5 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}\in ℂ$
7 rerpdivcl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \frac{{A}}{{B}}\in ℝ$
8 7 flcld ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{B}}⌋\in ℤ$
9 8 zcnd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{B}}⌋\in ℂ$
10 6 9 mulcld ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}⌊\frac{{A}}{{B}}⌋\in ℂ$
11 4 10 nncand ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}-\left({A}-{B}⌊\frac{{A}}{{B}}⌋\right)={B}⌊\frac{{A}}{{B}}⌋$
12 2 11 eqtrd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}-\left({A}\mathrm{mod}{B}\right)={B}⌊\frac{{A}}{{B}}⌋$
13 12 oveq1d ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \frac{{A}-\left({A}\mathrm{mod}{B}\right)}{{B}}=\frac{{B}⌊\frac{{A}}{{B}}⌋}{{B}}$
14 rpne0 ${⊢}{B}\in {ℝ}^{+}\to {B}\ne 0$
15 14 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}\ne 0$
16 9 6 15 divcan3d ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \frac{{B}⌊\frac{{A}}{{B}}⌋}{{B}}=⌊\frac{{A}}{{B}}⌋$
17 13 16 eqtrd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \frac{{A}-\left({A}\mathrm{mod}{B}\right)}{{B}}=⌊\frac{{A}}{{B}}⌋$