Metamath Proof Explorer


Theorem recreclt

Description: Given a positive number A , construct a new positive number less than both A and 1. (Contributed by NM, 28-Dec-2005)

Ref Expression
Assertion recreclt
|- ( ( A e. RR /\ 0 < A ) -> ( ( 1 / ( 1 + ( 1 / A ) ) ) < 1 /\ ( 1 / ( 1 + ( 1 / A ) ) ) < A ) )

Proof

Step Hyp Ref Expression
1 recgt0
 |-  ( ( A e. RR /\ 0 < A ) -> 0 < ( 1 / A ) )
2 gt0ne0
 |-  ( ( A e. RR /\ 0 < A ) -> A =/= 0 )
3 rereccl
 |-  ( ( A e. RR /\ A =/= 0 ) -> ( 1 / A ) e. RR )
4 2 3 syldan
 |-  ( ( A e. RR /\ 0 < A ) -> ( 1 / A ) e. RR )
5 1re
 |-  1 e. RR
6 ltaddpos
 |-  ( ( ( 1 / A ) e. RR /\ 1 e. RR ) -> ( 0 < ( 1 / A ) <-> 1 < ( 1 + ( 1 / A ) ) ) )
7 4 5 6 sylancl
 |-  ( ( A e. RR /\ 0 < A ) -> ( 0 < ( 1 / A ) <-> 1 < ( 1 + ( 1 / A ) ) ) )
8 1 7 mpbid
 |-  ( ( A e. RR /\ 0 < A ) -> 1 < ( 1 + ( 1 / A ) ) )
9 readdcl
 |-  ( ( 1 e. RR /\ ( 1 / A ) e. RR ) -> ( 1 + ( 1 / A ) ) e. RR )
10 5 4 9 sylancr
 |-  ( ( A e. RR /\ 0 < A ) -> ( 1 + ( 1 / A ) ) e. RR )
11 0lt1
 |-  0 < 1
12 0re
 |-  0 e. RR
13 lttr
 |-  ( ( 0 e. RR /\ 1 e. RR /\ ( 1 + ( 1 / A ) ) e. RR ) -> ( ( 0 < 1 /\ 1 < ( 1 + ( 1 / A ) ) ) -> 0 < ( 1 + ( 1 / A ) ) ) )
14 12 5 10 13 mp3an12i
 |-  ( ( A e. RR /\ 0 < A ) -> ( ( 0 < 1 /\ 1 < ( 1 + ( 1 / A ) ) ) -> 0 < ( 1 + ( 1 / A ) ) ) )
15 11 14 mpani
 |-  ( ( A e. RR /\ 0 < A ) -> ( 1 < ( 1 + ( 1 / A ) ) -> 0 < ( 1 + ( 1 / A ) ) ) )
16 8 15 mpd
 |-  ( ( A e. RR /\ 0 < A ) -> 0 < ( 1 + ( 1 / A ) ) )
17 recgt1
 |-  ( ( ( 1 + ( 1 / A ) ) e. RR /\ 0 < ( 1 + ( 1 / A ) ) ) -> ( 1 < ( 1 + ( 1 / A ) ) <-> ( 1 / ( 1 + ( 1 / A ) ) ) < 1 ) )
18 10 16 17 syl2anc
 |-  ( ( A e. RR /\ 0 < A ) -> ( 1 < ( 1 + ( 1 / A ) ) <-> ( 1 / ( 1 + ( 1 / A ) ) ) < 1 ) )
19 8 18 mpbid
 |-  ( ( A e. RR /\ 0 < A ) -> ( 1 / ( 1 + ( 1 / A ) ) ) < 1 )
20 ltaddpos
 |-  ( ( 1 e. RR /\ ( 1 / A ) e. RR ) -> ( 0 < 1 <-> ( 1 / A ) < ( ( 1 / A ) + 1 ) ) )
21 5 4 20 sylancr
 |-  ( ( A e. RR /\ 0 < A ) -> ( 0 < 1 <-> ( 1 / A ) < ( ( 1 / A ) + 1 ) ) )
22 11 21 mpbii
 |-  ( ( A e. RR /\ 0 < A ) -> ( 1 / A ) < ( ( 1 / A ) + 1 ) )
23 4 recnd
 |-  ( ( A e. RR /\ 0 < A ) -> ( 1 / A ) e. CC )
24 ax-1cn
 |-  1 e. CC
25 addcom
 |-  ( ( ( 1 / A ) e. CC /\ 1 e. CC ) -> ( ( 1 / A ) + 1 ) = ( 1 + ( 1 / A ) ) )
26 23 24 25 sylancl
 |-  ( ( A e. RR /\ 0 < A ) -> ( ( 1 / A ) + 1 ) = ( 1 + ( 1 / A ) ) )
27 22 26 breqtrd
 |-  ( ( A e. RR /\ 0 < A ) -> ( 1 / A ) < ( 1 + ( 1 / A ) ) )
28 simpl
 |-  ( ( A e. RR /\ 0 < A ) -> A e. RR )
29 simpr
 |-  ( ( A e. RR /\ 0 < A ) -> 0 < A )
30 ltrec1
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( ( 1 + ( 1 / A ) ) e. RR /\ 0 < ( 1 + ( 1 / A ) ) ) ) -> ( ( 1 / A ) < ( 1 + ( 1 / A ) ) <-> ( 1 / ( 1 + ( 1 / A ) ) ) < A ) )
31 28 29 10 16 30 syl22anc
 |-  ( ( A e. RR /\ 0 < A ) -> ( ( 1 / A ) < ( 1 + ( 1 / A ) ) <-> ( 1 / ( 1 + ( 1 / A ) ) ) < A ) )
32 27 31 mpbid
 |-  ( ( A e. RR /\ 0 < A ) -> ( 1 / ( 1 + ( 1 / A ) ) ) < A )
33 19 32 jca
 |-  ( ( A e. RR /\ 0 < A ) -> ( ( 1 / ( 1 + ( 1 / A ) ) ) < 1 /\ ( 1 / ( 1 + ( 1 / A ) ) ) < A ) )