Metamath Proof Explorer


Theorem rpgtrecnn

Description: Any positive real number is greater than the reciprocal of a positive integer. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Assertion rpgtrecnn
|- ( A e. RR+ -> E. n e. NN ( 1 / n ) < A )

Proof

Step Hyp Ref Expression
1 rpreccl
 |-  ( A e. RR+ -> ( 1 / A ) e. RR+ )
2 1 rpred
 |-  ( A e. RR+ -> ( 1 / A ) e. RR )
3 1 rpge0d
 |-  ( A e. RR+ -> 0 <_ ( 1 / A ) )
4 flge0nn0
 |-  ( ( ( 1 / A ) e. RR /\ 0 <_ ( 1 / A ) ) -> ( |_ ` ( 1 / A ) ) e. NN0 )
5 2 3 4 syl2anc
 |-  ( A e. RR+ -> ( |_ ` ( 1 / A ) ) e. NN0 )
6 nn0p1nn
 |-  ( ( |_ ` ( 1 / A ) ) e. NN0 -> ( ( |_ ` ( 1 / A ) ) + 1 ) e. NN )
7 5 6 syl
 |-  ( A e. RR+ -> ( ( |_ ` ( 1 / A ) ) + 1 ) e. NN )
8 flltp1
 |-  ( ( 1 / A ) e. RR -> ( 1 / A ) < ( ( |_ ` ( 1 / A ) ) + 1 ) )
9 2 8 syl
 |-  ( A e. RR+ -> ( 1 / A ) < ( ( |_ ` ( 1 / A ) ) + 1 ) )
10 7 nnrpd
 |-  ( A e. RR+ -> ( ( |_ ` ( 1 / A ) ) + 1 ) e. RR+ )
11 1 10 ltrecd
 |-  ( A e. RR+ -> ( ( 1 / A ) < ( ( |_ ` ( 1 / A ) ) + 1 ) <-> ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) < ( 1 / ( 1 / A ) ) ) )
12 9 11 mpbid
 |-  ( A e. RR+ -> ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) < ( 1 / ( 1 / A ) ) )
13 rpcn
 |-  ( A e. RR+ -> A e. CC )
14 rpne0
 |-  ( A e. RR+ -> A =/= 0 )
15 13 14 recrecd
 |-  ( A e. RR+ -> ( 1 / ( 1 / A ) ) = A )
16 12 15 breqtrd
 |-  ( A e. RR+ -> ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) < A )
17 oveq2
 |-  ( n = ( ( |_ ` ( 1 / A ) ) + 1 ) -> ( 1 / n ) = ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) )
18 17 breq1d
 |-  ( n = ( ( |_ ` ( 1 / A ) ) + 1 ) -> ( ( 1 / n ) < A <-> ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) < A ) )
19 18 rspcev
 |-  ( ( ( ( |_ ` ( 1 / A ) ) + 1 ) e. NN /\ ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) < A ) -> E. n e. NN ( 1 / n ) < A )
20 7 16 19 syl2anc
 |-  ( A e. RR+ -> E. n e. NN ( 1 / n ) < A )