Metamath Proof Explorer

Theorem dvdssqim

Description: Unidirectional form of dvdssq . (Contributed by Scott Fenton, 19-Apr-2014)

Ref Expression
Assertion dvdssqim 
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N -> ( M ^ 2 ) || ( N ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 divides 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> E. k e. ZZ ( k x. M ) = N ) )
2 zsqcl 
 |-  ( k e. ZZ -> ( k ^ 2 ) e. ZZ )
3 zsqcl 
 |-  ( M e. ZZ -> ( M ^ 2 ) e. ZZ )
4 dvdsmul2 
 |-  ( ( ( k ^ 2 ) e. ZZ /\ ( M ^ 2 ) e. ZZ ) -> ( M ^ 2 ) || ( ( k ^ 2 ) x. ( M ^ 2 ) ) )
5 2 3 4 syl2anr 
 |-  ( ( M e. ZZ /\ k e. ZZ ) -> ( M ^ 2 ) || ( ( k ^ 2 ) x. ( M ^ 2 ) ) )
6 zcn 
 |-  ( k e. ZZ -> k e. CC )
7 zcn 
 |-  ( M e. ZZ -> M e. CC )
8 sqmul 
 |-  ( ( k e. CC /\ M e. CC ) -> ( ( k x. M ) ^ 2 ) = ( ( k ^ 2 ) x. ( M ^ 2 ) ) )
9 6 7 8 syl2anr 
 |-  ( ( M e. ZZ /\ k e. ZZ ) -> ( ( k x. M ) ^ 2 ) = ( ( k ^ 2 ) x. ( M ^ 2 ) ) )
10 5 9 breqtrrd 
 |-  ( ( M e. ZZ /\ k e. ZZ ) -> ( M ^ 2 ) || ( ( k x. M ) ^ 2 ) )
11 oveq1 
 |-  ( ( k x. M ) = N -> ( ( k x. M ) ^ 2 ) = ( N ^ 2 ) )
12 11 breq2d 
 |-  ( ( k x. M ) = N -> ( ( M ^ 2 ) || ( ( k x. M ) ^ 2 ) <-> ( M ^ 2 ) || ( N ^ 2 ) ) )
13 10 12 syl5ibcom 
 |-  ( ( M e. ZZ /\ k e. ZZ ) -> ( ( k x. M ) = N -> ( M ^ 2 ) || ( N ^ 2 ) ) )
14 13 rexlimdva 
 |-  ( M e. ZZ -> ( E. k e. ZZ ( k x. M ) = N -> ( M ^ 2 ) || ( N ^ 2 ) ) )
15 14 adantr 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( E. k e. ZZ ( k x. M ) = N -> ( M ^ 2 ) || ( N ^ 2 ) ) )
16 1 15 sylbid 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N -> ( M ^ 2 ) || ( N ^ 2 ) ) )