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

Metamath Proof Explorer

Theorem rpnnen1lem3

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 rpnnen1lem3 
|- ( x e. RR -> A. n e. ran ( F ` x ) n <_ x )

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 3 mptex 
 |-  ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) e. _V
6 2 fvmpt2 
 |-  ( ( x e. RR /\ ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) e. _V ) -> ( F ` x ) = ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) )
7 5 6 mpan2 
 |-  ( x e. RR -> ( F ` x ) = ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) )
8 7 fveq1d 
 |-  ( x e. RR -> ( ( F ` x ) ` k ) = ( ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) ` k ) )
9 ovex 
 |-  ( sup ( T , RR , < ) / k ) e. _V
10 eqid 
 |-  ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) = ( k e. NN |-> ( sup ( T , RR , < ) / k ) )
11 10 fvmpt2 
 |-  ( ( k e. NN /\ ( sup ( T , RR , < ) / k ) e. _V ) -> ( ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) ` k ) = ( sup ( T , RR , < ) / k ) )
12 9 11 mpan2 
 |-  ( k e. NN -> ( ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) ` k ) = ( sup ( T , RR , < ) / k ) )
13 8 12 sylan9eq 
 |-  ( ( x e. RR /\ k e. NN ) -> ( ( F ` x ) ` k ) = ( sup ( T , RR , < ) / k ) )
14 1 reqabi 
 |-  ( n e. T <-> ( n e. ZZ /\ ( n / k ) < x ) )
15 zre 
 |-  ( n e. ZZ -> n e. RR )
16 15 adantl 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> n e. RR )
17 simpll 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> x e. RR )
18 nnre 
 |-  ( k e. NN -> k e. RR )
19 nngt0 
 |-  ( k e. NN -> 0 < k )
20 18 19 jca 
 |-  ( k e. NN -> ( k e. RR /\ 0 < k ) )
21 20 ad2antlr 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( k e. RR /\ 0 < k ) )
22 ltdivmul 
 |-  ( ( n e. RR /\ x e. RR /\ ( k e. RR /\ 0 < k ) ) -> ( ( n / k ) < x <-> n < ( k x. x ) ) )
23 16 17 21 22 syl3anc 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( ( n / k ) < x <-> n < ( k x. x ) ) )
24 18 ad2antlr 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> k e. RR )
25 remulcl 
 |-  ( ( k e. RR /\ x e. RR ) -> ( k x. x ) e. RR )
26 24 17 25 syl2anc 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( k x. x ) e. RR )
27 ltle 
 |-  ( ( n e. RR /\ ( k x. x ) e. RR ) -> ( n < ( k x. x ) -> n <_ ( k x. x ) ) )
28 16 26 27 syl2anc 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( n < ( k x. x ) -> n <_ ( k x. x ) ) )
29 23 28 sylbid 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( ( n / k ) < x -> n <_ ( k x. x ) ) )
30 29 impr 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ ( n e. ZZ /\ ( n / k ) < x ) ) -> n <_ ( k x. x ) )
31 14 30 sylan2b 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. T ) -> n <_ ( k x. x ) )
32 31 ralrimiva 
 |-  ( ( x e. RR /\ k e. NN ) -> A. n e. T n <_ ( k x. x ) )
33 ssrab2 
 |-  { n e. ZZ | ( n / k ) < x } C_ ZZ
34 1 33 eqsstri 
 |-  T C_ ZZ
35 zssre 
 |-  ZZ C_ RR
36 34 35 sstri 
 |-  T C_ RR
37 36 a1i 
 |-  ( ( x e. RR /\ k e. NN ) -> T C_ RR )
38 25 ancoms 
 |-  ( ( x e. RR /\ k e. RR ) -> ( k x. x ) e. RR )
39 18 38 sylan2 
 |-  ( ( x e. RR /\ k e. NN ) -> ( k x. x ) e. RR )
40 btwnz 
 |-  ( ( k x. x ) e. RR -> ( E. n e. ZZ n < ( k x. x ) /\ E. n e. ZZ ( k x. x ) < n ) )
41 40 simpld 
 |-  ( ( k x. x ) e. RR -> E. n e. ZZ n < ( k x. x ) )
42 39 41 syl 
 |-  ( ( x e. RR /\ k e. NN ) -> E. n e. ZZ n < ( k x. x ) )
43 23 rexbidva 
 |-  ( ( x e. RR /\ k e. NN ) -> ( E. n e. ZZ ( n / k ) < x <-> E. n e. ZZ n < ( k x. x ) ) )
44 42 43 mpbird 
 |-  ( ( x e. RR /\ k e. NN ) -> E. n e. ZZ ( n / k ) < x )
