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 )