This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid 
 |-  ( 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 )