Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
โข ( ( ๐ด โ โ+ โง ๐ โ โค ) โ ๐ด โ โ+ ) |
2 |
|
rpne0 |
โข ( ๐ด โ โ+ โ ๐ด โ 0 ) |
3 |
2
|
adantr |
โข ( ( ๐ด โ โ+ โง ๐ โ โค ) โ ๐ด โ 0 ) |
4 |
|
simpr |
โข ( ( ๐ด โ โ+ โง ๐ โ โค ) โ ๐ โ โค ) |
5 |
|
rpssre |
โข โ+ โ โ |
6 |
|
ax-resscn |
โข โ โ โ |
7 |
5 6
|
sstri |
โข โ+ โ โ |
8 |
|
rpmulcl |
โข ( ( ๐ฅ โ โ+ โง ๐ฆ โ โ+ ) โ ( ๐ฅ ยท ๐ฆ ) โ โ+ ) |
9 |
|
1rp |
โข 1 โ โ+ |
10 |
|
rpreccl |
โข ( ๐ฅ โ โ+ โ ( 1 / ๐ฅ ) โ โ+ ) |
11 |
10
|
adantr |
โข ( ( ๐ฅ โ โ+ โง ๐ฅ โ 0 ) โ ( 1 / ๐ฅ ) โ โ+ ) |
12 |
7 8 9 11
|
expcl2lem |
โข ( ( ๐ด โ โ+ โง ๐ด โ 0 โง ๐ โ โค ) โ ( ๐ด โ ๐ ) โ โ+ ) |
13 |
1 3 4 12
|
syl3anc |
โข ( ( ๐ด โ โ+ โง ๐ โ โค ) โ ( ๐ด โ ๐ ) โ โ+ ) |