Proof of Theorem lcmdvds
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | id 22 | . . . . . 6
⊢ (0
∥ 𝐾 → 0 ∥
𝐾) | 
| 2 |  | breq1 5145 | . . . . . . . 8
⊢ (𝑀 = 0 → (𝑀 ∥ 𝐾 ↔ 0 ∥ 𝐾)) | 
| 3 | 2 | adantl 481 | . . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 = 0) → (𝑀 ∥ 𝐾 ↔ 0 ∥ 𝐾)) | 
| 4 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝑀 = 0 → (𝑀 lcm 𝑁) = (0 lcm 𝑁)) | 
| 5 |  | 0z 12626 | . . . . . . . . . . 11
⊢ 0 ∈
ℤ | 
| 6 |  | lcmcom 16631 | . . . . . . . . . . 11
⊢ ((0
∈ ℤ ∧ 𝑁
∈ ℤ) → (0 lcm 𝑁) = (𝑁 lcm 0)) | 
| 7 | 5, 6 | mpan 690 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → (0 lcm
𝑁) = (𝑁 lcm 0)) | 
| 8 |  | lcm0val 16632 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → (𝑁 lcm 0) = 0) | 
| 9 | 7, 8 | eqtrd 2776 | . . . . . . . . 9
⊢ (𝑁 ∈ ℤ → (0 lcm
𝑁) = 0) | 
| 10 | 4, 9 | sylan9eqr 2798 | . . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 = 0) → (𝑀 lcm 𝑁) = 0) | 
| 11 | 10 | breq1d 5152 | . . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 = 0) → ((𝑀 lcm 𝑁) ∥ 𝐾 ↔ 0 ∥ 𝐾)) | 
| 12 | 3, 11 | imbi12d 344 | . . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 = 0) → ((𝑀 ∥ 𝐾 → (𝑀 lcm 𝑁) ∥ 𝐾) ↔ (0 ∥ 𝐾 → 0 ∥ 𝐾))) | 
| 13 | 1, 12 | mpbiri 258 | . . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 = 0) → (𝑀 ∥ 𝐾 → (𝑀 lcm 𝑁) ∥ 𝐾)) | 
| 14 | 13 | 3ad2antl3 1187 | . . . 4
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (𝑀 ∥ 𝐾 → (𝑀 lcm 𝑁) ∥ 𝐾)) | 
| 15 | 14 | adantrd 491 | . . 3
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾)) | 
| 16 | 15 | ex 412 | . 2
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 = 0 → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾))) | 
| 17 |  | breq1 5145 | . . . . . . . 8
⊢ (𝑁 = 0 → (𝑁 ∥ 𝐾 ↔ 0 ∥ 𝐾)) | 
| 18 | 17 | adantl 481 | . . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = 0) → (𝑁 ∥ 𝐾 ↔ 0 ∥ 𝐾)) | 
| 19 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑁 = 0 → (𝑀 lcm 𝑁) = (𝑀 lcm 0)) | 
| 20 |  | lcm0val 16632 | . . . . . . . . 9
⊢ (𝑀 ∈ ℤ → (𝑀 lcm 0) = 0) | 
| 21 | 19, 20 | sylan9eqr 2798 | . . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = 0) → (𝑀 lcm 𝑁) = 0) | 
| 22 | 21 | breq1d 5152 | . . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = 0) → ((𝑀 lcm 𝑁) ∥ 𝐾 ↔ 0 ∥ 𝐾)) | 
| 23 | 18, 22 | imbi12d 344 | . . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = 0) → ((𝑁 ∥ 𝐾 → (𝑀 lcm 𝑁) ∥ 𝐾) ↔ (0 ∥ 𝐾 → 0 ∥ 𝐾))) | 
| 24 | 1, 23 | mpbiri 258 | . . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = 0) → (𝑁 ∥ 𝐾 → (𝑀 lcm 𝑁) ∥ 𝐾)) | 
| 25 | 24 | 3ad2antl2 1186 | . . . 4
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (𝑁 ∥ 𝐾 → (𝑀 lcm 𝑁) ∥ 𝐾)) | 
| 26 | 25 | adantld 490 | . . 3
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾)) | 
| 27 | 26 | ex 412 | . 2
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 = 0 → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾))) | 
| 28 |  | neanior 3034 | . . . . . 6
⊢ ((𝑀 ≠ 0 ∧ 𝑁 ≠ 0) ↔ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) | 
| 29 |  | lcmcl 16639 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) ∈
ℕ0) | 
| 30 | 29 | nn0zd 12641 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) ∈ ℤ) | 
| 31 |  | dvds0 16310 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑀 lcm 𝑁) ∈ ℤ → (𝑀 lcm 𝑁) ∥ 0) | 
| 32 | 30, 31 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) ∥ 0) | 
| 33 | 32 | a1d 25 | . . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 ∥ 0 ∧ 𝑁 ∥ 0) → (𝑀 lcm 𝑁) ∥ 0)) | 
| 34 | 33 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 = 0) → ((𝑀 ∥ 0 ∧ 𝑁 ∥ 0) → (𝑀 lcm 𝑁) ∥ 0)) | 
| 35 |  | breq2 5146 | . . . . . . . . . . . . . . . . 17
⊢ (𝐾 = 0 → (𝑀 ∥ 𝐾 ↔ 𝑀 ∥ 0)) | 
| 36 |  | breq2 5146 | . . . . . . . . . . . . . . . . 17
⊢ (𝐾 = 0 → (𝑁 ∥ 𝐾 ↔ 𝑁 ∥ 0)) | 
| 37 | 35, 36 | anbi12d 632 | . . . . . . . . . . . . . . . 16
⊢ (𝐾 = 0 → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) ↔ (𝑀 ∥ 0 ∧ 𝑁 ∥ 0))) | 
| 38 |  | breq2 5146 | . . . . . . . . . . . . . . . 16
⊢ (𝐾 = 0 → ((𝑀 lcm 𝑁) ∥ 𝐾 ↔ (𝑀 lcm 𝑁) ∥ 0)) | 
| 39 | 37, 38 | imbi12d 344 | . . . . . . . . . . . . . . 15
⊢ (𝐾 = 0 → (((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾) ↔ ((𝑀 ∥ 0 ∧ 𝑁 ∥ 0) → (𝑀 lcm 𝑁) ∥ 0))) | 
| 40 | 39 | adantl 481 | . . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 = 0) → (((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾) ↔ ((𝑀 ∥ 0 ∧ 𝑁 ∥ 0) → (𝑀 lcm 𝑁) ∥ 0))) | 
| 41 | 34, 40 | mpbird 257 | . . . . . . . . . . . . 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 467 | . . . . . . . . 9
⊢
(((((𝑀 ∈
ℤ ∧ 𝑀 ≠ 0)
∧ (𝑁 ∈ ℤ
∧ 𝑁 ≠ 0)) ∧
𝐾 ∈ ℤ) ∧
𝐾 = 0) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾)) | 
| 46 |  | nnabscl 15365 | . . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → (abs‘𝑀) ∈
ℕ) | 
| 47 |  | nnabscl 15365 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈
ℕ) | 
| 48 |  | nnabscl 15365 | . . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℤ ∧ 𝐾 ≠ 0) → (abs‘𝐾) ∈
ℕ) | 
| 49 |  | lcmgcdlem 16644 | . . . . . . . . . . . . . . 15
⊢
(((abs‘𝑀)
∈ ℕ ∧ (abs‘𝑁) ∈ ℕ) → ((((abs‘𝑀) lcm (abs‘𝑁)) · ((abs‘𝑀) gcd (abs‘𝑁))) =
(abs‘((abs‘𝑀)
· (abs‘𝑁)))
∧ (((abs‘𝐾)
∈ ℕ ∧ ((abs‘𝑀) ∥ (abs‘𝐾) ∧ (abs‘𝑁) ∥ (abs‘𝐾))) → ((abs‘𝑀) lcm (abs‘𝑁)) ∥ (abs‘𝐾)))) | 
| 50 | 49 | simprd 495 | . . . . . . . . . . . . . 14
⊢
(((abs‘𝑀)
∈ ℕ ∧ (abs‘𝑁) ∈ ℕ) → (((abs‘𝐾) ∈ ℕ ∧
((abs‘𝑀) ∥
(abs‘𝐾) ∧
(abs‘𝑁) ∥
(abs‘𝐾))) →
((abs‘𝑀) lcm
(abs‘𝑁)) ∥
(abs‘𝐾))) | 
| 51 | 48, 50 | sylani 604 | . . . . . . . . . . . . 13
⊢
(((abs‘𝑀)
∈ ℕ ∧ (abs‘𝑁) ∈ ℕ) → (((𝐾 ∈ ℤ ∧ 𝐾 ≠ 0) ∧ ((abs‘𝑀) ∥ (abs‘𝐾) ∧ (abs‘𝑁) ∥ (abs‘𝐾))) → ((abs‘𝑀) lcm (abs‘𝑁)) ∥ (abs‘𝐾))) | 
| 52 | 46, 47, 51 | syl2an 596 | . . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (((𝐾 ∈ ℤ ∧ 𝐾 ≠ 0) ∧ ((abs‘𝑀) ∥ (abs‘𝐾) ∧ (abs‘𝑁) ∥ (abs‘𝐾))) → ((abs‘𝑀) lcm (abs‘𝑁)) ∥ (abs‘𝐾))) | 
| 53 | 52 | expdimp 452 | . . . . . . . . . . 11
⊢ ((((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) →
(((abs‘𝑀) ∥
(abs‘𝐾) ∧
(abs‘𝑁) ∥
(abs‘𝐾)) →
((abs‘𝑀) lcm
(abs‘𝑁)) ∥
(abs‘𝐾))) | 
| 54 |  | dvdsabsb 16314 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ∥ 𝐾 ↔ 𝑀 ∥ (abs‘𝐾))) | 
| 55 |  | zabscl 15353 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐾 ∈ ℤ →
(abs‘𝐾) ∈
ℤ) | 
| 56 |  | absdvdsb 16313 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℤ ∧
(abs‘𝐾) ∈
ℤ) → (𝑀 ∥
(abs‘𝐾) ↔
(abs‘𝑀) ∥
(abs‘𝐾))) | 
| 57 | 55, 56 | sylan2 593 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ∥ (abs‘𝐾) ↔ (abs‘𝑀) ∥ (abs‘𝐾))) | 
| 58 | 54, 57 | bitrd 279 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ∥ 𝐾 ↔ (abs‘𝑀) ∥ (abs‘𝐾))) | 
| 59 | 58 | adantlr 715 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → (𝑀 ∥ 𝐾 ↔ (abs‘𝑀) ∥ (abs‘𝐾))) | 
| 60 |  | dvdsabsb 16314 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 ∥ 𝐾 ↔ 𝑁 ∥ (abs‘𝐾))) | 
| 61 |  | absdvdsb 16313 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℤ ∧
(abs‘𝐾) ∈
ℤ) → (𝑁 ∥
(abs‘𝐾) ↔
(abs‘𝑁) ∥
(abs‘𝐾))) | 
| 62 | 55, 61 | sylan2 593 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 ∥ (abs‘𝐾) ↔ (abs‘𝑁) ∥ (abs‘𝐾))) | 
| 63 | 60, 62 | bitrd 279 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 ∥ 𝐾 ↔ (abs‘𝑁) ∥ (abs‘𝐾))) | 
| 64 | 63 | adantll 714 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → (𝑁 ∥ 𝐾 ↔ (abs‘𝑁) ∥ (abs‘𝐾))) | 
| 65 | 59, 64 | anbi12d 632 | . . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) ↔ ((abs‘𝑀) ∥ (abs‘𝐾) ∧ (abs‘𝑁) ∥ (abs‘𝐾)))) | 
| 66 | 65 | bicomd 223 | . . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) →
(((abs‘𝑀) ∥
(abs‘𝐾) ∧
(abs‘𝑁) ∥
(abs‘𝐾)) ↔
(𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾))) | 
| 67 |  | lcmabs 16643 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((abs‘𝑀) lcm
(abs‘𝑁)) = (𝑀 lcm 𝑁)) | 
| 68 | 67 | breq1d 5152 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(((abs‘𝑀) lcm
(abs‘𝑁)) ∥
(abs‘𝐾) ↔ (𝑀 lcm 𝑁) ∥ (abs‘𝐾))) | 
| 69 | 68 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) →
(((abs‘𝑀) lcm
(abs‘𝑁)) ∥
(abs‘𝐾) ↔ (𝑀 lcm 𝑁) ∥ (abs‘𝐾))) | 
| 70 |  | dvdsabsb 16314 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑀 lcm 𝑁) ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑀 lcm 𝑁) ∥ 𝐾 ↔ (𝑀 lcm 𝑁) ∥ (abs‘𝐾))) | 
| 71 | 30, 70 | sylan 580 | . . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → ((𝑀 lcm 𝑁) ∥ 𝐾 ↔ (𝑀 lcm 𝑁) ∥ (abs‘𝐾))) | 
| 72 | 69, 71 | bitr4d 282 | . . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) →
(((abs‘𝑀) lcm
(abs‘𝑁)) ∥
(abs‘𝐾) ↔ (𝑀 lcm 𝑁) ∥ 𝐾)) | 
| 73 | 66, 72 | imbi12d 344 | . . . . . . . . . . . . . 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 232 | . . . . . . . . . 10
⊢ ((((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾)) | 
| 78 | 77 | anassrs 467 | . . . . . . . . 9
⊢
(((((𝑀 ∈
ℤ ∧ 𝑀 ≠ 0)
∧ (𝑁 ∈ ℤ
∧ 𝑁 ≠ 0)) ∧
𝐾 ∈ ℤ) ∧
𝐾 ≠ 0) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾)) | 
| 79 | 45, 78 | pm2.61dane 3028 | . . . . . . . 8
⊢ ((((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ 𝐾 ∈ ℤ) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾)) | 
| 80 | 79 | ex 412 | . . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝐾 ∈ ℤ → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾))) | 
| 81 | 80 | an4s 660 | . . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝐾 ∈ ℤ → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾))) | 
| 82 | 28, 81 | sylan2br 595 | . . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → (𝐾 ∈ ℤ → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾))) | 
| 83 | 82 | impancom 451 | . . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → (¬
(𝑀 = 0 ∨ 𝑁 = 0) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾))) | 
| 84 | 83 | 3impa 1109 | . . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (¬
(𝑀 = 0 ∨ 𝑁 = 0) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾))) | 
| 85 | 84 | 3comr 1125 | . 2
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬
(𝑀 = 0 ∨ 𝑁 = 0) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾))) | 
| 86 | 16, 27, 85 | ecase3d 1034 | 1
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 lcm 𝑁) ∥ 𝐾)) |