Metamath Proof Explorer

Theorem recnz

Description: The reciprocal of a number greater than 1 is not an integer. (Contributed by NM, 3-May-2005)

Ref Expression
Assertion recnz 
|- ( ( A e. RR /\ 1 < A ) -> -. ( 1 / A ) e. ZZ )

Proof

Step Hyp Ref Expression
1 recgt1i 
 |-  ( ( A e. RR /\ 1 < A ) -> ( 0 < ( 1 / A ) /\ ( 1 / A ) < 1 ) )
2 1 simprd 
 |-  ( ( A e. RR /\ 1 < A ) -> ( 1 / A ) < 1 )
3 1 simpld 
 |-  ( ( A e. RR /\ 1 < A ) -> 0 < ( 1 / A ) )
4 zgt0ge1 
 |-  ( ( 1 / A ) e. ZZ -> ( 0 < ( 1 / A ) <-> 1 <_ ( 1 / A ) ) )
5 3 4 syl5ibcom 
 |-  ( ( A e. RR /\ 1 < A ) -> ( ( 1 / A ) e. ZZ -> 1 <_ ( 1 / A ) ) )
6 1re 
 |-  1 e. RR
7 0lt1 
 |-  0 < 1
8 0re 
 |-  0 e. RR
9 lttr 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ A e. RR ) -> ( ( 0 < 1 /\ 1 < A ) -> 0 < A ) )
10 8 6 9 mp3an12 
 |-  ( A e. RR -> ( ( 0 < 1 /\ 1 < A ) -> 0 < A ) )
11 7 10 mpani 
 |-  ( A e. RR -> ( 1 < A -> 0 < A ) )
12 11 imdistani 
 |-  ( ( A e. RR /\ 1 < A ) -> ( A e. RR /\ 0 < A ) )
13 gt0ne0 
 |-  ( ( A e. RR /\ 0 < A ) -> A =/= 0 )
14 12 13 syl 
 |-  ( ( A e. RR /\ 1 < A ) -> A =/= 0 )
15 rereccl 
 |-  ( ( A e. RR /\ A =/= 0 ) -> ( 1 / A ) e. RR )
16 14 15 syldan 
 |-  ( ( A e. RR /\ 1 < A ) -> ( 1 / A ) e. RR )
17 lenlt 
 |-  ( ( 1 e. RR /\ ( 1 / A ) e. RR ) -> ( 1 <_ ( 1 / A ) <-> -. ( 1 / A ) < 1 ) )
18 6 16 17 sylancr 
 |-  ( ( A e. RR /\ 1 < A ) -> ( 1 <_ ( 1 / A ) <-> -. ( 1 / A ) < 1 ) )
19 5 18 sylibd 
 |-  ( ( A e. RR /\ 1 < A ) -> ( ( 1 / A ) e. ZZ -> -. ( 1 / A ) < 1 ) )
20 2 19 mt2d 
 |-  ( ( A e. RR /\ 1 < A ) -> -. ( 1 / A ) e. ZZ )