Metamath Proof Explorer

Theorem rpnnen1lem2

Description: Lemma for rpnnen1 . (Contributed by Mario Carneiro, 12-May-2013)

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 ) ) )
Assertion rpnnen1lem2 
|- ( ( x e. RR /\ k e. NN ) -> sup ( T , RR , < ) e. ZZ )

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 1 ssrab3 
 |-  T C_ ZZ
4 nnre 
 |-  ( k e. NN -> k e. RR )
5 remulcl 
 |-  ( ( k e. RR /\ x e. RR ) -> ( k x. x ) e. RR )
6 5 ancoms 
 |-  ( ( x e. RR /\ k e. RR ) -> ( k x. x ) e. RR )
7 4 6 sylan2 
 |-  ( ( x e. RR /\ k e. NN ) -> ( k x. x ) e. RR )
8 btwnz 
 |-  ( ( k x. x ) e. RR -> ( E. n e. ZZ n < ( k x. x ) /\ E. n e. ZZ ( k x. x ) < n ) )
9 8 simpld 
 |-  ( ( k x. x ) e. RR -> E. n e. ZZ n < ( k x. x ) )
10 7 9 syl 
 |-  ( ( x e. RR /\ k e. NN ) -> E. n e. ZZ n < ( k x. x ) )
11 zre 
 |-  ( n e. ZZ -> n e. RR )
12 11 adantl 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> n e. RR )
13 simpll 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> x e. RR )
14 nngt0 
 |-  ( k e. NN -> 0 < k )
15 4 14 jca 
 |-  ( k e. NN -> ( k e. RR /\ 0 < k ) )
16 15 ad2antlr 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( k e. RR /\ 0 < k ) )
17 ltdivmul 
 |-  ( ( n e. RR /\ x e. RR /\ ( k e. RR /\ 0 < k ) ) -> ( ( n / k ) < x <-> n < ( k x. x ) ) )
18 12 13 16 17 syl3anc 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( ( n / k ) < x <-> n < ( k x. x ) ) )
19 18 rexbidva 
 |-  ( ( x e. RR /\ k e. NN ) -> ( E. n e. ZZ ( n / k ) < x <-> E. n e. ZZ n < ( k x. x ) ) )
20 10 19 mpbird 
 |-  ( ( x e. RR /\ k e. NN ) -> E. n e. ZZ ( n / k ) < x )
21 rabn0 
 |-  ( { n e. ZZ | ( n / k ) < x } =/= (/) <-> E. n e. ZZ ( n / k ) < x )
22 20 21 sylibr 
 |-  ( ( x e. RR /\ k e. NN ) -> { n e. ZZ | ( n / k ) < x } =/= (/) )
23 1 neeq1i 
 |-  ( T =/= (/) <-> { n e. ZZ | ( n / k ) < x } =/= (/) )
24 22 23 sylibr 
 |-  ( ( x e. RR /\ k e. NN ) -> T =/= (/) )
25 1 rabeq2i 
 |-  ( n e. T <-> ( n e. ZZ /\ ( n / k ) < x ) )
26 4 ad2antlr 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> k e. RR )
27 26 13 5 syl2anc 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( k x. x ) e. RR )
28 ltle 
 |-  ( ( n e. RR /\ ( k x. x ) e. RR ) -> ( n < ( k x. x ) -> n <_ ( k x. x ) ) )
29 12 27 28 syl2anc 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( n < ( k x. x ) -> n <_ ( k x. x ) ) )
30 18 29 sylbid 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( ( n / k ) < x -> n <_ ( k x. x ) ) )
31 30 impr 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ ( n e. ZZ /\ ( n / k ) < x ) ) -> n <_ ( k x. x ) )
32 25 31 sylan2b 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. T ) -> n <_ ( k x. x ) )
33 32 ralrimiva 
 |-  ( ( x e. RR /\ k e. NN ) -> A. n e. T n <_ ( k x. x ) )
34 brralrspcev 
 |-  ( ( ( k x. x ) e. RR /\ A. n e. T n <_ ( k x. x ) ) -> E. y e. RR A. n e. T n <_ y )
35 7 33 34 syl2anc 
 |-  ( ( x e. RR /\ k e. NN ) -> E. y e. RR A. n e. T n <_ y )
36 suprzcl 
 |-  ( ( T C_ ZZ /\ T =/= (/) /\ E. y e. RR A. n e. T n <_ y ) -> sup ( T , RR , < ) e. T )
37 3 24 35 36 mp3an2i 
 |-  ( ( x e. RR /\ k e. NN ) -> sup ( T , RR , < ) e. T )
38 3 37 sseldi 
 |-  ( ( x e. RR /\ k e. NN ) -> sup ( T , RR , < ) e. ZZ )