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

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 ) ) )
6 5 adantr 
 |-  ( ( ( 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 )
18 17 adantr 
 |-  ( ( 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 )
21 20 adantr 
 |-  ( ( 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 ) )
24 23 adantr 
 |-  ( ( ( 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 ) )
28 27 adantr 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ ( M ^ 2 ) || ( N ^ 2 ) ) -> ( ( M gcd N ) || M /\ ( M gcd N ) || N ) )
29 28 simprd 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ ( M ^ 2 ) || ( N ^ 2 ) ) -> ( M gcd N ) || N )
30 25 29 eqbrtrrd 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ ( M ^ 2 ) || ( N ^ 2 ) ) -> M || N )
31 30 ex 
 |-  ( ( M e. NN /\ N e. NN ) -> ( ( M ^ 2 ) || ( N ^ 2 ) -> M || N ) )
32 4 31 impbid 
 |-  ( ( M e. NN /\ N e. NN ) -> ( M || N <-> ( M ^ 2 ) || ( N ^ 2 ) ) )