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 mulridd 
 |-  ( ( 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 ) ) )