Theorem numdensq

Description: Squaring a rational squares its canonical components. (Contributed by Stefan O'Rear, 15-Sep-2014)

	Ref	Expression
Assertion	numdensq	$$⊢A\in \mathbb{Q}\to \left(\mathrm{numer}\left(A^2\right)={\mathrm{numer}\left(A\right)}^2\wedge \mathrm{denom}\left(A^2\right)={\mathrm{denom}\left(A\right)}^2\right)$$

Proof

Step	Hyp	Ref	Expression
1		qnumdencoprm	$$⊢A\in \mathbb{Q}\to \mathrm{numer}\left(A\right)\gcd \mathrm{denom}\left(A\right)=1$$
2	1	oveq1d	$$⊢A\in \mathbb{Q}\to {\left(\mathrm{numer}\left(A\right)\gcd \mathrm{denom}\left(A\right)\right)}^2=1^2$$
3		qnumcl	$$⊢A\in \mathbb{Q}\to \mathrm{numer}\left(A\right)\in \mathbb{Z}$$
4		qdencl	$$⊢A\in \mathbb{Q}\to \mathrm{denom}\left(A\right)\in \mathbb{N}$$
5	4	nnzd	$$⊢A\in \mathbb{Q}\to \mathrm{denom}\left(A\right)\in \mathbb{Z}$$
6		zgcdsq	$$⊢\left(\mathrm{numer}\left(A\right)\in \mathbb{Z}\wedge \mathrm{denom}\left(A\right)\in \mathbb{Z}\right)\to {\left(\mathrm{numer}\left(A\right)\gcd \mathrm{denom}\left(A\right)\right)}^2={\mathrm{numer}\left(A\right)}^2\gcd {\mathrm{denom}\left(A\right)}^2$$
7	3 5 6	syl2anc	$$⊢A\in \mathbb{Q}\to {\left(\mathrm{numer}\left(A\right)\gcd \mathrm{denom}\left(A\right)\right)}^2={\mathrm{numer}\left(A\right)}^2\gcd {\mathrm{denom}\left(A\right)}^2$$
8		sq1	$$⊢1^2=1$$
9	8	a1i	$$⊢A\in \mathbb{Q}\to 1^2=1$$
10	2 7 9	3eqtr3d	$$⊢A\in \mathbb{Q}\to {\mathrm{numer}\left(A\right)}^2\gcd {\mathrm{denom}\left(A\right)}^2=1$$
11		qeqnumdivden	$$⊢A\in \mathbb{Q}\to A=\frac{\mathrm{numer}\left(A\right)}{\mathrm{denom}\left(A\right)}$$
12	11	oveq1d	$$⊢A\in \mathbb{Q}\to A^2={\left(\frac{\mathrm{numer}\left(A\right)}{\mathrm{denom}\left(A\right)}\right)}^2$$
13	3	zcnd	$$⊢A\in \mathbb{Q}\to \mathrm{numer}\left(A\right)\in ℂ$$
14	4	nncnd	$$⊢A\in \mathbb{Q}\to \mathrm{denom}\left(A\right)\in ℂ$$
15	4	nnne0d	$$⊢A\in \mathbb{Q}\to \mathrm{denom}\left(A\right)\ne 0$$
16	13 14 15	sqdivd	$$⊢A\in \mathbb{Q}\to {\left(\frac{\mathrm{numer}\left(A\right)}{\mathrm{denom}\left(A\right)}\right)}^2=\frac{{\mathrm{numer}\left(A\right)}^2}{{\mathrm{denom}\left(A\right)}^2}$$
17	12 16	eqtrd	$$⊢A\in \mathbb{Q}\to A^2=\frac{{\mathrm{numer}\left(A\right)}^2}{{\mathrm{denom}\left(A\right)}^2}$$
18		qsqcl	$$⊢A\in \mathbb{Q}\to A^2\in \mathbb{Q}$$
19		zsqcl	$$⊢\mathrm{numer}\left(A\right)\in \mathbb{Z}\to {\mathrm{numer}\left(A\right)}^2\in \mathbb{Z}$$
20	3 19	syl	$$⊢A\in \mathbb{Q}\to {\mathrm{numer}\left(A\right)}^2\in \mathbb{Z}$$
21	4	nnsqcld	$$⊢A\in \mathbb{Q}\to {\mathrm{denom}\left(A\right)}^2\in \mathbb{N}$$
22		qnumdenbi	$$⊢\left(A^2\in \mathbb{Q}\wedge {\mathrm{numer}\left(A\right)}^2\in \mathbb{Z}\wedge {\mathrm{denom}\left(A\right)}^2\in \mathbb{N}\right)\to \left(\left({\mathrm{numer}\left(A\right)}^2\gcd {\mathrm{denom}\left(A\right)}^2=1\wedge A^2=\frac{{\mathrm{numer}\left(A\right)}^2}{{\mathrm{denom}\left(A\right)}^2}\right)\leftrightarrow \left(\mathrm{numer}\left(A^2\right)={\mathrm{numer}\left(A\right)}^2\wedge \mathrm{denom}\left(A^2\right)={\mathrm{denom}\left(A\right)}^2\right)\right)$$
23	18 20 21 22	syl3anc	$$⊢A\in \mathbb{Q}\to \left(\left({\mathrm{numer}\left(A\right)}^2\gcd {\mathrm{denom}\left(A\right)}^2=1\wedge A^2=\frac{{\mathrm{numer}\left(A\right)}^2}{{\mathrm{denom}\left(A\right)}^2}\right)\leftrightarrow \left(\mathrm{numer}\left(A^2\right)={\mathrm{numer}\left(A\right)}^2\wedge \mathrm{denom}\left(A^2\right)={\mathrm{denom}\left(A\right)}^2\right)\right)$$
24	10 17 23	mpbi2and	$$⊢A\in \mathbb{Q}\to \left(\mathrm{numer}\left(A^2\right)={\mathrm{numer}\left(A\right)}^2\wedge \mathrm{denom}\left(A^2\right)={\mathrm{denom}\left(A\right)}^2\right)$$