This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nn0gcdsq

Description: Squaring commutes with GCD, in particular two coprime numbers have coprime squares. (Contributed by Stefan O'Rear, 15-Sep-2014)

Ref Expression
Assertion nn0gcdsq 
|- ( ( A e. NN0 /\ B e. NN0 ) -> ( ( A gcd B ) ^ 2 ) = ( ( A ^ 2 ) gcd ( B ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( A e. NN0 <-> ( A e. NN \/ A = 0 ) )
2 elnn0 
 |-  ( B e. NN0 <-> ( B e. NN \/ B = 0 ) )
3 sqgcd 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( A gcd B ) ^ 2 ) = ( ( A ^ 2 ) gcd ( B ^ 2 ) ) )
4 nncn 
 |-  ( B e. NN -> B e. CC )
5 abssq 
 |-  ( B e. CC -> ( ( abs ` B ) ^ 2 ) = ( abs ` ( B ^ 2 ) ) )
6 4 5 syl 
 |-  ( B e. NN -> ( ( abs ` B ) ^ 2 ) = ( abs ` ( B ^ 2 ) ) )
7 nnz 
 |-  ( B e. NN -> B e. ZZ )
8 gcd0id 
 |-  ( B e. ZZ -> ( 0 gcd B ) = ( abs ` B ) )
9 7 8 syl 
 |-  ( B e. NN -> ( 0 gcd B ) = ( abs ` B ) )
10 9 oveq1d 
 |-  ( B e. NN -> ( ( 0 gcd B ) ^ 2 ) = ( ( abs ` B ) ^ 2 ) )
11 sq0 
 |-  ( 0 ^ 2 ) = 0
12 11 a1i 
 |-  ( B e. NN -> ( 0 ^ 2 ) = 0 )
13 12 oveq1d 
 |-  ( B e. NN -> ( ( 0 ^ 2 ) gcd ( B ^ 2 ) ) = ( 0 gcd ( B ^ 2 ) ) )
14 zsqcl 
 |-  ( B e. ZZ -> ( B ^ 2 ) e. ZZ )
15 gcd0id 
 |-  ( ( B ^ 2 ) e. ZZ -> ( 0 gcd ( B ^ 2 ) ) = ( abs ` ( B ^ 2 ) ) )
16 7 14 15 3syl 
 |-  ( B e. NN -> ( 0 gcd ( B ^ 2 ) ) = ( abs ` ( B ^ 2 ) ) )
17 13 16 eqtrd 
 |-  ( B e. NN -> ( ( 0 ^ 2 ) gcd ( B ^ 2 ) ) = ( abs ` ( B ^ 2 ) ) )
18 6 10 17 3eqtr4d 
 |-  ( B e. NN -> ( ( 0 gcd B ) ^ 2 ) = ( ( 0 ^ 2 ) gcd ( B ^ 2 ) ) )
19 18 adantl 
 |-  ( ( A = 0 /\ B e. NN ) -> ( ( 0 gcd B ) ^ 2 ) = ( ( 0 ^ 2 ) gcd ( B ^ 2 ) ) )
20 oveq1 
 |-  ( A = 0 -> ( A gcd B ) = ( 0 gcd B ) )
21 20 oveq1d 
 |-  ( A = 0 -> ( ( A gcd B ) ^ 2 ) = ( ( 0 gcd B ) ^ 2 ) )
22 oveq1 
 |-  ( A = 0 -> ( A ^ 2 ) = ( 0 ^ 2 ) )
23 22 oveq1d 
 |-  ( A = 0 -> ( ( A ^ 2 ) gcd ( B ^ 2 ) ) = ( ( 0 ^ 2 ) gcd ( B ^ 2 ) ) )
24 21 23 eqeq12d 
 |-  ( A = 0 -> ( ( ( A gcd B ) ^ 2 ) = ( ( A ^ 2 ) gcd ( B ^ 2 ) ) <-> ( ( 0 gcd B ) ^ 2 ) = ( ( 0 ^ 2 ) gcd ( B ^ 2 ) ) ) )
25 24 adantr 
 |-  ( ( A = 0 /\ B e. NN ) -> ( ( ( A gcd B ) ^ 2 ) = ( ( A ^ 2 ) gcd ( B ^ 2 ) ) <-> ( ( 0 gcd B ) ^ 2 ) = ( ( 0 ^ 2 ) gcd ( B ^ 2 ) ) ) )
26 19 25 mpbird 
 |-  ( ( A = 0 /\ B e. NN ) -> ( ( A gcd B ) ^ 2 ) = ( ( A ^ 2 ) gcd ( B ^ 2 ) ) )
27 nncn 
 |-  ( A e. NN -> A e. CC )
28 abssq 
 |-  ( A e. CC -> ( ( abs ` A ) ^ 2 ) = ( abs ` ( A ^ 2 ) ) )
29 27 28 syl 
 |-  ( A e. NN -> ( ( abs ` A ) ^ 2 ) = ( abs ` ( A ^ 2 ) ) )
30 nnz 
 |-  ( A e. NN -> A e. ZZ )
31 gcdid0 
 |-  ( A e. ZZ -> ( A gcd 0 ) = ( abs ` A ) )
32 30 31 syl 
 |-  ( A e. NN -> ( A gcd 0 ) = ( abs ` A ) )
33 32 oveq1d 
 |-  ( A e. NN -> ( ( A gcd 0 ) ^ 2 ) = ( ( abs ` A ) ^ 2 ) )
34 11 a1i 
 |-  ( A e. NN -> ( 0 ^ 2 ) = 0 )
35 34 oveq2d 
 |-  ( A e. NN -> ( ( A ^ 2 ) gcd ( 0 ^ 2 ) ) = ( ( A ^ 2 ) gcd 0 ) )
36 zsqcl 
 |-  ( A e. ZZ -> ( A ^ 2 ) e. ZZ )
37 gcdid0 
 |-  ( ( A ^ 2 ) e. ZZ -> ( ( A ^ 2 ) gcd 0 ) = ( abs ` ( A ^ 2 ) ) )
38 30 36 37 3syl 
 |-  ( A e. NN -> ( ( A ^ 2 ) gcd 0 ) = ( abs ` ( A ^ 2 ) ) )
39 35 38 eqtrd 
 |-  ( A e. NN -> ( ( A ^ 2 ) gcd ( 0 ^ 2 ) ) = ( abs ` ( A ^ 2 ) ) )
40 29 33 39 3eqtr4d 
 |-  ( A e. NN -> ( ( A gcd 0 ) ^ 2 ) = ( ( A ^ 2 ) gcd ( 0 ^ 2 ) ) )
41 40 adantr 
 |-  ( ( A e. NN /\ B = 0 ) -> ( ( A gcd 0 ) ^ 2 ) = ( ( A ^ 2 ) gcd ( 0 ^ 2 ) ) )
42 oveq2 
 |-  ( B = 0 -> ( A gcd B ) = ( A gcd 0 ) )
43 42 oveq1d 
 |-  ( B = 0 -> ( ( A gcd B ) ^ 2 ) = ( ( A gcd 0 ) ^ 2 ) )
44 oveq1 
 |-  ( B = 0 -> ( B ^ 2 ) = ( 0 ^ 2 ) )
45 44 oveq2d 
 |-  ( B = 0 -> ( ( A ^ 2 ) gcd ( B ^ 2 ) ) = ( ( A ^ 2 ) gcd ( 0 ^ 2 ) ) )
46 43 45 eqeq12d 
 |-  ( B = 0 -> ( ( ( A gcd B ) ^ 2 ) = ( ( A ^ 2 ) gcd ( B ^ 2 ) ) <-> ( ( A gcd 0 ) ^ 2 ) = ( ( A ^ 2 ) gcd ( 0 ^ 2 ) ) ) )
47 46 adantl 
 |-  ( ( A e. NN /\ B = 0 ) -> ( ( ( A gcd B ) ^ 2 ) = ( ( A ^ 2 ) gcd ( B ^ 2 ) ) <-> ( ( A gcd 0 ) ^ 2 ) = ( ( A ^ 2 ) gcd ( 0 ^ 2 ) ) ) )
48 41 47 mpbird 
 |-  ( ( A e. NN /\ B = 0 ) -> ( ( A gcd B ) ^ 2 ) = ( ( A ^ 2 ) gcd ( B ^ 2 ) ) )
49 gcd0val 
 |-  ( 0 gcd 0 ) = 0
50 49 oveq1i 
 |-  ( ( 0 gcd 0 ) ^ 2 ) = ( 0 ^ 2 )
51 11 11 oveq12i 
 |-  ( ( 0 ^ 2 ) gcd ( 0 ^ 2 ) ) = ( 0 gcd 0 )
52 51 49 eqtri 
 |-  ( ( 0 ^ 2 ) gcd ( 0 ^ 2 ) ) = 0
53 11 50 52 3eqtr4i 
 |-  ( ( 0 gcd 0 ) ^ 2 ) = ( ( 0 ^ 2 ) gcd ( 0 ^ 2 ) )
54 oveq12 
 |-  ( ( A = 0 /\ B = 0 ) -> ( A gcd B ) = ( 0 gcd 0 ) )
55 54 oveq1d 
 |-  ( ( A = 0 /\ B = 0 ) -> ( ( A gcd B ) ^ 2 ) = ( ( 0 gcd 0 ) ^ 2 ) )
56 22 44 oveqan12d 
 |-  ( ( A = 0 /\ B = 0 ) -> ( ( A ^ 2 ) gcd ( B ^ 2 ) ) = ( ( 0 ^ 2 ) gcd ( 0 ^ 2 ) ) )
57 53 55 56 3eqtr4a 
 |-  ( ( A = 0 /\ B = 0 ) -> ( ( A gcd B ) ^ 2 ) = ( ( A ^ 2 ) gcd ( B ^ 2 ) ) )
58 3 26 48 57 ccase 
 |-  ( ( ( A e. NN \/ A = 0 ) /\ ( B e. NN \/ B = 0 ) ) -> ( ( A gcd B ) ^ 2 ) = ( ( A ^ 2 ) gcd ( B ^ 2 ) ) )
59 1 2 58 syl2anb 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( A gcd B ) ^ 2 ) = ( ( A ^ 2 ) gcd ( B ^ 2 ) ) )