Theorem qsqcl

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

	Ref	Expression
Assertion	qsqcl	$$⊢A\in \mathbb{Q}\to A^2\in \mathbb{Q}$$

Proof

Step	Hyp	Ref	Expression
1		qcn	$$⊢A\in \mathbb{Q}\to A\in ℂ$$
2		sqval	$$⊢A\in ℂ\to A^2=AA$$
3	1 2	syl	$$⊢A\in \mathbb{Q}\to A^2=AA$$
4		qmulcl	$$⊢\left(A\in \mathbb{Q}\wedge A\in \mathbb{Q}\right)\to AA\in \mathbb{Q}$$
5	4	anidms	$$⊢A\in \mathbb{Q}\to AA\in \mathbb{Q}$$
6	3 5	eqeltrd	$$⊢A\in \mathbb{Q}\to A^2\in \mathbb{Q}$$