Theorem denexp

Description: 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 ) )

Proof

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 ) )