Metamath Proof Explorer

Theorem dvdssq

Description: Two numbers are divisible iff their squares are. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( M = 0 -> ( M || N <-> 0 || N ) )
2 sq0i 
 |-  ( M = 0 -> ( M ^ 2 ) = 0 )
3 2 breq1d 
 |-  ( M = 0 -> ( ( M ^ 2 ) || ( N ^ 2 ) <-> 0 || ( N ^ 2 ) ) )
4 1 3 bibi12d 
 |-  ( M = 0 -> ( ( M || N <-> ( M ^ 2 ) || ( N ^ 2 ) ) <-> ( 0 || N <-> 0 || ( N ^ 2 ) ) ) )
5 nnabscl 
 |-  ( ( M e. ZZ /\ M =/= 0 ) -> ( abs ` M ) e. NN )
6 breq2 
 |-  ( N = 0 -> ( ( abs ` M ) || N <-> ( abs ` M ) || 0 ) )
7 sq0i 
 |-  ( N = 0 -> ( N ^ 2 ) = 0 )
8 7 breq2d 
 |-  ( N = 0 -> ( ( ( abs ` M ) ^ 2 ) || ( N ^ 2 ) <-> ( ( abs ` M ) ^ 2 ) || 0 ) )
9 6 8 bibi12d 
 |-  ( N = 0 -> ( ( ( abs ` M ) || N <-> ( ( abs ` M ) ^ 2 ) || ( N ^ 2 ) ) <-> ( ( abs ` M ) || 0 <-> ( ( abs ` M ) ^ 2 ) || 0 ) ) )
10 nnabscl 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> ( abs ` N ) e. NN )
11 dvdssqlem 
 |-  ( ( ( abs ` M ) e. NN /\ ( abs ` N ) e. NN ) -> ( ( abs ` M ) || ( abs ` N ) <-> ( ( abs ` M ) ^ 2 ) || ( ( abs ` N ) ^ 2 ) ) )
12 10 11 sylan2 
 |-  ( ( ( abs ` M ) e. NN /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( abs ` M ) || ( abs ` N ) <-> ( ( abs ` M ) ^ 2 ) || ( ( abs ` N ) ^ 2 ) ) )
13 nnz 
 |-  ( ( abs ` M ) e. NN -> ( abs ` M ) e. ZZ )
14 simpl 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> N e. ZZ )
15 dvdsabsb 
 |-  ( ( ( abs ` M ) e. ZZ /\ N e. ZZ ) -> ( ( abs ` M ) || N <-> ( abs ` M ) || ( abs ` N ) ) )
16 13 14 15 syl2an 
 |-  ( ( ( abs ` M ) e. NN /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( abs ` M ) || N <-> ( abs ` M ) || ( abs ` N ) ) )
17 nnsqcl 
 |-  ( ( abs ` M ) e. NN -> ( ( abs ` M ) ^ 2 ) e. NN )
18 17 nnzd 
 |-  ( ( abs ` M ) e. NN -> ( ( abs ` M ) ^ 2 ) e. ZZ )
19 zsqcl 
 |-  ( N e. ZZ -> ( N ^ 2 ) e. ZZ )
20 19 adantr 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> ( N ^ 2 ) e. ZZ )
21 dvdsabsb 
 |-  ( ( ( ( abs ` M ) ^ 2 ) e. ZZ /\ ( N ^ 2 ) e. ZZ ) -> ( ( ( abs ` M ) ^ 2 ) || ( N ^ 2 ) <-> ( ( abs ` M ) ^ 2 ) || ( abs ` ( N ^ 2 ) ) ) )
22 18 20 21 syl2an 
 |-  ( ( ( abs ` M ) e. NN /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( ( abs ` M ) ^ 2 ) || ( N ^ 2 ) <-> ( ( abs ` M ) ^ 2 ) || ( abs ` ( N ^ 2 ) ) ) )
23 zcn 
 |-  ( N e. ZZ -> N e. CC )
24 23 adantr 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> N e. CC )
25 abssq 
 |-  ( N e. CC -> ( ( abs ` N ) ^ 2 ) = ( abs ` ( N ^ 2 ) ) )
26 24 25 syl 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> ( ( abs ` N ) ^ 2 ) = ( abs ` ( N ^ 2 ) ) )
27 26 breq2d 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> ( ( ( abs ` M ) ^ 2 ) || ( ( abs ` N ) ^ 2 ) <-> ( ( abs ` M ) ^ 2 ) || ( abs ` ( N ^ 2 ) ) ) )
28 27 adantl 
 |-  ( ( ( abs ` M ) e. NN /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( ( abs ` M ) ^ 2 ) || ( ( abs ` N ) ^ 2 ) <-> ( ( abs ` M ) ^ 2 ) || ( abs ` ( N ^ 2 ) ) ) )
29 22 28 bitr4d 
 |-  ( ( ( abs ` M ) e. NN /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( ( abs ` M ) ^ 2 ) || ( N ^ 2 ) <-> ( ( abs ` M ) ^ 2 ) || ( ( abs ` N ) ^ 2 ) ) )
