# Metamath Proof Explorer

## Theorem dvdssqlem

Description: Lemma for dvdssq . (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion dvdssqlem
`|- ( ( M e. NN /\ N e. NN ) -> ( M || N <-> ( M ^ 2 ) || ( N ^ 2 ) ) )`

### Proof

Step Hyp Ref Expression
1 nnz
` |-  ( M e. NN -> M e. ZZ )`
2 nnz
` |-  ( N e. NN -> N e. ZZ )`
3 dvdssqim
` |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N -> ( M ^ 2 ) || ( N ^ 2 ) ) )`
4 1 2 3 syl2an
` |-  ( ( M e. NN /\ N e. NN ) -> ( M || N -> ( M ^ 2 ) || ( N ^ 2 ) ) )`
5 sqgcd
` |-  ( ( M e. NN /\ N e. NN ) -> ( ( M gcd N ) ^ 2 ) = ( ( M ^ 2 ) gcd ( N ^ 2 ) ) )`
` |-  ( ( ( M e. NN /\ N e. NN ) /\ ( M ^ 2 ) || ( N ^ 2 ) ) -> ( ( M gcd N ) ^ 2 ) = ( ( M ^ 2 ) gcd ( N ^ 2 ) ) )`
7 nnsqcl
` |-  ( M e. NN -> ( M ^ 2 ) e. NN )`
8 nnsqcl
` |-  ( N e. NN -> ( N ^ 2 ) e. NN )`
9 gcdeq
` |-  ( ( ( M ^ 2 ) e. NN /\ ( N ^ 2 ) e. NN ) -> ( ( ( M ^ 2 ) gcd ( N ^ 2 ) ) = ( M ^ 2 ) <-> ( M ^ 2 ) || ( N ^ 2 ) ) )`
10 7 8 9 syl2an
` |-  ( ( M e. NN /\ N e. NN ) -> ( ( ( M ^ 2 ) gcd ( N ^ 2 ) ) = ( M ^ 2 ) <-> ( M ^ 2 ) || ( N ^ 2 ) ) )`
11 10 biimpar
` |-  ( ( ( M e. NN /\ N e. NN ) /\ ( M ^ 2 ) || ( N ^ 2 ) ) -> ( ( M ^ 2 ) gcd ( N ^ 2 ) ) = ( M ^ 2 ) )`
12 6 11 eqtrd
` |-  ( ( ( M e. NN /\ N e. NN ) /\ ( M ^ 2 ) || ( N ^ 2 ) ) -> ( ( M gcd N ) ^ 2 ) = ( M ^ 2 ) )`
13 gcdcl
` |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. NN0 )`
14 1 2 13 syl2an
` |-  ( ( M e. NN /\ N e. NN ) -> ( M gcd N ) e. NN0 )`
15 14 nn0red
` |-  ( ( M e. NN /\ N e. NN ) -> ( M gcd N ) e. RR )`
16 14 nn0ge0d
` |-  ( ( M e. NN /\ N e. NN ) -> 0 <_ ( M gcd N ) )`
17 nnre
` |-  ( M e. NN -> M e. RR )`
` |-  ( ( M e. NN /\ N e. NN ) -> M e. RR )`
19 nnnn0
` |-  ( M e. NN -> M e. NN0 )`
20 19 nn0ge0d
` |-  ( M e. NN -> 0 <_ M )`
` |-  ( ( M e. NN /\ N e. NN ) -> 0 <_ M )`
22 sq11
` |-  ( ( ( ( M gcd N ) e. RR /\ 0 <_ ( M gcd N ) ) /\ ( M e. RR /\ 0 <_ M ) ) -> ( ( ( M gcd N ) ^ 2 ) = ( M ^ 2 ) <-> ( M gcd N ) = M ) )`
23 15 16 18 21 22 syl22anc
` |-  ( ( M e. NN /\ N e. NN ) -> ( ( ( M gcd N ) ^ 2 ) = ( M ^ 2 ) <-> ( M gcd N ) = M ) )`
` |-  ( ( ( M e. NN /\ N e. NN ) /\ ( M ^ 2 ) || ( N ^ 2 ) ) -> ( ( ( M gcd N ) ^ 2 ) = ( M ^ 2 ) <-> ( M gcd N ) = M ) )`
25 12 24 mpbid
` |-  ( ( ( M e. NN /\ N e. NN ) /\ ( M ^ 2 ) || ( N ^ 2 ) ) -> ( M gcd N ) = M )`
26 gcddvds
` |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) || M /\ ( M gcd N ) || N ) )`
27 1 2 26 syl2an
` |-  ( ( M e. NN /\ N e. NN ) -> ( ( M gcd N ) || M /\ ( M gcd N ) || N ) )`
` |-  ( ( ( M e. NN /\ N e. NN ) /\ ( M ^ 2 ) || ( N ^ 2 ) ) -> ( ( M gcd N ) || M /\ ( M gcd N ) || N ) )`
` |-  ( ( ( M e. NN /\ N e. NN ) /\ ( M ^ 2 ) || ( N ^ 2 ) ) -> ( M gcd N ) || N )`
` |-  ( ( ( M e. NN /\ N e. NN ) /\ ( M ^ 2 ) || ( N ^ 2 ) ) -> M || N )`
` |-  ( ( M e. NN /\ N e. NN ) -> ( ( M ^ 2 ) || ( N ^ 2 ) -> M || N ) )`
` |-  ( ( M e. NN /\ N e. NN ) -> ( M || N <-> ( M ^ 2 ) || ( N ^ 2 ) ) )`