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 ( ( ๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด ) โ†’ ( ๐ด / ( 1 + ๐ด ) ) < 1 )

Proof

Step Hyp Ref Expression
1 ltp1 โŠข ( ๐ด โˆˆ โ„ โ†’ ๐ด < ( ๐ด + 1 ) )
2 recn โŠข ( ๐ด โˆˆ โ„ โ†’ ๐ด โˆˆ โ„‚ )
3 ax-1cn โŠข 1 โˆˆ โ„‚
4 addcom โŠข ( ( ๐ด โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ ) โ†’ ( ๐ด + 1 ) = ( 1 + ๐ด ) )
5 2 3 4 sylancl โŠข ( ๐ด โˆˆ โ„ โ†’ ( ๐ด + 1 ) = ( 1 + ๐ด ) )
6 1 5 breqtrd โŠข ( ๐ด โˆˆ โ„ โ†’ ๐ด < ( 1 + ๐ด ) )
7 6 adantr โŠข ( ( ๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด ) โ†’ ๐ด < ( 1 + ๐ด ) )
8 2 adantr โŠข ( ( ๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด ) โ†’ ๐ด โˆˆ โ„‚ )
9 1re โŠข 1 โˆˆ โ„
10 readdcl โŠข ( ( 1 โˆˆ โ„ โˆง ๐ด โˆˆ โ„ ) โ†’ ( 1 + ๐ด ) โˆˆ โ„ )
11 9 10 mpan โŠข ( ๐ด โˆˆ โ„ โ†’ ( 1 + ๐ด ) โˆˆ โ„ )
12 11 adantr โŠข ( ( ๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด ) โ†’ ( 1 + ๐ด ) โˆˆ โ„ )
13 12 recnd โŠข ( ( ๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด ) โ†’ ( 1 + ๐ด ) โˆˆ โ„‚ )
14 0lt1 โŠข 0 < 1
15 addgtge0 โŠข ( ( ( 1 โˆˆ โ„ โˆง ๐ด โˆˆ โ„ ) โˆง ( 0 < 1 โˆง 0 โ‰ค ๐ด ) ) โ†’ 0 < ( 1 + ๐ด ) )
16 14 15 mpanr1 โŠข ( ( ( 1 โˆˆ โ„ โˆง ๐ด โˆˆ โ„ ) โˆง 0 โ‰ค ๐ด ) โ†’ 0 < ( 1 + ๐ด ) )
17 9 16 mpanl1 โŠข ( ( ๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด ) โ†’ 0 < ( 1 + ๐ด ) )
18 17 gt0ne0d โŠข ( ( ๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด ) โ†’ ( 1 + ๐ด ) โ‰  0 )
19 8 13 18 divcan1d โŠข ( ( ๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด ) โ†’ ( ( ๐ด / ( 1 + ๐ด ) ) ยท ( 1 + ๐ด ) ) = ๐ด )
20 11 recnd โŠข ( ๐ด โˆˆ โ„ โ†’ ( 1 + ๐ด ) โˆˆ โ„‚ )
21 20 mullidd โŠข ( ๐ด โˆˆ โ„ โ†’ ( 1 ยท ( 1 + ๐ด ) ) = ( 1 + ๐ด ) )
22 21 adantr โŠข ( ( ๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด ) โ†’ ( 1 ยท ( 1 + ๐ด ) ) = ( 1 + ๐ด ) )
23 7 19 22 3brtr4d โŠข ( ( ๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด ) โ†’ ( ( ๐ด / ( 1 + ๐ด ) ) ยท ( 1 + ๐ด ) ) < ( 1 ยท ( 1 + ๐ด ) ) )
24 simpl โŠข ( ( ๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด ) โ†’ ๐ด โˆˆ โ„ )
25 24 12 18 redivcld โŠข ( ( ๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด ) โ†’ ( ๐ด / ( 1 + ๐ด ) ) โˆˆ โ„ )
26 ltmul1 โŠข ( ( ( ๐ด / ( 1 + ๐ด ) ) โˆˆ โ„ โˆง 1 โˆˆ โ„ โˆง ( ( 1 + ๐ด ) โˆˆ โ„ โˆง 0 < ( 1 + ๐ด ) ) ) โ†’ ( ( ๐ด / ( 1 + ๐ด ) ) < 1 โ†” ( ( ๐ด / ( 1 + ๐ด ) ) ยท ( 1 + ๐ด ) ) < ( 1 ยท ( 1 + ๐ด ) ) ) )
27 9 26 mp3an2 โŠข ( ( ( ๐ด / ( 1 + ๐ด ) ) โˆˆ โ„ โˆง ( ( 1 + ๐ด ) โˆˆ โ„ โˆง 0 < ( 1 + ๐ด ) ) ) โ†’ ( ( ๐ด / ( 1 + ๐ด ) ) < 1 โ†” ( ( ๐ด / ( 1 + ๐ด ) ) ยท ( 1 + ๐ด ) ) < ( 1 ยท ( 1 + ๐ด ) ) ) )
28 25 12 17 27 syl12anc โŠข ( ( ๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด ) โ†’ ( ( ๐ด / ( 1 + ๐ด ) ) < 1 โ†” ( ( ๐ด / ( 1 + ๐ด ) ) ยท ( 1 + ๐ด ) ) < ( 1 ยท ( 1 + ๐ด ) ) ) )
29 23 28 mpbird โŠข ( ( ๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด ) โ†’ ( ๐ด / ( 1 + ๐ด ) ) < 1 )