Metamath Proof Explorer

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 ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝐴 ∈ ℕ0 ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) )
2 elnn0 ⊢ ( 𝐵 ∈ ℕ0 ↔ ( 𝐵 ∈ ℕ ∨ 𝐵 = 0 ) )
3 sqgcd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) )
4 nncn ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℂ )
5 abssq ⊢ ( 𝐵 ∈ ℂ → ( ( abs ‘ 𝐵 ) ↑ 2 ) = ( abs ‘ ( 𝐵 ↑ 2 ) ) )
6 4 5 syl ⊢ ( 𝐵 ∈ ℕ → ( ( abs ‘ 𝐵 ) ↑ 2 ) = ( abs ‘ ( 𝐵 ↑ 2 ) ) )
7 nnz ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
8 gcd0id ⊢ ( 𝐵 ∈ ℤ → ( 0 gcd 𝐵 ) = ( abs ‘ 𝐵 ) )
9 7 8 syl ⊢ ( 𝐵 ∈ ℕ → ( 0 gcd 𝐵 ) = ( abs ‘ 𝐵 ) )
10 9 oveq1d ⊢ ( 𝐵 ∈ ℕ → ( ( 0 gcd 𝐵 ) ↑ 2 ) = ( ( abs ‘ 𝐵 ) ↑ 2 ) )
11 sq0 ⊢ ( 0 ↑ 2 ) = 0
12 11 a1i ⊢ ( 𝐵 ∈ ℕ → ( 0 ↑ 2 ) = 0 )
13 12 oveq1d ⊢ ( 𝐵 ∈ ℕ → ( ( 0 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = ( 0 gcd ( 𝐵 ↑ 2 ) ) )
14 zsqcl ⊢ ( 𝐵 ∈ ℤ → ( 𝐵 ↑ 2 ) ∈ ℤ )
15 gcd0id ⊢ ( ( 𝐵 ↑ 2 ) ∈ ℤ → ( 0 gcd ( 𝐵 ↑ 2 ) ) = ( abs ‘ ( 𝐵 ↑ 2 ) ) )
16 7 14 15 3syl ⊢ ( 𝐵 ∈ ℕ → ( 0 gcd ( 𝐵 ↑ 2 ) ) = ( abs ‘ ( 𝐵 ↑ 2 ) ) )
17 13 16 eqtrd ⊢ ( 𝐵 ∈ ℕ → ( ( 0 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = ( abs ‘ ( 𝐵 ↑ 2 ) ) )
18 6 10 17 3eqtr4d ⊢ ( 𝐵 ∈ ℕ → ( ( 0 gcd 𝐵 ) ↑ 2 ) = ( ( 0 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) )
19 18 adantl ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) → ( ( 0 gcd 𝐵 ) ↑ 2 ) = ( ( 0 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) )
20 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 gcd 𝐵 ) = ( 0 gcd 𝐵 ) )
21 20 oveq1d ⊢ ( 𝐴 = 0 → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = ( ( 0 gcd 𝐵 ) ↑ 2 ) )
22 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 ↑ 2 ) = ( 0 ↑ 2 ) )
23 22 oveq1d ⊢ ( 𝐴 = 0 → ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = ( ( 0 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) )
24 21 23 eqeq12d ⊢ ( 𝐴 = 0 → ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) ↔ ( ( 0 gcd 𝐵 ) ↑ 2 ) = ( ( 0 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) ) )
25 24 adantr ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) → ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) ↔ ( ( 0 gcd 𝐵 ) ↑ 2 ) = ( ( 0 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) ) )
26 19 25 mpbird ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) )
27 nncn ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
28 abssq ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( abs ‘ ( 𝐴 ↑ 2 ) ) )
29 27 28 syl ⊢ ( 𝐴 ∈ ℕ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( abs ‘ ( 𝐴 ↑ 2 ) ) )
30 nnz ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
31 gcdid0 ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 gcd 0 ) = ( abs ‘ 𝐴 ) )
32 30 31 syl ⊢ ( 𝐴 ∈ ℕ → ( 𝐴 gcd 0 ) = ( abs ‘ 𝐴 ) )
33 32 oveq1d ⊢ ( 𝐴 ∈ ℕ → ( ( 𝐴 gcd 0 ) ↑ 2 ) = ( ( abs ‘ 𝐴 ) ↑ 2 ) )
34 11 a1i ⊢ ( 𝐴 ∈ ℕ → ( 0 ↑ 2 ) = 0 )
35 34 oveq2d ⊢ ( 𝐴 ∈ ℕ → ( ( 𝐴 ↑ 2 ) gcd ( 0 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) gcd 0 ) )
36 zsqcl ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ↑ 2 ) ∈ ℤ )
37 gcdid0 ⊢ ( ( 𝐴 ↑ 2 ) ∈ ℤ → ( ( 𝐴 ↑ 2 ) gcd 0 ) = ( abs ‘ ( 𝐴 ↑ 2 ) ) )
38 30 36 37 3syl ⊢ ( 𝐴 ∈ ℕ → ( ( 𝐴 ↑ 2 ) gcd 0 ) = ( abs ‘ ( 𝐴 ↑ 2 ) ) )
39 35 38 eqtrd ⊢ ( 𝐴 ∈ ℕ → ( ( 𝐴 ↑ 2 ) gcd ( 0 ↑ 2 ) ) = ( abs ‘ ( 𝐴 ↑ 2 ) ) )
40 29 33 39 3eqtr4d ⊢ ( 𝐴 ∈ ℕ → ( ( 𝐴 gcd 0 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) gcd ( 0 ↑ 2 ) ) )
41 40 adantr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) → ( ( 𝐴 gcd 0 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) gcd ( 0 ↑ 2 ) ) )
42 oveq2 ⊢ ( 𝐵 = 0 → ( 𝐴 gcd 𝐵 ) = ( 𝐴 gcd 0 ) )
43 42 oveq1d ⊢ ( 𝐵 = 0 → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = ( ( 𝐴 gcd 0 ) ↑ 2 ) )
44 oveq1 ⊢ ( 𝐵 = 0 → ( 𝐵 ↑ 2 ) = ( 0 ↑ 2 ) )
45 44 oveq2d ⊢ ( 𝐵 = 0 → ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) gcd ( 0 ↑ 2 ) ) )
46 43 45 eqeq12d ⊢ ( 𝐵 = 0 → ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) ↔ ( ( 𝐴 gcd 0 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) gcd ( 0 ↑ 2 ) ) ) )
47 46 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) → ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) ↔ ( ( 𝐴 gcd 0 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) gcd ( 0 ↑ 2 ) ) ) )
48 41 47 mpbird ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) )
49 gcd0val ⊢ ( 0 gcd 0 ) = 0
50 49 oveq1i ⊢ ( ( 0 gcd 0 ) ↑ 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 ⊢ ( ( 0 gcd 0 ) ↑ 2 ) = ( ( 0 ↑ 2 ) gcd ( 0 ↑ 2 ) )
54 oveq12 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( 𝐴 gcd 𝐵 ) = ( 0 gcd 0 ) )
55 54 oveq1d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = ( ( 0 gcd 0 ) ↑ 2 ) )
56 22 44 oveqan12d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = ( ( 0 ↑ 2 ) gcd ( 0 ↑ 2 ) ) )
57 53 55 56 3eqtr4a ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) )
58 3 26 48 57 ccase ⊢ ( ( ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) ∧ ( 𝐵 ∈ ℕ ∨ 𝐵 = 0 ) ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) )
59 1 2 58 syl2anb ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) )