Description: Elevating to a nonnegative power commutes with canonical numerator. Similar to numsq , extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | numexp | |- ( ( A e. QQ /\ N e. NN0 ) -> ( numer ` ( A ^ N ) ) = ( ( numer ` A ) ^ N ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | numdenexp | |- ( ( A e. QQ /\ N e. NN0 ) -> ( ( numer ` ( A ^ N ) ) = ( ( numer ` A ) ^ N ) /\ ( denom ` ( A ^ N ) ) = ( ( denom ` A ) ^ N ) ) ) |
|
| 2 | 1 | simpld | |- ( ( A e. QQ /\ N e. NN0 ) -> ( numer ` ( A ^ N ) ) = ( ( numer ` A ) ^ N ) ) |