Metamath Proof Explorer

Theorem densq

Description: Square commutes with canonical denominator. (Contributed by Stefan O'Rear, 15-Sep-2014)

Ref Expression
Assertion densq 
|- ( A e. QQ -> ( denom ` ( A ^ 2 ) ) = ( ( denom ` A ) ^ 2 ) )

Proof

Step Hyp Ref Expression
1 numdensq 
 |-  ( A e. QQ -> ( ( numer ` ( A ^ 2 ) ) = ( ( numer ` A ) ^ 2 ) /\ ( denom ` ( A ^ 2 ) ) = ( ( denom ` A ) ^ 2 ) ) )
2 1 simprd 
 |-  ( A e. QQ -> ( denom ` ( A ^ 2 ) ) = ( ( denom ` A ) ^ 2 ) )