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 N M gcd N 2 = M 2 gcd N 2

Proof

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