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 )
7 6 adantr
 |-  ( ( 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 )
10 9 adantl
 |-  ( ( 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 )
17 11 adantr
 |-  ( ( 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 )
22 12 adantl
 |-  ( ( 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 )
29 28 adantr
 |-  ( ( 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 )
34 33 adantl
 |-  ( ( 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 )
45 44 adantr
 |-  ( ( 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 )
48 47 adantr
 |-  ( ( 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 )
57 56 adantl
 |-  ( ( M e. NN /\ N e. NN ) -> N e. RR )
58 nngt0
 |-  ( N e. NN -> 0 < N )
59 58 adantl
 |-  ( ( 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 ) )
73 72 adantr
 |-  ( ( 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 ) ) )