Theorem densq

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

	Ref	Expression
Assertion	densq	⊢ ( 𝐴 ∈ ℚ → ( denom ‘ ( 𝐴 ↑ 2 ) ) = ( ( denom ‘ 𝐴 ) ↑ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		numdensq	⊢ ( 𝐴 ∈ ℚ → ( ( numer ‘ ( 𝐴 ↑ 2 ) ) = ( ( numer ‘ 𝐴 ) ↑ 2 ) ∧ ( denom ‘ ( 𝐴 ↑ 2 ) ) = ( ( denom ‘ 𝐴 ) ↑ 2 ) ) )
2	1	simprd	⊢ ( 𝐴 ∈ ℚ → ( denom ‘ ( 𝐴 ↑ 2 ) ) = ( ( denom ‘ 𝐴 ) ↑ 2 ) )