This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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