45 rabn0 
 |-  ( { n e. ZZ | ( n / k ) < x } =/= (/) <-> E. n e. ZZ ( n / k ) < x )
46 44 45 sylibr 
 |-  ( ( x e. RR /\ k e. NN ) -> { n e. ZZ | ( n / k ) < x } =/= (/) )
47 1 neeq1i 
 |-  ( T =/= (/) <-> { n e. ZZ | ( n / k ) < x } =/= (/) )
48 46 47 sylibr 
 |-  ( ( x e. RR /\ k e. NN ) -> T =/= (/) )
49 breq2 
 |-  ( y = ( k x. x ) -> ( n <_ y <-> n <_ ( k x. x ) ) )
50 49 ralbidv 
 |-  ( y = ( k x. x ) -> ( A. n e. T n <_ y <-> A. n e. T n <_ ( k x. x ) ) )
51 50 rspcev 
 |-  ( ( ( k x. x ) e. RR /\ A. n e. T n <_ ( k x. x ) ) -> E. y e. RR A. n e. T n <_ y )
52 39 32 51 syl2anc 
 |-  ( ( x e. RR /\ k e. NN ) -> E. y e. RR A. n e. T n <_ y )
53 suprleub 
 |-  ( ( ( T C_ RR /\ T =/= (/) /\ E. y e. RR A. n e. T n <_ y ) /\ ( k x. x ) e. RR ) -> ( sup ( T , RR , < ) <_ ( k x. x ) <-> A. n e. T n <_ ( k x. x ) ) )
54 37 48 52 39 53 syl31anc 
 |-  ( ( x e. RR /\ k e. NN ) -> ( sup ( T , RR , < ) <_ ( k x. x ) <-> A. n e. T n <_ ( k x. x ) ) )
55 32 54 mpbird 
 |-  ( ( x e. RR /\ k e. NN ) -> sup ( T , RR , < ) <_ ( k x. x ) )
56 1 2 rpnnen1lem2 
 |-  ( ( x e. RR /\ k e. NN ) -> sup ( T , RR , < ) e. ZZ )
57 56 zred 
 |-  ( ( x e. RR /\ k e. NN ) -> sup ( T , RR , < ) e. RR )
58 simpl 
 |-  ( ( x e. RR /\ k e. NN ) -> x e. RR )
59 20 adantl 
 |-  ( ( x e. RR /\ k e. NN ) -> ( k e. RR /\ 0 < k ) )
60 ledivmul 
 |-  ( ( sup ( T , RR , < ) e. RR /\ x e. RR /\ ( k e. RR /\ 0 < k ) ) -> ( ( sup ( T , RR , < ) / k ) <_ x <-> sup ( T , RR , < ) <_ ( k x. x ) ) )
61 57 58 59 60 syl3anc 
 |-  ( ( x e. RR /\ k e. NN ) -> ( ( sup ( T , RR , < ) / k ) <_ x <-> sup ( T , RR , < ) <_ ( k x. x ) ) )
62 55 61 mpbird 
 |-  ( ( x e. RR /\ k e. NN ) -> ( sup ( T , RR , < ) / k ) <_ x )
63 13 62 eqbrtrd 
 |-  ( ( x e. RR /\ k e. NN ) -> ( ( F ` x ) ` k ) <_ x )
64 63 ralrimiva 
 |-  ( x e. RR -> A. k e. NN ( ( F ` x ) ` k ) <_ x )
65 1 2 3 4 rpnnen1lem1 
 |-  ( x e. RR -> ( F ` x ) e. ( QQ ^m NN ) )
66 4 3 elmap 
 |-  ( ( F ` x ) e. ( QQ ^m NN ) <-> ( F ` x ) : NN --> QQ )
67 65 66 sylib 
 |-  ( x e. RR -> ( F ` x ) : NN --> QQ )
68 ffn 
 |-  ( ( F ` x ) : NN --> QQ -> ( F ` x ) Fn NN )
69 breq1 
 |-  ( n = ( ( F ` x ) ` k ) -> ( n <_ x <-> ( ( F ` x ) ` k ) <_ x ) )
70 69 ralrn 
 |-  ( ( F ` x ) Fn NN -> ( A. n e. ran ( F ` x ) n <_ x <-> A. k e. NN ( ( F ` x ) ` k ) <_ x ) )
71 67 68 70 3syl 
 |-  ( x e. RR -> ( A. n e. ran ( F ` x ) n <_ x <-> A. k e. NN ( ( F ` x ) ` k ) <_ x ) )
72 64 71 mpbird 
 |-  ( x e. RR -> A. n e. ran ( F ` x ) n <_ x )