Theorem recnnltrp

Description: N is a natural number large enough that its reciprocal is smaller than the given positive E . (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypothesis	recnnltrp.1	|- N = ( ( |_ ` ( 1 / E ) ) + 1 )
Assertion	recnnltrp	|- ( E e. RR+ -> ( N e. NN /\ ( 1 / N ) < E ) )

Proof

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