Metamath Proof Explorer

Theorem rpnnen1lem1

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 rpnnen1lem1 
|- ( x e. RR -> ( F ` x ) e. ( 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 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 ssrab2 
 |-  { n e. ZZ | ( n / k ) < x } C_ ZZ
9 1 8 eqsstri 
 |-  T C_ ZZ
10 9 a1i 
 |-  ( ( x e. RR /\ k e. NN ) -> T C_ ZZ )
11 nnre 
 |-  ( k e. NN -> k e. RR )
12 remulcl 
 |-  ( ( k e. RR /\ x e. RR ) -> ( k x. x ) e. RR )
13 12 ancoms 
 |-  ( ( x e. RR /\ k e. RR ) -> ( k x. x ) e. RR )
14 11 13 sylan2 
 |-  ( ( x e. RR /\ k e. NN ) -> ( k x. x ) e. RR )
15 btwnz 
 |-  ( ( k x. x ) e. RR -> ( E. n e. ZZ n < ( k x. x ) /\ E. n e. ZZ ( k x. x ) < n ) )
16 15 simpld 
 |-  ( ( k x. x ) e. RR -> E. n e. ZZ n < ( k x. x ) )
17 14 16 syl 
 |-  ( ( x e. RR /\ k e. NN ) -> E. n e. ZZ n < ( k x. x ) )
18 zre 
 |-  ( n e. ZZ -> n e. RR )
19 18 adantl 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> n e. RR )
20 simpll 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> x e. RR )
21 nngt0 
 |-  ( k e. NN -> 0 < k )
22 11 21 jca 
 |-  ( k e. NN -> ( k e. RR /\ 0 < k ) )
23 22 ad2antlr 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( k e. RR /\ 0 < k ) )
24 ltdivmul 
 |-  ( ( n e. RR /\ x e. RR /\ ( k e. RR /\ 0 < k ) ) -> ( ( n / k ) < x <-> n < ( k x. x ) ) )
25 19 20 23 24 syl3anc 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( ( n / k ) < x <-> n < ( k x. x ) ) )
26 25 rexbidva 
 |-  ( ( x e. RR /\ k e. NN ) -> ( E. n e. ZZ ( n / k ) < x <-> E. n e. ZZ n < ( k x. x ) ) )
27 17 26 mpbird 
 |-  ( ( x e. RR /\ k e. NN ) -> E. n e. ZZ ( n / k ) < x )
28 rabn0 
 |-  ( { n e. ZZ | ( n / k ) < x } =/= (/) <-> E. n e. ZZ ( n / k ) < x )
29 27 28 sylibr 
 |-  ( ( x e. RR /\ k e. NN ) -> { n e. ZZ | ( n / k ) < x } =/= (/) )
30 1 neeq1i 
 |-  ( T =/= (/) <-> { n e. ZZ | ( n / k ) < x } =/= (/) )
31 29 30 sylibr 
 |-  ( ( x e. RR /\ k e. NN ) -> T =/= (/) )
32 1 rabeq2i 
 |-  ( n e. T <-> ( n e. ZZ /\ ( n / k ) < x ) )
33 11 ad2antlr 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> k e. RR )
34 33 20 12 syl2anc 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( k x. x ) e. RR )
35 ltle 
 |-  ( ( n e. RR /\ ( k x. x ) e. RR ) -> ( n < ( k x. x ) -> n <_ ( k x. x ) ) )
36 19 34 35 syl2anc 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( n < ( k x. x ) -> n <_ ( k x. x ) ) )
37 25 36 sylbid 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( ( n / k ) < x -> n <_ ( k x. x ) ) )
38 37 impr 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ ( n e. ZZ /\ ( n / k ) < x ) ) -> n <_ ( k x. x ) )
39 32 38 sylan2b 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. T ) -> n <_ ( k x. x ) )
40 39 ralrimiva 
 |-  ( ( x e. RR /\ k e. NN ) -> A. n e. T n <_ ( k x. x ) )
41 breq2 
 |-  ( y = ( k x. x ) -> ( n <_ y <-> n <_ ( k x. x ) ) )
42 41 ralbidv 
 |-  ( y = ( k x. x ) -> ( A. n e. T n <_ y <-> A. n e. T n <_ ( k x. x ) ) )
43 42 rspcev 
 |-  ( ( ( k x. x ) e. RR /\ A. n e. T n <_ ( k x. x ) ) -> E. y e. RR A. n e. T n <_ y )
44 14 40 43 syl2anc 
 |-  ( ( x e. RR /\ k e. NN ) -> E. y e. RR A. n e. T n <_ y )
45 suprzcl 
 |-  ( ( T C_ ZZ /\ T =/= (/) /\ E. y e. RR A. n e. T n <_ y ) -> sup ( T , RR , < ) e. T )
46 10 31 44 45 syl3anc 
 |-  ( ( x e. RR /\ k e. NN ) -> sup ( T , RR , < ) e. T )
47 9 46 sselid 
 |-  ( ( x e. RR /\ k e. NN ) -> sup ( T , RR , < ) e. ZZ )
48 znq 
 |-  ( ( sup ( T , RR , < ) e. ZZ /\ k e. NN ) -> ( sup ( T , RR , < ) / k ) e. QQ )
49 47 48 sylancom 
 |-  ( ( x e. RR /\ k e. NN ) -> ( sup ( T , RR , < ) / k ) e. QQ )
50 eqid 
 |-  ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) = ( k e. NN |-> ( sup ( T , RR , < ) / k ) )
51 49 50 fmptd 
 |-  ( x e. RR -> ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) : NN --> QQ )
52 4 3 elmap 
 |-  ( ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) e. ( QQ ^m NN ) <-> ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) : NN --> QQ )
53 51 52 sylibr 
 |-  ( x e. RR -> ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) e. ( QQ ^m NN ) )
54 7 53 eqeltrd 
 |-  ( x e. RR -> ( F ` x ) e. ( QQ ^m NN ) )