# Metamath Proof Explorer

## Theorem modelico

Description: Modular reduction produces a half-open interval. (Contributed by Stefan O'Rear, 12-Sep-2014)

Ref Expression
Assertion modelico ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{B}\in \left[0,{B}\right)$

### Proof

Step Hyp Ref Expression
1 modcl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{B}\in ℝ$
2 modge0 ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to 0\le {A}\mathrm{mod}{B}$
3 modlt ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{B}<{B}$
4 0re ${⊢}0\in ℝ$
5 rpxr ${⊢}{B}\in {ℝ}^{+}\to {B}\in {ℝ}^{*}$
6 5 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}\in {ℝ}^{*}$
7 elico2 ${⊢}\left(0\in ℝ\wedge {B}\in {ℝ}^{*}\right)\to \left({A}\mathrm{mod}{B}\in \left[0,{B}\right)↔\left({A}\mathrm{mod}{B}\in ℝ\wedge 0\le {A}\mathrm{mod}{B}\wedge {A}\mathrm{mod}{B}<{B}\right)\right)$
8 4 6 7 sylancr ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{B}\in \left[0,{B}\right)↔\left({A}\mathrm{mod}{B}\in ℝ\wedge 0\le {A}\mathrm{mod}{B}\wedge {A}\mathrm{mod}{B}<{B}\right)\right)$
9 1 2 3 8 mpbir3and ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{B}\in \left[0,{B}\right)$