Theorem qsqcl

Description: The square of a rational is rational. (Contributed by Stefan O'Rear, 15-Sep-2014)

	Ref	Expression
Assertion	qsqcl	⊢ ( 𝐴 ∈ ℚ → ( 𝐴 ↑ 2 ) ∈ ℚ )

Proof

Step	Hyp	Ref	Expression
1		qcn	⊢ ( 𝐴 ∈ ℚ → 𝐴 ∈ ℂ )
2		sqval	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
3	1 2	syl	⊢ ( 𝐴 ∈ ℚ → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
4		qmulcl	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐴 ∈ ℚ ) → ( 𝐴 · 𝐴 ) ∈ ℚ )
5	4	anidms	⊢ ( 𝐴 ∈ ℚ → ( 𝐴 · 𝐴 ) ∈ ℚ )
6	3 5	eqeltrd	⊢ ( 𝐴 ∈ ℚ → ( 𝐴 ↑ 2 ) ∈ ℚ )