Theorem numsq

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

	Ref	Expression
Assertion	numsq	⊢ ( 𝐴 ∈ ℚ → ( numer ‘ ( 𝐴 ↑ 2 ) ) = ( ( numer ‘ 𝐴 ) ↑ 2 ) )

Proof

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