This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qsqcl

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

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

Step	Hyp	Ref	Expression
1		qcn	$⊢ A \in ℚ \to A \in ℂ$
2		sqval	$⊢ A \in ℂ \to A^{2} = A A$
3	1 2	syl	$⊢ A \in ℚ \to A^{2} = A A$
4		qmulcl	$⊢ (A \in ℚ \land A \in ℚ) \to A A \in ℚ$
5	4	anidms	$⊢ A \in ℚ \to A A \in ℚ$
6	3 5	eqeltrd	$⊢ A \in ℚ \to A^{2} \in ℚ$