30 12 16 29 3bitr4d 
 |-  ( ( ( abs ` M ) e. NN /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( abs ` M ) || N <-> ( ( abs ` M ) ^ 2 ) || ( N ^ 2 ) ) )
31 30 anassrs 
 |-  ( ( ( ( abs ` M ) e. NN /\ N e. ZZ ) /\ N =/= 0 ) -> ( ( abs ` M ) || N <-> ( ( abs ` M ) ^ 2 ) || ( N ^ 2 ) ) )
32 dvds0 
 |-  ( ( abs ` M ) e. ZZ -> ( abs ` M ) || 0 )
33 zsqcl 
 |-  ( ( abs ` M ) e. ZZ -> ( ( abs ` M ) ^ 2 ) e. ZZ )
34 dvds0 
 |-  ( ( ( abs ` M ) ^ 2 ) e. ZZ -> ( ( abs ` M ) ^ 2 ) || 0 )
35 33 34 syl 
 |-  ( ( abs ` M ) e. ZZ -> ( ( abs ` M ) ^ 2 ) || 0 )
36 32 35 2thd 
 |-  ( ( abs ` M ) e. ZZ -> ( ( abs ` M ) || 0 <-> ( ( abs ` M ) ^ 2 ) || 0 ) )
37 13 36 syl 
 |-  ( ( abs ` M ) e. NN -> ( ( abs ` M ) || 0 <-> ( ( abs ` M ) ^ 2 ) || 0 ) )
38 37 adantr 
 |-  ( ( ( abs ` M ) e. NN /\ N e. ZZ ) -> ( ( abs ` M ) || 0 <-> ( ( abs ` M ) ^ 2 ) || 0 ) )
39 9 31 38 pm2.61ne 
 |-  ( ( ( abs ` M ) e. NN /\ N e. ZZ ) -> ( ( abs ` M ) || N <-> ( ( abs ` M ) ^ 2 ) || ( N ^ 2 ) ) )
40 5 39 sylan 
 |-  ( ( ( M e. ZZ /\ M =/= 0 ) /\ N e. ZZ ) -> ( ( abs ` M ) || N <-> ( ( abs ` M ) ^ 2 ) || ( N ^ 2 ) ) )
41 absdvdsb 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> ( abs ` M ) || N ) )
42 41 adantlr 
 |-  ( ( ( M e. ZZ /\ M =/= 0 ) /\ N e. ZZ ) -> ( M || N <-> ( abs ` M ) || N ) )
43 zsqcl 
 |-  ( M e. ZZ -> ( M ^ 2 ) e. ZZ )
44 43 adantr 
 |-  ( ( M e. ZZ /\ M =/= 0 ) -> ( M ^ 2 ) e. ZZ )
