Theorem irrapx1

Description: Dirichlet's approximation theorem. Every positive irrational number has infinitely many rational approximations which are closer than the inverse squares of their reduced denominators. Lemma 61 in vandenDries p. 42. (Contributed by Stefan O'Rear, 14-Sep-2014)

	Ref	Expression
Assertion	irrapx1	$$⊢A\in \left({ℝ}^{+}\setminus \mathbb{Q}\right)\to \left\{y\in \mathbb{Q}|\left(0<y\wedge \left|y-A\right|<{\mathrm{denom}\left(y\right)}^{-2}\right)\right\}\approx \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		qnnen	$$⊢\mathbb{Q}\approx \mathbb{N}$$
2		nnenom	$$⊢\mathbb{N}\approx \mathrm{\omega }$$
3	1 2	entri	$$⊢\mathbb{Q}\approx \mathrm{\omega }$$
4	3 2	pm3.2i	$$⊢\left(\mathbb{Q}\approx \mathrm{\omega }\wedge \mathbb{N}\approx \mathrm{\omega }\right)$$
5		ssrab2	$$⊢\left\{y\in \mathbb{Q}|\left(0<y\wedge \left|y-A\right|<{\mathrm{denom}\left(y\right)}^{-2}\right)\right\}\subseteq \mathbb{Q}$$
6		qssre	$$⊢\mathbb{Q}\subseteq ℝ$$
7	5 6	sstri	$$⊢\left\{y\in \mathbb{Q}|\left(0<y\wedge \left|y-A\right|<{\mathrm{denom}\left(y\right)}^{-2}\right)\right\}\subseteq ℝ$$
8	7	a1i	$$⊢A\in \left({ℝ}^{+}\setminus \mathbb{Q}\right)\to \left\{y\in \mathbb{Q}|\left(0<y\wedge \left|y-A\right|<{\mathrm{denom}\left(y\right)}^{-2}\right)\right\}\subseteq ℝ$$
9		eldifi	$$⊢A\in \left({ℝ}^{+}\setminus \mathbb{Q}\right)\to A\in {ℝ}^{+}$$
10	9	rpred	$$⊢A\in \left({ℝ}^{+}\setminus \mathbb{Q}\right)\to A\in ℝ$$
11		eldifn	$$⊢A\in \left({ℝ}^{+}\setminus \mathbb{Q}\right)\to \neg A\in \mathbb{Q}$$
12		elrabi	$$⊢A\in \left\{y\in \mathbb{Q}|\left(0<y\wedge \left|y-A\right|<{\mathrm{denom}\left(y\right)}^{-2}\right)\right\}\to A\in \mathbb{Q}$$
13	11 12	nsyl	$$⊢A\in \left({ℝ}^{+}\setminus \mathbb{Q}\right)\to \neg A\in \left\{y\in \mathbb{Q}|\left(0<y\wedge \left|y-A\right|<{\mathrm{denom}\left(y\right)}^{-2}\right)\right\}$$
14		irrapxlem6	$$⊢\left(A\in {ℝ}^{+}\wedge a\in {ℝ}^{+}\right)\to \exists b\in \left\{y\in \mathbb{Q}|\left(0<y\wedge \left|y-A\right|<{\mathrm{denom}\left(y\right)}^{-2}\right)\right\}\left|b-A\right|<a$$
15	9 14	sylan	$$⊢\left(A\in \left({ℝ}^{+}\setminus \mathbb{Q}\right)\wedge a\in {ℝ}^{+}\right)\to \exists b\in \left\{y\in \mathbb{Q}|\left(0<y\wedge \left|y-A\right|<{\mathrm{denom}\left(y\right)}^{-2}\right)\right\}\left|b-A\right|<a$$
16	15	ralrimiva	$$⊢A\in \left({ℝ}^{+}\setminus \mathbb{Q}\right)\to \forall a\in {ℝ}^{+}\exists b\in \left\{y\in \mathbb{Q}|\left(0<y\wedge \left|y-A\right|<{\mathrm{denom}\left(y\right)}^{-2}\right)\right\}\left|b-A\right|<a$$
17		rencldnfi	$$⊢\left(\left(\left\{y\in \mathbb{Q}|\left(0<y\wedge \left|y-A\right|<{\mathrm{denom}\left(y\right)}^{-2}\right)\right\}\subseteq ℝ\wedge A\in ℝ\wedge \neg A\in \left\{y\in \mathbb{Q}|\left(0<y\wedge \left|y-A\right|<{\mathrm{denom}\left(y\right)}^{-2}\right)\right\}\right)\wedge \forall a\in {ℝ}^{+}\exists b\in \left\{y\in \mathbb{Q}|\left(0<y\wedge \left|y-A\right|<{\mathrm{denom}\left(y\right)}^{-2}\right)\right\}\left|b-A\right|<a\right)\to \neg \left\{y\in \mathbb{Q}|\left(0<y\wedge \left|y-A\right|<{\mathrm{denom}\left(y\right)}^{-2}\right)\right\}\in \mathrm{Fin}$$
18	8 10 13 16 17	syl31anc	$$⊢A\in \left({ℝ}^{+}\setminus \mathbb{Q}\right)\to \neg \left\{y\in \mathbb{Q}|\left(0<y\wedge \left|y-A\right|<{\mathrm{denom}\left(y\right)}^{-2}\right)\right\}\in \mathrm{Fin}$$
19	18 5	jctil	$$⊢A\in \left({ℝ}^{+}\setminus \mathbb{Q}\right)\to \left(\left\{y\in \mathbb{Q}|\left(0<y\wedge \left|y-A\right|<{\mathrm{denom}\left(y\right)}^{-2}\right)\right\}\subseteq \mathbb{Q}\wedge \neg \left\{y\in \mathbb{Q}|\left(0<y\wedge \left|y-A\right|<{\mathrm{denom}\left(y\right)}^{-2}\right)\right\}\in \mathrm{Fin}\right)$$
20		ctbnfien	$$⊢\left(\left(\mathbb{Q}\approx \mathrm{\omega }\wedge \mathbb{N}\approx \mathrm{\omega }\right)\wedge \left(\left\{y\in \mathbb{Q}|\left(0<y\wedge \left|y-A\right|<{\mathrm{denom}\left(y\right)}^{-2}\right)\right\}\subseteq \mathbb{Q}\wedge \neg \left\{y\in \mathbb{Q}|\left(0<y\wedge \left|y-A\right|<{\mathrm{denom}\left(y\right)}^{-2}\right)\right\}\in \mathrm{Fin}\right)\right)\to \left\{y\in \mathbb{Q}|\left(0<y\wedge \left|y-A\right|<{\mathrm{denom}\left(y\right)}^{-2}\right)\right\}\approx \mathbb{N}$$
21	4 19 20	sylancr	$$⊢A\in \left({ℝ}^{+}\setminus \mathbb{Q}\right)\to \left\{y\in \mathbb{Q}|\left(0<y\wedge \left|y-A\right|<{\mathrm{denom}\left(y\right)}^{-2}\right)\right\}\approx \mathbb{N}$$