Metamath Proof Explorer


Theorem rpexpcl

Description: Closure law for integer exponentiation of positive reals. (Contributed by NM, 24-Feb-2008) (Revised by Mario Carneiro, 9-Sep-2014)

Ref Expression
Assertion rpexpcl ( ( ๐ด โˆˆ โ„+ โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐ด โ†‘ ๐‘ ) โˆˆ โ„+ )

Proof

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