# Metamath Proof Explorer

## Theorem modid2

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

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

### Proof

Step Hyp Ref Expression
1 modge0 ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to 0\le {A}\mathrm{mod}{B}$
2 modlt ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{B}<{B}$
3 1 2 jca ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left(0\le {A}\mathrm{mod}{B}\wedge {A}\mathrm{mod}{B}<{B}\right)$
4 breq2 ${⊢}{A}\mathrm{mod}{B}={A}\to \left(0\le {A}\mathrm{mod}{B}↔0\le {A}\right)$
5 breq1 ${⊢}{A}\mathrm{mod}{B}={A}\to \left({A}\mathrm{mod}{B}<{B}↔{A}<{B}\right)$
6 4 5 anbi12d ${⊢}{A}\mathrm{mod}{B}={A}\to \left(\left(0\le {A}\mathrm{mod}{B}\wedge {A}\mathrm{mod}{B}<{B}\right)↔\left(0\le {A}\wedge {A}<{B}\right)\right)$
7 3 6 syl5ibcom ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{B}={A}\to \left(0\le {A}\wedge {A}<{B}\right)\right)$
8 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}$
9 8 ex ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left(\left(0\le {A}\wedge {A}<{B}\right)\to {A}\mathrm{mod}{B}={A}\right)$
10 7 9 impbid ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{B}={A}↔\left(0\le {A}\wedge {A}<{B}\right)\right)$