Theorem zgcdsq

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

	Ref	Expression
Assertion	zgcdsq	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gcdabs	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( abs ‘ 𝐴 ) gcd ( abs ‘ 𝐵 ) ) = ( 𝐴 gcd 𝐵 ) )
2	1	eqcomd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 gcd 𝐵 ) = ( ( abs ‘ 𝐴 ) gcd ( abs ‘ 𝐵 ) ) )
3	2	oveq1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = ( ( ( abs ‘ 𝐴 ) gcd ( abs ‘ 𝐵 ) ) ↑ 2 ) )
4		nn0abscl	⊢ ( 𝐴 ∈ ℤ → ( abs ‘ 𝐴 ) ∈ ℕ0 )
5		nn0abscl	⊢ ( 𝐵 ∈ ℤ → ( abs ‘ 𝐵 ) ∈ ℕ0 )
6		nn0gcdsq	⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℕ0 ∧ ( abs ‘ 𝐵 ) ∈ ℕ0 ) → ( ( ( abs ‘ 𝐴 ) gcd ( abs ‘ 𝐵 ) ) ↑ 2 ) = ( ( ( abs ‘ 𝐴 ) ↑ 2 ) gcd ( ( abs ‘ 𝐵 ) ↑ 2 ) ) )
7	4 5 6	syl2an	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ( abs ‘ 𝐴 ) gcd ( abs ‘ 𝐵 ) ) ↑ 2 ) = ( ( ( abs ‘ 𝐴 ) ↑ 2 ) gcd ( ( abs ‘ 𝐵 ) ↑ 2 ) ) )
8		zre	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
9	8	adantr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∈ ℝ )
10		absresq	⊢ ( 𝐴 ∈ ℝ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 ↑ 2 ) )
11	9 10	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 ↑ 2 ) )
12		zre	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℝ )
13	12	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℝ )
14		absresq	⊢ ( 𝐵 ∈ ℝ → ( ( abs ‘ 𝐵 ) ↑ 2 ) = ( 𝐵 ↑ 2 ) )
15	13 14	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( abs ‘ 𝐵 ) ↑ 2 ) = ( 𝐵 ↑ 2 ) )
16	11 15	oveq12d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ( abs ‘ 𝐴 ) ↑ 2 ) gcd ( ( abs ‘ 𝐵 ) ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) )
17	3 7 16	3eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) )