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

Metamath Proof Explorer

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 ) )