Theorem rpnnen1

Description: One half of rpnnen , where we show an injection from the real numbers to sequences of rational numbers. Specifically, we map a real number x to the sequence ( Fx ) : NN --> QQ (see rpnnen1lem6 ) such that ( ( Fx )k ) is the largest rational number with denominator k that is strictly less than x . In this manner, we get a monotonically increasing sequence that converges to x , and since each sequence converges to a unique real number, this mapping from reals to sequences of rational numbers is injective. Note: The NN and QQ existence hypotheses provide for use with either nnex and qex , or nnexALT and qexALT . The proof should not be modified to use any of those 4 theorems. (Contributed by Mario Carneiro, 13-May-2013) (Revised by Mario Carneiro, 16-Jun-2013) (Revised by NM, 15-Aug-2021) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	rpnnen1.n	$$⊢\mathbb{N}\in \mathrm{V}$$
	rpnnen1.q	$$⊢\mathbb{Q}\in \mathrm{V}$$
Assertion	rpnnen1	$$⊢ℝ\preccurlyeq \left({\mathbb{Q}}^{\mathbb{N}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		rpnnen1.n	$$⊢\mathbb{N}\in \mathrm{V}$$
2		rpnnen1.q	$$⊢\mathbb{Q}\in \mathrm{V}$$
3		oveq1	$$⊢m=n\to \frac{m}{k}=\frac{n}{k}$$
4	3	breq1d	$$⊢m=n\to \left(\frac{m}{k}<x\leftrightarrow \frac{n}{k}<x\right)$$
5	4	cbvrabv	$$⊢\left\{m\in \mathbb{Z}|\frac{m}{k}<x\right\}=\left\{n\in \mathbb{Z}|\frac{n}{k}<x\right\}$$
6		oveq2	$$⊢j=k\to \frac{m}{j}=\frac{m}{k}$$
7	6	breq1d	$$⊢j=k\to \left(\frac{m}{j}<y\leftrightarrow \frac{m}{k}<y\right)$$
8	7	rabbidv	$$⊢j=k\to \left\{m\in \mathbb{Z}|\frac{m}{j}<y\right\}=\left\{m\in \mathbb{Z}|\frac{m}{k}<y\right\}$$
9	8	supeq1d	$$⊢j=k\to sup\left(\left\{m\in \mathbb{Z}|\frac{m}{j}<y\right\},ℝ,<\right)=sup\left(\left\{m\in \mathbb{Z}|\frac{m}{k}<y\right\},ℝ,<\right)$$
10		id	$$⊢j=k\to j=k$$
11	9 10	oveq12d	$$⊢j=k\to \frac{sup\left(\left\{m\in \mathbb{Z}|\frac{m}{j}<y\right\},ℝ,<\right)}{j}=\frac{sup\left(\left\{m\in \mathbb{Z}|\frac{m}{k}<y\right\},ℝ,<\right)}{k}$$
12	11	cbvmptv	$$⊢\left(j\in \mathbb{N}⟼\frac{sup\left(\left\{m\in \mathbb{Z}|\frac{m}{j}<y\right\},ℝ,<\right)}{j}\right)=\left(k\in \mathbb{N}⟼\frac{sup\left(\left\{m\in \mathbb{Z}|\frac{m}{k}<y\right\},ℝ,<\right)}{k}\right)$$
13		breq2	$$⊢y=x\to \left(\frac{m}{k}<y\leftrightarrow \frac{m}{k}<x\right)$$
14	13	rabbidv	$$⊢y=x\to \left\{m\in \mathbb{Z}|\frac{m}{k}<y\right\}=\left\{m\in \mathbb{Z}|\frac{m}{k}<x\right\}$$
15	14	supeq1d	$$⊢y=x\to sup\left(\left\{m\in \mathbb{Z}|\frac{m}{k}<y\right\},ℝ,<\right)=sup\left(\left\{m\in \mathbb{Z}|\frac{m}{k}<x\right\},ℝ,<\right)$$
16	15	oveq1d	$$⊢y=x\to \frac{sup\left(\left\{m\in \mathbb{Z}|\frac{m}{k}<y\right\},ℝ,<\right)}{k}=\frac{sup\left(\left\{m\in \mathbb{Z}|\frac{m}{k}<x\right\},ℝ,<\right)}{k}$$
17	16	mpteq2dv	$$⊢y=x\to \left(k\in \mathbb{N}⟼\frac{sup\left(\left\{m\in \mathbb{Z}|\frac{m}{k}<y\right\},ℝ,<\right)}{k}\right)=\left(k\in \mathbb{N}⟼\frac{sup\left(\left\{m\in \mathbb{Z}|\frac{m}{k}<x\right\},ℝ,<\right)}{k}\right)$$
18	12 17	eqtrid	$$⊢y=x\to \left(j\in \mathbb{N}⟼\frac{sup\left(\left\{m\in \mathbb{Z}|\frac{m}{j}<y\right\},ℝ,<\right)}{j}\right)=\left(k\in \mathbb{N}⟼\frac{sup\left(\left\{m\in \mathbb{Z}|\frac{m}{k}<x\right\},ℝ,<\right)}{k}\right)$$
19	18	cbvmptv	$$⊢\left(y\in ℝ⟼\left(j\in \mathbb{N}⟼\frac{sup\left(\left\{m\in \mathbb{Z}|\frac{m}{j}<y\right\},ℝ,<\right)}{j}\right)\right)=\left(x\in ℝ⟼\left(k\in \mathbb{N}⟼\frac{sup\left(\left\{m\in \mathbb{Z}|\frac{m}{k}<x\right\},ℝ,<\right)}{k}\right)\right)$$
20	5 19 1 2	rpnnen1lem6	$$⊢ℝ\preccurlyeq \left({\mathbb{Q}}^{\mathbb{N}}\right)$$