Proof of Theorem dvdssq
| Step | Hyp | Ref
| Expression |
| 1 | | breq1 5146 |
. . 3
⊢ (𝑀 = 0 → (𝑀 ∥ 𝑁 ↔ 0 ∥ 𝑁)) |
| 2 | | sq0i 14232 |
. . . 4
⊢ (𝑀 = 0 → (𝑀↑2) = 0) |
| 3 | 2 | breq1d 5153 |
. . 3
⊢ (𝑀 = 0 → ((𝑀↑2) ∥ (𝑁↑2) ↔ 0 ∥ (𝑁↑2))) |
| 4 | 1, 3 | bibi12d 345 |
. 2
⊢ (𝑀 = 0 → ((𝑀 ∥ 𝑁 ↔ (𝑀↑2) ∥ (𝑁↑2)) ↔ (0 ∥ 𝑁 ↔ 0 ∥ (𝑁↑2)))) |
| 5 | | nnabscl 15364 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → (abs‘𝑀) ∈
ℕ) |
| 6 | | breq2 5147 |
. . . . . . 7
⊢ (𝑁 = 0 → ((abs‘𝑀) ∥ 𝑁 ↔ (abs‘𝑀) ∥ 0)) |
| 7 | | sq0i 14232 |
. . . . . . . 8
⊢ (𝑁 = 0 → (𝑁↑2) = 0) |
| 8 | 7 | breq2d 5155 |
. . . . . . 7
⊢ (𝑁 = 0 → (((abs‘𝑀)↑2) ∥ (𝑁↑2) ↔
((abs‘𝑀)↑2)
∥ 0)) |
| 9 | 6, 8 | bibi12d 345 |
. . . . . 6
⊢ (𝑁 = 0 → (((abs‘𝑀) ∥ 𝑁 ↔ ((abs‘𝑀)↑2) ∥ (𝑁↑2)) ↔ ((abs‘𝑀) ∥ 0 ↔
((abs‘𝑀)↑2)
∥ 0))) |
| 10 | | nnabscl 15364 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈
ℕ) |
| 11 | | dvdssqlem 16603 |
. . . . . . . . 9
⊢
(((abs‘𝑀)
∈ ℕ ∧ (abs‘𝑁) ∈ ℕ) → ((abs‘𝑀) ∥ (abs‘𝑁) ↔ ((abs‘𝑀)↑2) ∥
((abs‘𝑁)↑2))) |
| 12 | 10, 11 | sylan2 593 |
. . . . . . . 8
⊢
(((abs‘𝑀)
∈ ℕ ∧ (𝑁
∈ ℤ ∧ 𝑁 ≠
0)) → ((abs‘𝑀)
∥ (abs‘𝑁)
↔ ((abs‘𝑀)↑2) ∥ ((abs‘𝑁)↑2))) |
| 13 | | nnz 12634 |
. . . . . . . . 9
⊢
((abs‘𝑀)
∈ ℕ → (abs‘𝑀) ∈ ℤ) |
| 14 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝑁 ∈
ℤ) |
| 15 | | dvdsabsb 16313 |
. . . . . . . . 9
⊢
(((abs‘𝑀)
∈ ℤ ∧ 𝑁
∈ ℤ) → ((abs‘𝑀) ∥ 𝑁 ↔ (abs‘𝑀) ∥ (abs‘𝑁))) |
| 16 | 13, 14, 15 | syl2an 596 |
. . . . . . . 8
⊢
(((abs‘𝑀)
∈ ℕ ∧ (𝑁
∈ ℤ ∧ 𝑁 ≠
0)) → ((abs‘𝑀)
∥ 𝑁 ↔
(abs‘𝑀) ∥
(abs‘𝑁))) |
| 17 | | nnsqcl 14168 |
. . . . . . . . . . 11
⊢
((abs‘𝑀)
∈ ℕ → ((abs‘𝑀)↑2) ∈ ℕ) |
| 18 | 17 | nnzd 12640 |
. . . . . . . . . 10
⊢
((abs‘𝑀)
∈ ℕ → ((abs‘𝑀)↑2) ∈ ℤ) |
| 19 | | zsqcl 14169 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → (𝑁↑2) ∈
ℤ) |
| 20 | 19 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑁↑2) ∈
ℤ) |
| 21 | | dvdsabsb 16313 |
. . . . . . . . . 10
⊢
((((abs‘𝑀)↑2) ∈ ℤ ∧ (𝑁↑2) ∈ ℤ) →
(((abs‘𝑀)↑2)
∥ (𝑁↑2) ↔
((abs‘𝑀)↑2)
∥ (abs‘(𝑁↑2)))) |
| 22 | 18, 20, 21 | syl2an 596 |
. . . . . . . . 9
⊢
(((abs‘𝑀)
∈ ℕ ∧ (𝑁
∈ ℤ ∧ 𝑁 ≠
0)) → (((abs‘𝑀)↑2) ∥ (𝑁↑2) ↔ ((abs‘𝑀)↑2) ∥
(abs‘(𝑁↑2)))) |
| 23 | | zcn 12618 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
| 24 | 23 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝑁 ∈
ℂ) |
| 25 | | abssq 15345 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℂ →
((abs‘𝑁)↑2) =
(abs‘(𝑁↑2))) |
| 26 | 24, 25 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) →
((abs‘𝑁)↑2) =
(abs‘(𝑁↑2))) |
| 27 | 26 | breq2d 5155 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) →
(((abs‘𝑀)↑2)
∥ ((abs‘𝑁)↑2) ↔ ((abs‘𝑀)↑2) ∥
(abs‘(𝑁↑2)))) |
| 28 | 27 | adantl 481 |
. . . . . . . . 9
⊢
(((abs‘𝑀)
∈ ℕ ∧ (𝑁
∈ ℤ ∧ 𝑁 ≠
0)) → (((abs‘𝑀)↑2) ∥ ((abs‘𝑁)↑2) ↔
((abs‘𝑀)↑2)
∥ (abs‘(𝑁↑2)))) |
| 29 | 22, 28 | bitr4d 282 |
. . . . . . . 8
⊢
(((abs‘𝑀)
∈ ℕ ∧ (𝑁
∈ ℤ ∧ 𝑁 ≠
0)) → (((abs‘𝑀)↑2) ∥ (𝑁↑2) ↔ ((abs‘𝑀)↑2) ∥
((abs‘𝑁)↑2))) |
| 30 | 12, 16, 29 | 3bitr4d 311 |
. . . . . . 7
⊢
(((abs‘𝑀)
∈ ℕ ∧ (𝑁
∈ ℤ ∧ 𝑁 ≠
0)) → ((abs‘𝑀)
∥ 𝑁 ↔
((abs‘𝑀)↑2)
∥ (𝑁↑2))) |
| 31 | 30 | anassrs 467 |
. . . . . 6
⊢
((((abs‘𝑀)
∈ ℕ ∧ 𝑁
∈ ℤ) ∧ 𝑁
≠ 0) → ((abs‘𝑀) ∥ 𝑁 ↔ ((abs‘𝑀)↑2) ∥ (𝑁↑2))) |
| 32 | | dvds0 16309 |
. . . . . . . . 9
⊢
((abs‘𝑀)
∈ ℤ → (abs‘𝑀) ∥ 0) |
| 33 | | zsqcl 14169 |
. . . . . . . . . 10
⊢
((abs‘𝑀)
∈ ℤ → ((abs‘𝑀)↑2) ∈ ℤ) |
| 34 | | dvds0 16309 |
. . . . . . . . . 10
⊢
(((abs‘𝑀)↑2) ∈ ℤ →
((abs‘𝑀)↑2)
∥ 0) |
| 35 | 33, 34 | syl 17 |
. . . . . . . . 9
⊢
((abs‘𝑀)
∈ ℤ → ((abs‘𝑀)↑2) ∥ 0) |
| 36 | 32, 35 | 2thd 265 |
. . . . . . . 8
⊢
((abs‘𝑀)
∈ ℤ → ((abs‘𝑀) ∥ 0 ↔ ((abs‘𝑀)↑2) ∥
0)) |
| 37 | 13, 36 | syl 17 |
. . . . . . 7
⊢
((abs‘𝑀)
∈ ℕ → ((abs‘𝑀) ∥ 0 ↔ ((abs‘𝑀)↑2) ∥
0)) |
| 38 | 37 | adantr 480 |
. . . . . 6
⊢
(((abs‘𝑀)
∈ ℕ ∧ 𝑁
∈ ℤ) → ((abs‘𝑀) ∥ 0 ↔ ((abs‘𝑀)↑2) ∥
0)) |
| 39 | 9, 31, 38 | pm2.61ne 3027 |
. . . . 5
⊢
(((abs‘𝑀)
∈ ℕ ∧ 𝑁
∈ ℤ) → ((abs‘𝑀) ∥ 𝑁 ↔ ((abs‘𝑀)↑2) ∥ (𝑁↑2))) |
| 40 | 5, 39 | sylan 580 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ 𝑁 ∈ ℤ) → ((abs‘𝑀) ∥ 𝑁 ↔ ((abs‘𝑀)↑2) ∥ (𝑁↑2))) |
| 41 | | absdvdsb 16312 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (abs‘𝑀) ∥ 𝑁)) |
| 42 | 41 | adantlr 715 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (abs‘𝑀) ∥ 𝑁)) |
| 43 | | zsqcl 14169 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → (𝑀↑2) ∈
ℤ) |
| 44 | 43 | adantr 480 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → (𝑀↑2) ∈
ℤ) |
| 45 | | absdvdsb 16312 |
. . . . . 6
⊢ (((𝑀↑2) ∈ ℤ ∧
(𝑁↑2) ∈ ℤ)
→ ((𝑀↑2) ∥
(𝑁↑2) ↔
(abs‘(𝑀↑2))
∥ (𝑁↑2))) |
| 46 | 44, 19, 45 | syl2an 596 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ 𝑁 ∈ ℤ) → ((𝑀↑2) ∥ (𝑁↑2) ↔ (abs‘(𝑀↑2)) ∥ (𝑁↑2))) |
| 47 | | zcn 12618 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
| 48 | | abssq 15345 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℂ →
((abs‘𝑀)↑2) =
(abs‘(𝑀↑2))) |
| 49 | 47, 48 | syl 17 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℤ →
((abs‘𝑀)↑2) =
(abs‘(𝑀↑2))) |
| 50 | 49 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ →
(abs‘(𝑀↑2)) =
((abs‘𝑀)↑2)) |
| 51 | 50 | adantr 480 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) →
(abs‘(𝑀↑2)) =
((abs‘𝑀)↑2)) |
| 52 | 51 | breq1d 5153 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) →
((abs‘(𝑀↑2))
∥ (𝑁↑2) ↔
((abs‘𝑀)↑2)
∥ (𝑁↑2))) |
| 53 | 52 | adantr 480 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ 𝑁 ∈ ℤ) → ((abs‘(𝑀↑2)) ∥ (𝑁↑2) ↔
((abs‘𝑀)↑2)
∥ (𝑁↑2))) |
| 54 | 46, 53 | bitrd 279 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ 𝑁 ∈ ℤ) → ((𝑀↑2) ∥ (𝑁↑2) ↔ ((abs‘𝑀)↑2) ∥ (𝑁↑2))) |
| 55 | 40, 42, 54 | 3bitr4d 311 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (𝑀↑2) ∥ (𝑁↑2))) |
| 56 | 55 | an32s 652 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑀 ∥ 𝑁 ↔ (𝑀↑2) ∥ (𝑁↑2))) |
| 57 | | 0dvds 16314 |
. . . . 5
⊢ (𝑁 ∈ ℤ → (0
∥ 𝑁 ↔ 𝑁 = 0)) |
| 58 | | sqeq0 14160 |
. . . . . 6
⊢ (𝑁 ∈ ℂ → ((𝑁↑2) = 0 ↔ 𝑁 = 0)) |
| 59 | 23, 58 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ ℤ → ((𝑁↑2) = 0 ↔ 𝑁 = 0)) |
| 60 | 57, 59 | bitr4d 282 |
. . . 4
⊢ (𝑁 ∈ ℤ → (0
∥ 𝑁 ↔ (𝑁↑2) = 0)) |
| 61 | | 0dvds 16314 |
. . . . 5
⊢ ((𝑁↑2) ∈ ℤ →
(0 ∥ (𝑁↑2)
↔ (𝑁↑2) =
0)) |
| 62 | 19, 61 | syl 17 |
. . . 4
⊢ (𝑁 ∈ ℤ → (0
∥ (𝑁↑2) ↔
(𝑁↑2) =
0)) |
| 63 | 60, 62 | bitr4d 282 |
. . 3
⊢ (𝑁 ∈ ℤ → (0
∥ 𝑁 ↔ 0 ∥
(𝑁↑2))) |
| 64 | 63 | adantl 481 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0
∥ 𝑁 ↔ 0 ∥
(𝑁↑2))) |
| 65 | 4, 56, 64 | pm2.61ne 3027 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (𝑀↑2) ∥ (𝑁↑2))) |