Metamath Proof Explorer

Theorem dvdssqlem

Description: Lemma for dvdssq . (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion dvdssqlem ⊢ M ∈ ℕ ∧ N ∈ ℕ → M ∥ N ↔ M 2 ∥ N 2

Proof

Step Hyp Ref Expression
1 nnz ⊢ M ∈ ℕ → M ∈ ℤ
2 nnz ⊢ N ∈ ℕ → N ∈ ℤ
3 dvdssqim ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ N → M 2 ∥ N 2
4 1 2 3 syl2an ⊢ M ∈ ℕ ∧ N ∈ ℕ → M ∥ N → M 2 ∥ N 2
5 sqgcd ⊢ M ∈ ℕ ∧ N ∈ ℕ → M gcd N 2 = M 2 gcd N 2
6 5 adantr ⊢ M ∈ ℕ ∧ N ∈ ℕ ∧ M 2 ∥ N 2 → M gcd N 2 = M 2 gcd N 2
7 nnsqcl ⊢ M ∈ ℕ → M 2 ∈ ℕ
8 nnsqcl ⊢ N ∈ ℕ → N 2 ∈ ℕ
9 gcdeq ⊢ M 2 ∈ ℕ ∧ N 2 ∈ ℕ → M 2 gcd N 2 = M 2 ↔ M 2 ∥ N 2
10 7 8 9 syl2an ⊢ M ∈ ℕ ∧ N ∈ ℕ → M 2 gcd N 2 = M 2 ↔ M 2 ∥ N 2
11 10 biimpar ⊢ M ∈ ℕ ∧ N ∈ ℕ ∧ M 2 ∥ N 2 → M 2 gcd N 2 = M 2
12 6 11 eqtrd ⊢ M ∈ ℕ ∧ N ∈ ℕ ∧ M 2 ∥ N 2 → M gcd N 2 = M 2
13 gcdcl ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N ∈ ℕ 0
14 1 2 13 syl2an ⊢ M ∈ ℕ ∧ N ∈ ℕ → M gcd N ∈ ℕ 0
15 14 nn0red ⊢ M ∈ ℕ ∧ N ∈ ℕ → M gcd N ∈ ℝ
16 14 nn0ge0d ⊢ M ∈ ℕ ∧ N ∈ ℕ → 0 ≤ M gcd N
17 nnre ⊢ M ∈ ℕ → M ∈ ℝ
18 17 adantr ⊢ M ∈ ℕ ∧ N ∈ ℕ → M ∈ ℝ
19 nnnn0 ⊢ M ∈ ℕ → M ∈ ℕ 0
20 19 nn0ge0d ⊢ M ∈ ℕ → 0 ≤ M
21 20 adantr ⊢ M ∈ ℕ ∧ N ∈ ℕ → 0 ≤ M
22 sq11 ⊢ M gcd N ∈ ℝ ∧ 0 ≤ M gcd N ∧ M ∈ ℝ ∧ 0 ≤ M → M gcd N 2 = M 2 ↔ M gcd N = M
23 15 16 18 21 22 syl22anc ⊢ M ∈ ℕ ∧ N ∈ ℕ → M gcd N 2 = M 2 ↔ M gcd N = M
24 23 adantr ⊢ M ∈ ℕ ∧ N ∈ ℕ ∧ M 2 ∥ N 2 → M gcd N 2 = M 2 ↔ M gcd N = M
25 12 24 mpbid ⊢ M ∈ ℕ ∧ N ∈ ℕ ∧ M 2 ∥ N 2 → M gcd N = M
26 gcddvds ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N ∥ M ∧ M gcd N ∥ N
27 1 2 26 syl2an ⊢ M ∈ ℕ ∧ N ∈ ℕ → M gcd N ∥ M ∧ M gcd N ∥ N
28 27 adantr ⊢ M ∈ ℕ ∧ N ∈ ℕ ∧ M 2 ∥ N 2 → M gcd N ∥ M ∧ M gcd N ∥ N
29 28 simprd ⊢ M ∈ ℕ ∧ N ∈ ℕ ∧ M 2 ∥ N 2 → M gcd N ∥ N
30 25 29 eqbrtrrd ⊢ M ∈ ℕ ∧ N ∈ ℕ ∧ M 2 ∥ N 2 → M ∥ N
31 30 ex ⊢ M ∈ ℕ ∧ N ∈ ℕ → M 2 ∥ N 2 → M ∥ N
32 4 31 impbid ⊢ M ∈ ℕ ∧ N ∈ ℕ → M ∥ N ↔ M 2 ∥ N 2