Description: Value of exponentiation to integer powers. (Contributed by NM, 20-May-2004) (Revised by Mario Carneiro, 4-Jun-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | expval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr | |
|
2 | 1 | eqeq1d | |
3 | 1 | breq2d | |
4 | simpl | |
|
5 | 4 | sneqd | |
6 | 5 | xpeq2d | |
7 | 6 | seqeq3d | |
8 | 7 1 | fveq12d | |
9 | 1 | negeqd | |
10 | 7 9 | fveq12d | |
11 | 10 | oveq2d | |
12 | 3 8 11 | ifbieq12d | |
13 | 2 12 | ifbieq2d | |
14 | df-exp | |
|
15 | 1ex | |
|
16 | fvex | |
|
17 | ovex | |
|
18 | 16 17 | ifex | |
19 | 15 18 | ifex | |
20 | 13 14 19 | ovmpoa | |