Metamath Proof Explorer

Theorem rpnnen1lem4

Description: Lemma for rpnnen1 . (Contributed by Mario Carneiro, 12-May-2013) (Revised by NM, 13-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 rpnnen1lem4 
|- ( x e. RR -> sup ( ran ( F ` x ) , RR , < ) e. RR )

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 1 2 3 4 rpnnen1lem1 
 |-  ( x e. RR -> ( F ` x ) e. ( QQ ^m NN ) )
6 4 3 elmap 
 |-  ( ( F ` x ) e. ( QQ ^m NN ) <-> ( F ` x ) : NN --> QQ )
7 5 6 sylib 
 |-  ( x e. RR -> ( F ` x ) : NN --> QQ )
8 frn 
 |-  ( ( F ` x ) : NN --> QQ -> ran ( F ` x ) C_ QQ )
9 qssre 
 |-  QQ C_ RR
10 8 9 sstrdi 
 |-  ( ( F ` x ) : NN --> QQ -> ran ( F ` x ) C_ RR )
11 7 10 syl 
 |-  ( x e. RR -> ran ( F ` x ) C_ RR )
12 1nn 
 |-  1 e. NN
13 12 ne0ii 
 |-  NN =/= (/)
14 fdm 
 |-  ( ( F ` x ) : NN --> QQ -> dom ( F ` x ) = NN )
15 14 neeq1d 
 |-  ( ( F ` x ) : NN --> QQ -> ( dom ( F ` x ) =/= (/) <-> NN =/= (/) ) )
16 13 15 mpbiri 
 |-  ( ( F ` x ) : NN --> QQ -> dom ( F ` x ) =/= (/) )
17 dm0rn0 
 |-  ( dom ( F ` x ) = (/) <-> ran ( F ` x ) = (/) )
18 17 necon3bii 
 |-  ( dom ( F ` x ) =/= (/) <-> ran ( F ` x ) =/= (/) )
19 16 18 sylib 
 |-  ( ( F ` x ) : NN --> QQ -> ran ( F ` x ) =/= (/) )
20 7 19 syl 
 |-  ( x e. RR -> ran ( F ` x ) =/= (/) )
21 1 2 3 4 rpnnen1lem3 
 |-  ( x e. RR -> A. n e. ran ( F ` x ) n <_ x )
22 breq2 
 |-  ( y = x -> ( n <_ y <-> n <_ x ) )
23 22 ralbidv 
 |-  ( y = x -> ( A. n e. ran ( F ` x ) n <_ y <-> A. n e. ran ( F ` x ) n <_ x ) )
24 23 rspcev 
 |-  ( ( x e. RR /\ A. n e. ran ( F ` x ) n <_ x ) -> E. y e. RR A. n e. ran ( F ` x ) n <_ y )
25 21 24 mpdan 
 |-  ( x e. RR -> E. y e. RR A. n e. ran ( F ` x ) n <_ y )
26 suprcl 
 |-  ( ( ran ( F ` x ) C_ RR /\ ran ( F ` x ) =/= (/) /\ E. y e. RR A. n e. ran ( F ` x ) n <_ y ) -> sup ( ran ( F ` x ) , RR , < ) e. RR )
27 11 20 25 26 syl3anc 
 |-  ( x e. RR -> sup ( ran ( F ` x ) , RR , < ) e. RR )