Metamath Proof Explorer
Description: Closure of integer exponentiation of reals. (Contributed by Mario
Carneiro, 4-Jun-2014) (Revised by Mario Carneiro, 9-Sep-2014)
|
|
Ref |
Expression |
|
Assertion |
reexpclz |
โข ( ( ๐ด โ โ โง ๐ด โ 0 โง ๐ โ โค ) โ ( ๐ด โ ๐ ) โ โ ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
ax-resscn |
โข โ โ โ |
2 |
|
remulcl |
โข ( ( ๐ฅ โ โ โง ๐ฆ โ โ ) โ ( ๐ฅ ยท ๐ฆ ) โ โ ) |
3 |
|
1re |
โข 1 โ โ |
4 |
|
rereccl |
โข ( ( ๐ฅ โ โ โง ๐ฅ โ 0 ) โ ( 1 / ๐ฅ ) โ โ ) |
5 |
1 2 3 4
|
expcl2lem |
โข ( ( ๐ด โ โ โง ๐ด โ 0 โง ๐ โ โค ) โ ( ๐ด โ ๐ ) โ โ ) |