Step | Hyp | Ref
| Expression |
1 | | ltp1 12094 |
. . . . 5
โข (๐ด โ โ โ ๐ด < (๐ด + 1)) |
2 | | recn 11238 |
. . . . . 6
โข (๐ด โ โ โ ๐ด โ
โ) |
3 | | ax-1cn 11206 |
. . . . . 6
โข 1 โ
โ |
4 | | addcom 11440 |
. . . . . 6
โข ((๐ด โ โ โง 1 โ
โ) โ (๐ด + 1) =
(1 + ๐ด)) |
5 | 2, 3, 4 | sylancl 584 |
. . . . 5
โข (๐ด โ โ โ (๐ด + 1) = (1 + ๐ด)) |
6 | 1, 5 | breqtrd 5178 |
. . . 4
โข (๐ด โ โ โ ๐ด < (1 + ๐ด)) |
7 | 6 | adantr 479 |
. . 3
โข ((๐ด โ โ โง 0 โค
๐ด) โ ๐ด < (1 + ๐ด)) |
8 | 2 | adantr 479 |
. . . 4
โข ((๐ด โ โ โง 0 โค
๐ด) โ ๐ด โ โ) |
9 | | 1re 11254 |
. . . . . . 7
โข 1 โ
โ |
10 | | readdcl 11231 |
. . . . . . 7
โข ((1
โ โ โง ๐ด
โ โ) โ (1 + ๐ด) โ โ) |
11 | 9, 10 | mpan 688 |
. . . . . 6
โข (๐ด โ โ โ (1 +
๐ด) โ
โ) |
12 | 11 | adantr 479 |
. . . . 5
โข ((๐ด โ โ โง 0 โค
๐ด) โ (1 + ๐ด) โ
โ) |
13 | 12 | recnd 11282 |
. . . 4
โข ((๐ด โ โ โง 0 โค
๐ด) โ (1 + ๐ด) โ
โ) |
14 | | 0lt1 11776 |
. . . . . . 7
โข 0 <
1 |
15 | | addgtge0 11742 |
. . . . . . 7
โข (((1
โ โ โง ๐ด
โ โ) โง (0 < 1 โง 0 โค ๐ด)) โ 0 < (1 + ๐ด)) |
16 | 14, 15 | mpanr1 701 |
. . . . . 6
โข (((1
โ โ โง ๐ด
โ โ) โง 0 โค ๐ด) โ 0 < (1 + ๐ด)) |
17 | 9, 16 | mpanl1 698 |
. . . . 5
โข ((๐ด โ โ โง 0 โค
๐ด) โ 0 < (1 + ๐ด)) |
18 | 17 | gt0ne0d 11818 |
. . . 4
โข ((๐ด โ โ โง 0 โค
๐ด) โ (1 + ๐ด) โ 0) |
19 | 8, 13, 18 | divcan1d 12031 |
. . 3
โข ((๐ด โ โ โง 0 โค
๐ด) โ ((๐ด / (1 + ๐ด)) ยท (1 + ๐ด)) = ๐ด) |
20 | 11 | recnd 11282 |
. . . . 5
โข (๐ด โ โ โ (1 +
๐ด) โ
โ) |
21 | 20 | mullidd 11272 |
. . . 4
โข (๐ด โ โ โ (1
ยท (1 + ๐ด)) = (1 +
๐ด)) |
22 | 21 | adantr 479 |
. . 3
โข ((๐ด โ โ โง 0 โค
๐ด) โ (1 ยท (1 +
๐ด)) = (1 + ๐ด)) |
23 | 7, 19, 22 | 3brtr4d 5184 |
. 2
โข ((๐ด โ โ โง 0 โค
๐ด) โ ((๐ด / (1 + ๐ด)) ยท (1 + ๐ด)) < (1 ยท (1 + ๐ด))) |
24 | | simpl 481 |
. . . 4
โข ((๐ด โ โ โง 0 โค
๐ด) โ ๐ด โ โ) |
25 | 24, 12, 18 | redivcld 12082 |
. . 3
โข ((๐ด โ โ โง 0 โค
๐ด) โ (๐ด / (1 + ๐ด)) โ โ) |
26 | | ltmul1 12104 |
. . . 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 835 |
. 2
โข ((๐ด โ โ โง 0 โค
๐ด) โ ((๐ด / (1 + ๐ด)) < 1 โ ((๐ด / (1 + ๐ด)) ยท (1 + ๐ด)) < (1 ยท (1 + ๐ด)))) |
29 | 23, 28 | mpbird 256 |
1
โข ((๐ด โ โ โง 0 โค
๐ด) โ (๐ด / (1 + ๐ด)) < 1) |