# Metamath Proof Explorer

## Theorem mod0

Description: A mod B is zero iff A is evenly divisible by B . (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Fan Zheng, 7-Jun-2016)

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

### 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 eqeq1d ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{B}=0↔{A}-{B}⌊\frac{{A}}{{B}}⌋=0\right)$
3 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
4 3 adantr ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\in ℂ$
5 rpre ${⊢}{B}\in {ℝ}^{+}\to {B}\in ℝ$
6 5 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}\in ℝ$
7 refldivcl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{B}}⌋\in ℝ$
8 6 7 remulcld ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}⌊\frac{{A}}{{B}}⌋\in ℝ$
9 8 recnd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}⌊\frac{{A}}{{B}}⌋\in ℂ$
10 4 9 subeq0ad ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({A}-{B}⌊\frac{{A}}{{B}}⌋=0↔{A}={B}⌊\frac{{A}}{{B}}⌋\right)$
11 2 10 bitrd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{B}=0↔{A}={B}⌊\frac{{A}}{{B}}⌋\right)$
12 7 recnd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{B}}⌋\in ℂ$
13 rpcnne0 ${⊢}{B}\in {ℝ}^{+}\to \left({B}\in ℂ\wedge {B}\ne 0\right)$
14 13 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({B}\in ℂ\wedge {B}\ne 0\right)$
15 divmul2 ${⊢}\left({A}\in ℂ\wedge ⌊\frac{{A}}{{B}}⌋\in ℂ\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to \left(\frac{{A}}{{B}}=⌊\frac{{A}}{{B}}⌋↔{A}={B}⌊\frac{{A}}{{B}}⌋\right)$
16 4 12 14 15 syl3anc ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left(\frac{{A}}{{B}}=⌊\frac{{A}}{{B}}⌋↔{A}={B}⌊\frac{{A}}{{B}}⌋\right)$
17 eqcom ${⊢}\frac{{A}}{{B}}=⌊\frac{{A}}{{B}}⌋↔⌊\frac{{A}}{{B}}⌋=\frac{{A}}{{B}}$
18 16 17 bitr3di ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({A}={B}⌊\frac{{A}}{{B}}⌋↔⌊\frac{{A}}{{B}}⌋=\frac{{A}}{{B}}\right)$
19 11 18 bitrd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{B}=0↔⌊\frac{{A}}{{B}}⌋=\frac{{A}}{{B}}\right)$
20 rerpdivcl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \frac{{A}}{{B}}\in ℝ$
21 flidz ${⊢}\frac{{A}}{{B}}\in ℝ\to \left(⌊\frac{{A}}{{B}}⌋=\frac{{A}}{{B}}↔\frac{{A}}{{B}}\in ℤ\right)$
22 20 21 syl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left(⌊\frac{{A}}{{B}}⌋=\frac{{A}}{{B}}↔\frac{{A}}{{B}}\in ℤ\right)$
23 19 22 bitrd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{B}=0↔\frac{{A}}{{B}}\in ℤ\right)$