Metamath Proof Explorer


Theorem reexpclz

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 โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐ด โ†‘ ๐‘ ) โˆˆ โ„ )