# Metamath Proof Explorer

## Theorem irrapxlem6

Description: Lemma for irrapx1 . Explicit description of a non-closed set. (Contributed by Stefan O'Rear, 13-Sep-2014)

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

### Proof

Step Hyp Ref Expression
1 simplr ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge {a}\in ℚ\right)\wedge \left(0<{a}\wedge \left|{a}-{A}\right|<{B}\wedge \left|{a}-{A}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)\to {a}\in ℚ$
2 simpr1 ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge {a}\in ℚ\right)\wedge \left(0<{a}\wedge \left|{a}-{A}\right|<{B}\wedge \left|{a}-{A}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)\to 0<{a}$
3 simpr3 ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge {a}\in ℚ\right)\wedge \left(0<{a}\wedge \left|{a}-{A}\right|<{B}\wedge \left|{a}-{A}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)\to \left|{a}-{A}\right|<{\mathrm{denom}\left({a}\right)}^{-2}$
4 2 3 jca ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge {a}\in ℚ\right)\wedge \left(0<{a}\wedge \left|{a}-{A}\right|<{B}\wedge \left|{a}-{A}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)\to \left(0<{a}\wedge \left|{a}-{A}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)$
5 breq2 ${⊢}{y}={a}\to \left(0<{y}↔0<{a}\right)$
6 fvoveq1 ${⊢}{y}={a}\to \left|{y}-{A}\right|=\left|{a}-{A}\right|$
7 fveq2 ${⊢}{y}={a}\to \mathrm{denom}\left({y}\right)=\mathrm{denom}\left({a}\right)$
8 7 oveq1d ${⊢}{y}={a}\to {\mathrm{denom}\left({y}\right)}^{-2}={\mathrm{denom}\left({a}\right)}^{-2}$
9 6 8 breq12d ${⊢}{y}={a}\to \left(\left|{y}-{A}\right|<{\mathrm{denom}\left({y}\right)}^{-2}↔\left|{a}-{A}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)$
10 5 9 anbi12d ${⊢}{y}={a}\to \left(\left(0<{y}\wedge \left|{y}-{A}\right|<{\mathrm{denom}\left({y}\right)}^{-2}\right)↔\left(0<{a}\wedge \left|{a}-{A}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)$
11 10 elrab ${⊢}{a}\in \left\{{y}\in ℚ|\left(0<{y}\wedge \left|{y}-{A}\right|<{\mathrm{denom}\left({y}\right)}^{-2}\right)\right\}↔\left({a}\in ℚ\wedge \left(0<{a}\wedge \left|{a}-{A}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)$
12 1 4 11 sylanbrc ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge {a}\in ℚ\right)\wedge \left(0<{a}\wedge \left|{a}-{A}\right|<{B}\wedge \left|{a}-{A}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)\to {a}\in \left\{{y}\in ℚ|\left(0<{y}\wedge \left|{y}-{A}\right|<{\mathrm{denom}\left({y}\right)}^{-2}\right)\right\}$
13 simpr2 ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge {a}\in ℚ\right)\wedge \left(0<{a}\wedge \left|{a}-{A}\right|<{B}\wedge \left|{a}-{A}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)\to \left|{a}-{A}\right|<{B}$
14 fvoveq1 ${⊢}{x}={a}\to \left|{x}-{A}\right|=\left|{a}-{A}\right|$
15 14 breq1d ${⊢}{x}={a}\to \left(\left|{x}-{A}\right|<{B}↔\left|{a}-{A}\right|<{B}\right)$
16 15 rspcev ${⊢}\left({a}\in \left\{{y}\in ℚ|\left(0<{y}\wedge \left|{y}-{A}\right|<{\mathrm{denom}\left({y}\right)}^{-2}\right)\right\}\wedge \left|{a}-{A}\right|<{B}\right)\to \exists {x}\in \left\{{y}\in ℚ|\left(0<{y}\wedge \left|{y}-{A}\right|<{\mathrm{denom}\left({y}\right)}^{-2}\right)\right\}\phantom{\rule{.4em}{0ex}}\left|{x}-{A}\right|<{B}$
17 12 13 16 syl2anc ${⊢}\left(\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge {a}\in ℚ\right)\wedge \left(0<{a}\wedge \left|{a}-{A}\right|<{B}\wedge \left|{a}-{A}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)\to \exists {x}\in \left\{{y}\in ℚ|\left(0<{y}\wedge \left|{y}-{A}\right|<{\mathrm{denom}\left({y}\right)}^{-2}\right)\right\}\phantom{\rule{.4em}{0ex}}\left|{x}-{A}\right|<{B}$
18 irrapxlem5 ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to \exists {a}\in ℚ\phantom{\rule{.4em}{0ex}}\left(0<{a}\wedge \left|{a}-{A}\right|<{B}\wedge \left|{a}-{A}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)$
19 17 18 r19.29a ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to \exists {x}\in \left\{{y}\in ℚ|\left(0<{y}\wedge \left|{y}-{A}\right|<{\mathrm{denom}\left({y}\right)}^{-2}\right)\right\}\phantom{\rule{.4em}{0ex}}\left|{x}-{A}\right|<{B}$