Theorem rpnnen1lem6

Description: Lemma for rpnnen1 . (Contributed by Mario Carneiro, 12-May-2013) (Revised by NM, 15-Aug-2021) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	rpnnen1lem.1	|- T = { n e. ZZ | ( n / k ) < x }
	rpnnen1lem.2	|- F = ( x e. RR |-> ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) )
	rpnnen1lem.n	|- NN e. _V
	rpnnen1lem.q	|- QQ e. _V
Assertion	rpnnen1lem6	|- RR ~<_ ( QQ ^m NN )

Proof

Step	Hyp	Ref	Expression
1		rpnnen1lem.1	|- T = { n e. ZZ | ( n / k ) < x }
2		rpnnen1lem.2	|- F = ( x e. RR |-> ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) )
3		rpnnen1lem.n	|- NN e. _V
4		rpnnen1lem.q	|- QQ e. _V
5		ovex	|- ( QQ ^m NN ) e. _V
6	1 2 3 4	rpnnen1lem1	|- ( x e. RR -> ( F ` x ) e. ( QQ ^m NN ) )
7		rneq	|- ( ( F ` x ) = ( F ` y ) -> ran ( F ` x ) = ran ( F ` y ) )
8	7	supeq1d	|- ( ( F ` x ) = ( F ` y ) -> sup ( ran ( F ` x ) , RR , < ) = sup ( ran ( F ` y ) , RR , < ) )
9	1 2 3 4	rpnnen1lem5	|- ( x e. RR -> sup ( ran ( F ` x ) , RR , < ) = x )
10		fveq2	|- ( x = y -> ( F ` x ) = ( F ` y ) )
11	10	rneqd	|- ( x = y -> ran ( F ` x ) = ran ( F ` y ) )
12	11	supeq1d	|- ( x = y -> sup ( ran ( F ` x ) , RR , < ) = sup ( ran ( F ` y ) , RR , < ) )
13		id	|- ( x = y -> x = y )
14	12 13	eqeq12d	|- ( x = y -> ( sup ( ran ( F ` x ) , RR , < ) = x <-> sup ( ran ( F ` y ) , RR , < ) = y ) )
15	14 9	vtoclga	|- ( y e. RR -> sup ( ran ( F ` y ) , RR , < ) = y )
16	9 15	eqeqan12d	|- ( ( x e. RR /\ y e. RR ) -> ( sup ( ran ( F ` x ) , RR , < ) = sup ( ran ( F ` y ) , RR , < ) <-> x = y ) )
17	8 16	syl5ib	|- ( ( x e. RR /\ y e. RR ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
18	17 10	impbid1	|- ( ( x e. RR /\ y e. RR ) -> ( ( F ` x ) = ( F ` y ) <-> x = y ) )
19	6 18	dom2	|- ( ( QQ ^m NN ) e. _V -> RR ~<_ ( QQ ^m NN ) )
20	5 19	ax-mp	|- RR ~<_ ( QQ ^m NN )