# Metamath Proof Explorer

## Theorem irrapxlem3

Description: Lemma for irrapx1 . By subtraction, there is a multiple very close to an integer. (Contributed by Stefan O'Rear, 13-Sep-2014)

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

### Proof

Step Hyp Ref Expression
1 irrapxlem2 ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to \exists {a}\in \left(0\dots {B}\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in \left(0\dots {B}\right)\phantom{\rule{.4em}{0ex}}\left({a}<{b}\wedge \left|\left({A}{a}\mathrm{mod}1\right)-\left({A}{b}\mathrm{mod}1\right)\right|<\frac{1}{{B}}\right)$
2 1m1e0 ${⊢}1-1=0$
3 elfzelz ${⊢}{a}\in \left(0\dots {B}\right)\to {a}\in ℤ$
4 3 ad2antrl ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\to {a}\in ℤ$
5 4 zred ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\to {a}\in ℝ$
6 elfzelz ${⊢}{b}\in \left(0\dots {B}\right)\to {b}\in ℤ$
7 6 ad2antll ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\to {b}\in ℤ$
8 7 zred ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\to {b}\in ℝ$
9 5 8 posdifd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\to \left({a}<{b}↔0<{b}-{a}\right)$
10 9 biimpa ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to 0<{b}-{a}$
11 2 10 eqbrtrid ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to 1-1<{b}-{a}$
12 1z ${⊢}1\in ℤ$
13 simplrr ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {b}\in \left(0\dots {B}\right)$
14 13 6 syl ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {b}\in ℤ$
15 simplrl ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {a}\in \left(0\dots {B}\right)$
16 15 3 syl ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {a}\in ℤ$
17 14 16 zsubcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {b}-{a}\in ℤ$
18 zlem1lt ${⊢}\left(1\in ℤ\wedge {b}-{a}\in ℤ\right)\to \left(1\le {b}-{a}↔1-1<{b}-{a}\right)$
19 12 17 18 sylancr ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to \left(1\le {b}-{a}↔1-1<{b}-{a}\right)$
20 11 19 mpbird ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to 1\le {b}-{a}$
21 14 zred ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {b}\in ℝ$
22 16 zred ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {a}\in ℝ$
23 21 22 resubcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {b}-{a}\in ℝ$
24 0red ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to 0\in ℝ$
25 21 24 resubcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {b}-0\in ℝ$
26 simpllr ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {B}\in ℕ$
27 26 nnred ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {B}\in ℝ$
28 elfzle1 ${⊢}{a}\in \left(0\dots {B}\right)\to 0\le {a}$
29 15 28 syl ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to 0\le {a}$
30 24 22 21 29 lesub2dd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {b}-{a}\le {b}-0$
31 21 recnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {b}\in ℂ$
32 31 subid1d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {b}-0={b}$
33 elfzle2 ${⊢}{b}\in \left(0\dots {B}\right)\to {b}\le {B}$
34 13 33 syl ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {b}\le {B}$
35 32 34 eqbrtrd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {b}-0\le {B}$
36 23 25 27 30 35 letrd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {b}-{a}\le {B}$
37 12 a1i ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to 1\in ℤ$
38 26 nnzd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {B}\in ℤ$
39 elfz ${⊢}\left({b}-{a}\in ℤ\wedge 1\in ℤ\wedge {B}\in ℤ\right)\to \left({b}-{a}\in \left(1\dots {B}\right)↔\left(1\le {b}-{a}\wedge {b}-{a}\le {B}\right)\right)$
40 17 37 38 39 syl3anc ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to \left({b}-{a}\in \left(1\dots {B}\right)↔\left(1\le {b}-{a}\wedge {b}-{a}\le {B}\right)\right)$
41 20 36 40 mpbir2and ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {b}-{a}\in \left(1\dots {B}\right)$
42 41 adantrr ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge \left({a}<{b}\wedge \left|\left({A}{a}\mathrm{mod}1\right)-\left({A}{b}\mathrm{mod}1\right)\right|<\frac{1}{{B}}\right)\right)\to {b}-{a}\in \left(1\dots {B}\right)$
43 rpre ${⊢}{A}\in {ℝ}^{+}\to {A}\in ℝ$
44 43 ad3antrrr ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {A}\in ℝ$
45 44 22 remulcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {A}{a}\in ℝ$
46 44 21 remulcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {A}{b}\in ℝ$
47 simpr ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {a}<{b}$
48 22 21 47 ltled ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {a}\le {b}$
49 rpgt0 ${⊢}{A}\in {ℝ}^{+}\to 0<{A}$
50 49 ad3antrrr ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to 0<{A}$
51 lemul2 ${⊢}\left({a}\in ℝ\wedge {b}\in ℝ\wedge \left({A}\in ℝ\wedge 0<{A}\right)\right)\to \left({a}\le {b}↔{A}{a}\le {A}{b}\right)$
52 22 21 44 50 51 syl112anc ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to \left({a}\le {b}↔{A}{a}\le {A}{b}\right)$
53 48 52 mpbid ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {A}{a}\le {A}{b}$
54 flword2 ${⊢}\left({A}{a}\in ℝ\wedge {A}{b}\in ℝ\wedge {A}{a}\le {A}{b}\right)\to ⌊{A}{b}⌋\in {ℤ}_{\ge ⌊{A}{a}⌋}$
55 45 46 53 54 syl3anc ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to ⌊{A}{b}⌋\in {ℤ}_{\ge ⌊{A}{a}⌋}$
56 uznn0sub ${⊢}⌊{A}{b}⌋\in {ℤ}_{\ge ⌊{A}{a}⌋}\to ⌊{A}{b}⌋-⌊{A}{a}⌋\in {ℕ}_{0}$
57 55 56 syl ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to ⌊{A}{b}⌋-⌊{A}{a}⌋\in {ℕ}_{0}$
58 57 adantrr ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge \left({a}<{b}\wedge \left|\left({A}{a}\mathrm{mod}1\right)-\left({A}{b}\mathrm{mod}1\right)\right|<\frac{1}{{B}}\right)\right)\to ⌊{A}{b}⌋-⌊{A}{a}⌋\in {ℕ}_{0}$
59 44 recnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {A}\in ℂ$
60 22 recnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {a}\in ℂ$
61 59 31 60 subdid ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {A}\left({b}-{a}\right)={A}{b}-{A}{a}$
62 61 oveq1d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {A}\left({b}-{a}\right)-\left(⌊{A}{b}⌋-⌊{A}{a}⌋\right)={A}{b}-{A}{a}-\left(⌊{A}{b}⌋-⌊{A}{a}⌋\right)$
63 46 recnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {A}{b}\in ℂ$
64 45 recnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {A}{a}\in ℂ$
65 46 flcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to ⌊{A}{b}⌋\in ℤ$
66 65 zcnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to ⌊{A}{b}⌋\in ℂ$
67 45 flcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to ⌊{A}{a}⌋\in ℤ$
68 67 zcnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to ⌊{A}{a}⌋\in ℂ$
69 63 64 66 68 sub4d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {A}{b}-{A}{a}-\left(⌊{A}{b}⌋-⌊{A}{a}⌋\right)={A}{b}-⌊{A}{b}⌋-\left({A}{a}-⌊{A}{a}⌋\right)$
70 modfrac ${⊢}{A}{b}\in ℝ\to {A}{b}\mathrm{mod}1={A}{b}-⌊{A}{b}⌋$
71 46 70 syl ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {A}{b}\mathrm{mod}1={A}{b}-⌊{A}{b}⌋$
72 71 eqcomd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {A}{b}-⌊{A}{b}⌋={A}{b}\mathrm{mod}1$
73 modfrac ${⊢}{A}{a}\in ℝ\to {A}{a}\mathrm{mod}1={A}{a}-⌊{A}{a}⌋$
74 45 73 syl ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {A}{a}\mathrm{mod}1={A}{a}-⌊{A}{a}⌋$
75 74 eqcomd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {A}{a}-⌊{A}{a}⌋={A}{a}\mathrm{mod}1$
76 72 75 oveq12d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {A}{b}-⌊{A}{b}⌋-\left({A}{a}-⌊{A}{a}⌋\right)=\left({A}{b}\mathrm{mod}1\right)-\left({A}{a}\mathrm{mod}1\right)$
77 62 69 76 3eqtrd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {A}\left({b}-{a}\right)-\left(⌊{A}{b}⌋-⌊{A}{a}⌋\right)=\left({A}{b}\mathrm{mod}1\right)-\left({A}{a}\mathrm{mod}1\right)$
78 77 fveq2d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to \left|{A}\left({b}-{a}\right)-\left(⌊{A}{b}⌋-⌊{A}{a}⌋\right)\right|=\left|\left({A}{b}\mathrm{mod}1\right)-\left({A}{a}\mathrm{mod}1\right)\right|$
79 1rp ${⊢}1\in {ℝ}^{+}$
80 79 a1i ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to 1\in {ℝ}^{+}$
81 46 80 modcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {A}{b}\mathrm{mod}1\in ℝ$
82 81 recnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {A}{b}\mathrm{mod}1\in ℂ$
83 45 80 modcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {A}{a}\mathrm{mod}1\in ℝ$
84 83 recnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to {A}{a}\mathrm{mod}1\in ℂ$
85 82 84 abssubd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to \left|\left({A}{b}\mathrm{mod}1\right)-\left({A}{a}\mathrm{mod}1\right)\right|=\left|\left({A}{a}\mathrm{mod}1\right)-\left({A}{b}\mathrm{mod}1\right)\right|$
86 78 85 eqtr2d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to \left|\left({A}{a}\mathrm{mod}1\right)-\left({A}{b}\mathrm{mod}1\right)\right|=\left|{A}\left({b}-{a}\right)-\left(⌊{A}{b}⌋-⌊{A}{a}⌋\right)\right|$
87 86 breq1d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to \left(\left|\left({A}{a}\mathrm{mod}1\right)-\left({A}{b}\mathrm{mod}1\right)\right|<\frac{1}{{B}}↔\left|{A}\left({b}-{a}\right)-\left(⌊{A}{b}⌋-⌊{A}{a}⌋\right)\right|<\frac{1}{{B}}\right)$
88 87 biimpd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge {a}<{b}\right)\to \left(\left|\left({A}{a}\mathrm{mod}1\right)-\left({A}{b}\mathrm{mod}1\right)\right|<\frac{1}{{B}}\to \left|{A}\left({b}-{a}\right)-\left(⌊{A}{b}⌋-⌊{A}{a}⌋\right)\right|<\frac{1}{{B}}\right)$
89 88 impr ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge \left({a}<{b}\wedge \left|\left({A}{a}\mathrm{mod}1\right)-\left({A}{b}\mathrm{mod}1\right)\right|<\frac{1}{{B}}\right)\right)\to \left|{A}\left({b}-{a}\right)-\left(⌊{A}{b}⌋-⌊{A}{a}⌋\right)\right|<\frac{1}{{B}}$
90 oveq2 ${⊢}{x}={b}-{a}\to {A}{x}={A}\left({b}-{a}\right)$
91 90 fvoveq1d ${⊢}{x}={b}-{a}\to \left|{A}{x}-{y}\right|=\left|{A}\left({b}-{a}\right)-{y}\right|$
92 91 breq1d ${⊢}{x}={b}-{a}\to \left(\left|{A}{x}-{y}\right|<\frac{1}{{B}}↔\left|{A}\left({b}-{a}\right)-{y}\right|<\frac{1}{{B}}\right)$
93 oveq2 ${⊢}{y}=⌊{A}{b}⌋-⌊{A}{a}⌋\to {A}\left({b}-{a}\right)-{y}={A}\left({b}-{a}\right)-\left(⌊{A}{b}⌋-⌊{A}{a}⌋\right)$
94 93 fveq2d ${⊢}{y}=⌊{A}{b}⌋-⌊{A}{a}⌋\to \left|{A}\left({b}-{a}\right)-{y}\right|=\left|{A}\left({b}-{a}\right)-\left(⌊{A}{b}⌋-⌊{A}{a}⌋\right)\right|$
95 94 breq1d ${⊢}{y}=⌊{A}{b}⌋-⌊{A}{a}⌋\to \left(\left|{A}\left({b}-{a}\right)-{y}\right|<\frac{1}{{B}}↔\left|{A}\left({b}-{a}\right)-\left(⌊{A}{b}⌋-⌊{A}{a}⌋\right)\right|<\frac{1}{{B}}\right)$
96 92 95 rspc2ev ${⊢}\left({b}-{a}\in \left(1\dots {B}\right)\wedge ⌊{A}{b}⌋-⌊{A}{a}⌋\in {ℕ}_{0}\wedge \left|{A}\left({b}-{a}\right)-\left(⌊{A}{b}⌋-⌊{A}{a}⌋\right)\right|<\frac{1}{{B}}\right)\to \exists {x}\in \left(1\dots {B}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left|{A}{x}-{y}\right|<\frac{1}{{B}}$
97 42 58 89 96 syl3anc ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\wedge \left({a}<{b}\wedge \left|\left({A}{a}\mathrm{mod}1\right)-\left({A}{b}\mathrm{mod}1\right)\right|<\frac{1}{{B}}\right)\right)\to \exists {x}\in \left(1\dots {B}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left|{A}{x}-{y}\right|<\frac{1}{{B}}$
98 97 ex ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge \left({a}\in \left(0\dots {B}\right)\wedge {b}\in \left(0\dots {B}\right)\right)\right)\to \left(\left({a}<{b}\wedge \left|\left({A}{a}\mathrm{mod}1\right)-\left({A}{b}\mathrm{mod}1\right)\right|<\frac{1}{{B}}\right)\to \exists {x}\in \left(1\dots {B}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left|{A}{x}-{y}\right|<\frac{1}{{B}}\right)$
99 98 rexlimdvva ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to \left(\exists {a}\in \left(0\dots {B}\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in \left(0\dots {B}\right)\phantom{\rule{.4em}{0ex}}\left({a}<{b}\wedge \left|\left({A}{a}\mathrm{mod}1\right)-\left({A}{b}\mathrm{mod}1\right)\right|<\frac{1}{{B}}\right)\to \exists {x}\in \left(1\dots {B}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left|{A}{x}-{y}\right|<\frac{1}{{B}}\right)$
100 1 99 mpd ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to \exists {x}\in \left(1\dots {B}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left|{A}{x}-{y}\right|<\frac{1}{{B}}$