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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl | |
|
2 | rpne0 | |
|
3 | 2 | adantr | |
4 | simpr | |
|
5 | rpssre | |
|
6 | ax-resscn | |
|
7 | 5 6 | sstri | |
8 | rpmulcl | |
|
9 | 1rp | |
|
10 | rpreccl | |
|
11 | 10 | adantr | |
12 | 7 8 9 11 | expcl2lem | |
13 | 1 3 4 12 | syl3anc | |