Metamath Proof Explorer

Theorem nnge2recico01

Description: The reciprocal of an integer greater than 1 is in the right open interval between 0 and 1. (Contributed by AV, 10-Apr-2026)

Ref Expression
Assertion nnge2recico01 
|- ( N e. ( ZZ>= ` 2 ) -> ( 1 / N ) e. ( 0 [,) 1 ) )

Proof

Step Hyp Ref Expression
1 eluzelre 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. RR )
2 eluz2n0 
 |-  ( N e. ( ZZ>= ` 2 ) -> N =/= 0 )
3 1 2 rereccld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 / N ) e. RR )
4 1red 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 e. RR )
5 0le1 
 |-  0 <_ 1
6 5 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 0 <_ 1 )
7 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
8 7 nngt0d 
 |-  ( N e. ( ZZ>= ` 2 ) -> 0 < N )
9 divge0 
 |-  ( ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( N e. RR /\ 0 < N ) ) -> 0 <_ ( 1 / N ) )
10 4 6 1 8 9 syl22anc 
 |-  ( N e. ( ZZ>= ` 2 ) -> 0 <_ ( 1 / N ) )
11 eluz2gt1 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 < N )
12 recgt1 
 |-  ( ( N e. RR /\ 0 < N ) -> ( 1 < N <-> ( 1 / N ) < 1 ) )
13 1 8 12 syl2anc 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 < N <-> ( 1 / N ) < 1 ) )
14 11 13 mpbid 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 / N ) < 1 )
15 0re 
 |-  0 e. RR
16 1xr 
 |-  1 e. RR*
17 15 16 pm3.2i 
 |-  ( 0 e. RR /\ 1 e. RR* )
18 elico2 
 |-  ( ( 0 e. RR /\ 1 e. RR* ) -> ( ( 1 / N ) e. ( 0 [,) 1 ) <-> ( ( 1 / N ) e. RR /\ 0 <_ ( 1 / N ) /\ ( 1 / N ) < 1 ) ) )
19 17 18 mp1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 1 / N ) e. ( 0 [,) 1 ) <-> ( ( 1 / N ) e. RR /\ 0 <_ ( 1 / N ) /\ ( 1 / N ) < 1 ) ) )
20 3 10 14 19 mpbir3and 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 / N ) e. ( 0 [,) 1 ) )