Step | Hyp | Ref
| Expression |
1 | | ltp1 12058 |
. . . . 5
โข (๐ด โ โ โ ๐ด < (๐ด + 1)) |
2 | | recn 11202 |
. . . . . 6
โข (๐ด โ โ โ ๐ด โ
โ) |
3 | | ax-1cn 11170 |
. . . . . 6
โข 1 โ
โ |
4 | | addcom 11404 |
. . . . . 6
โข ((๐ด โ โ โง 1 โ
โ) โ (๐ด + 1) =
(1 + ๐ด)) |
5 | 2, 3, 4 | sylancl 585 |
. . . . 5
โข (๐ด โ โ โ (๐ด + 1) = (1 + ๐ด)) |
6 | 1, 5 | breqtrd 5167 |
. . . 4
โข (๐ด โ โ โ ๐ด < (1 + ๐ด)) |
7 | 6 | adantr 480 |
. . 3
โข ((๐ด โ โ โง 0 โค
๐ด) โ ๐ด < (1 + ๐ด)) |
8 | 2 | adantr 480 |
. . . 4
โข ((๐ด โ โ โง 0 โค
๐ด) โ ๐ด โ โ) |
9 | | 1re 11218 |
. . . . . . 7
โข 1 โ
โ |
10 | | readdcl 11195 |
. . . . . . 7
โข ((1
โ โ โง ๐ด
โ โ) โ (1 + ๐ด) โ โ) |
11 | 9, 10 | mpan 687 |
. . . . . 6
โข (๐ด โ โ โ (1 +
๐ด) โ
โ) |
12 | 11 | adantr 480 |
. . . . 5
โข ((๐ด โ โ โง 0 โค
๐ด) โ (1 + ๐ด) โ
โ) |
13 | 12 | recnd 11246 |
. . . 4
โข ((๐ด โ โ โง 0 โค
๐ด) โ (1 + ๐ด) โ
โ) |
14 | | 0lt1 11740 |
. . . . . . 7
โข 0 <
1 |
15 | | addgtge0 11706 |
. . . . . . 7
โข (((1
โ โ โง ๐ด
โ โ) โง (0 < 1 โง 0 โค ๐ด)) โ 0 < (1 + ๐ด)) |
16 | 14, 15 | mpanr1 700 |
. . . . . 6
โข (((1
โ โ โง ๐ด
โ โ) โง 0 โค ๐ด) โ 0 < (1 + ๐ด)) |
17 | 9, 16 | mpanl1 697 |
. . . . 5
โข ((๐ด โ โ โง 0 โค
๐ด) โ 0 < (1 + ๐ด)) |
18 | 17 | gt0ne0d 11782 |
. . . 4
โข ((๐ด โ โ โง 0 โค
๐ด) โ (1 + ๐ด) โ 0) |
19 | 8, 13, 18 | divcan1d 11995 |
. . 3
โข ((๐ด โ โ โง 0 โค
๐ด) โ ((๐ด / (1 + ๐ด)) ยท (1 + ๐ด)) = ๐ด) |
20 | 11 | recnd 11246 |
. . . . 5
โข (๐ด โ โ โ (1 +
๐ด) โ
โ) |
21 | 20 | mullidd 11236 |
. . . 4
โข (๐ด โ โ โ (1
ยท (1 + ๐ด)) = (1 +
๐ด)) |
22 | 21 | adantr 480 |
. . 3
โข ((๐ด โ โ โง 0 โค
๐ด) โ (1 ยท (1 +
๐ด)) = (1 + ๐ด)) |
23 | 7, 19, 22 | 3brtr4d 5173 |
. 2
โข ((๐ด โ โ โง 0 โค
๐ด) โ ((๐ด / (1 + ๐ด)) ยท (1 + ๐ด)) < (1 ยท (1 + ๐ด))) |
24 | | simpl 482 |
. . . 4
โข ((๐ด โ โ โง 0 โค
๐ด) โ ๐ด โ โ) |
25 | 24, 12, 18 | redivcld 12046 |
. . 3
โข ((๐ด โ โ โง 0 โค
๐ด) โ (๐ด / (1 + ๐ด)) โ โ) |
26 | | ltmul1 12068 |
. . . 4
โข (((๐ด / (1 + ๐ด)) โ โ โง 1 โ โ
โง ((1 + ๐ด) โ
โ โง 0 < (1 + ๐ด))) โ ((๐ด / (1 + ๐ด)) < 1 โ ((๐ด / (1 + ๐ด)) ยท (1 + ๐ด)) < (1 ยท (1 + ๐ด)))) |
27 | 9, 26 | mp3an2 1445 |
. . 3
โข (((๐ด / (1 + ๐ด)) โ โ โง ((1 + ๐ด) โ โ โง 0 < (1
+ ๐ด))) โ ((๐ด / (1 + ๐ด)) < 1 โ ((๐ด / (1 + ๐ด)) ยท (1 + ๐ด)) < (1 ยท (1 + ๐ด)))) |
28 | 25, 12, 17, 27 | syl12anc 834 |
. 2
โข ((๐ด โ โ โง 0 โค
๐ด) โ ((๐ด / (1 + ๐ด)) < 1 โ ((๐ด / (1 + ๐ด)) ยท (1 + ๐ด)) < (1 ยท (1 + ๐ด)))) |
29 | 23, 28 | mpbird 257 |
1
โข ((๐ด โ โ โง 0 โค
๐ด) โ (๐ด / (1 + ๐ด)) < 1) |