Proof of Theorem lcmdvds
Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . 6
⊢ (0
∥ 𝐾 → 0 ∥
𝐾) |
2 | | breq1 5071 |
. . . . . . . 8
⊢ (𝑀 = 0 → (𝑀 ∥ 𝐾 ↔ 0 ∥ 𝐾)) |
3 | 2 | adantl 485 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 = 0) → (𝑀 ∥ 𝐾 ↔ 0 ∥ 𝐾)) |
4 | | oveq1 7239 |
. . . . . . . . 9
⊢ (𝑀 = 0 → (𝑀 lcm 𝑁) = (0 lcm 𝑁)) |
5 | | 0z 12212 |
. . . . . . . . . . 11
⊢ 0 ∈
ℤ |
6 | | lcmcom 16178 |
. . . . . . . . . . 11
⊢ ((0
∈ ℤ ∧ 𝑁
∈ ℤ) → (0 lcm 𝑁) = (𝑁 lcm 0)) |
7 | 5, 6 | mpan 690 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → (0 lcm
𝑁) = (𝑁 lcm 0)) |
8 | | lcm0val 16179 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → (𝑁 lcm 0) = 0) |
9 | 7, 8 | eqtrd 2778 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → (0 lcm
𝑁) = 0) |
10 | 4, 9 | sylan9eqr 2801 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 = 0) → (𝑀 lcm 𝑁) = 0) |
11 | 10 | breq1d 5078 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 = 0) → ((𝑀 lcm 𝑁) ∥ 𝐾 ↔ 0 ∥ 𝐾)) |
12 | 3, 11 | imbi12d 348 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 = 0) → ((𝑀 ∥ 𝐾 → (𝑀 lcm 𝑁) ∥ 𝐾) ↔ (0 ∥ 𝐾 → 0 ∥ 𝐾))) |
13 | 1, 12 | mpbiri 261 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 = 0) → (𝑀 ∥ 𝐾 → (𝑀 lcm 𝑁) ∥ 𝐾)) |
14 | 13 | 3ad2antl3 1189 |
. . . 4
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (𝑀 ∥ 𝐾 → (𝑀 lcm 𝑁) ∥ 𝐾)) |
15 | 14 | adantrd 495 |
. . 3
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾)) |
16 | 15 | ex 416 |
. 2
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 = 0 → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾))) |
17 | | breq1 5071 |
. . . . . . . 8
⊢ (𝑁 = 0 → (𝑁 ∥ 𝐾 ↔ 0 ∥ 𝐾)) |
18 | 17 | adantl 485 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = 0) → (𝑁 ∥ 𝐾 ↔ 0 ∥ 𝐾)) |
19 | | oveq2 7240 |
. . . . . . . . 9
⊢ (𝑁 = 0 → (𝑀 lcm 𝑁) = (𝑀 lcm 0)) |
20 | | lcm0val 16179 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℤ → (𝑀 lcm 0) = 0) |
21 | 19, 20 | sylan9eqr 2801 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = 0) → (𝑀 lcm 𝑁) = 0) |
22 | 21 | breq1d 5078 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = 0) → ((𝑀 lcm 𝑁) ∥ 𝐾 ↔ 0 ∥ 𝐾)) |
23 | 18, 22 | imbi12d 348 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = 0) → ((𝑁 ∥ 𝐾 → (𝑀 lcm 𝑁) ∥ 𝐾) ↔ (0 ∥ 𝐾 → 0 ∥ 𝐾))) |
24 | 1, 23 | mpbiri 261 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = 0) → (𝑁 ∥ 𝐾 → (𝑀 lcm 𝑁) ∥ 𝐾)) |
25 | 24 | 3ad2antl2 1188 |
. . . 4
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (𝑁 ∥ 𝐾 → (𝑀 lcm 𝑁) ∥ 𝐾)) |
26 | 25 | adantld 494 |
. . 3
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾)) |
27 | 26 | ex 416 |
. 2
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 = 0 → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾))) |
28 | | neanior 3035 |
. . . . . 6
⊢ ((𝑀 ≠ 0 ∧ 𝑁 ≠ 0) ↔ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) |
29 | | lcmcl 16186 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) ∈
ℕ0) |
30 | 29 | nn0zd 12305 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) ∈ ℤ) |
31 | | dvds0 15861 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 lcm 𝑁) ∈ ℤ → (𝑀 lcm 𝑁) ∥ 0) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) ∥ 0) |
33 | 32 | a1d 25 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 ∥ 0 ∧ 𝑁 ∥ 0) → (𝑀 lcm 𝑁) ∥ 0)) |
34 | 33 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 = 0) → ((𝑀 ∥ 0 ∧ 𝑁 ∥ 0) → (𝑀 lcm 𝑁) ∥ 0)) |
35 | | breq2 5072 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 = 0 → (𝑀 ∥ 𝐾 ↔ 𝑀 ∥ 0)) |
36 | | breq2 5072 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 = 0 → (𝑁 ∥ 𝐾 ↔ 𝑁 ∥ 0)) |
37 | 35, 36 | anbi12d 634 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 = 0 → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) ↔ (𝑀 ∥ 0 ∧ 𝑁 ∥ 0))) |
38 | | breq2 5072 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 = 0 → ((𝑀 lcm 𝑁) ∥ 𝐾 ↔ (𝑀 lcm 𝑁) ∥ 0)) |
39 | 37, 38 | imbi12d 348 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 = 0 → (((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾) ↔ ((𝑀 ∥ 0 ∧ 𝑁 ∥ 0) → (𝑀 lcm 𝑁) ∥ 0))) |
40 | 39 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 = 0) → (((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾) ↔ ((𝑀 ∥ 0 ∧ 𝑁 ∥ 0) → (𝑀 lcm 𝑁) ∥ 0))) |
41 | 34, 40 | mpbird 260 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 = 0) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾)) |
42 | 41 | adantrl 716 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐾 = 0)) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾)) |
43 | 42 | adantllr 719 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐾 = 0)) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾)) |
44 | 43 | adantlrr 721 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝐾 ∈ ℤ ∧ 𝐾 = 0)) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾)) |
45 | 44 | anassrs 471 |
. . . . . . . . 9
⊢
(((((𝑀 ∈
ℤ ∧ 𝑀 ≠ 0)
∧ (𝑁 ∈ ℤ
∧ 𝑁 ≠ 0)) ∧
𝐾 ∈ ℤ) ∧
𝐾 = 0) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾)) |
46 | | nnabscl 14917 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → (abs‘𝑀) ∈
ℕ) |
47 | | nnabscl 14917 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈
ℕ) |
48 | | nnabscl 14917 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℤ ∧ 𝐾 ≠ 0) → (abs‘𝐾) ∈
ℕ) |
49 | | lcmgcdlem 16191 |
. . . . . . . . . . . . . . 15
⊢
(((abs‘𝑀)
∈ ℕ ∧ (abs‘𝑁) ∈ ℕ) → ((((abs‘𝑀) lcm (abs‘𝑁)) · ((abs‘𝑀) gcd (abs‘𝑁))) =
(abs‘((abs‘𝑀)
· (abs‘𝑁)))
∧ (((abs‘𝐾)
∈ ℕ ∧ ((abs‘𝑀) ∥ (abs‘𝐾) ∧ (abs‘𝑁) ∥ (abs‘𝐾))) → ((abs‘𝑀) lcm (abs‘𝑁)) ∥ (abs‘𝐾)))) |
50 | 49 | simprd 499 |
. . . . . . . . . . . . . 14
⊢
(((abs‘𝑀)
∈ ℕ ∧ (abs‘𝑁) ∈ ℕ) → (((abs‘𝐾) ∈ ℕ ∧
((abs‘𝑀) ∥
(abs‘𝐾) ∧
(abs‘𝑁) ∥
(abs‘𝐾))) →
((abs‘𝑀) lcm
(abs‘𝑁)) ∥
(abs‘𝐾))) |
51 | 48, 50 | sylani 607 |
. . . . . . . . . . . . 13
⊢
(((abs‘𝑀)
∈ ℕ ∧ (abs‘𝑁) ∈ ℕ) → (((𝐾 ∈ ℤ ∧ 𝐾 ≠ 0) ∧ ((abs‘𝑀) ∥ (abs‘𝐾) ∧ (abs‘𝑁) ∥ (abs‘𝐾))) → ((abs‘𝑀) lcm (abs‘𝑁)) ∥ (abs‘𝐾))) |
52 | 46, 47, 51 | syl2an 599 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (((𝐾 ∈ ℤ ∧ 𝐾 ≠ 0) ∧ ((abs‘𝑀) ∥ (abs‘𝐾) ∧ (abs‘𝑁) ∥ (abs‘𝐾))) → ((abs‘𝑀) lcm (abs‘𝑁)) ∥ (abs‘𝐾))) |
53 | 52 | expdimp 456 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) →
(((abs‘𝑀) ∥
(abs‘𝐾) ∧
(abs‘𝑁) ∥
(abs‘𝐾)) →
((abs‘𝑀) lcm
(abs‘𝑁)) ∥
(abs‘𝐾))) |
54 | | dvdsabsb 15865 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ∥ 𝐾 ↔ 𝑀 ∥ (abs‘𝐾))) |
55 | | zabscl 14905 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐾 ∈ ℤ →
(abs‘𝐾) ∈
ℤ) |
56 | | absdvdsb 15864 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℤ ∧
(abs‘𝐾) ∈
ℤ) → (𝑀 ∥
(abs‘𝐾) ↔
(abs‘𝑀) ∥
(abs‘𝐾))) |
57 | 55, 56 | sylan2 596 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ∥ (abs‘𝐾) ↔ (abs‘𝑀) ∥ (abs‘𝐾))) |
58 | 54, 57 | bitrd 282 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ∥ 𝐾 ↔ (abs‘𝑀) ∥ (abs‘𝐾))) |
59 | 58 | adantlr 715 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → (𝑀 ∥ 𝐾 ↔ (abs‘𝑀) ∥ (abs‘𝐾))) |
60 | | dvdsabsb 15865 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 ∥ 𝐾 ↔ 𝑁 ∥ (abs‘𝐾))) |
61 | | absdvdsb 15864 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℤ ∧
(abs‘𝐾) ∈
ℤ) → (𝑁 ∥
(abs‘𝐾) ↔
(abs‘𝑁) ∥
(abs‘𝐾))) |
62 | 55, 61 | sylan2 596 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 ∥ (abs‘𝐾) ↔ (abs‘𝑁) ∥ (abs‘𝐾))) |
63 | 60, 62 | bitrd 282 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 ∥ 𝐾 ↔ (abs‘𝑁) ∥ (abs‘𝐾))) |
64 | 63 | adantll 714 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → (𝑁 ∥ 𝐾 ↔ (abs‘𝑁) ∥ (abs‘𝐾))) |
65 | 59, 64 | anbi12d 634 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) ↔ ((abs‘𝑀) ∥ (abs‘𝐾) ∧ (abs‘𝑁) ∥ (abs‘𝐾)))) |
66 | 65 | bicomd 226 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) →
(((abs‘𝑀) ∥
(abs‘𝐾) ∧
(abs‘𝑁) ∥
(abs‘𝐾)) ↔
(𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾))) |
67 | | lcmabs 16190 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((abs‘𝑀) lcm
(abs‘𝑁)) = (𝑀 lcm 𝑁)) |
68 | 67 | breq1d 5078 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(((abs‘𝑀) lcm
(abs‘𝑁)) ∥
(abs‘𝐾) ↔ (𝑀 lcm 𝑁) ∥ (abs‘𝐾))) |
69 | 68 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) →
(((abs‘𝑀) lcm
(abs‘𝑁)) ∥
(abs‘𝐾) ↔ (𝑀 lcm 𝑁) ∥ (abs‘𝐾))) |
70 | | dvdsabsb 15865 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 lcm 𝑁) ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑀 lcm 𝑁) ∥ 𝐾 ↔ (𝑀 lcm 𝑁) ∥ (abs‘𝐾))) |
71 | 30, 70 | sylan 583 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → ((𝑀 lcm 𝑁) ∥ 𝐾 ↔ (𝑀 lcm 𝑁) ∥ (abs‘𝐾))) |
72 | 69, 71 | bitr4d 285 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) →
(((abs‘𝑀) lcm
(abs‘𝑁)) ∥
(abs‘𝐾) ↔ (𝑀 lcm 𝑁) ∥ 𝐾)) |
73 | 66, 72 | imbi12d 348 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) →
((((abs‘𝑀) ∥
(abs‘𝐾) ∧
(abs‘𝑁) ∥
(abs‘𝐾)) →
((abs‘𝑀) lcm
(abs‘𝑁)) ∥
(abs‘𝐾)) ↔
((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾))) |
74 | 73 | adantrr 717 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) →
((((abs‘𝑀) ∥
(abs‘𝐾) ∧
(abs‘𝑁) ∥
(abs‘𝐾)) →
((abs‘𝑀) lcm
(abs‘𝑁)) ∥
(abs‘𝐾)) ↔
((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾))) |
75 | 74 | adantllr 719 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → ((((abs‘𝑀) ∥ (abs‘𝐾) ∧ (abs‘𝑁) ∥ (abs‘𝐾)) → ((abs‘𝑀) lcm (abs‘𝑁)) ∥ (abs‘𝐾)) ↔ ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾))) |
76 | 75 | adantlrr 721 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) →
((((abs‘𝑀) ∥
(abs‘𝐾) ∧
(abs‘𝑁) ∥
(abs‘𝐾)) →
((abs‘𝑀) lcm
(abs‘𝑁)) ∥
(abs‘𝐾)) ↔
((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾))) |
77 | 53, 76 | mpbid 235 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾)) |
78 | 77 | anassrs 471 |
. . . . . . . . 9
⊢
(((((𝑀 ∈
ℤ ∧ 𝑀 ≠ 0)
∧ (𝑁 ∈ ℤ
∧ 𝑁 ≠ 0)) ∧
𝐾 ∈ ℤ) ∧
𝐾 ≠ 0) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾)) |
79 | 45, 78 | pm2.61dane 3030 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ 𝐾 ∈ ℤ) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾)) |
80 | 79 | ex 416 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝐾 ∈ ℤ → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾))) |
81 | 80 | an4s 660 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝐾 ∈ ℤ → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾))) |
82 | 28, 81 | sylan2br 598 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → (𝐾 ∈ ℤ → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾))) |
83 | 82 | impancom 455 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → (¬
(𝑀 = 0 ∨ 𝑁 = 0) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾))) |
84 | 83 | 3impa 1112 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (¬
(𝑀 = 0 ∨ 𝑁 = 0) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾))) |
85 | 84 | 3comr 1127 |
. 2
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬
(𝑀 = 0 ∨ 𝑁 = 0) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾))) |
86 | 16, 27, 85 | ecase3d 1034 |
1
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾)) |