Proof of Theorem dvdsabseq
| Step | Hyp | Ref
| Expression |
| 1 | | dvdszrcl 16295 |
. . 3
⊢ (𝑀 ∥ 𝑁 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
| 2 | | simpr 484 |
. . . . . 6
⊢ ((𝑀 ∥ 𝑁 ∧ 𝑁 ∥ 𝑀) → 𝑁 ∥ 𝑀) |
| 3 | | breq1 5146 |
. . . . . . . 8
⊢ (𝑁 = 0 → (𝑁 ∥ 𝑀 ↔ 0 ∥ 𝑀)) |
| 4 | | 0dvds 16314 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → (0
∥ 𝑀 ↔ 𝑀 = 0)) |
| 5 | 4 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0
∥ 𝑀 ↔ 𝑀 = 0)) |
| 6 | | zcn 12618 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
| 7 | 6 | abs00ad 15329 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℤ →
((abs‘𝑀) = 0 ↔
𝑀 = 0)) |
| 8 | 7 | bicomd 223 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → (𝑀 = 0 ↔ (abs‘𝑀) = 0)) |
| 9 | 8 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 = 0 ↔ (abs‘𝑀) = 0)) |
| 10 | 5, 9 | bitrd 279 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0
∥ 𝑀 ↔
(abs‘𝑀) =
0)) |
| 11 | 3, 10 | sylan9bb 509 |
. . . . . . 7
⊢ ((𝑁 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑁 ∥ 𝑀 ↔ (abs‘𝑀) = 0)) |
| 12 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑁 = 0 → (abs‘𝑁) =
(abs‘0)) |
| 13 | | abs0 15324 |
. . . . . . . . . 10
⊢
(abs‘0) = 0 |
| 14 | 12, 13 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝑁 = 0 → (abs‘𝑁) = 0) |
| 15 | 14 | adantr 480 |
. . . . . . . 8
⊢ ((𝑁 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (abs‘𝑁) = 0) |
| 16 | 15 | eqeq2d 2748 |
. . . . . . 7
⊢ ((𝑁 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((abs‘𝑀) = (abs‘𝑁) ↔ (abs‘𝑀) = 0)) |
| 17 | 11, 16 | bitr4d 282 |
. . . . . 6
⊢ ((𝑁 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑁 ∥ 𝑀 ↔ (abs‘𝑀) = (abs‘𝑁))) |
| 18 | 2, 17 | imbitrid 244 |
. . . . 5
⊢ ((𝑁 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑀 ∥ 𝑁 ∧ 𝑁 ∥ 𝑀) → (abs‘𝑀) = (abs‘𝑁))) |
| 19 | 18 | expd 415 |
. . . 4
⊢ ((𝑁 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑀 ∥ 𝑁 → (𝑁 ∥ 𝑀 → (abs‘𝑀) = (abs‘𝑁)))) |
| 20 | | simprl 771 |
. . . . . 6
⊢ ((¬
𝑁 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑀 ∈
ℤ) |
| 21 | | simpr 484 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈
ℤ) |
| 22 | 21 | adantl 481 |
. . . . . 6
⊢ ((¬
𝑁 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈
ℤ) |
| 23 | | neqne 2948 |
. . . . . . 7
⊢ (¬
𝑁 = 0 → 𝑁 ≠ 0) |
| 24 | 23 | adantr 480 |
. . . . . 6
⊢ ((¬
𝑁 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ≠ 0) |
| 25 | | dvdsleabs2 16349 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑀 ∥ 𝑁 → (abs‘𝑀) ≤ (abs‘𝑁))) |
| 26 | 20, 22, 24, 25 | syl3anc 1373 |
. . . . 5
⊢ ((¬
𝑁 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑀 ∥ 𝑁 → (abs‘𝑀) ≤ (abs‘𝑁))) |
| 27 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑁 ∥ 𝑀 ∧ 𝑀 ∥ 𝑁) → 𝑀 ∥ 𝑁) |
| 28 | | breq1 5146 |
. . . . . . . . . . . . 13
⊢ (𝑀 = 0 → (𝑀 ∥ 𝑁 ↔ 0 ∥ 𝑁)) |
| 29 | | 0dvds 16314 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℤ → (0
∥ 𝑁 ↔ 𝑁 = 0)) |
| 30 | | zcn 12618 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
| 31 | 30 | abs00ad 15329 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℤ →
((abs‘𝑁) = 0 ↔
𝑁 = 0)) |
| 32 | | eqcom 2744 |
. . . . . . . . . . . . . . . 16
⊢
((abs‘𝑁) = 0
↔ 0 = (abs‘𝑁)) |
| 33 | 31, 32 | bitr3di 286 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℤ → (𝑁 = 0 ↔ 0 = (abs‘𝑁))) |
| 34 | 29, 33 | bitrd 279 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℤ → (0
∥ 𝑁 ↔ 0 =
(abs‘𝑁))) |
| 35 | 34 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0
∥ 𝑁 ↔ 0 =
(abs‘𝑁))) |
| 36 | 28, 35 | sylan9bb 509 |
. . . . . . . . . . . 12
⊢ ((𝑀 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑀 ∥ 𝑁 ↔ 0 = (abs‘𝑁))) |
| 37 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 = 0 → (abs‘𝑀) =
(abs‘0)) |
| 38 | 37, 13 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
⊢ (𝑀 = 0 → (abs‘𝑀) = 0) |
| 39 | 38 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑀 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (abs‘𝑀) = 0) |
| 40 | 39 | eqeq1d 2739 |
. . . . . . . . . . . 12
⊢ ((𝑀 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((abs‘𝑀) = (abs‘𝑁) ↔ 0 = (abs‘𝑁))) |
| 41 | 36, 40 | bitr4d 282 |
. . . . . . . . . . 11
⊢ ((𝑀 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑀 ∥ 𝑁 ↔ (abs‘𝑀) = (abs‘𝑁))) |
| 42 | 27, 41 | imbitrid 244 |
. . . . . . . . . 10
⊢ ((𝑀 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 ∥ 𝑀 ∧ 𝑀 ∥ 𝑁) → (abs‘𝑀) = (abs‘𝑁))) |
| 43 | 42 | a1dd 50 |
. . . . . . . . 9
⊢ ((𝑀 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 ∥ 𝑀 ∧ 𝑀 ∥ 𝑁) → ((abs‘𝑀) ≤ (abs‘𝑁) → (abs‘𝑀) = (abs‘𝑁)))) |
| 44 | 43 | expcomd 416 |
. . . . . . . 8
⊢ ((𝑀 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑀 ∥ 𝑁 → (𝑁 ∥ 𝑀 → ((abs‘𝑀) ≤ (abs‘𝑁) → (abs‘𝑀) = (abs‘𝑁))))) |
| 45 | 21 | adantl 481 |
. . . . . . . . . . 11
⊢ ((¬
𝑀 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈
ℤ) |
| 46 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((¬
𝑀 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑀 ∈
ℤ) |
| 47 | | neqne 2948 |
. . . . . . . . . . . 12
⊢ (¬
𝑀 = 0 → 𝑀 ≠ 0) |
| 48 | 47 | adantr 480 |
. . . . . . . . . . 11
⊢ ((¬
𝑀 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑀 ≠ 0) |
| 49 | | dvdsleabs2 16349 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → (𝑁 ∥ 𝑀 → (abs‘𝑁) ≤ (abs‘𝑀))) |
| 50 | 45, 46, 48, 49 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((¬
𝑀 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑁 ∥ 𝑀 → (abs‘𝑁) ≤ (abs‘𝑀))) |
| 51 | | eqcom 2744 |
. . . . . . . . . . . . . 14
⊢
((abs‘𝑀) =
(abs‘𝑁) ↔
(abs‘𝑁) =
(abs‘𝑀)) |
| 52 | 30 | abscld 15475 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℤ →
(abs‘𝑁) ∈
ℝ) |
| 53 | 6 | abscld 15475 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℤ →
(abs‘𝑀) ∈
ℝ) |
| 54 | | letri3 11346 |
. . . . . . . . . . . . . . 15
⊢
(((abs‘𝑁)
∈ ℝ ∧ (abs‘𝑀) ∈ ℝ) → ((abs‘𝑁) = (abs‘𝑀) ↔ ((abs‘𝑁) ≤ (abs‘𝑀) ∧ (abs‘𝑀) ≤ (abs‘𝑁)))) |
| 55 | 52, 53, 54 | syl2anr 597 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((abs‘𝑁) =
(abs‘𝑀) ↔
((abs‘𝑁) ≤
(abs‘𝑀) ∧
(abs‘𝑀) ≤
(abs‘𝑁)))) |
| 56 | 51, 55 | bitrid 283 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((abs‘𝑀) =
(abs‘𝑁) ↔
((abs‘𝑁) ≤
(abs‘𝑀) ∧
(abs‘𝑀) ≤
(abs‘𝑁)))) |
| 57 | 56 | biimprd 248 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(((abs‘𝑁) ≤
(abs‘𝑀) ∧
(abs‘𝑀) ≤
(abs‘𝑁)) →
(abs‘𝑀) =
(abs‘𝑁))) |
| 58 | 57 | expd 415 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((abs‘𝑁) ≤
(abs‘𝑀) →
((abs‘𝑀) ≤
(abs‘𝑁) →
(abs‘𝑀) =
(abs‘𝑁)))) |
| 59 | 58 | adantl 481 |
. . . . . . . . . 10
⊢ ((¬
𝑀 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) →
((abs‘𝑁) ≤
(abs‘𝑀) →
((abs‘𝑀) ≤
(abs‘𝑁) →
(abs‘𝑀) =
(abs‘𝑁)))) |
| 60 | 50, 59 | syld 47 |
. . . . . . . . 9
⊢ ((¬
𝑀 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑁 ∥ 𝑀 → ((abs‘𝑀) ≤ (abs‘𝑁) → (abs‘𝑀) = (abs‘𝑁)))) |
| 61 | 60 | a1d 25 |
. . . . . . . 8
⊢ ((¬
𝑀 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑀 ∥ 𝑁 → (𝑁 ∥ 𝑀 → ((abs‘𝑀) ≤ (abs‘𝑁) → (abs‘𝑀) = (abs‘𝑁))))) |
| 62 | 44, 61 | pm2.61ian 812 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 → (𝑁 ∥ 𝑀 → ((abs‘𝑀) ≤ (abs‘𝑁) → (abs‘𝑀) = (abs‘𝑁))))) |
| 63 | 62 | com34 91 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 → ((abs‘𝑀) ≤ (abs‘𝑁) → (𝑁 ∥ 𝑀 → (abs‘𝑀) = (abs‘𝑁))))) |
| 64 | 63 | adantl 481 |
. . . . 5
⊢ ((¬
𝑁 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑀 ∥ 𝑁 → ((abs‘𝑀) ≤ (abs‘𝑁) → (𝑁 ∥ 𝑀 → (abs‘𝑀) = (abs‘𝑁))))) |
| 65 | 26, 64 | mpdd 43 |
. . . 4
⊢ ((¬
𝑁 = 0 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑀 ∥ 𝑁 → (𝑁 ∥ 𝑀 → (abs‘𝑀) = (abs‘𝑁)))) |
| 66 | 19, 65 | pm2.61ian 812 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 → (𝑁 ∥ 𝑀 → (abs‘𝑀) = (abs‘𝑁)))) |
| 67 | 1, 66 | mpcom 38 |
. 2
⊢ (𝑀 ∥ 𝑁 → (𝑁 ∥ 𝑀 → (abs‘𝑀) = (abs‘𝑁))) |
| 68 | 67 | imp 406 |
1
⊢ ((𝑀 ∥ 𝑁 ∧ 𝑁 ∥ 𝑀) → (abs‘𝑀) = (abs‘𝑁)) |