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