# Metamath Proof Explorer

## Theorem irrapxlem2

Description: Lemma for irrapx1 . Two multiples in the same bucket means they are very close mod 1. (Contributed by Stefan O'Rear, 12-Sep-2014)

Ref Expression
Assertion irrapxlem2 ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to \exists {x}\in \left(0\dots {B}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in \left(0\dots {B}\right)\phantom{\rule{.4em}{0ex}}\left({x}<{y}\wedge \left|\left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\right|<\frac{1}{{B}}\right)$

### Proof

Step Hyp Ref Expression
1 irrapxlem1 ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to \exists {x}\in \left(0\dots {B}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in \left(0\dots {B}\right)\phantom{\rule{.4em}{0ex}}\left({x}<{y}\wedge ⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋=⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋\right)$
2 nnre ${⊢}{B}\in ℕ\to {B}\in ℝ$
3 2 ad3antlr ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {B}\in ℝ$
4 rpre ${⊢}{A}\in {ℝ}^{+}\to {A}\in ℝ$
5 4 ad3antrrr ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {A}\in ℝ$
6 elfzelz ${⊢}{x}\in \left(0\dots {B}\right)\to {x}\in ℤ$
7 6 zred ${⊢}{x}\in \left(0\dots {B}\right)\to {x}\in ℝ$
8 7 ad2antlr ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {x}\in ℝ$
9 5 8 remulcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {A}{x}\in ℝ$
10 1rp ${⊢}1\in {ℝ}^{+}$
11 10 a1i ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to 1\in {ℝ}^{+}$
12 9 11 modcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {A}{x}\mathrm{mod}1\in ℝ$
13 3 12 remulcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {B}\left({A}{x}\mathrm{mod}1\right)\in ℝ$
14 intfrac ${⊢}{B}\left({A}{x}\mathrm{mod}1\right)\in ℝ\to {B}\left({A}{x}\mathrm{mod}1\right)=⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋+\left({B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\right)$
15 13 14 syl ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {B}\left({A}{x}\mathrm{mod}1\right)=⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋+\left({B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\right)$
16 elfzelz ${⊢}{y}\in \left(0\dots {B}\right)\to {y}\in ℤ$
17 16 zred ${⊢}{y}\in \left(0\dots {B}\right)\to {y}\in ℝ$
18 17 adantl ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {y}\in ℝ$
19 5 18 remulcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {A}{y}\in ℝ$
20 19 11 modcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {A}{y}\mathrm{mod}1\in ℝ$
21 3 20 remulcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {B}\left({A}{y}\mathrm{mod}1\right)\in ℝ$
22 intfrac ${⊢}{B}\left({A}{y}\mathrm{mod}1\right)\in ℝ\to {B}\left({A}{y}\mathrm{mod}1\right)=⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋+\left({B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\right)$
23 21 22 syl ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {B}\left({A}{y}\mathrm{mod}1\right)=⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋+\left({B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\right)$
24 15 23 oveq12d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {B}\left({A}{x}\mathrm{mod}1\right)-{B}\left({A}{y}\mathrm{mod}1\right)=⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋+\left({B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\right)-\left(⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋+\left({B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\right)\right)$
25 24 fveq2d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to \left|{B}\left({A}{x}\mathrm{mod}1\right)-{B}\left({A}{y}\mathrm{mod}1\right)\right|=\left|⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋+\left({B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\right)-\left(⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋+\left({B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\right)\right)\right|$
26 25 adantr ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\wedge ⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋=⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋\right)\to \left|{B}\left({A}{x}\mathrm{mod}1\right)-{B}\left({A}{y}\mathrm{mod}1\right)\right|=\left|⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋+\left({B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\right)-\left(⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋+\left({B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\right)\right)\right|$
27 simpr ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\wedge ⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋=⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋\right)\to ⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋=⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋$
28 27 oveq1d ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\wedge ⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋=⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋\right)\to ⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋+\left({B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\right)=⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋+\left({B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\right)$
29 28 oveq1d ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\wedge ⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋=⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋\right)\to ⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋+\left({B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\right)-\left(⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋+\left({B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\right)\right)=⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋+\left({B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\right)-\left(⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋+\left({B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\right)\right)$
30 29 fveq2d ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\wedge ⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋=⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋\right)\to \left|⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋+\left({B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\right)-\left(⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋+\left({B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\right)\right)\right|=\left|⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋+\left({B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\right)-\left(⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋+\left({B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\right)\right)\right|$
31 21 flcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to ⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋\in ℤ$
32 31 zcnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to ⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋\in ℂ$
33 13 11 modcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\in ℝ$
34 33 recnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\in ℂ$
35 21 11 modcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\in ℝ$
36 35 recnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\in ℂ$
37 32 34 36 pnpcand ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to ⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋+\left({B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\right)-\left(⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋+\left({B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\right)\right)=\left({B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\right)-\left({B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\right)$
38 37 fveq2d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to \left|⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋+\left({B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\right)-\left(⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋+\left({B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\right)\right)\right|=\left|\left({B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\right)-\left({B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\right)\right|$
39 0red ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to 0\in ℝ$
40 1red ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to 1\in ℝ$
41 modelico ${⊢}\left({B}\left({A}{x}\mathrm{mod}1\right)\in ℝ\wedge 1\in {ℝ}^{+}\right)\to {B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\in \left[0,1\right)$
42 13 10 41 sylancl ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\in \left[0,1\right)$
43 modelico ${⊢}\left({B}\left({A}{y}\mathrm{mod}1\right)\in ℝ\wedge 1\in {ℝ}^{+}\right)\to {B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\in \left[0,1\right)$
44 21 10 43 sylancl ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\in \left[0,1\right)$
45 icodiamlt ${⊢}\left(\left(0\in ℝ\wedge 1\in ℝ\right)\wedge \left({B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\in \left[0,1\right)\wedge {B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\in \left[0,1\right)\right)\right)\to \left|\left({B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\right)-\left({B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\right)\right|<1-0$
46 39 40 42 44 45 syl22anc ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to \left|\left({B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\right)-\left({B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\right)\right|<1-0$
47 1m0e1 ${⊢}1-0=1$
48 46 47 breqtrdi ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to \left|\left({B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\right)-\left({B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\right)\right|<1$
49 38 48 eqbrtrd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to \left|⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋+\left({B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\right)-\left(⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋+\left({B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\right)\right)\right|<1$
50 49 adantr ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\wedge ⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋=⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋\right)\to \left|⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋+\left({B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\right)-\left(⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋+\left({B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\right)\right)\right|<1$
51 30 50 eqbrtrd ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\wedge ⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋=⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋\right)\to \left|⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋+\left({B}\left({A}{x}\mathrm{mod}1\right)\mathrm{mod}1\right)-\left(⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋+\left({B}\left({A}{y}\mathrm{mod}1\right)\mathrm{mod}1\right)\right)\right|<1$
52 26 51 eqbrtrd ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\wedge ⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋=⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋\right)\to \left|{B}\left({A}{x}\mathrm{mod}1\right)-{B}\left({A}{y}\mathrm{mod}1\right)\right|<1$
53 52 ex ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to \left(⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋=⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋\to \left|{B}\left({A}{x}\mathrm{mod}1\right)-{B}\left({A}{y}\mathrm{mod}1\right)\right|<1\right)$
54 12 20 resubcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to \left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\in ℝ$
55 54 recnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to \left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\in ℂ$
56 55 abscld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to \left|\left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\right|\in ℝ$
57 nngt0 ${⊢}{B}\in ℕ\to 0<{B}$
58 57 ad3antlr ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to 0<{B}$
59 58 gt0ne0d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {B}\ne 0$
60 3 59 rereccld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to \frac{1}{{B}}\in ℝ$
61 ltmul2 ${⊢}\left(\left|\left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\right|\in ℝ\wedge \frac{1}{{B}}\in ℝ\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left(\left|\left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\right|<\frac{1}{{B}}↔{B}\left|\left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\right|<{B}\left(\frac{1}{{B}}\right)\right)$
62 56 60 3 58 61 syl112anc ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to \left(\left|\left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\right|<\frac{1}{{B}}↔{B}\left|\left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\right|<{B}\left(\frac{1}{{B}}\right)\right)$
63 nnnn0 ${⊢}{B}\in ℕ\to {B}\in {ℕ}_{0}$
64 63 nn0ge0d ${⊢}{B}\in ℕ\to 0\le {B}$
65 64 ad3antlr ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to 0\le {B}$
66 3 65 absidd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to \left|{B}\right|={B}$
67 66 eqcomd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {B}=\left|{B}\right|$
68 67 oveq1d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {B}\left|\left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\right|=\left|{B}\right|\left|\left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\right|$
69 3 recnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {B}\in ℂ$
70 69 55 absmuld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to \left|{B}\left(\left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\right)\right|=\left|{B}\right|\left|\left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\right|$
71 12 recnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {A}{x}\mathrm{mod}1\in ℂ$
72 20 recnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {A}{y}\mathrm{mod}1\in ℂ$
73 69 71 72 subdid ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {B}\left(\left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\right)={B}\left({A}{x}\mathrm{mod}1\right)-{B}\left({A}{y}\mathrm{mod}1\right)$
74 73 fveq2d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to \left|{B}\left(\left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\right)\right|=\left|{B}\left({A}{x}\mathrm{mod}1\right)-{B}\left({A}{y}\mathrm{mod}1\right)\right|$
75 68 70 74 3eqtr2d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {B}\left|\left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\right|=\left|{B}\left({A}{x}\mathrm{mod}1\right)-{B}\left({A}{y}\mathrm{mod}1\right)\right|$
76 69 59 recidd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to {B}\left(\frac{1}{{B}}\right)=1$
77 75 76 breq12d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to \left({B}\left|\left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\right|<{B}\left(\frac{1}{{B}}\right)↔\left|{B}\left({A}{x}\mathrm{mod}1\right)-{B}\left({A}{y}\mathrm{mod}1\right)\right|<1\right)$
78 62 77 bitrd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to \left(\left|\left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\right|<\frac{1}{{B}}↔\left|{B}\left({A}{x}\mathrm{mod}1\right)-{B}\left({A}{y}\mathrm{mod}1\right)\right|<1\right)$
79 53 78 sylibrd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to \left(⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋=⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋\to \left|\left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\right|<\frac{1}{{B}}\right)$
80 79 anim2d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\wedge {y}\in \left(0\dots {B}\right)\right)\to \left(\left({x}<{y}\wedge ⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋=⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋\right)\to \left({x}<{y}\wedge \left|\left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\right|<\frac{1}{{B}}\right)\right)$
81 80 reximdva ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {x}\in \left(0\dots {B}\right)\right)\to \left(\exists {y}\in \left(0\dots {B}\right)\phantom{\rule{.4em}{0ex}}\left({x}<{y}\wedge ⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋=⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋\right)\to \exists {y}\in \left(0\dots {B}\right)\phantom{\rule{.4em}{0ex}}\left({x}<{y}\wedge \left|\left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\right|<\frac{1}{{B}}\right)\right)$
82 81 reximdva ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to \left(\exists {x}\in \left(0\dots {B}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in \left(0\dots {B}\right)\phantom{\rule{.4em}{0ex}}\left({x}<{y}\wedge ⌊{B}\left({A}{x}\mathrm{mod}1\right)⌋=⌊{B}\left({A}{y}\mathrm{mod}1\right)⌋\right)\to \exists {x}\in \left(0\dots {B}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in \left(0\dots {B}\right)\phantom{\rule{.4em}{0ex}}\left({x}<{y}\wedge \left|\left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\right|<\frac{1}{{B}}\right)\right)$
83 1 82 mpd ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to \exists {x}\in \left(0\dots {B}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in \left(0\dots {B}\right)\phantom{\rule{.4em}{0ex}}\left({x}<{y}\wedge \left|\left({A}{x}\mathrm{mod}1\right)-\left({A}{y}\mathrm{mod}1\right)\right|<\frac{1}{{B}}\right)$