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	|- NN e. _V
	rpnnen1.q	|- QQ e. _V
Assertion	rpnnen1	|- RR ~<_ ( QQ ^m NN )

Proof

Step	Hyp	Ref	Expression
1		rpnnen1.n	|- NN e. _V
2		rpnnen1.q	|- QQ e. _V
3		oveq1	|- ( m = n -> ( m / k ) = ( n / k ) )
4	3	breq1d	|- ( m = n -> ( ( m / k ) < x <-> ( n / k ) < x ) )
5	4	cbvrabv	|- { m e. ZZ | ( m / k ) < x } = { n e. ZZ | ( n / k ) < x }
6		oveq2	|- ( j = k -> ( m / j ) = ( m / k ) )
7	6	breq1d	|- ( j = k -> ( ( m / j ) < y <-> ( m / k ) < y ) )
8	7	rabbidv	|- ( j = k -> { m e. ZZ | ( m / j ) < y } = { m e. ZZ | ( m / k ) < y } )
9	8	supeq1d	|- ( j = k -> sup ( { m e. ZZ | ( m / j ) < y } , RR , < ) = sup ( { m e. ZZ | ( m / k ) < y } , RR , < ) )
10		id	|- ( j = k -> j = k )
11	9 10	oveq12d	|- ( j = k -> ( sup ( { m e. ZZ | ( m / j ) < y } , RR , < ) / j ) = ( sup ( { m e. ZZ | ( m / k ) < y } , RR , < ) / k ) )
12	11	cbvmptv	|- ( j e. NN |-> ( sup ( { m e. ZZ | ( m / j ) < y } , RR , < ) / j ) ) = ( k e. NN |-> ( sup ( { m e. ZZ | ( m / k ) < y } , RR , < ) / k ) )
13		breq2	|- ( y = x -> ( ( m / k ) < y <-> ( m / k ) < x ) )
14	13	rabbidv	|- ( y = x -> { m e. ZZ | ( m / k ) < y } = { m e. ZZ | ( m / k ) < x } )
15	14	supeq1d	|- ( y = x -> sup ( { m e. ZZ | ( m / k ) < y } , RR , < ) = sup ( { m e. ZZ | ( m / k ) < x } , RR , < ) )
16	15	oveq1d	|- ( y = x -> ( sup ( { m e. ZZ | ( m / k ) < y } , RR , < ) / k ) = ( sup ( { m e. ZZ | ( m / k ) < x } , RR , < ) / k ) )
17	16	mpteq2dv	|- ( y = x -> ( k e. NN |-> ( sup ( { m e. ZZ | ( m / k ) < y } , RR , < ) / k ) ) = ( k e. NN |-> ( sup ( { m e. ZZ | ( m / k ) < x } , RR , < ) / k ) ) )
18	12 17	syl5eq	|- ( y = x -> ( j e. NN |-> ( sup ( { m e. ZZ | ( m / j ) < y } , RR , < ) / j ) ) = ( k e. NN |-> ( sup ( { m e. ZZ | ( m / k ) < x } , RR , < ) / k ) ) )
19	18	cbvmptv	|- ( y e. RR |-> ( j e. NN |-> ( sup ( { m e. ZZ | ( m / j ) < y } , RR , < ) / j ) ) ) = ( x e. RR |-> ( k e. NN |-> ( sup ( { m e. ZZ | ( m / k ) < x } , RR , < ) / k ) ) )
20	5 19 1 2	rpnnen1lem6	|- RR ~<_ ( QQ ^m NN )