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

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 )