Description: Elevating to a nonnegative power commutes with canonical denominator. Similar to densq , extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | denexp | |- ( ( A e. QQ /\ N e. NN0 ) -> ( denom ` ( A ^ N ) ) = ( ( denom ` 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 | simprd | |- ( ( A e. QQ /\ N e. NN0 ) -> ( denom ` ( A ^ N ) ) = ( ( denom ` A ) ^ N ) ) |