# Metamath Proof Explorer

## Theorem irrapxlem5

Description: Lemma for irrapx1 . Switching to real intervals and fraction syntax. (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion irrapxlem5 ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left(0<{x}\wedge \left|{x}-{A}\right|<{B}\wedge \left|{x}-{A}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)$

### Proof

Step Hyp Ref Expression
1 simpr ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to {B}\in {ℝ}^{+}$
2 1 rpreccld ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to \frac{1}{{B}}\in {ℝ}^{+}$
3 2 rprege0d ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to \left(\frac{1}{{B}}\in ℝ\wedge 0\le \frac{1}{{B}}\right)$
4 flge0nn0 ${⊢}\left(\frac{1}{{B}}\in ℝ\wedge 0\le \frac{1}{{B}}\right)\to ⌊\frac{1}{{B}}⌋\in {ℕ}_{0}$
5 nn0p1nn ${⊢}⌊\frac{1}{{B}}⌋\in {ℕ}_{0}\to ⌊\frac{1}{{B}}⌋+1\in ℕ$
6 3 4 5 3syl ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to ⌊\frac{1}{{B}}⌋+1\in ℕ$
7 irrapxlem4 ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊\frac{1}{{B}}⌋+1\in ℕ\right)\to \exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}$
8 6 7 syldan ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to \exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}$
9 simplrr ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {b}\in ℕ$
10 nnq ${⊢}{b}\in ℕ\to {b}\in ℚ$
11 9 10 syl ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {b}\in ℚ$
12 simplrl ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}\in ℕ$
13 nnq ${⊢}{a}\in ℕ\to {a}\in ℚ$
14 12 13 syl ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}\in ℚ$
15 12 nnne0d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}\ne 0$
16 qdivcl ${⊢}\left({b}\in ℚ\wedge {a}\in ℚ\wedge {a}\ne 0\right)\to \frac{{b}}{{a}}\in ℚ$
17 11 14 15 16 syl3anc ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{{b}}{{a}}\in ℚ$
18 9 nnrpd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {b}\in {ℝ}^{+}$
19 12 nnrpd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}\in {ℝ}^{+}$
20 18 19 rpdivcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{{b}}{{a}}\in {ℝ}^{+}$
21 20 rpgt0d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to 0<\frac{{b}}{{a}}$
22 12 nnred ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}\in ℝ$
23 12 nnnn0d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}\in {ℕ}_{0}$
24 23 nn0ge0d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to 0\le {a}$
25 22 24 absidd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \left|{a}\right|={a}$
26 25 eqcomd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}=\left|{a}\right|$
27 26 oveq1d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}\left|\left(\frac{{b}}{{a}}\right)-{A}\right|=\left|{a}\right|\left|\left(\frac{{b}}{{a}}\right)-{A}\right|$
28 12 nncnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}\in ℂ$
29 qre ${⊢}\frac{{b}}{{a}}\in ℚ\to \frac{{b}}{{a}}\in ℝ$
30 17 29 syl ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{{b}}{{a}}\in ℝ$
31 rpre ${⊢}{A}\in {ℝ}^{+}\to {A}\in ℝ$
32 31 ad3antrrr ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {A}\in ℝ$
33 30 32 resubcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \left(\frac{{b}}{{a}}\right)-{A}\in ℝ$
34 33 recnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \left(\frac{{b}}{{a}}\right)-{A}\in ℂ$
35 28 34 absmuld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \left|{a}\left(\left(\frac{{b}}{{a}}\right)-{A}\right)\right|=\left|{a}\right|\left|\left(\frac{{b}}{{a}}\right)-{A}\right|$
36 27 35 eqtr4d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}\left|\left(\frac{{b}}{{a}}\right)-{A}\right|=\left|{a}\left(\left(\frac{{b}}{{a}}\right)-{A}\right)\right|$
37 qcn ${⊢}\frac{{b}}{{a}}\in ℚ\to \frac{{b}}{{a}}\in ℂ$
38 17 37 syl ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{{b}}{{a}}\in ℂ$
39 rpcn ${⊢}{A}\in {ℝ}^{+}\to {A}\in ℂ$
40 39 ad3antrrr ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {A}\in ℂ$
41 28 38 40 subdid ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}\left(\left(\frac{{b}}{{a}}\right)-{A}\right)={a}\left(\frac{{b}}{{a}}\right)-{a}{A}$
42 9 nncnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {b}\in ℂ$
43 42 28 15 divcan2d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}\left(\frac{{b}}{{a}}\right)={b}$
44 28 40 mulcomd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}{A}={A}{a}$
45 43 44 oveq12d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}\left(\frac{{b}}{{a}}\right)-{a}{A}={b}-{A}{a}$
46 41 45 eqtrd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}\left(\left(\frac{{b}}{{a}}\right)-{A}\right)={b}-{A}{a}$
47 46 fveq2d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \left|{a}\left(\left(\frac{{b}}{{a}}\right)-{A}\right)\right|=\left|{b}-{A}{a}\right|$
48 32 22 remulcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {A}{a}\in ℝ$
49 48 recnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {A}{a}\in ℂ$
50 42 49 abssubd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \left|{b}-{A}{a}\right|=\left|{A}{a}-{b}\right|$
51 36 47 50 3eqtrd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}\left|\left(\frac{{b}}{{a}}\right)-{A}\right|=\left|{A}{a}-{b}\right|$
52 9 nnred ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {b}\in ℝ$
53 48 52 resubcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {A}{a}-{b}\in ℝ$
54 53 recnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {A}{a}-{b}\in ℂ$
55 54 abscld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \left|{A}{a}-{b}\right|\in ℝ$
56 simpllr ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {B}\in {ℝ}^{+}$
57 56 rprecred ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{1}{{B}}\in ℝ$
58 56 rpreccld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{1}{{B}}\in {ℝ}^{+}$
59 58 rpge0d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to 0\le \frac{1}{{B}}$
60 57 59 4 syl2anc ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to ⌊\frac{1}{{B}}⌋\in {ℕ}_{0}$
61 60 5 syl ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to ⌊\frac{1}{{B}}⌋+1\in ℕ$
62 61 nnrpd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to ⌊\frac{1}{{B}}⌋+1\in {ℝ}^{+}$
63 62 19 ifcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)\in {ℝ}^{+}$
64 63 rprecred ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\in ℝ$
65 56 rpred ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {B}\in ℝ$
66 22 65 remulcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}{B}\in ℝ$
67 simpr ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}$
68 58 rprecred ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{1}{\frac{1}{{B}}}\in ℝ$
69 61 nnred ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to ⌊\frac{1}{{B}}⌋+1\in ℝ$
70 69 22 ifcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)\in ℝ$
71 fllep1 ${⊢}\frac{1}{{B}}\in ℝ\to \frac{1}{{B}}\le ⌊\frac{1}{{B}}⌋+1$
72 57 71 syl ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{1}{{B}}\le ⌊\frac{1}{{B}}⌋+1$
73 max2 ${⊢}\left({a}\in ℝ\wedge ⌊\frac{1}{{B}}⌋+1\in ℝ\right)\to ⌊\frac{1}{{B}}⌋+1\le if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)$
74 22 69 73 syl2anc ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to ⌊\frac{1}{{B}}⌋+1\le if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)$
75 57 69 70 72 74 letrd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{1}{{B}}\le if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)$
76 58 63 lerecd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \left(\frac{1}{{B}}\le if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)↔\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\le \frac{1}{\frac{1}{{B}}}\right)$
77 75 76 mpbid ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\le \frac{1}{\frac{1}{{B}}}$
78 65 recnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {B}\in ℂ$
79 56 rpne0d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {B}\ne 0$
80 78 79 recrecd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{1}{\frac{1}{{B}}}={B}$
81 78 mulid2d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to 1{B}={B}$
82 80 81 eqtr4d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{1}{\frac{1}{{B}}}=1{B}$
83 12 nnge1d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to 1\le {a}$
84 1red ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to 1\in ℝ$
85 84 22 56 lemul1d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \left(1\le {a}↔1{B}\le {a}{B}\right)$
86 83 85 mpbid ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to 1{B}\le {a}{B}$
87 82 86 eqbrtrd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{1}{\frac{1}{{B}}}\le {a}{B}$
88 64 68 66 77 87 letrd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\le {a}{B}$
89 55 64 66 67 88 ltletrd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \left|{A}{a}-{b}\right|<{a}{B}$
90 51 89 eqbrtrd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}\left|\left(\frac{{b}}{{a}}\right)-{A}\right|<{a}{B}$
91 34 abscld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \left|\left(\frac{{b}}{{a}}\right)-{A}\right|\in ℝ$
92 12 nngt0d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to 0<{a}$
93 ltmul2 ${⊢}\left(\left|\left(\frac{{b}}{{a}}\right)-{A}\right|\in ℝ\wedge {B}\in ℝ\wedge \left({a}\in ℝ\wedge 0<{a}\right)\right)\to \left(\left|\left(\frac{{b}}{{a}}\right)-{A}\right|<{B}↔{a}\left|\left(\frac{{b}}{{a}}\right)-{A}\right|<{a}{B}\right)$
94 91 65 22 92 93 syl112anc ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \left(\left|\left(\frac{{b}}{{a}}\right)-{A}\right|<{B}↔{a}\left|\left(\frac{{b}}{{a}}\right)-{A}\right|<{a}{B}\right)$
95 90 94 mpbird ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \left|\left(\frac{{b}}{{a}}\right)-{A}\right|<{B}$
96 22 22 remulcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}{a}\in ℝ$
97 22 15 msqgt0d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to 0<{a}{a}$
98 97 gt0ne0d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}{a}\ne 0$
99 96 98 rereccld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{1}{{a}{a}}\in ℝ$
100 qdencl ${⊢}\frac{{b}}{{a}}\in ℚ\to \mathrm{denom}\left(\frac{{b}}{{a}}\right)\in ℕ$
101 17 100 syl ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \mathrm{denom}\left(\frac{{b}}{{a}}\right)\in ℕ$
102 101 nnred ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \mathrm{denom}\left(\frac{{b}}{{a}}\right)\in ℝ$
103 102 102 remulcld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \mathrm{denom}\left(\frac{{b}}{{a}}\right)\mathrm{denom}\left(\frac{{b}}{{a}}\right)\in ℝ$
104 101 nnne0d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \mathrm{denom}\left(\frac{{b}}{{a}}\right)\ne 0$
105 102 104 msqgt0d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to 0<\mathrm{denom}\left(\frac{{b}}{{a}}\right)\mathrm{denom}\left(\frac{{b}}{{a}}\right)$
106 105 gt0ne0d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \mathrm{denom}\left(\frac{{b}}{{a}}\right)\mathrm{denom}\left(\frac{{b}}{{a}}\right)\ne 0$
107 103 106 rereccld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{1}{\mathrm{denom}\left(\frac{{b}}{{a}}\right)\mathrm{denom}\left(\frac{{b}}{{a}}\right)}\in ℝ$
108 22 15 rereccld ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{1}{{a}}\in ℝ$
109 max1 ${⊢}\left({a}\in ℝ\wedge ⌊\frac{1}{{B}}⌋+1\in ℝ\right)\to {a}\le if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)$
110 22 69 109 syl2anc ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}\le if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)$
111 19 63 lerecd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \left({a}\le if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)↔\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\le \frac{1}{{a}}\right)$
112 110 111 mpbid ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\le \frac{1}{{a}}$
113 55 64 108 67 112 ltletrd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \left|{A}{a}-{b}\right|<\frac{1}{{a}}$
114 28 28 28 15 15 divdiv1d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{\frac{{a}}{{a}}}{{a}}=\frac{{a}}{{a}{a}}$
115 28 15 dividd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{{a}}{{a}}=1$
116 115 oveq1d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{\frac{{a}}{{a}}}{{a}}=\frac{1}{{a}}$
117 96 recnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}{a}\in ℂ$
118 28 117 98 divrecd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{{a}}{{a}{a}}={a}\left(\frac{1}{{a}{a}}\right)$
119 114 116 118 3eqtr3rd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}\left(\frac{1}{{a}{a}}\right)=\frac{1}{{a}}$
120 113 51 119 3brtr4d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {a}\left|\left(\frac{{b}}{{a}}\right)-{A}\right|<{a}\left(\frac{1}{{a}{a}}\right)$
121 ltmul2 ${⊢}\left(\left|\left(\frac{{b}}{{a}}\right)-{A}\right|\in ℝ\wedge \frac{1}{{a}{a}}\in ℝ\wedge \left({a}\in ℝ\wedge 0<{a}\right)\right)\to \left(\left|\left(\frac{{b}}{{a}}\right)-{A}\right|<\frac{1}{{a}{a}}↔{a}\left|\left(\frac{{b}}{{a}}\right)-{A}\right|<{a}\left(\frac{1}{{a}{a}}\right)\right)$
122 91 99 22 92 121 syl112anc ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \left(\left|\left(\frac{{b}}{{a}}\right)-{A}\right|<\frac{1}{{a}{a}}↔{a}\left|\left(\frac{{b}}{{a}}\right)-{A}\right|<{a}\left(\frac{1}{{a}{a}}\right)\right)$
123 120 122 mpbird ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \left|\left(\frac{{b}}{{a}}\right)-{A}\right|<\frac{1}{{a}{a}}$
124 9 nnzd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {b}\in ℤ$
125 divdenle ${⊢}\left({b}\in ℤ\wedge {a}\in ℕ\right)\to \mathrm{denom}\left(\frac{{b}}{{a}}\right)\le {a}$
126 124 12 125 syl2anc ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \mathrm{denom}\left(\frac{{b}}{{a}}\right)\le {a}$
127 101 nnnn0d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \mathrm{denom}\left(\frac{{b}}{{a}}\right)\in {ℕ}_{0}$
128 127 nn0ge0d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to 0\le \mathrm{denom}\left(\frac{{b}}{{a}}\right)$
129 le2msq ${⊢}\left(\left(\mathrm{denom}\left(\frac{{b}}{{a}}\right)\in ℝ\wedge 0\le \mathrm{denom}\left(\frac{{b}}{{a}}\right)\right)\wedge \left({a}\in ℝ\wedge 0\le {a}\right)\right)\to \left(\mathrm{denom}\left(\frac{{b}}{{a}}\right)\le {a}↔\mathrm{denom}\left(\frac{{b}}{{a}}\right)\mathrm{denom}\left(\frac{{b}}{{a}}\right)\le {a}{a}\right)$
130 102 128 22 24 129 syl22anc ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \left(\mathrm{denom}\left(\frac{{b}}{{a}}\right)\le {a}↔\mathrm{denom}\left(\frac{{b}}{{a}}\right)\mathrm{denom}\left(\frac{{b}}{{a}}\right)\le {a}{a}\right)$
131 126 130 mpbid ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \mathrm{denom}\left(\frac{{b}}{{a}}\right)\mathrm{denom}\left(\frac{{b}}{{a}}\right)\le {a}{a}$
132 lerec ${⊢}\left(\left(\mathrm{denom}\left(\frac{{b}}{{a}}\right)\mathrm{denom}\left(\frac{{b}}{{a}}\right)\in ℝ\wedge 0<\mathrm{denom}\left(\frac{{b}}{{a}}\right)\mathrm{denom}\left(\frac{{b}}{{a}}\right)\right)\wedge \left({a}{a}\in ℝ\wedge 0<{a}{a}\right)\right)\to \left(\mathrm{denom}\left(\frac{{b}}{{a}}\right)\mathrm{denom}\left(\frac{{b}}{{a}}\right)\le {a}{a}↔\frac{1}{{a}{a}}\le \frac{1}{\mathrm{denom}\left(\frac{{b}}{{a}}\right)\mathrm{denom}\left(\frac{{b}}{{a}}\right)}\right)$
133 103 105 96 97 132 syl22anc ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \left(\mathrm{denom}\left(\frac{{b}}{{a}}\right)\mathrm{denom}\left(\frac{{b}}{{a}}\right)\le {a}{a}↔\frac{1}{{a}{a}}\le \frac{1}{\mathrm{denom}\left(\frac{{b}}{{a}}\right)\mathrm{denom}\left(\frac{{b}}{{a}}\right)}\right)$
134 131 133 mpbid ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{1}{{a}{a}}\le \frac{1}{\mathrm{denom}\left(\frac{{b}}{{a}}\right)\mathrm{denom}\left(\frac{{b}}{{a}}\right)}$
135 91 99 107 123 134 ltletrd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \left|\left(\frac{{b}}{{a}}\right)-{A}\right|<\frac{1}{\mathrm{denom}\left(\frac{{b}}{{a}}\right)\mathrm{denom}\left(\frac{{b}}{{a}}\right)}$
136 101 nncnd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \mathrm{denom}\left(\frac{{b}}{{a}}\right)\in ℂ$
137 2nn0 ${⊢}2\in {ℕ}_{0}$
138 expneg ${⊢}\left(\mathrm{denom}\left(\frac{{b}}{{a}}\right)\in ℂ\wedge 2\in {ℕ}_{0}\right)\to {\mathrm{denom}\left(\frac{{b}}{{a}}\right)}^{-2}=\frac{1}{{\mathrm{denom}\left(\frac{{b}}{{a}}\right)}^{2}}$
139 136 137 138 sylancl ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {\mathrm{denom}\left(\frac{{b}}{{a}}\right)}^{-2}=\frac{1}{{\mathrm{denom}\left(\frac{{b}}{{a}}\right)}^{2}}$
140 136 sqvald ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {\mathrm{denom}\left(\frac{{b}}{{a}}\right)}^{2}=\mathrm{denom}\left(\frac{{b}}{{a}}\right)\mathrm{denom}\left(\frac{{b}}{{a}}\right)$
141 140 oveq2d ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \frac{1}{{\mathrm{denom}\left(\frac{{b}}{{a}}\right)}^{2}}=\frac{1}{\mathrm{denom}\left(\frac{{b}}{{a}}\right)\mathrm{denom}\left(\frac{{b}}{{a}}\right)}$
142 139 141 eqtrd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to {\mathrm{denom}\left(\frac{{b}}{{a}}\right)}^{-2}=\frac{1}{\mathrm{denom}\left(\frac{{b}}{{a}}\right)\mathrm{denom}\left(\frac{{b}}{{a}}\right)}$
143 135 142 breqtrrd ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \left|\left(\frac{{b}}{{a}}\right)-{A}\right|<{\mathrm{denom}\left(\frac{{b}}{{a}}\right)}^{-2}$
144 breq2 ${⊢}{x}=\frac{{b}}{{a}}\to \left(0<{x}↔0<\frac{{b}}{{a}}\right)$
145 fvoveq1 ${⊢}{x}=\frac{{b}}{{a}}\to \left|{x}-{A}\right|=\left|\left(\frac{{b}}{{a}}\right)-{A}\right|$
146 145 breq1d ${⊢}{x}=\frac{{b}}{{a}}\to \left(\left|{x}-{A}\right|<{B}↔\left|\left(\frac{{b}}{{a}}\right)-{A}\right|<{B}\right)$
147 fveq2 ${⊢}{x}=\frac{{b}}{{a}}\to \mathrm{denom}\left({x}\right)=\mathrm{denom}\left(\frac{{b}}{{a}}\right)$
148 147 oveq1d ${⊢}{x}=\frac{{b}}{{a}}\to {\mathrm{denom}\left({x}\right)}^{-2}={\mathrm{denom}\left(\frac{{b}}{{a}}\right)}^{-2}$
149 145 148 breq12d ${⊢}{x}=\frac{{b}}{{a}}\to \left(\left|{x}-{A}\right|<{\mathrm{denom}\left({x}\right)}^{-2}↔\left|\left(\frac{{b}}{{a}}\right)-{A}\right|<{\mathrm{denom}\left(\frac{{b}}{{a}}\right)}^{-2}\right)$
150 144 146 149 3anbi123d ${⊢}{x}=\frac{{b}}{{a}}\to \left(\left(0<{x}\wedge \left|{x}-{A}\right|<{B}\wedge \left|{x}-{A}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)↔\left(0<\frac{{b}}{{a}}\wedge \left|\left(\frac{{b}}{{a}}\right)-{A}\right|<{B}\wedge \left|\left(\frac{{b}}{{a}}\right)-{A}\right|<{\mathrm{denom}\left(\frac{{b}}{{a}}\right)}^{-2}\right)\right)$
151 150 rspcev ${⊢}\left(\frac{{b}}{{a}}\in ℚ\wedge \left(0<\frac{{b}}{{a}}\wedge \left|\left(\frac{{b}}{{a}}\right)-{A}\right|<{B}\wedge \left|\left(\frac{{b}}{{a}}\right)-{A}\right|<{\mathrm{denom}\left(\frac{{b}}{{a}}\right)}^{-2}\right)\right)\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left(0<{x}\wedge \left|{x}-{A}\right|<{B}\wedge \left|{x}-{A}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)$
152 17 21 95 143 151 syl13anc ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\right)\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left(0<{x}\wedge \left|{x}-{A}\right|<{B}\wedge \left|{x}-{A}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)$
153 152 ex ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({a}\in ℕ\wedge {b}\in ℕ\right)\right)\to \left(\left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left(0<{x}\wedge \left|{x}-{A}\right|<{B}\wedge \left|{x}-{A}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)\right)$
154 153 rexlimdvva ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to \left(\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le ⌊\frac{1}{{B}}⌋+1,⌊\frac{1}{{B}}⌋+1,{a}\right)}\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left(0<{x}\wedge \left|{x}-{A}\right|<{B}\wedge \left|{x}-{A}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)\right)$
155 8 154 mpd ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left(0<{x}\wedge \left|{x}-{A}\right|<{B}\wedge \left|{x}-{A}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)$