# Metamath Proof Explorer

## Theorem modirr

Description: A number modulo an irrational multiple of it is nonzero. (Contributed by NM, 11-Nov-2008)

Ref Expression
Assertion modirr ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\wedge \frac{{A}}{{B}}\in \left(ℝ\setminus ℚ\right)\right)\to {A}\mathrm{mod}{B}\ne 0$

### Proof

Step Hyp Ref Expression
1 eldif ${⊢}\frac{{A}}{{B}}\in \left(ℝ\setminus ℚ\right)↔\left(\frac{{A}}{{B}}\in ℝ\wedge ¬\frac{{A}}{{B}}\in ℚ\right)$
2 modval ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{B}={A}-{B}⌊\frac{{A}}{{B}}⌋$
3 2 eqeq1d ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{B}=0↔{A}-{B}⌊\frac{{A}}{{B}}⌋=0\right)$
4 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
5 4 adantr ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\in ℂ$
6 rpre ${⊢}{B}\in {ℝ}^{+}\to {B}\in ℝ$
7 6 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}\in ℝ$
8 refldivcl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{B}}⌋\in ℝ$
9 7 8 remulcld ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}⌊\frac{{A}}{{B}}⌋\in ℝ$
10 9 recnd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}⌊\frac{{A}}{{B}}⌋\in ℂ$
11 5 10 subeq0ad ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({A}-{B}⌊\frac{{A}}{{B}}⌋=0↔{A}={B}⌊\frac{{A}}{{B}}⌋\right)$
12 rerpdivcl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \frac{{A}}{{B}}\in ℝ$
13 reflcl ${⊢}\frac{{A}}{{B}}\in ℝ\to ⌊\frac{{A}}{{B}}⌋\in ℝ$
14 13 recnd ${⊢}\frac{{A}}{{B}}\in ℝ\to ⌊\frac{{A}}{{B}}⌋\in ℂ$
15 12 14 syl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{B}}⌋\in ℂ$
16 rpcnne0 ${⊢}{B}\in {ℝ}^{+}\to \left({B}\in ℂ\wedge {B}\ne 0\right)$
17 16 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({B}\in ℂ\wedge {B}\ne 0\right)$
18 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)$
19 5 15 17 18 syl3anc ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left(\frac{{A}}{{B}}=⌊\frac{{A}}{{B}}⌋↔{A}={B}⌊\frac{{A}}{{B}}⌋\right)$
20 eqcom ${⊢}\frac{{A}}{{B}}=⌊\frac{{A}}{{B}}⌋↔⌊\frac{{A}}{{B}}⌋=\frac{{A}}{{B}}$
21 19 20 bitr3di ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({A}={B}⌊\frac{{A}}{{B}}⌋↔⌊\frac{{A}}{{B}}⌋=\frac{{A}}{{B}}\right)$
22 3 11 21 3bitrd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{B}=0↔⌊\frac{{A}}{{B}}⌋=\frac{{A}}{{B}}\right)$
23 flidz ${⊢}\frac{{A}}{{B}}\in ℝ\to \left(⌊\frac{{A}}{{B}}⌋=\frac{{A}}{{B}}↔\frac{{A}}{{B}}\in ℤ\right)$
24 zq ${⊢}\frac{{A}}{{B}}\in ℤ\to \frac{{A}}{{B}}\in ℚ$
25 23 24 syl6bi ${⊢}\frac{{A}}{{B}}\in ℝ\to \left(⌊\frac{{A}}{{B}}⌋=\frac{{A}}{{B}}\to \frac{{A}}{{B}}\in ℚ\right)$
26 12 25 syl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left(⌊\frac{{A}}{{B}}⌋=\frac{{A}}{{B}}\to \frac{{A}}{{B}}\in ℚ\right)$
27 22 26 sylbid ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{B}=0\to \frac{{A}}{{B}}\in ℚ\right)$
28 27 necon3bd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left(¬\frac{{A}}{{B}}\in ℚ\to {A}\mathrm{mod}{B}\ne 0\right)$
29 28 adantld ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left(\left(\frac{{A}}{{B}}\in ℝ\wedge ¬\frac{{A}}{{B}}\in ℚ\right)\to {A}\mathrm{mod}{B}\ne 0\right)$
30 1 29 syl5bi ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left(\frac{{A}}{{B}}\in \left(ℝ\setminus ℚ\right)\to {A}\mathrm{mod}{B}\ne 0\right)$
31 30 3impia ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\wedge \frac{{A}}{{B}}\in \left(ℝ\setminus ℚ\right)\right)\to {A}\mathrm{mod}{B}\ne 0$