45 absdvdsb 
 |-  ( ( ( M ^ 2 ) e. ZZ /\ ( N ^ 2 ) e. ZZ ) -> ( ( M ^ 2 ) || ( N ^ 2 ) <-> ( abs ` ( M ^ 2 ) ) || ( N ^ 2 ) ) )
46 44 19 45 syl2an 
 |-  ( ( ( M e. ZZ /\ M =/= 0 ) /\ N e. ZZ ) -> ( ( M ^ 2 ) || ( N ^ 2 ) <-> ( abs ` ( M ^ 2 ) ) || ( N ^ 2 ) ) )
47 zcn 
 |-  ( M e. ZZ -> M e. CC )
48 abssq 
 |-  ( M e. CC -> ( ( abs ` M ) ^ 2 ) = ( abs ` ( M ^ 2 ) ) )
49 47 48 syl 
 |-  ( M e. ZZ -> ( ( abs ` M ) ^ 2 ) = ( abs ` ( M ^ 2 ) ) )
50 49 eqcomd 
 |-  ( M e. ZZ -> ( abs ` ( M ^ 2 ) ) = ( ( abs ` M ) ^ 2 ) )
51 50 adantr 
 |-  ( ( M e. ZZ /\ M =/= 0 ) -> ( abs ` ( M ^ 2 ) ) = ( ( abs ` M ) ^ 2 ) )
52 51 breq1d 
 |-  ( ( M e. ZZ /\ M =/= 0 ) -> ( ( abs ` ( M ^ 2 ) ) || ( N ^ 2 ) <-> ( ( abs ` M ) ^ 2 ) || ( N ^ 2 ) ) )
53 52 adantr 
 |-  ( ( ( M e. ZZ /\ M =/= 0 ) /\ N e. ZZ ) -> ( ( abs ` ( M ^ 2 ) ) || ( N ^ 2 ) <-> ( ( abs ` M ) ^ 2 ) || ( N ^ 2 ) ) )
54 46 53 bitrd 
 |-  ( ( ( M e. ZZ /\ M =/= 0 ) /\ N e. ZZ ) -> ( ( M ^ 2 ) || ( N ^ 2 ) <-> ( ( abs ` M ) ^ 2 ) || ( N ^ 2 ) ) )
55 40 42 54 3bitr4d 
 |-  ( ( ( M e. ZZ /\ M =/= 0 ) /\ N e. ZZ ) -> ( M || N <-> ( M ^ 2 ) || ( N ^ 2 ) ) )
56 55 an32s 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ M =/= 0 ) -> ( M || N <-> ( M ^ 2 ) || ( N ^ 2 ) ) )
57 0dvds 
 |-  ( N e. ZZ -> ( 0 || N <-> N = 0 ) )
58 sqeq0 
 |-  ( N e. CC -> ( ( N ^ 2 ) = 0 <-> N = 0 ) )
59 23 58 syl 
 |-  ( N e. ZZ -> ( ( N ^ 2 ) = 0 <-> N = 0 ) )
60 57 59 bitr4d 
 |-  ( N e. ZZ -> ( 0 || N <-> ( N ^ 2 ) = 0 ) )
61 0dvds 
 |-  ( ( N ^ 2 ) e. ZZ -> ( 0 || ( N ^ 2 ) <-> ( N ^ 2 ) = 0 ) )
62 19 61 syl 
 |-  ( N e. ZZ -> ( 0 || ( N ^ 2 ) <-> ( N ^ 2 ) = 0 ) )
63 60 62 bitr4d 
 |-  ( N e. ZZ -> ( 0 || N <-> 0 || ( N ^ 2 ) ) )
64 63 adantl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( 0 || N <-> 0 || ( N ^ 2 ) ) )
65 4 56 64 pm2.61ne 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> ( M ^ 2 ) || ( N ^ 2 ) ) )