Metamath Proof Explorer

Theorem sqgcd

Description: Square distributes over gcd. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion sqgcd ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) = ( ( 𝑀 ↑ 2 ) gcd ( 𝑁 ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 gcdnncl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 gcd 𝑁 ) ∈ ℕ )
2 1 nnsqcld ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ∈ ℕ )
3 2 nncnd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ∈ ℂ )
4 3 mulid1d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) · 1 ) = ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) )
5 nnsqcl ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ↑ 2 ) ∈ ℕ )
6 5 nnzd ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ↑ 2 ) ∈ ℤ )
7 6 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ↑ 2 ) ∈ ℤ )
8 nnsqcl ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ↑ 2 ) ∈ ℕ )
9 8 nnzd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ↑ 2 ) ∈ ℤ )
10 9 adantl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ↑ 2 ) ∈ ℤ )
11 nnz ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
12 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
13 gcddvds ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) )
14 11 12 13 syl2an ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) )
15 14 simpld ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 gcd 𝑁 ) ∥ 𝑀 )
16 1 nnzd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 gcd 𝑁 ) ∈ ℤ )
17 11 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝑀 ∈ ℤ )
18 dvdssqim ⊢ ( ( ( 𝑀 gcd 𝑁 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 → ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ∥ ( 𝑀 ↑ 2 ) ) )
19 16 17 18 syl2anc ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 → ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ∥ ( 𝑀 ↑ 2 ) ) )
20 15 19 mpd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ∥ ( 𝑀 ↑ 2 ) )
21 14 simprd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 gcd 𝑁 ) ∥ 𝑁 )
22 12 adantl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℤ )
23 dvdssqim ⊢ ( ( ( 𝑀 gcd 𝑁 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑁 → ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )
24 16 22 23 syl2anc ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑁 → ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )
25 21 24 mpd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) )
26 gcddiv ⊢ ( ( ( ( 𝑀 ↑ 2 ) ∈ ℤ ∧ ( 𝑁 ↑ 2 ) ∈ ℤ ∧ ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ∈ ℕ ) ∧ ( ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ∥ ( 𝑀 ↑ 2 ) ∧ ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) ) → ( ( ( 𝑀 ↑ 2 ) gcd ( 𝑁 ↑ 2 ) ) / ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ) = ( ( ( 𝑀 ↑ 2 ) / ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ) gcd ( ( 𝑁 ↑ 2 ) / ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ) ) )
27 7 10 2 20 25 26 syl32anc ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 ↑ 2 ) gcd ( 𝑁 ↑ 2 ) ) / ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ) = ( ( ( 𝑀 ↑ 2 ) / ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ) gcd ( ( 𝑁 ↑ 2 ) / ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ) ) )
28 nncn ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℂ )
29 28 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝑀 ∈ ℂ )
30 1 nncnd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 gcd 𝑁 ) ∈ ℂ )
31 1 nnne0d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 gcd 𝑁 ) ≠ 0 )
32 29 30 31 sqdivd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) ↑ 2 ) = ( ( 𝑀 ↑ 2 ) / ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ) )
33 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
34 33 adantl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
35 34 30 31 sqdivd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 / ( 𝑀 gcd 𝑁 ) ) ↑ 2 ) = ( ( 𝑁 ↑ 2 ) / ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ) )
36 32 35 oveq12d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) ↑ 2 ) gcd ( ( 𝑁 / ( 𝑀 gcd 𝑁 ) ) ↑ 2 ) ) = ( ( ( 𝑀 ↑ 2 ) / ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ) gcd ( ( 𝑁 ↑ 2 ) / ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ) ) )
37 gcddiv ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 gcd 𝑁 ) ∈ ℕ ) ∧ ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) ) → ( ( 𝑀 gcd 𝑁 ) / ( 𝑀 gcd 𝑁 ) ) = ( ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) gcd ( 𝑁 / ( 𝑀 gcd 𝑁 ) ) ) )
38 17 22 1 14 37 syl31anc ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 gcd 𝑁 ) / ( 𝑀 gcd 𝑁 ) ) = ( ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) gcd ( 𝑁 / ( 𝑀 gcd 𝑁 ) ) ) )
39 30 31 dividd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 gcd 𝑁 ) / ( 𝑀 gcd 𝑁 ) ) = 1 )
40 38 39 eqtr3d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) gcd ( 𝑁 / ( 𝑀 gcd 𝑁 ) ) ) = 1 )
41 dvdsval2 ⊢ ( ( ( 𝑀 gcd 𝑁 ) ∈ ℤ ∧ ( 𝑀 gcd 𝑁 ) ≠ 0 ∧ 𝑀 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ↔ ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) ∈ ℤ ) )
42 16 31 17 41 syl3anc ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ↔ ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) ∈ ℤ ) )
43 15 42 mpbid ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) ∈ ℤ )
44 nnre ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ )
45 44 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝑀 ∈ ℝ )
46 1 nnred ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 gcd 𝑁 ) ∈ ℝ )
47 nngt0 ⊢ ( 𝑀 ∈ ℕ → 0 < 𝑀 )
48 47 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 0 < 𝑀 )
49 1 nngt0d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 0 < ( 𝑀 gcd 𝑁 ) )
50 45 46 48 49 divgt0d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 0 < ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) )
51 elnnz ⊢ ( ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) ∈ ℕ ↔ ( ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) ∈ ℤ ∧ 0 < ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) ) )
52 43 50 51 sylanbrc ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) ∈ ℕ )
53 dvdsval2 ⊢ ( ( ( 𝑀 gcd 𝑁 ) ∈ ℤ ∧ ( 𝑀 gcd 𝑁 ) ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ↔ ( 𝑁 / ( 𝑀 gcd 𝑁 ) ) ∈ ℤ ) )
54 16 31 22 53 syl3anc ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ↔ ( 𝑁 / ( 𝑀 gcd 𝑁 ) ) ∈ ℤ ) )
55 21 54 mpbid ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 / ( 𝑀 gcd 𝑁 ) ) ∈ ℤ )
56 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
57 56 adantl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℝ )
58 nngt0 ⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
59 58 adantl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 0 < 𝑁 )
60 57 46 59 49 divgt0d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 0 < ( 𝑁 / ( 𝑀 gcd 𝑁 ) ) )
61 elnnz ⊢ ( ( 𝑁 / ( 𝑀 gcd 𝑁 ) ) ∈ ℕ ↔ ( ( 𝑁 / ( 𝑀 gcd 𝑁 ) ) ∈ ℤ ∧ 0 < ( 𝑁 / ( 𝑀 gcd 𝑁 ) ) ) )
62 55 60 61 sylanbrc ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 / ( 𝑀 gcd 𝑁 ) ) ∈ ℕ )
63 2nn ⊢ 2 ∈ ℕ
64 rppwr ⊢ ( ( ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) ∈ ℕ ∧ ( 𝑁 / ( 𝑀 gcd 𝑁 ) ) ∈ ℕ ∧ 2 ∈ ℕ ) → ( ( ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) gcd ( 𝑁 / ( 𝑀 gcd 𝑁 ) ) ) = 1 → ( ( ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) ↑ 2 ) gcd ( ( 𝑁 / ( 𝑀 gcd 𝑁 ) ) ↑ 2 ) ) = 1 ) )
65 63 64 mp3an3 ⊢ ( ( ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) ∈ ℕ ∧ ( 𝑁 / ( 𝑀 gcd 𝑁 ) ) ∈ ℕ ) → ( ( ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) gcd ( 𝑁 / ( 𝑀 gcd 𝑁 ) ) ) = 1 → ( ( ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) ↑ 2 ) gcd ( ( 𝑁 / ( 𝑀 gcd 𝑁 ) ) ↑ 2 ) ) = 1 ) )
66 52 62 65 syl2anc ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) gcd ( 𝑁 / ( 𝑀 gcd 𝑁 ) ) ) = 1 → ( ( ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) ↑ 2 ) gcd ( ( 𝑁 / ( 𝑀 gcd 𝑁 ) ) ↑ 2 ) ) = 1 ) )
67 40 66 mpd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) ↑ 2 ) gcd ( ( 𝑁 / ( 𝑀 gcd 𝑁 ) ) ↑ 2 ) ) = 1 )
68 27 36 67 3eqtr2d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 ↑ 2 ) gcd ( 𝑁 ↑ 2 ) ) / ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ) = 1 )
69 6 9 anim12i ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 ↑ 2 ) ∈ ℤ ∧ ( 𝑁 ↑ 2 ) ∈ ℤ ) )
70 5 nnne0d ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ↑ 2 ) ≠ 0 )
71 70 neneqd ⊢ ( 𝑀 ∈ ℕ → ¬ ( 𝑀 ↑ 2 ) = 0 )
72 71 intnanrd ⊢ ( 𝑀 ∈ ℕ → ¬ ( ( 𝑀 ↑ 2 ) = 0 ∧ ( 𝑁 ↑ 2 ) = 0 ) )
73 72 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ¬ ( ( 𝑀 ↑ 2 ) = 0 ∧ ( 𝑁 ↑ 2 ) = 0 ) )
74 gcdn0cl ⊢ ( ( ( ( 𝑀 ↑ 2 ) ∈ ℤ ∧ ( 𝑁 ↑ 2 ) ∈ ℤ ) ∧ ¬ ( ( 𝑀 ↑ 2 ) = 0 ∧ ( 𝑁 ↑ 2 ) = 0 ) ) → ( ( 𝑀 ↑ 2 ) gcd ( 𝑁 ↑ 2 ) ) ∈ ℕ )
75 69 73 74 syl2anc ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 ↑ 2 ) gcd ( 𝑁 ↑ 2 ) ) ∈ ℕ )
76 75 nncnd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 ↑ 2 ) gcd ( 𝑁 ↑ 2 ) ) ∈ ℂ )
77 2 nnne0d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ≠ 0 )
78 ax-1cn ⊢ 1 ∈ ℂ
79 divmul ⊢ ( ( ( ( 𝑀 ↑ 2 ) gcd ( 𝑁 ↑ 2 ) ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ∈ ℂ ∧ ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ≠ 0 ) ) → ( ( ( ( 𝑀 ↑ 2 ) gcd ( 𝑁 ↑ 2 ) ) / ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ) = 1 ↔ ( ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) · 1 ) = ( ( 𝑀 ↑ 2 ) gcd ( 𝑁 ↑ 2 ) ) ) )
80 78 79 mp3an2 ⊢ ( ( ( ( 𝑀 ↑ 2 ) gcd ( 𝑁 ↑ 2 ) ) ∈ ℂ ∧ ( ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ∈ ℂ ∧ ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ≠ 0 ) ) → ( ( ( ( 𝑀 ↑ 2 ) gcd ( 𝑁 ↑ 2 ) ) / ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ) = 1 ↔ ( ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) · 1 ) = ( ( 𝑀 ↑ 2 ) gcd ( 𝑁 ↑ 2 ) ) ) )
81 76 3 77 80 syl12anc ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( ( 𝑀 ↑ 2 ) gcd ( 𝑁 ↑ 2 ) ) / ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) ) = 1 ↔ ( ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) · 1 ) = ( ( 𝑀 ↑ 2 ) gcd ( 𝑁 ↑ 2 ) ) ) )
82 68 81 mpbid ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) · 1 ) = ( ( 𝑀 ↑ 2 ) gcd ( 𝑁 ↑ 2 ) ) )
83 4 82 eqtr3d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 gcd 𝑁 ) ↑ 2 ) = ( ( 𝑀 ↑ 2 ) gcd ( 𝑁 ↑ 2 ) ) )