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 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝑀 ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝑀 = 0 → ( 𝑀 ∥ 𝑁 ↔ 0 ∥ 𝑁 ) )
2 sq0i ⊢ ( 𝑀 = 0 → ( 𝑀 ↑ 2 ) = 0 )
3 2 breq1d ⊢ ( 𝑀 = 0 → ( ( 𝑀 ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ↔ 0 ∥ ( 𝑁 ↑ 2 ) ) )
4 1 3 bibi12d ⊢ ( 𝑀 = 0 → ( ( 𝑀 ∥ 𝑁 ↔ ( 𝑀 ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) ↔ ( 0 ∥ 𝑁 ↔ 0 ∥ ( 𝑁 ↑ 2 ) ) ) )
5 nnabscl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) → ( abs ‘ 𝑀 ) ∈ ℕ )
6 breq2 ⊢ ( 𝑁 = 0 → ( ( abs ‘ 𝑀 ) ∥ 𝑁 ↔ ( abs ‘ 𝑀 ) ∥ 0 ) )
7 sq0i ⊢ ( 𝑁 = 0 → ( 𝑁 ↑ 2 ) = 0 )
8 7 breq2d ⊢ ( 𝑁 = 0 → ( ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ↔ ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ 0 ) )
9 6 8 bibi12d ⊢ ( 𝑁 = 0 → ( ( ( abs ‘ 𝑀 ) ∥ 𝑁 ↔ ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) ↔ ( ( abs ‘ 𝑀 ) ∥ 0 ↔ ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ 0 ) ) )
10 nnabscl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( abs ‘ 𝑁 ) ∈ ℕ )
11 dvdssqlem ⊢ ( ( ( abs ‘ 𝑀 ) ∈ ℕ ∧ ( abs ‘ 𝑁 ) ∈ ℕ ) → ( ( abs ‘ 𝑀 ) ∥ ( abs ‘ 𝑁 ) ↔ ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ ( ( abs ‘ 𝑁 ) ↑ 2 ) ) )
12 10 11 sylan2 ⊢ ( ( ( abs ‘ 𝑀 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( abs ‘ 𝑀 ) ∥ ( abs ‘ 𝑁 ) ↔ ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ ( ( abs ‘ 𝑁 ) ↑ 2 ) ) )
13 nnz ⊢ ( ( abs ‘ 𝑀 ) ∈ ℕ → ( abs ‘ 𝑀 ) ∈ ℤ )
14 simpl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → 𝑁 ∈ ℤ )
15 dvdsabsb ⊢ ( ( ( abs ‘ 𝑀 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) ∥ 𝑁 ↔ ( abs ‘ 𝑀 ) ∥ ( abs ‘ 𝑁 ) ) )
16 13 14 15 syl2an ⊢ ( ( ( abs ‘ 𝑀 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( abs ‘ 𝑀 ) ∥ 𝑁 ↔ ( abs ‘ 𝑀 ) ∥ ( abs ‘ 𝑁 ) ) )
17 nnsqcl ⊢ ( ( abs ‘ 𝑀 ) ∈ ℕ → ( ( abs ‘ 𝑀 ) ↑ 2 ) ∈ ℕ )
18 17 nnzd ⊢ ( ( abs ‘ 𝑀 ) ∈ ℕ → ( ( abs ‘ 𝑀 ) ↑ 2 ) ∈ ℤ )
19 zsqcl ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ↑ 2 ) ∈ ℤ )
20 19 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝑁 ↑ 2 ) ∈ ℤ )
21 dvdsabsb ⊢ ( ( ( ( abs ‘ 𝑀 ) ↑ 2 ) ∈ ℤ ∧ ( 𝑁 ↑ 2 ) ∈ ℤ ) → ( ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ↔ ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ ( abs ‘ ( 𝑁 ↑ 2 ) ) ) )
22 18 20 21 syl2an ⊢ ( ( ( abs ‘ 𝑀 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ↔ ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ ( abs ‘ ( 𝑁 ↑ 2 ) ) ) )
23 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
24 23 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → 𝑁 ∈ ℂ )
25 abssq ⊢ ( 𝑁 ∈ ℂ → ( ( abs ‘ 𝑁 ) ↑ 2 ) = ( abs ‘ ( 𝑁 ↑ 2 ) ) )
26 24 25 syl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( ( abs ‘ 𝑁 ) ↑ 2 ) = ( abs ‘ ( 𝑁 ↑ 2 ) ) )
27 26 breq2d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ ( ( abs ‘ 𝑁 ) ↑ 2 ) ↔ ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ ( abs ‘ ( 𝑁 ↑ 2 ) ) ) )
28 27 adantl ⊢ ( ( ( abs ‘ 𝑀 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ ( ( abs ‘ 𝑁 ) ↑ 2 ) ↔ ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ ( abs ‘ ( 𝑁 ↑ 2 ) ) ) )
29 22 28 bitr4d ⊢ ( ( ( abs ‘ 𝑀 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ↔ ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ ( ( abs ‘ 𝑁 ) ↑ 2 ) ) )
30 12 16 29 3bitr4d ⊢ ( ( ( abs ‘ 𝑀 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( abs ‘ 𝑀 ) ∥ 𝑁 ↔ ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )
31 30 anassrs ⊢ ( ( ( ( abs ‘ 𝑀 ) ∈ ℕ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≠ 0 ) → ( ( abs ‘ 𝑀 ) ∥ 𝑁 ↔ ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )
32 dvds0 ⊢ ( ( abs ‘ 𝑀 ) ∈ ℤ → ( abs ‘ 𝑀 ) ∥ 0 )
33 zsqcl ⊢ ( ( abs ‘ 𝑀 ) ∈ ℤ → ( ( abs ‘ 𝑀 ) ↑ 2 ) ∈ ℤ )
34 dvds0 ⊢ ( ( ( abs ‘ 𝑀 ) ↑ 2 ) ∈ ℤ → ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ 0 )
35 33 34 syl ⊢ ( ( abs ‘ 𝑀 ) ∈ ℤ → ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ 0 )
36 32 35 2thd ⊢ ( ( abs ‘ 𝑀 ) ∈ ℤ → ( ( abs ‘ 𝑀 ) ∥ 0 ↔ ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ 0 ) )
37 13 36 syl ⊢ ( ( abs ‘ 𝑀 ) ∈ ℕ → ( ( abs ‘ 𝑀 ) ∥ 0 ↔ ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ 0 ) )
38 37 adantr ⊢ ( ( ( abs ‘ 𝑀 ) ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) ∥ 0 ↔ ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ 0 ) )
39 9 31 38 pm2.61ne ⊢ ( ( ( abs ‘ 𝑀 ) ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) ∥ 𝑁 ↔ ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )
40 5 39 sylan ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) ∥ 𝑁 ↔ ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )
41 absdvdsb ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ( abs ‘ 𝑀 ) ∥ 𝑁 ) )
42 41 adantlr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ( abs ‘ 𝑀 ) ∥ 𝑁 ) )
43 zsqcl ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ↑ 2 ) ∈ ℤ )
44 43 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) → ( 𝑀 ↑ 2 ) ∈ ℤ )
45 absdvdsb ⊢ ( ( ( 𝑀 ↑ 2 ) ∈ ℤ ∧ ( 𝑁 ↑ 2 ) ∈ ℤ ) → ( ( 𝑀 ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ↔ ( abs ‘ ( 𝑀 ↑ 2 ) ) ∥ ( 𝑁 ↑ 2 ) ) )
46 44 19 45 syl2an ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ↔ ( abs ‘ ( 𝑀 ↑ 2 ) ) ∥ ( 𝑁 ↑ 2 ) ) )
47 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
48 abssq ⊢ ( 𝑀 ∈ ℂ → ( ( abs ‘ 𝑀 ) ↑ 2 ) = ( abs ‘ ( 𝑀 ↑ 2 ) ) )
49 47 48 syl ⊢ ( 𝑀 ∈ ℤ → ( ( abs ‘ 𝑀 ) ↑ 2 ) = ( abs ‘ ( 𝑀 ↑ 2 ) ) )
50 49 eqcomd ⊢ ( 𝑀 ∈ ℤ → ( abs ‘ ( 𝑀 ↑ 2 ) ) = ( ( abs ‘ 𝑀 ) ↑ 2 ) )
51 50 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) → ( abs ‘ ( 𝑀 ↑ 2 ) ) = ( ( abs ‘ 𝑀 ) ↑ 2 ) )
52 51 breq1d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) → ( ( abs ‘ ( 𝑀 ↑ 2 ) ) ∥ ( 𝑁 ↑ 2 ) ↔ ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )
53 52 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ ( 𝑀 ↑ 2 ) ) ∥ ( 𝑁 ↑ 2 ) ↔ ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )
54 46 53 bitrd ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ↔ ( ( abs ‘ 𝑀 ) ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )
55 40 42 54 3bitr4d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝑀 ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )
56 55 an32s ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝑀 ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )
57 0dvds ⊢ ( 𝑁 ∈ ℤ → ( 0 ∥ 𝑁 ↔ 𝑁 = 0 ) )
58 sqeq0 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 ↑ 2 ) = 0 ↔ 𝑁 = 0 ) )
59 23 58 syl ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 ↑ 2 ) = 0 ↔ 𝑁 = 0 ) )
60 57 59 bitr4d ⊢ ( 𝑁 ∈ ℤ → ( 0 ∥ 𝑁 ↔ ( 𝑁 ↑ 2 ) = 0 ) )
61 0dvds ⊢ ( ( 𝑁 ↑ 2 ) ∈ ℤ → ( 0 ∥ ( 𝑁 ↑ 2 ) ↔ ( 𝑁 ↑ 2 ) = 0 ) )
62 19 61 syl ⊢ ( 𝑁 ∈ ℤ → ( 0 ∥ ( 𝑁 ↑ 2 ) ↔ ( 𝑁 ↑ 2 ) = 0 ) )
63 60 62 bitr4d ⊢ ( 𝑁 ∈ ℤ → ( 0 ∥ 𝑁 ↔ 0 ∥ ( 𝑁 ↑ 2 ) ) )
64 63 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 ∥ 𝑁 ↔ 0 ∥ ( 𝑁 ↑ 2 ) ) )
65 4 56 64 pm2.61ne ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝑀 ↑ 2 ) ∥ ( 𝑁 ↑ 2 ) ) )