Metamath Proof Explorer


Theorem recp1lt1

Description: Construct a number less than 1 from any nonnegative number. (Contributed by NM, 30-Dec-2005)

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

Proof

Step Hyp Ref Expression
1 ltp1
 |-  ( A e. RR -> A < ( A + 1 ) )
2 recn
 |-  ( A e. RR -> A e. CC )
3 ax-1cn
 |-  1 e. CC
4 addcom
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( A + 1 ) = ( 1 + A ) )
5 2 3 4 sylancl
 |-  ( A e. RR -> ( A + 1 ) = ( 1 + A ) )
6 1 5 breqtrd
 |-  ( A e. RR -> A < ( 1 + A ) )
7 6 adantr
 |-  ( ( A e. RR /\ 0 <_ A ) -> A < ( 1 + A ) )
8 2 adantr
 |-  ( ( A e. RR /\ 0 <_ A ) -> A e. CC )
9 1re
 |-  1 e. RR
10 readdcl
 |-  ( ( 1 e. RR /\ A e. RR ) -> ( 1 + A ) e. RR )
11 9 10 mpan
 |-  ( A e. RR -> ( 1 + A ) e. RR )
12 11 adantr
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( 1 + A ) e. RR )
13 12 recnd
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( 1 + A ) e. CC )
14 0lt1
 |-  0 < 1
15 addgtge0
 |-  ( ( ( 1 e. RR /\ A e. RR ) /\ ( 0 < 1 /\ 0 <_ A ) ) -> 0 < ( 1 + A ) )
16 14 15 mpanr1
 |-  ( ( ( 1 e. RR /\ A e. RR ) /\ 0 <_ A ) -> 0 < ( 1 + A ) )
17 9 16 mpanl1
 |-  ( ( A e. RR /\ 0 <_ A ) -> 0 < ( 1 + A ) )
18 17 gt0ne0d
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( 1 + A ) =/= 0 )
19 8 13 18 divcan1d
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( ( A / ( 1 + A ) ) x. ( 1 + A ) ) = A )
20 11 recnd
 |-  ( A e. RR -> ( 1 + A ) e. CC )
21 20 mulid2d
 |-  ( A e. RR -> ( 1 x. ( 1 + A ) ) = ( 1 + A ) )
22 21 adantr
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( 1 x. ( 1 + A ) ) = ( 1 + A ) )
23 7 19 22 3brtr4d
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( ( A / ( 1 + A ) ) x. ( 1 + A ) ) < ( 1 x. ( 1 + A ) ) )
24 simpl
 |-  ( ( A e. RR /\ 0 <_ A ) -> A e. RR )
25 24 12 18 redivcld
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( A / ( 1 + A ) ) e. RR )
26 ltmul1
 |-  ( ( ( A / ( 1 + A ) ) e. RR /\ 1 e. RR /\ ( ( 1 + A ) e. RR /\ 0 < ( 1 + A ) ) ) -> ( ( A / ( 1 + A ) ) < 1 <-> ( ( A / ( 1 + A ) ) x. ( 1 + A ) ) < ( 1 x. ( 1 + A ) ) ) )
27 9 26 mp3an2
 |-  ( ( ( A / ( 1 + A ) ) e. RR /\ ( ( 1 + A ) e. RR /\ 0 < ( 1 + A ) ) ) -> ( ( A / ( 1 + A ) ) < 1 <-> ( ( A / ( 1 + A ) ) x. ( 1 + A ) ) < ( 1 x. ( 1 + A ) ) ) )
28 25 12 17 27 syl12anc
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( ( A / ( 1 + A ) ) < 1 <-> ( ( A / ( 1 + A ) ) x. ( 1 + A ) ) < ( 1 x. ( 1 + A ) ) ) )
29 23 28 mpbird
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( A / ( 1 + A ) ) < 1 )