# 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
`|- ( ( M e. NN /\ N e. NN ) -> ( ( M gcd N ) ^ 2 ) = ( ( M ^ 2 ) gcd ( N ^ 2 ) ) )`

### Proof

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