# Metamath Proof Explorer

## Theorem irrapxlem4

Description: Lemma for irrapx1 . Eliminate ranges, use positivity of the input to force positivity of the output by increasing B as needed. (Contributed by Stefan O'Rear, 13-Sep-2014)

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

### Proof

Step Hyp Ref Expression
1 elfznn ${⊢}{a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\to {a}\in ℕ$
2 1 ad3antlr ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {a}\in ℕ$
3 nn0z ${⊢}{b}\in {ℕ}_{0}\to {b}\in ℤ$
4 3 ad2antlr ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {b}\in ℤ$
5 simpl ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to {A}\in {ℝ}^{+}$
6 5 ad3antrrr ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {A}\in {ℝ}^{+}$
7 6 rpred ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {A}\in ℝ$
8 2 nnred ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {a}\in ℝ$
9 7 8 remulcld ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {A}{a}\in ℝ$
10 nn0re ${⊢}{b}\in {ℕ}_{0}\to {b}\in ℝ$
11 10 ad2antlr ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {b}\in ℝ$
12 9 11 resubcld ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {A}{a}-{b}\in ℝ$
13 12 recnd ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {A}{a}-{b}\in ℂ$
14 13 abscld ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \left|{A}{a}-{b}\right|\in ℝ$
15 5 rpreccld ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to \frac{1}{{A}}\in {ℝ}^{+}$
16 15 rprege0d ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to \left(\frac{1}{{A}}\in ℝ\wedge 0\le \frac{1}{{A}}\right)$
17 flge0nn0 ${⊢}\left(\frac{1}{{A}}\in ℝ\wedge 0\le \frac{1}{{A}}\right)\to ⌊\frac{1}{{A}}⌋\in {ℕ}_{0}$
18 nn0p1nn ${⊢}⌊\frac{1}{{A}}⌋\in {ℕ}_{0}\to ⌊\frac{1}{{A}}⌋+1\in ℕ$
19 16 17 18 3syl ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to ⌊\frac{1}{{A}}⌋+1\in ℕ$
20 19 ad3antrrr ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to ⌊\frac{1}{{A}}⌋+1\in ℕ$
21 simpr ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to {B}\in ℕ$
22 21 ad3antrrr ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {B}\in ℕ$
23 20 22 ifcld ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\in ℕ$
24 23 nnrecred ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\in ℝ$
25 0red ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to 0\in ℝ$
26 9 25 resubcld ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {A}{a}-0\in ℝ$
27 simpr ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}$
28 20 nnrecred ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \frac{1}{⌊\frac{1}{{A}}⌋+1}\in ℝ$
29 22 nnred ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {B}\in ℝ$
30 6 rprecred ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \frac{1}{{A}}\in ℝ$
31 30 flcld ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to ⌊\frac{1}{{A}}⌋\in ℤ$
32 31 zred ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to ⌊\frac{1}{{A}}⌋\in ℝ$
33 peano2re ${⊢}⌊\frac{1}{{A}}⌋\in ℝ\to ⌊\frac{1}{{A}}⌋+1\in ℝ$
34 32 33 syl ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to ⌊\frac{1}{{A}}⌋+1\in ℝ$
35 max2 ${⊢}\left({B}\in ℝ\wedge ⌊\frac{1}{{A}}⌋+1\in ℝ\right)\to ⌊\frac{1}{{A}}⌋+1\le if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)$
36 29 34 35 syl2anc ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to ⌊\frac{1}{{A}}⌋+1\le if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)$
37 20 nngt0d ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to 0<⌊\frac{1}{{A}}⌋+1$
38 23 nnred ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\in ℝ$
39 23 nngt0d ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to 0
40 lerec ${⊢}\left(\left(⌊\frac{1}{{A}}⌋+1\in ℝ\wedge 0<⌊\frac{1}{{A}}⌋+1\right)\wedge \left(if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\in ℝ\wedge 0
41 34 37 38 39 40 syl22anc ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \left(⌊\frac{1}{{A}}⌋+1\le if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)↔\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\le \frac{1}{⌊\frac{1}{{A}}⌋+1}\right)$
42 36 41 mpbid ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\le \frac{1}{⌊\frac{1}{{A}}⌋+1}$
43 fllep1 ${⊢}\frac{1}{{A}}\in ℝ\to \frac{1}{{A}}\le ⌊\frac{1}{{A}}⌋+1$
44 30 43 syl ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \frac{1}{{A}}\le ⌊\frac{1}{{A}}⌋+1$
45 20 nncnd ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to ⌊\frac{1}{{A}}⌋+1\in ℂ$
46 20 nnne0d ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to ⌊\frac{1}{{A}}⌋+1\ne 0$
47 45 46 recrecd ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \frac{1}{\frac{1}{⌊\frac{1}{{A}}⌋+1}}=⌊\frac{1}{{A}}⌋+1$
48 44 47 breqtrrd ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \frac{1}{{A}}\le \frac{1}{\frac{1}{⌊\frac{1}{{A}}⌋+1}}$
49 34 37 recgt0d ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to 0<\frac{1}{⌊\frac{1}{{A}}⌋+1}$
50 6 rpgt0d ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to 0<{A}$
51 lerec ${⊢}\left(\left(\frac{1}{⌊\frac{1}{{A}}⌋+1}\in ℝ\wedge 0<\frac{1}{⌊\frac{1}{{A}}⌋+1}\right)\wedge \left({A}\in ℝ\wedge 0<{A}\right)\right)\to \left(\frac{1}{⌊\frac{1}{{A}}⌋+1}\le {A}↔\frac{1}{{A}}\le \frac{1}{\frac{1}{⌊\frac{1}{{A}}⌋+1}}\right)$
52 28 49 7 50 51 syl22anc ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \left(\frac{1}{⌊\frac{1}{{A}}⌋+1}\le {A}↔\frac{1}{{A}}\le \frac{1}{\frac{1}{⌊\frac{1}{{A}}⌋+1}}\right)$
53 48 52 mpbird ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \frac{1}{⌊\frac{1}{{A}}⌋+1}\le {A}$
54 24 28 7 42 53 letrd ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\le {A}$
55 7 recnd ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {A}\in ℂ$
56 55 mulid1d ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {A}\cdot 1={A}$
57 2 nnge1d ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to 1\le {a}$
58 1red ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to 1\in ℝ$
59 58 8 6 lemul2d ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \left(1\le {a}↔{A}\cdot 1\le {A}{a}\right)$
60 57 59 mpbid ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {A}\cdot 1\le {A}{a}$
61 56 60 eqbrtrrd ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {A}\le {A}{a}$
62 9 recnd ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {A}{a}\in ℂ$
63 62 subid1d ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {A}{a}-0={A}{a}$
64 61 63 breqtrrd ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {A}\le {A}{a}-0$
65 24 7 26 54 64 letrd ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\le {A}{a}-0$
66 14 24 26 27 65 ltletrd ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \left|{A}{a}-{b}\right|<{A}{a}-0$
67 12 26 absltd ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \left(\left|{A}{a}-{b}\right|<{A}{a}-0↔\left(-\left({A}{a}-0\right)<{A}{a}-{b}\wedge {A}{a}-{b}<{A}{a}-0\right)\right)$
68 66 67 mpbid ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \left(-\left({A}{a}-0\right)<{A}{a}-{b}\wedge {A}{a}-{b}<{A}{a}-0\right)$
69 68 simprd ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {A}{a}-{b}<{A}{a}-0$
70 25 11 9 ltsub2d ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \left(0<{b}↔{A}{a}-{b}<{A}{a}-0\right)$
71 69 70 mpbird ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to 0<{b}$
72 elnnz ${⊢}{b}\in ℕ↔\left({b}\in ℤ\wedge 0<{b}\right)$
73 4 71 72 sylanbrc ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {b}\in ℕ$
74 22 2 ifcld ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to if\left({a}\le {B},{B},{a}\right)\in ℕ$
75 74 nnrecred ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \frac{1}{if\left({a}\le {B},{B},{a}\right)}\in ℝ$
76 elfzle2 ${⊢}{a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\to {a}\le if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)$
77 76 ad3antlr ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {a}\le if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)$
78 max1 ${⊢}\left({B}\in ℝ\wedge ⌊\frac{1}{{A}}⌋+1\in ℝ\right)\to {B}\le if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)$
79 29 34 78 syl2anc ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {B}\le if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)$
80 maxle ${⊢}\left({a}\in ℝ\wedge {B}\in ℝ\wedge if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\in ℝ\right)\to \left(if\left({a}\le {B},{B},{a}\right)\le if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)↔\left({a}\le if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\wedge {B}\le if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)$
81 8 29 38 80 syl3anc ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \left(if\left({a}\le {B},{B},{a}\right)\le if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)↔\left({a}\le if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\wedge {B}\le if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)$
82 77 79 81 mpbir2and ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to if\left({a}\le {B},{B},{a}\right)\le if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)$
83 29 8 ifcld ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to if\left({a}\le {B},{B},{a}\right)\in ℝ$
84 22 nngt0d ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to 0<{B}$
85 max2 ${⊢}\left({a}\in ℝ\wedge {B}\in ℝ\right)\to {B}\le if\left({a}\le {B},{B},{a}\right)$
86 8 29 85 syl2anc ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to {B}\le if\left({a}\le {B},{B},{a}\right)$
87 25 29 83 84 86 ltletrd ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to 0
88 lerec ${⊢}\left(\left(if\left({a}\le {B},{B},{a}\right)\in ℝ\wedge 0
89 83 87 38 39 88 syl22anc ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \left(if\left({a}\le {B},{B},{a}\right)\le if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)↔\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\le \frac{1}{if\left({a}\le {B},{B},{a}\right)}\right)$
90 82 89 mpbid ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\le \frac{1}{if\left({a}\le {B},{B},{a}\right)}$
91 14 24 75 27 90 ltletrd ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le {B},{B},{a}\right)}$
92 oveq2 ${⊢}{x}={a}\to {A}{x}={A}{a}$
93 92 fvoveq1d ${⊢}{x}={a}\to \left|{A}{x}-{y}\right|=\left|{A}{a}-{y}\right|$
94 breq1 ${⊢}{x}={a}\to \left({x}\le {B}↔{a}\le {B}\right)$
95 id ${⊢}{x}={a}\to {x}={a}$
96 94 95 ifbieq2d ${⊢}{x}={a}\to if\left({x}\le {B},{B},{x}\right)=if\left({a}\le {B},{B},{a}\right)$
97 96 oveq2d ${⊢}{x}={a}\to \frac{1}{if\left({x}\le {B},{B},{x}\right)}=\frac{1}{if\left({a}\le {B},{B},{a}\right)}$
98 93 97 breq12d ${⊢}{x}={a}\to \left(\left|{A}{x}-{y}\right|<\frac{1}{if\left({x}\le {B},{B},{x}\right)}↔\left|{A}{a}-{y}\right|<\frac{1}{if\left({a}\le {B},{B},{a}\right)}\right)$
99 oveq2 ${⊢}{y}={b}\to {A}{a}-{y}={A}{a}-{b}$
100 99 fveq2d ${⊢}{y}={b}\to \left|{A}{a}-{y}\right|=\left|{A}{a}-{b}\right|$
101 100 breq1d ${⊢}{y}={b}\to \left(\left|{A}{a}-{y}\right|<\frac{1}{if\left({a}\le {B},{B},{a}\right)}↔\left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le {B},{B},{a}\right)}\right)$
102 98 101 rspc2ev ${⊢}\left({a}\in ℕ\wedge {b}\in ℕ\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({a}\le {B},{B},{a}\right)}\right)\to \exists {x}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{A}{x}-{y}\right|<\frac{1}{if\left({x}\le {B},{B},{x}\right)}$
103 2 73 91 102 syl3anc ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\wedge {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\right)\wedge {b}\in {ℕ}_{0}\right)\wedge \left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}\right)\to \exists {x}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{A}{x}-{y}\right|<\frac{1}{if\left({x}\le {B},{B},{x}\right)}$
104 19 21 ifcld ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\in ℕ$
105 irrapxlem3 ${⊢}\left({A}\in {ℝ}^{+}\wedge if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\in ℕ\right)\to \exists {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}$
106 5 104 105 syl2anc ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to \exists {a}\in \left(1\dots if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left|{A}{a}-{b}\right|<\frac{1}{if\left({B}\le ⌊\frac{1}{{A}}⌋+1,⌊\frac{1}{{A}}⌋+1,{B}\right)}$
107 103 106 r19.29vva ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℕ\right)\to \exists {x}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{A}{x}-{y}\right|<\frac{1}{if\left({x}\le {B},{B},{x}\right)}$