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

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 ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝑀 ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )

Proof

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