Metamath Proof Explorer

Theorem zgcdsq

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

Ref Expression
Assertion zgcdsq ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B 2 = A 2 gcd B 2

Proof

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