# Metamath Proof Explorer

## Theorem modid

Description: Identity law for modulo. (Contributed by NM, 29-Dec-2008)

Ref Expression
Assertion modid ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{B}\right)\right)\to {A}\mathrm{mod}{B}={A}$

### 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 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{B}\right)\right)\to {A}\mathrm{mod}{B}={A}-{B}⌊\frac{{A}}{{B}}⌋$
3 rerpdivcl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \frac{{A}}{{B}}\in ℝ$
4 3 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{B}\right)\right)\to \frac{{A}}{{B}}\in ℝ$
5 4 recnd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{B}\right)\right)\to \frac{{A}}{{B}}\in ℂ$
6 addid2 ${⊢}\frac{{A}}{{B}}\in ℂ\to 0+\left(\frac{{A}}{{B}}\right)=\frac{{A}}{{B}}$
7 6 fveq2d ${⊢}\frac{{A}}{{B}}\in ℂ\to ⌊0+\left(\frac{{A}}{{B}}\right)⌋=⌊\frac{{A}}{{B}}⌋$
8 5 7 syl ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{B}\right)\right)\to ⌊0+\left(\frac{{A}}{{B}}\right)⌋=⌊\frac{{A}}{{B}}⌋$
9 rpregt0 ${⊢}{B}\in {ℝ}^{+}\to \left({B}\in ℝ\wedge 0<{B}\right)$
10 divge0 ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to 0\le \frac{{A}}{{B}}$
11 9 10 sylan2 ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge {B}\in {ℝ}^{+}\right)\to 0\le \frac{{A}}{{B}}$
12 11 an32s ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge 0\le {A}\right)\to 0\le \frac{{A}}{{B}}$
13 12 adantrr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{B}\right)\right)\to 0\le \frac{{A}}{{B}}$
14 simpr ${⊢}\left({B}\in {ℝ}^{+}\wedge {A}<{B}\right)\to {A}<{B}$
15 rpcn ${⊢}{B}\in {ℝ}^{+}\to {B}\in ℂ$
16 15 mulid1d ${⊢}{B}\in {ℝ}^{+}\to {B}\cdot 1={B}$
17 16 adantr ${⊢}\left({B}\in {ℝ}^{+}\wedge {A}<{B}\right)\to {B}\cdot 1={B}$
18 14 17 breqtrrd ${⊢}\left({B}\in {ℝ}^{+}\wedge {A}<{B}\right)\to {A}<{B}\cdot 1$
19 18 ad2ant2l ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{B}\right)\right)\to {A}<{B}\cdot 1$
20 simpll ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{B}\right)\right)\to {A}\in ℝ$
21 9 ad2antlr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{B}\right)\right)\to \left({B}\in ℝ\wedge 0<{B}\right)$
22 1re ${⊢}1\in ℝ$
23 ltdivmul ${⊢}\left({A}\in ℝ\wedge 1\in ℝ\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left(\frac{{A}}{{B}}<1↔{A}<{B}\cdot 1\right)$
24 22 23 mp3an2 ${⊢}\left({A}\in ℝ\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left(\frac{{A}}{{B}}<1↔{A}<{B}\cdot 1\right)$
25 20 21 24 syl2anc ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{B}\right)\right)\to \left(\frac{{A}}{{B}}<1↔{A}<{B}\cdot 1\right)$
26 19 25 mpbird ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{B}\right)\right)\to \frac{{A}}{{B}}<1$
27 0z ${⊢}0\in ℤ$
28 flbi2 ${⊢}\left(0\in ℤ\wedge \frac{{A}}{{B}}\in ℝ\right)\to \left(⌊0+\left(\frac{{A}}{{B}}\right)⌋=0↔\left(0\le \frac{{A}}{{B}}\wedge \frac{{A}}{{B}}<1\right)\right)$
29 27 4 28 sylancr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{B}\right)\right)\to \left(⌊0+\left(\frac{{A}}{{B}}\right)⌋=0↔\left(0\le \frac{{A}}{{B}}\wedge \frac{{A}}{{B}}<1\right)\right)$
30 13 26 29 mpbir2and ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{B}\right)\right)\to ⌊0+\left(\frac{{A}}{{B}}\right)⌋=0$
31 8 30 eqtr3d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{B}\right)\right)\to ⌊\frac{{A}}{{B}}⌋=0$
32 31 oveq2d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{B}\right)\right)\to {B}⌊\frac{{A}}{{B}}⌋={B}\cdot 0$
33 15 mul01d ${⊢}{B}\in {ℝ}^{+}\to {B}\cdot 0=0$
34 33 ad2antlr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{B}\right)\right)\to {B}\cdot 0=0$
35 32 34 eqtrd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{B}\right)\right)\to {B}⌊\frac{{A}}{{B}}⌋=0$
36 35 oveq2d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{B}\right)\right)\to {A}-{B}⌊\frac{{A}}{{B}}⌋={A}-0$
37 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
38 37 subid1d ${⊢}{A}\in ℝ\to {A}-0={A}$
39 38 ad2antrr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{B}\right)\right)\to {A}-0={A}$
40 36 39 eqtrd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{B}\right)\right)\to {A}-{B}⌊\frac{{A}}{{B}}⌋={A}$
41 2 40 eqtrd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{B}\right)\right)\to {A}\mathrm{mod}{B}={A}$