# 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 )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) ) ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( M e. ZZ /\ M =/= 0 ) /\ N e. ZZ ) -> ( M || N <-> ( abs ` M ) || N ) )`
43 zsqcl
` |-  ( M e. ZZ -> ( M ^ 2 ) e. ZZ )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( 0 || N <-> 0 || ( N ^ 2 ) ) )`
` |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> ( M ^ 2 ) || ( N ^ 2 ) ) )`