Theorem zgcdsq

Description: nn0gcdsq extended to integers by symmetry. (Contributed by Stefan O'Rear, 15-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		gcdabs	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to \left|A\right|\gcd \left|B\right|=A\gcd B$$
2	1	eqcomd	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to A\gcd B=\left|A\right|\gcd \left|B\right|$$
3	2	oveq1d	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to {\left(A\gcd B\right)}^2={\left(\left|A\right|\gcd \left|B\right|\right)}^2$$
4		nn0abscl	$$⊢A\in \mathbb{Z}\to \left|A\right|\in {\mathbb{N}}_0$$
5		nn0abscl	$$⊢B\in \mathbb{Z}\to \left|B\right|\in {\mathbb{N}}_0$$
6		nn0gcdsq	$$⊢\left(\left|A\right|\in {\mathbb{N}}_0\wedge \left|B\right|\in {\mathbb{N}}_0\right)\to {\left(\left|A\right|\gcd \left|B\right|\right)}^2={\left|A\right|}^2\gcd {\left|B\right|}^2$$
7	4 5 6	syl2an	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to {\left(\left|A\right|\gcd \left|B\right|\right)}^2={\left|A\right|}^2\gcd {\left|B\right|}^2$$
8		zre	$$⊢A\in \mathbb{Z}\to A\in ℝ$$
9	8	adantr	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to A\in ℝ$$
10		absresq	$$⊢A\in ℝ\to {\left|A\right|}^2=A^2$$
11	9 10	syl	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to {\left|A\right|}^2=A^2$$
12		zre	$$⊢B\in \mathbb{Z}\to B\in ℝ$$
13	12	adantl	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to B\in ℝ$$
14		absresq	$$⊢B\in ℝ\to {\left|B\right|}^2=B^2$$
15	13 14	syl	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to {\left|B\right|}^2=B^2$$
16	11 15	oveq12d	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to {\left|A\right|}^2\gcd {\left|B\right|}^2=A^2\gcd B^2$$
17	3 7 16	3eqtrd	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to {\left(A\gcd B\right)}^2=A^2\gcd B^2$$