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

Metamath Proof Explorer

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 ) ) )