# Metamath Proof Explorer

## Theorem modlt

Description: The modulo operation is less than its second argument. (Contributed by NM, 10-Nov-2008)

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

### Proof

Step Hyp Ref Expression
1 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
2 rpcnne0 ${⊢}{B}\in {ℝ}^{+}\to \left({B}\in ℂ\wedge {B}\ne 0\right)$
3 divcan2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to {B}\left(\frac{{A}}{{B}}\right)={A}$
4 3 3expb ${⊢}\left({A}\in ℂ\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to {B}\left(\frac{{A}}{{B}}\right)={A}$
5 1 2 4 syl2an ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}\left(\frac{{A}}{{B}}\right)={A}$
6 5 oveq1d ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}\left(\frac{{A}}{{B}}\right)-{B}⌊\frac{{A}}{{B}}⌋={A}-{B}⌊\frac{{A}}{{B}}⌋$
7 rpcn ${⊢}{B}\in {ℝ}^{+}\to {B}\in ℂ$
8 7 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}\in ℂ$
9 rerpdivcl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \frac{{A}}{{B}}\in ℝ$
10 9 recnd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \frac{{A}}{{B}}\in ℂ$
11 refldivcl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{B}}⌋\in ℝ$
12 11 recnd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{B}}⌋\in ℂ$
13 8 10 12 subdid ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}\left(\left(\frac{{A}}{{B}}\right)-⌊\frac{{A}}{{B}}⌋\right)={B}\left(\frac{{A}}{{B}}\right)-{B}⌊\frac{{A}}{{B}}⌋$
14 modval ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{B}={A}-{B}⌊\frac{{A}}{{B}}⌋$
15 6 13 14 3eqtr4rd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{B}={B}\left(\left(\frac{{A}}{{B}}\right)-⌊\frac{{A}}{{B}}⌋\right)$
16 fraclt1 ${⊢}\frac{{A}}{{B}}\in ℝ\to \left(\frac{{A}}{{B}}\right)-⌊\frac{{A}}{{B}}⌋<1$
17 9 16 syl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left(\frac{{A}}{{B}}\right)-⌊\frac{{A}}{{B}}⌋<1$
18 divid ${⊢}\left({B}\in ℂ\wedge {B}\ne 0\right)\to \frac{{B}}{{B}}=1$
19 2 18 syl ${⊢}{B}\in {ℝ}^{+}\to \frac{{B}}{{B}}=1$
20 19 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \frac{{B}}{{B}}=1$
21 17 20 breqtrrd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left(\frac{{A}}{{B}}\right)-⌊\frac{{A}}{{B}}⌋<\frac{{B}}{{B}}$
22 9 11 resubcld ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left(\frac{{A}}{{B}}\right)-⌊\frac{{A}}{{B}}⌋\in ℝ$
23 rpre ${⊢}{B}\in {ℝ}^{+}\to {B}\in ℝ$
24 23 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}\in ℝ$
25 rpregt0 ${⊢}{B}\in {ℝ}^{+}\to \left({B}\in ℝ\wedge 0<{B}\right)$
26 25 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({B}\in ℝ\wedge 0<{B}\right)$
27 ltmuldiv2 ${⊢}\left(\left(\frac{{A}}{{B}}\right)-⌊\frac{{A}}{{B}}⌋\in ℝ\wedge {B}\in ℝ\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left({B}\left(\left(\frac{{A}}{{B}}\right)-⌊\frac{{A}}{{B}}⌋\right)<{B}↔\left(\frac{{A}}{{B}}\right)-⌊\frac{{A}}{{B}}⌋<\frac{{B}}{{B}}\right)$
28 22 24 26 27 syl3anc ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({B}\left(\left(\frac{{A}}{{B}}\right)-⌊\frac{{A}}{{B}}⌋\right)<{B}↔\left(\frac{{A}}{{B}}\right)-⌊\frac{{A}}{{B}}⌋<\frac{{B}}{{B}}\right)$
29 21 28 mpbird ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}\left(\left(\frac{{A}}{{B}}\right)-⌊\frac{{A}}{{B}}⌋\right)<{B}$
30 15 29 eqbrtrd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{B}<{B}$