Proof of Theorem lcmneg
| Step | Hyp | Ref
| Expression |
| 1 | | lcm0val 16631 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → (𝑁 lcm 0) = 0) |
| 2 | | znegcl 12652 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → -𝑁 ∈
ℤ) |
| 3 | | lcm0val 16631 |
. . . . . . . . 9
⊢ (-𝑁 ∈ ℤ → (-𝑁 lcm 0) = 0) |
| 4 | 2, 3 | syl 17 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → (-𝑁 lcm 0) = 0) |
| 5 | 1, 4 | eqtr4d 2780 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → (𝑁 lcm 0) = (-𝑁 lcm 0)) |
| 6 | 5 | ad2antlr 727 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (𝑁 lcm 0) = (-𝑁 lcm 0)) |
| 7 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑀 = 0 → (𝑁 lcm 𝑀) = (𝑁 lcm 0)) |
| 8 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑀 = 0 → (-𝑁 lcm 𝑀) = (-𝑁 lcm 0)) |
| 9 | 7, 8 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑀 = 0 → ((𝑁 lcm 𝑀) = (-𝑁 lcm 𝑀) ↔ (𝑁 lcm 0) = (-𝑁 lcm 0))) |
| 10 | 9 | adantl 481 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → ((𝑁 lcm 𝑀) = (-𝑁 lcm 𝑀) ↔ (𝑁 lcm 0) = (-𝑁 lcm 0))) |
| 11 | 6, 10 | mpbird 257 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (𝑁 lcm 𝑀) = (-𝑁 lcm 𝑀)) |
| 12 | | lcmcom 16630 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) = (𝑁 lcm 𝑀)) |
| 13 | | lcmcom 16630 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) = (-𝑁 lcm 𝑀)) |
| 14 | 2, 13 | sylan2 593 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) = (-𝑁 lcm 𝑀)) |
| 15 | 12, 14 | eqeq12d 2753 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 lcm 𝑁) = (𝑀 lcm -𝑁) ↔ (𝑁 lcm 𝑀) = (-𝑁 lcm 𝑀))) |
| 16 | 15 | adantr 480 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → ((𝑀 lcm 𝑁) = (𝑀 lcm -𝑁) ↔ (𝑁 lcm 𝑀) = (-𝑁 lcm 𝑀))) |
| 17 | 11, 16 | mpbird 257 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (𝑀 lcm 𝑁) = (𝑀 lcm -𝑁)) |
| 18 | | neg0 11555 |
. . . . . . . 8
⊢ -0 =
0 |
| 19 | 18 | oveq2i 7442 |
. . . . . . 7
⊢ (𝑀 lcm -0) = (𝑀 lcm 0) |
| 20 | 19 | eqcomi 2746 |
. . . . . 6
⊢ (𝑀 lcm 0) = (𝑀 lcm -0) |
| 21 | | oveq2 7439 |
. . . . . 6
⊢ (𝑁 = 0 → (𝑀 lcm 𝑁) = (𝑀 lcm 0)) |
| 22 | | negeq 11500 |
. . . . . . 7
⊢ (𝑁 = 0 → -𝑁 = -0) |
| 23 | 22 | oveq2d 7447 |
. . . . . 6
⊢ (𝑁 = 0 → (𝑀 lcm -𝑁) = (𝑀 lcm -0)) |
| 24 | 20, 21, 23 | 3eqtr4a 2803 |
. . . . 5
⊢ (𝑁 = 0 → (𝑀 lcm 𝑁) = (𝑀 lcm -𝑁)) |
| 25 | 24 | adantl 481 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (𝑀 lcm 𝑁) = (𝑀 lcm -𝑁)) |
| 26 | 17, 25 | jaodan 960 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm 𝑁) = (𝑀 lcm -𝑁)) |
| 27 | | dvdslcm 16635 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (𝑀 ∥ (𝑀 lcm -𝑁) ∧ -𝑁 ∥ (𝑀 lcm -𝑁))) |
| 28 | 2, 27 | sylan2 593 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ (𝑀 lcm -𝑁) ∧ -𝑁 ∥ (𝑀 lcm -𝑁))) |
| 29 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈
ℤ) |
| 30 | | lcmcl 16638 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) ∈
ℕ0) |
| 31 | 2, 30 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) ∈
ℕ0) |
| 32 | 31 | nn0zd 12639 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) ∈ ℤ) |
| 33 | | negdvdsb 16310 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ (𝑀 lcm -𝑁) ∈ ℤ) → (𝑁 ∥ (𝑀 lcm -𝑁) ↔ -𝑁 ∥ (𝑀 lcm -𝑁))) |
| 34 | 29, 32, 33 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∥ (𝑀 lcm -𝑁) ↔ -𝑁 ∥ (𝑀 lcm -𝑁))) |
| 35 | 34 | anbi2d 630 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 ∥ (𝑀 lcm -𝑁) ∧ 𝑁 ∥ (𝑀 lcm -𝑁)) ↔ (𝑀 ∥ (𝑀 lcm -𝑁) ∧ -𝑁 ∥ (𝑀 lcm -𝑁)))) |
| 36 | 28, 35 | mpbird 257 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ (𝑀 lcm -𝑁) ∧ 𝑁 ∥ (𝑀 lcm -𝑁))) |
| 37 | 36 | adantr 480 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 ∥ (𝑀 lcm -𝑁) ∧ 𝑁 ∥ (𝑀 lcm -𝑁))) |
| 38 | | zcn 12618 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
| 39 | 38 | negeq0d 11612 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → (𝑁 = 0 ↔ -𝑁 = 0)) |
| 40 | 39 | orbi2d 916 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → ((𝑀 = 0 ∨ 𝑁 = 0) ↔ (𝑀 = 0 ∨ -𝑁 = 0))) |
| 41 | 40 | notbid 318 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → (¬
(𝑀 = 0 ∨ 𝑁 = 0) ↔ ¬ (𝑀 = 0 ∨ -𝑁 = 0))) |
| 42 | 41 | biimpa 476 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → ¬ (𝑀 = 0 ∨ -𝑁 = 0)) |
| 43 | 42 | adantll 714 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → ¬ (𝑀 = 0 ∨ -𝑁 = 0)) |
| 44 | | lcmn0cl 16634 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ -𝑁 = 0)) → (𝑀 lcm -𝑁) ∈ ℕ) |
| 45 | 2, 44 | sylanl2 681 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ -𝑁 = 0)) → (𝑀 lcm -𝑁) ∈ ℕ) |
| 46 | 43, 45 | syldan 591 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm -𝑁) ∈ ℕ) |
| 47 | | simpl 482 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
| 48 | | 3anass 1095 |
. . . . . . 7
⊢ (((𝑀 lcm -𝑁) ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ ((𝑀 lcm -𝑁) ∈ ℕ ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) |
| 49 | 46, 47, 48 | sylanbrc 583 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → ((𝑀 lcm -𝑁) ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
| 50 | | simpr 484 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → ¬ (𝑀 = 0 ∨ 𝑁 = 0)) |
| 51 | | lcmledvds 16636 |
. . . . . 6
⊢ ((((𝑀 lcm -𝑁) ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → ((𝑀 ∥ (𝑀 lcm -𝑁) ∧ 𝑁 ∥ (𝑀 lcm -𝑁)) → (𝑀 lcm 𝑁) ≤ (𝑀 lcm -𝑁))) |
| 52 | 49, 50, 51 | syl2anc 584 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → ((𝑀 ∥ (𝑀 lcm -𝑁) ∧ 𝑁 ∥ (𝑀 lcm -𝑁)) → (𝑀 lcm 𝑁) ≤ (𝑀 lcm -𝑁))) |
| 53 | 37, 52 | mpd 15 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm 𝑁) ≤ (𝑀 lcm -𝑁)) |
| 54 | | dvdslcm 16635 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ (𝑀 lcm 𝑁) ∧ 𝑁 ∥ (𝑀 lcm 𝑁))) |
| 55 | 54 | adantr 480 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 ∥ (𝑀 lcm 𝑁) ∧ 𝑁 ∥ (𝑀 lcm 𝑁))) |
| 56 | | simplr 769 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → 𝑁 ∈ ℤ) |
| 57 | | lcmn0cl 16634 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm 𝑁) ∈ ℕ) |
| 58 | 57 | nnzd 12640 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm 𝑁) ∈ ℤ) |
| 59 | | negdvdsb 16310 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ (𝑀 lcm 𝑁) ∈ ℤ) → (𝑁 ∥ (𝑀 lcm 𝑁) ↔ -𝑁 ∥ (𝑀 lcm 𝑁))) |
| 60 | 56, 58, 59 | syl2anc 584 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → (𝑁 ∥ (𝑀 lcm 𝑁) ↔ -𝑁 ∥ (𝑀 lcm 𝑁))) |
| 61 | 60 | anbi2d 630 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ 𝑁 ∥ (𝑀 lcm 𝑁)) ↔ (𝑀 ∥ (𝑀 lcm 𝑁) ∧ -𝑁 ∥ (𝑀 lcm 𝑁)))) |
| 62 | | lcmledvds 16636 |
. . . . . . . . . 10
⊢ ((((𝑀 lcm 𝑁) ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ -𝑁 = 0)) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ -𝑁 ∥ (𝑀 lcm 𝑁)) → (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁))) |
| 63 | 62 | ex 412 |
. . . . . . . . 9
⊢ (((𝑀 lcm 𝑁) ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (¬ (𝑀 = 0 ∨ -𝑁 = 0) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ -𝑁 ∥ (𝑀 lcm 𝑁)) → (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁)))) |
| 64 | 2, 63 | syl3an3 1166 |
. . . . . . . 8
⊢ (((𝑀 lcm 𝑁) ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (𝑀 = 0 ∨ -𝑁 = 0) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ -𝑁 ∥ (𝑀 lcm 𝑁)) → (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁)))) |
| 65 | 64 | 3expib 1123 |
. . . . . . 7
⊢ ((𝑀 lcm 𝑁) ∈ ℕ → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (𝑀 = 0 ∨ -𝑁 = 0) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ -𝑁 ∥ (𝑀 lcm 𝑁)) → (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁))))) |
| 66 | 57, 47, 43, 65 | syl3c 66 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ -𝑁 ∥ (𝑀 lcm 𝑁)) → (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁))) |
| 67 | 61, 66 | sylbid 240 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ 𝑁 ∥ (𝑀 lcm 𝑁)) → (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁))) |
| 68 | 55, 67 | mpd 15 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁)) |
| 69 | | lcmcl 16638 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) ∈
ℕ0) |
| 70 | 69 | nn0red 12588 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) ∈ ℝ) |
| 71 | 30 | nn0red 12588 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) ∈ ℝ) |
| 72 | 2, 71 | sylan2 593 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) ∈ ℝ) |
| 73 | 70, 72 | letri3d 11403 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 lcm 𝑁) = (𝑀 lcm -𝑁) ↔ ((𝑀 lcm 𝑁) ≤ (𝑀 lcm -𝑁) ∧ (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁)))) |
| 74 | 73 | adantr 480 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → ((𝑀 lcm 𝑁) = (𝑀 lcm -𝑁) ↔ ((𝑀 lcm 𝑁) ≤ (𝑀 lcm -𝑁) ∧ (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁)))) |
| 75 | 53, 68, 74 | mpbir2and 713 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm 𝑁) = (𝑀 lcm -𝑁)) |
| 76 | 26, 75 | pm2.61dan 813 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) = (𝑀 lcm -𝑁)) |
| 77 | 76 | eqcomd 2743 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) = (𝑀 lcm 𝑁)) |