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

Metamath Proof Explorer

Theorem nnrecl

Description: There exists a positive integer whose reciprocal is less than a given positive real. Exercise 3 of Apostol p. 28. (Contributed by NM, 8-Nov-2004)

Ref Expression
Assertion nnrecl 
|- ( ( A e. RR /\ 0 < A ) -> E. n e. NN ( 1 / n ) < A )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. RR /\ 0 < A ) -> A e. RR )
2 gt0ne0 
 |-  ( ( A e. RR /\ 0 < A ) -> A =/= 0 )
3 1 2 rereccld 
 |-  ( ( A e. RR /\ 0 < A ) -> ( 1 / A ) e. RR )
4 arch 
 |-  ( ( 1 / A ) e. RR -> E. n e. NN ( 1 / A ) < n )
5 3 4 syl 
 |-  ( ( A e. RR /\ 0 < A ) -> E. n e. NN ( 1 / A ) < n )
6 recgt0 
 |-  ( ( A e. RR /\ 0 < A ) -> 0 < ( 1 / A ) )
7 3 6 jca 
 |-  ( ( A e. RR /\ 0 < A ) -> ( ( 1 / A ) e. RR /\ 0 < ( 1 / A ) ) )
8 nnre 
 |-  ( n e. NN -> n e. RR )
9 nngt0 
 |-  ( n e. NN -> 0 < n )
10 8 9 jca 
 |-  ( n e. NN -> ( n e. RR /\ 0 < n ) )
11 ltrec 
 |-  ( ( ( ( 1 / A ) e. RR /\ 0 < ( 1 / A ) ) /\ ( n e. RR /\ 0 < n ) ) -> ( ( 1 / A ) < n <-> ( 1 / n ) < ( 1 / ( 1 / A ) ) ) )
12 7 10 11 syl2an 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ n e. NN ) -> ( ( 1 / A ) < n <-> ( 1 / n ) < ( 1 / ( 1 / A ) ) ) )
13 recn 
 |-  ( A e. RR -> A e. CC )
14 13 adantr 
 |-  ( ( A e. RR /\ 0 < A ) -> A e. CC )
15 14 2 recrecd 
 |-  ( ( A e. RR /\ 0 < A ) -> ( 1 / ( 1 / A ) ) = A )
16 15 breq2d 
 |-  ( ( A e. RR /\ 0 < A ) -> ( ( 1 / n ) < ( 1 / ( 1 / A ) ) <-> ( 1 / n ) < A ) )
17 16 adantr 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ n e. NN ) -> ( ( 1 / n ) < ( 1 / ( 1 / A ) ) <-> ( 1 / n ) < A ) )
18 12 17 bitrd 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ n e. NN ) -> ( ( 1 / A ) < n <-> ( 1 / n ) < A ) )
19 18 rexbidva 
 |-  ( ( A e. RR /\ 0 < A ) -> ( E. n e. NN ( 1 / A ) < n <-> E. n e. NN ( 1 / n ) < A ) )
20 5 19 mpbid 
 |-  ( ( A e. RR /\ 0 < A ) -> E. n e. NN ( 1 / n ) < A )