Theorem nn0gcdsq

Description: Squaring commutes with GCD, in particular two coprime numbers have coprime squares. (Contributed by Stefan O'Rear, 15-Sep-2014)

	Ref	Expression
Assertion	nn0gcdsq	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to {\left(A\gcd B\right)}^2=A^2\gcd B^2$$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$$⊢A\in {\mathbb{N}}_0\leftrightarrow \left(A\in \mathbb{N}\vee A=0\right)$$
2		elnn0	$$⊢B\in {\mathbb{N}}_0\leftrightarrow \left(B\in \mathbb{N}\vee B=0\right)$$
3		sqgcd	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to {\left(A\gcd B\right)}^2=A^2\gcd B^2$$
4		nncn	$$⊢B\in \mathbb{N}\to B\in ℂ$$
5		abssq	$$⊢B\in ℂ\to {\left|B\right|}^2=\left|B^2\right|$$
6	4 5	syl	$$⊢B\in \mathbb{N}\to {\left|B\right|}^2=\left|B^2\right|$$
7		nnz	$$⊢B\in \mathbb{N}\to B\in \mathbb{Z}$$
8		gcd0id	$$⊢B\in \mathbb{Z}\to 0\gcd B=\left|B\right|$$
9	7 8	syl	$$⊢B\in \mathbb{N}\to 0\gcd B=\left|B\right|$$
10	9	oveq1d	$$⊢B\in \mathbb{N}\to {\left(0\gcd B\right)}^2={\left|B\right|}^2$$
11		sq0	$$⊢0^2=0$$
12	11	a1i	$$⊢B\in \mathbb{N}\to 0^2=0$$
13	12	oveq1d	$$⊢B\in \mathbb{N}\to 0^2\gcd B^2=0\gcd B^2$$
14		zsqcl	$$⊢B\in \mathbb{Z}\to B^2\in \mathbb{Z}$$
15		gcd0id	$$⊢B^2\in \mathbb{Z}\to 0\gcd B^2=\left|B^2\right|$$
16	7 14 15	3syl	$$⊢B\in \mathbb{N}\to 0\gcd B^2=\left|B^2\right|$$
17	13 16	eqtrd	$$⊢B\in \mathbb{N}\to 0^2\gcd B^2=\left|B^2\right|$$
18	6 10 17	3eqtr4d	$$⊢B\in \mathbb{N}\to {\left(0\gcd B\right)}^2=0^2\gcd B^2$$
19	18	adantl	$$⊢\left(A=0\wedge B\in \mathbb{N}\right)\to {\left(0\gcd B\right)}^2=0^2\gcd B^2$$
20		oveq1	$$⊢A=0\to A\gcd B=0\gcd B$$
21	20	oveq1d	$$⊢A=0\to {\left(A\gcd B\right)}^2={\left(0\gcd B\right)}^2$$
22		oveq1	$$⊢A=0\to A^2=0^2$$
23	22	oveq1d	$$⊢A=0\to A^2\gcd B^2=0^2\gcd B^2$$
24	21 23	eqeq12d	$$⊢A=0\to \left({\left(A\gcd B\right)}^2=A^2\gcd B^2\leftrightarrow {\left(0\gcd B\right)}^2=0^2\gcd B^2\right)$$
25	24	adantr	$$⊢\left(A=0\wedge B\in \mathbb{N}\right)\to \left({\left(A\gcd B\right)}^2=A^2\gcd B^2\leftrightarrow {\left(0\gcd B\right)}^2=0^2\gcd B^2\right)$$
26	19 25	mpbird	$$⊢\left(A=0\wedge B\in \mathbb{N}\right)\to {\left(A\gcd B\right)}^2=A^2\gcd B^2$$
27		nncn	$$⊢A\in \mathbb{N}\to A\in ℂ$$
28		abssq	$$⊢A\in ℂ\to {\left|A\right|}^2=\left|A^2\right|$$
29	27 28	syl	$$⊢A\in \mathbb{N}\to {\left|A\right|}^2=\left|A^2\right|$$
30		nnz	$$⊢A\in \mathbb{N}\to A\in \mathbb{Z}$$
31		gcdid0	$$⊢A\in \mathbb{Z}\to A\gcd 0=\left|A\right|$$
32	30 31	syl	$$⊢A\in \mathbb{N}\to A\gcd 0=\left|A\right|$$
33	32	oveq1d	$$⊢A\in \mathbb{N}\to {\left(A\gcd 0\right)}^2={\left|A\right|}^2$$
34	11	a1i	$$⊢A\in \mathbb{N}\to 0^2=0$$
35	34	oveq2d	$$⊢A\in \mathbb{N}\to A^2\gcd 0^2=A^2\gcd 0$$
36		zsqcl	$$⊢A\in \mathbb{Z}\to A^2\in \mathbb{Z}$$
37		gcdid0	$$⊢A^2\in \mathbb{Z}\to A^2\gcd 0=\left|A^2\right|$$
38	30 36 37	3syl	$$⊢A\in \mathbb{N}\to A^2\gcd 0=\left|A^2\right|$$
39	35 38	eqtrd	$$⊢A\in \mathbb{N}\to A^2\gcd 0^2=\left|A^2\right|$$
40	29 33 39	3eqtr4d	$$⊢A\in \mathbb{N}\to {\left(A\gcd 0\right)}^2=A^2\gcd 0^2$$
41	40	adantr	$$⊢\left(A\in \mathbb{N}\wedge B=0\right)\to {\left(A\gcd 0\right)}^2=A^2\gcd 0^2$$
42		oveq2	$$⊢B=0\to A\gcd B=A\gcd 0$$
43	42	oveq1d	$$⊢B=0\to {\left(A\gcd B\right)}^2={\left(A\gcd 0\right)}^2$$
44		oveq1	$$⊢B=0\to B^2=0^2$$
45	44	oveq2d	$$⊢B=0\to A^2\gcd B^2=A^2\gcd 0^2$$
46	43 45	eqeq12d	$$⊢B=0\to \left({\left(A\gcd B\right)}^2=A^2\gcd B^2\leftrightarrow {\left(A\gcd 0\right)}^2=A^2\gcd 0^2\right)$$
47	46	adantl	$$⊢\left(A\in \mathbb{N}\wedge B=0\right)\to \left({\left(A\gcd B\right)}^2=A^2\gcd B^2\leftrightarrow {\left(A\gcd 0\right)}^2=A^2\gcd 0^2\right)$$
48	41 47	mpbird	$$⊢\left(A\in \mathbb{N}\wedge B=0\right)\to {\left(A\gcd B\right)}^2=A^2\gcd B^2$$
49		gcd0val	$$⊢0\gcd 0=0$$
50	49	oveq1i	$$⊢{\left(0\gcd 0\right)}^2=0^2$$
51	11 11	oveq12i	$$⊢0^2\gcd 0^2=0\gcd 0$$
52	51 49	eqtri	$$⊢0^2\gcd 0^2=0$$
53	11 50 52	3eqtr4i	$$⊢{\left(0\gcd 0\right)}^2=0^2\gcd 0^2$$
54		oveq12	$$⊢\left(A=0\wedge B=0\right)\to A\gcd B=0\gcd 0$$
55	54	oveq1d	$$⊢\left(A=0\wedge B=0\right)\to {\left(A\gcd B\right)}^2={\left(0\gcd 0\right)}^2$$
56	22 44	oveqan12d	$$⊢\left(A=0\wedge B=0\right)\to A^2\gcd B^2=0^2\gcd 0^2$$
57	53 55 56	3eqtr4a	$$⊢\left(A=0\wedge B=0\right)\to {\left(A\gcd B\right)}^2=A^2\gcd B^2$$
58	3 26 48 57	ccase	$$⊢\left(\left(A\in \mathbb{N}\vee A=0\right)\wedge \left(B\in \mathbb{N}\vee B=0\right)\right)\to {\left(A\gcd B\right)}^2=A^2\gcd B^2$$
59	1 2 58	syl2anb	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to {\left(A\gcd B\right)}^2=A^2\gcd B^2$$