| Step | Hyp | Ref
| Expression |
| 1 | | nnmulcl 12290 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 · 𝑁) ∈ ℕ) |
| 2 | 1 | nnred 12281 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 · 𝑁) ∈ ℝ) |
| 3 | | nnz 12634 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
| 4 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℤ) |
| 5 | 4 | zred 12722 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℝ) |
| 6 | | nnz 12634 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
| 7 | 6 | adantl 481 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℤ) |
| 8 | 7 | zred 12722 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℝ) |
| 9 | | 0red 11264 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 0 ∈
ℝ) |
| 10 | | nnre 12273 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
| 11 | | nngt0 12297 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 0 <
𝑀) |
| 12 | 9, 10, 11 | ltled 11409 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → 0 ≤
𝑀) |
| 13 | 12 | adantr 480 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 ≤
𝑀) |
| 14 | | 0red 11264 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 0 ∈
ℝ) |
| 15 | | nnre 12273 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
| 16 | | nngt0 12297 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
| 17 | 14, 15, 16 | ltled 11409 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 0 ≤
𝑁) |
| 18 | 17 | adantl 481 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 ≤
𝑁) |
| 19 | 5, 8, 13, 18 | mulge0d 11840 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 ≤
(𝑀 · 𝑁)) |
| 20 | 2, 19 | absidd 15461 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(abs‘(𝑀 ·
𝑁)) = (𝑀 · 𝑁)) |
| 21 | 3, 6 | anim12i 613 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ∈ ℤ ∧ 𝑁 ∈
ℤ)) |
| 22 | | nnne0 12300 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → 𝑀 ≠ 0) |
| 23 | 22 | neneqd 2945 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → ¬
𝑀 = 0) |
| 24 | | nnne0 12300 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
| 25 | 24 | neneqd 2945 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ¬
𝑁 = 0) |
| 26 | 23, 25 | anim12i 613 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (¬
𝑀 = 0 ∧ ¬ 𝑁 = 0)) |
| 27 | | ioran 986 |
. . . . . . 7
⊢ (¬
(𝑀 = 0 ∨ 𝑁 = 0) ↔ (¬ 𝑀 = 0 ∧ ¬ 𝑁 = 0)) |
| 28 | 26, 27 | sylibr 234 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ¬
(𝑀 = 0 ∨ 𝑁 = 0)) |
| 29 | | lcmn0val 16632 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm 𝑁) = inf({𝑥 ∈ ℕ ∣ (𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥)}, ℝ, < )) |
| 30 | 21, 28, 29 | syl2anc 584 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 lcm 𝑁) = inf({𝑥 ∈ ℕ ∣ (𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥)}, ℝ, < )) |
| 31 | | ltso 11341 |
. . . . . . 7
⊢ < Or
ℝ |
| 32 | 31 | a1i 11 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → < Or
ℝ) |
| 33 | | gcddvds 16540 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)) |
| 34 | 33 | simpld 494 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∥ 𝑀) |
| 35 | | gcdcl 16543 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈
ℕ0) |
| 36 | 35 | nn0zd 12639 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈ ℤ) |
| 37 | | dvdsmultr1 16333 |
. . . . . . . . . . . 12
⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 → (𝑀 gcd 𝑁) ∥ (𝑀 · 𝑁))) |
| 38 | 37 | 3expb 1121 |
. . . . . . . . . . 11
⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑀 gcd 𝑁) ∥ 𝑀 → (𝑀 gcd 𝑁) ∥ (𝑀 · 𝑁))) |
| 39 | 36, 38 | mpancom 688 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 → (𝑀 gcd 𝑁) ∥ (𝑀 · 𝑁))) |
| 40 | 34, 39 | mpd 15 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∥ (𝑀 · 𝑁)) |
| 41 | 21, 40 | syl 17 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∥ (𝑀 · 𝑁)) |
| 42 | | gcdnncl 16544 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℕ) |
| 43 | | nndivdvds 16299 |
. . . . . . . . 9
⊢ (((𝑀 · 𝑁) ∈ ℕ ∧ (𝑀 gcd 𝑁) ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ (𝑀 · 𝑁) ↔ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℕ)) |
| 44 | 1, 42, 43 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ (𝑀 · 𝑁) ↔ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℕ)) |
| 45 | 41, 44 | mpbid 232 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℕ) |
| 46 | 45 | nnred 12281 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℝ) |
| 47 | | breq2 5147 |
. . . . . . . 8
⊢ (𝑥 = ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) → (𝑀 ∥ 𝑥 ↔ 𝑀 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)))) |
| 48 | | breq2 5147 |
. . . . . . . 8
⊢ (𝑥 = ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) → (𝑁 ∥ 𝑥 ↔ 𝑁 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)))) |
| 49 | 47, 48 | anbi12d 632 |
. . . . . . 7
⊢ (𝑥 = ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) → ((𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥) ↔ (𝑀 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∧ 𝑁 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))))) |
| 50 | 33 | simprd 495 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∥ 𝑁) |
| 51 | 21, 50 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∥ 𝑁) |
| 52 | 21, 36 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℤ) |
| 53 | 42 | nnne0d 12316 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ≠ 0) |
| 54 | | dvdsval2 16293 |
. . . . . . . . . . . 12
⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ (𝑀 gcd 𝑁) ≠ 0 ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑁 ↔ (𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ)) |
| 55 | 52, 53, 7, 54 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ 𝑁 ↔ (𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ)) |
| 56 | 51, 55 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ) |
| 57 | | dvdsmul1 16315 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ (𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ) → 𝑀 ∥ (𝑀 · (𝑁 / (𝑀 gcd 𝑁)))) |
| 58 | 4, 56, 57 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∥ (𝑀 · (𝑁 / (𝑀 gcd 𝑁)))) |
| 59 | | nncn 12274 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) |
| 60 | 59 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℂ) |
| 61 | | nncn 12274 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
| 62 | 61 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℂ) |
| 63 | 42 | nncnd 12282 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℂ) |
| 64 | 60, 62, 63, 53 | divassd 12078 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) = (𝑀 · (𝑁 / (𝑀 gcd 𝑁)))) |
| 65 | 58, 64 | breqtrrd 5171 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) |
| 66 | 21, 34 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∥ 𝑀) |
| 67 | | dvdsval2 16293 |
. . . . . . . . . . . 12
⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ (𝑀 gcd 𝑁) ≠ 0 ∧ 𝑀 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ↔ (𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ)) |
| 68 | 52, 53, 4, 67 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ↔ (𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ)) |
| 69 | 66, 68 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ) |
| 70 | | dvdsmul1 16315 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ (𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ) → 𝑁 ∥ (𝑁 · (𝑀 / (𝑀 gcd 𝑁)))) |
| 71 | 7, 69, 70 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∥ (𝑁 · (𝑀 / (𝑀 gcd 𝑁)))) |
| 72 | 60, 62 | mulcomd 11282 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 · 𝑁) = (𝑁 · 𝑀)) |
| 73 | 72 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) = ((𝑁 · 𝑀) / (𝑀 gcd 𝑁))) |
| 74 | 62, 60, 63, 53 | divassd 12078 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 · 𝑀) / (𝑀 gcd 𝑁)) = (𝑁 · (𝑀 / (𝑀 gcd 𝑁)))) |
| 75 | 73, 74 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) = (𝑁 · (𝑀 / (𝑀 gcd 𝑁)))) |
| 76 | 71, 75 | breqtrrd 5171 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) |
| 77 | 65, 76 | jca 511 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∧ 𝑁 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)))) |
| 78 | 49, 45, 77 | elrabd 3694 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ {𝑥 ∈ ℕ ∣ (𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥)}) |
| 79 | 46 | adantr 480 |
. . . . . . 7
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ {𝑥 ∈ ℕ ∣ (𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥)}) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℝ) |
| 80 | | elrabi 3687 |
. . . . . . . . 9
⊢ (𝑛 ∈ {𝑥 ∈ ℕ ∣ (𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥)} → 𝑛 ∈ ℕ) |
| 81 | 80 | nnred 12281 |
. . . . . . . 8
⊢ (𝑛 ∈ {𝑥 ∈ ℕ ∣ (𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥)} → 𝑛 ∈ ℝ) |
| 82 | 81 | adantl 481 |
. . . . . . 7
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ {𝑥 ∈ ℕ ∣ (𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥)}) → 𝑛 ∈ ℝ) |
| 83 | | breq2 5147 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑛 → (𝑀 ∥ 𝑥 ↔ 𝑀 ∥ 𝑛)) |
| 84 | | breq2 5147 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑛 → (𝑁 ∥ 𝑥 ↔ 𝑁 ∥ 𝑛)) |
| 85 | 83, 84 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → ((𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥) ↔ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) |
| 86 | 85 | elrab 3692 |
. . . . . . . 8
⊢ (𝑛 ∈ {𝑥 ∈ ℕ ∣ (𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥)} ↔ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) |
| 87 | | bezout 16580 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℤ
(𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) |
| 88 | 21, 87 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℤ
(𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) |
| 89 | 88 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) |
| 90 | | nncn 12274 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
| 91 | 90 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑛 ∈
ℂ) |
| 92 | 1 | nncnd 12282 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 · 𝑁) ∈ ℂ) |
| 93 | 92 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 · 𝑁) ∈ ℂ) |
| 94 | 63 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 gcd 𝑁) ∈ ℂ) |
| 95 | 60 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑀 ∈
ℂ) |
| 96 | 61 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑁 ∈
ℂ) |
| 97 | 22 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑀 ≠ 0) |
| 98 | 24 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑁 ≠ 0) |
| 99 | 95, 96, 97, 98 | mulne0d 11915 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 · 𝑁) ≠ 0) |
| 100 | 53 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 gcd 𝑁) ≠ 0) |
| 101 | 91, 93, 94, 99, 100 | divdiv2d 12075 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) = ((𝑛 · (𝑀 gcd 𝑁)) / (𝑀 · 𝑁))) |
| 102 | 101 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑀 ∈
ℕ ∧ 𝑁 ∈
ℕ) ∧ 𝑛 ∈
ℕ) ∧ (𝑥 ∈
ℤ ∧ 𝑦 ∈
ℤ)) ∧ (𝑀 gcd
𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) = ((𝑛 · (𝑀 gcd 𝑁)) / (𝑀 · 𝑁))) |
| 103 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)) → (𝑛 · (𝑀 gcd 𝑁)) = (𝑛 · ((𝑀 · 𝑥) + (𝑁 · 𝑦)))) |
| 104 | 103 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)) → ((𝑛 · (𝑀 gcd 𝑁)) / (𝑀 · 𝑁)) = ((𝑛 · ((𝑀 · 𝑥) + (𝑁 · 𝑦))) / (𝑀 · 𝑁))) |
| 105 | | zcn 12618 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
| 106 | 105 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑥 ∈
ℂ) |
| 107 | 95, 106 | mulcld 11281 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 · 𝑥) ∈ ℂ) |
| 108 | | zcn 12618 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℂ) |
| 109 | 108 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑦 ∈
ℂ) |
| 110 | 96, 109 | mulcld 11281 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑁 · 𝑦) ∈ ℂ) |
| 111 | 91, 107, 110 | adddid 11285 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · ((𝑀 · 𝑥) + (𝑁 · 𝑦))) = ((𝑛 · (𝑀 · 𝑥)) + (𝑛 · (𝑁 · 𝑦)))) |
| 112 | 111 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑛 · ((𝑀 · 𝑥) + (𝑁 · 𝑦))) / (𝑀 · 𝑁)) = (((𝑛 · (𝑀 · 𝑥)) + (𝑛 · (𝑁 · 𝑦))) / (𝑀 · 𝑁))) |
| 113 | 91, 107 | mulcld 11281 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · (𝑀 · 𝑥)) ∈ ℂ) |
| 114 | 91, 110 | mulcld 11281 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · (𝑁 · 𝑦)) ∈ ℂ) |
| 115 | 113, 114,
93, 99 | divdird 12081 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) →
(((𝑛 · (𝑀 · 𝑥)) + (𝑛 · (𝑁 · 𝑦))) / (𝑀 · 𝑁)) = (((𝑛 · (𝑀 · 𝑥)) / (𝑀 · 𝑁)) + ((𝑛 · (𝑁 · 𝑦)) / (𝑀 · 𝑁)))) |
| 116 | 112, 115 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑛 · ((𝑀 · 𝑥) + (𝑁 · 𝑦))) / (𝑀 · 𝑁)) = (((𝑛 · (𝑀 · 𝑥)) / (𝑀 · 𝑁)) + ((𝑛 · (𝑁 · 𝑦)) / (𝑀 · 𝑁)))) |
| 117 | 104, 116 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑀 ∈
ℕ ∧ 𝑁 ∈
ℕ) ∧ 𝑛 ∈
ℕ) ∧ (𝑥 ∈
ℤ ∧ 𝑦 ∈
ℤ)) ∧ (𝑀 gcd
𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → ((𝑛 · (𝑀 gcd 𝑁)) / (𝑀 · 𝑁)) = (((𝑛 · (𝑀 · 𝑥)) / (𝑀 · 𝑁)) + ((𝑛 · (𝑁 · 𝑦)) / (𝑀 · 𝑁)))) |
| 118 | 91, 95, 106 | mul12d 11470 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · (𝑀 · 𝑥)) = (𝑀 · (𝑛 · 𝑥))) |
| 119 | 118 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑛 · (𝑀 · 𝑥)) / (𝑀 · 𝑁)) = ((𝑀 · (𝑛 · 𝑥)) / (𝑀 · 𝑁))) |
| 120 | 91, 106 | mulcld 11281 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · 𝑥) ∈ ℂ) |
| 121 | 120, 96, 95, 98, 97 | divcan5d 12069 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 · (𝑛 · 𝑥)) / (𝑀 · 𝑁)) = ((𝑛 · 𝑥) / 𝑁)) |
| 122 | 119, 121 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑛 · (𝑀 · 𝑥)) / (𝑀 · 𝑁)) = ((𝑛 · 𝑥) / 𝑁)) |
| 123 | 91, 96, 109 | mul12d 11470 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · (𝑁 · 𝑦)) = (𝑁 · (𝑛 · 𝑦))) |
| 124 | 123 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑛 · (𝑁 · 𝑦)) / (𝑀 · 𝑁)) = ((𝑁 · (𝑛 · 𝑦)) / (𝑀 · 𝑁))) |
| 125 | 72 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 · 𝑁) = (𝑁 · 𝑀)) |
| 126 | 125 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑁 · (𝑛 · 𝑦)) / (𝑀 · 𝑁)) = ((𝑁 · (𝑛 · 𝑦)) / (𝑁 · 𝑀))) |
| 127 | 91, 109 | mulcld 11281 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · 𝑦) ∈ ℂ) |
| 128 | 127, 95, 96, 97, 98 | divcan5d 12069 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑁 · (𝑛 · 𝑦)) / (𝑁 · 𝑀)) = ((𝑛 · 𝑦) / 𝑀)) |
| 129 | 124, 126,
128 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑛 · (𝑁 · 𝑦)) / (𝑀 · 𝑁)) = ((𝑛 · 𝑦) / 𝑀)) |
| 130 | 122, 129 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) →
(((𝑛 · (𝑀 · 𝑥)) / (𝑀 · 𝑁)) + ((𝑛 · (𝑁 · 𝑦)) / (𝑀 · 𝑁))) = (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀))) |
| 131 | 130 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑀 ∈
ℕ ∧ 𝑁 ∈
ℕ) ∧ 𝑛 ∈
ℕ) ∧ (𝑥 ∈
ℤ ∧ 𝑦 ∈
ℤ)) ∧ (𝑀 gcd
𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → (((𝑛 · (𝑀 · 𝑥)) / (𝑀 · 𝑁)) + ((𝑛 · (𝑁 · 𝑦)) / (𝑀 · 𝑁))) = (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀))) |
| 132 | 102, 117,
131 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑀 ∈
ℕ ∧ 𝑁 ∈
ℕ) ∧ 𝑛 ∈
ℕ) ∧ (𝑥 ∈
ℤ ∧ 𝑦 ∈
ℤ)) ∧ (𝑀 gcd
𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) = (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀))) |
| 133 | 132 | ex 412 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)) → (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) = (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)))) |
| 134 | 133 | adantlrr 721 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)) → (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) = (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)))) |
| 135 | 134 | imp 406 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑀 ∈
ℕ ∧ 𝑁 ∈
ℕ) ∧ (𝑛 ∈
ℕ ∧ (𝑀 ∥
𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) = (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀))) |
| 136 | 6 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑁 ∈
ℤ) |
| 137 | | nnz 12634 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
| 138 | 137 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑛 ∈
ℤ) |
| 139 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑥 ∈
ℤ) |
| 140 | | dvdsmultr1 16333 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝑁 ∥ 𝑛 → 𝑁 ∥ (𝑛 · 𝑥))) |
| 141 | 136, 138,
139, 140 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑁 ∥ 𝑛 → 𝑁 ∥ (𝑛 · 𝑥))) |
| 142 | 138, 139 | zmulcld 12728 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · 𝑥) ∈ ℤ) |
| 143 | | dvdsval2 16293 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ (𝑛 · 𝑥) ∈ ℤ) → (𝑁 ∥ (𝑛 · 𝑥) ↔ ((𝑛 · 𝑥) / 𝑁) ∈ ℤ)) |
| 144 | 136, 98, 142, 143 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑁 ∥ (𝑛 · 𝑥) ↔ ((𝑛 · 𝑥) / 𝑁) ∈ ℤ)) |
| 145 | 141, 144 | sylibd 239 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑁 ∥ 𝑛 → ((𝑛 · 𝑥) / 𝑁) ∈ ℤ)) |
| 146 | 145 | adantld 490 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛) → ((𝑛 · 𝑥) / 𝑁) ∈ ℤ)) |
| 147 | 146 | 3impia 1118 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛)) → ((𝑛 · 𝑥) / 𝑁) ∈ ℤ) |
| 148 | 3 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑀 ∈
ℤ) |
| 149 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑦 ∈
ℤ) |
| 150 | | dvdsmultr1 16333 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑀 ∥ 𝑛 → 𝑀 ∥ (𝑛 · 𝑦))) |
| 151 | 148, 138,
149, 150 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 ∥ 𝑛 → 𝑀 ∥ (𝑛 · 𝑦))) |
| 152 | 138, 149 | zmulcld 12728 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · 𝑦) ∈ ℤ) |
| 153 | | dvdsval2 16293 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝑛 · 𝑦) ∈ ℤ) → (𝑀 ∥ (𝑛 · 𝑦) ↔ ((𝑛 · 𝑦) / 𝑀) ∈ ℤ)) |
| 154 | 148, 97, 152, 153 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 ∥ (𝑛 · 𝑦) ↔ ((𝑛 · 𝑦) / 𝑀) ∈ ℤ)) |
| 155 | 151, 154 | sylibd 239 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 ∥ 𝑛 → ((𝑛 · 𝑦) / 𝑀) ∈ ℤ)) |
| 156 | 155 | adantrd 491 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛) → ((𝑛 · 𝑦) / 𝑀) ∈ ℤ)) |
| 157 | 156 | 3impia 1118 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛)) → ((𝑛 · 𝑦) / 𝑀) ∈ ℤ) |
| 158 | 147, 157 | zaddcld 12726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛)) → (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)) ∈ ℤ) |
| 159 | 158 | 3expia 1122 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛) → (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)) ∈ ℤ)) |
| 160 | 159 | an32s 652 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ 𝑛 ∈ ℕ) → ((𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛) → (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)) ∈ ℤ)) |
| 161 | 160 | impr 454 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)) ∈ ℤ) |
| 162 | 161 | an32s 652 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)) ∈ ℤ) |
| 163 | 162 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑀 ∈
ℕ ∧ 𝑁 ∈
ℕ) ∧ (𝑛 ∈
ℕ ∧ (𝑀 ∥
𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)) ∈ ℤ) |
| 164 | 135, 163 | eqeltrd 2841 |
. . . . . . . . . . . . . 14
⊢
(((((𝑀 ∈
ℕ ∧ 𝑁 ∈
ℕ) ∧ (𝑛 ∈
ℕ ∧ (𝑀 ∥
𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) ∈ ℤ) |
| 165 | 45 | nnzd 12640 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℤ) |
| 166 | 165 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℤ) |
| 167 | 1 | nnne0d 12316 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 · 𝑁) ≠ 0) |
| 168 | 92, 63, 167, 53 | divne0d 12059 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ≠ 0) |
| 169 | 168 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ≠ 0) |
| 170 | 138 | adantlrr 721 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑛 ∈ ℤ) |
| 171 | | dvdsval2 16293 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℤ ∧ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ≠ 0 ∧ 𝑛 ∈ ℤ) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) ∈ ℤ)) |
| 172 | 166, 169,
170, 171 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) ∈ ℤ)) |
| 173 | 172 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝑀 ∈
ℕ ∧ 𝑁 ∈
ℕ) ∧ (𝑛 ∈
ℕ ∧ (𝑀 ∥
𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) ∈ ℤ)) |
| 174 | 164, 173 | mpbird 257 |
. . . . . . . . . . . . 13
⊢
(((((𝑀 ∈
ℕ ∧ 𝑁 ∈
ℕ) ∧ (𝑛 ∈
ℕ ∧ (𝑀 ∥
𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛) |
| 175 | 174 | ex 412 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛)) |
| 176 | 175 | reximdvva 3207 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛)) |
| 177 | 89, 176 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛) |
| 178 | | 1z 12647 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
| 179 | | ne0i 4341 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℤ → ℤ ≠ ∅) |
| 180 | | r19.9rzv 4500 |
. . . . . . . . . . . 12
⊢ (ℤ
≠ ∅ → (((𝑀
· 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ ∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛)) |
| 181 | 178, 179,
180 | mp2b 10 |
. . . . . . . . . . 11
⊢ (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ ∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛) |
| 182 | | r19.9rzv 4500 |
. . . . . . . . . . . 12
⊢ (ℤ
≠ ∅ → (∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛)) |
| 183 | 178, 179,
182 | mp2b 10 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛) |
| 184 | 181, 183 | bitri 275 |
. . . . . . . . . 10
⊢ (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛) |
| 185 | 177, 184 | sylibr 234 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛) |
| 186 | 165 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℤ) |
| 187 | | simprl 771 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → 𝑛 ∈ ℕ) |
| 188 | | dvdsle 16347 |
. . . . . . . . . 10
⊢ ((((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℤ ∧ 𝑛 ∈ ℕ) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ≤ 𝑛)) |
| 189 | 186, 187,
188 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ≤ 𝑛)) |
| 190 | 185, 189 | mpd 15 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ≤ 𝑛) |
| 191 | 86, 190 | sylan2b 594 |
. . . . . . 7
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ {𝑥 ∈ ℕ ∣ (𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥)}) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ≤ 𝑛) |
| 192 | 79, 82, 191 | lensymd 11412 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ {𝑥 ∈ ℕ ∣ (𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥)}) → ¬ 𝑛 < ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) |
| 193 | 32, 46, 78, 192 | infmin 9534 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
inf({𝑥 ∈ ℕ
∣ (𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥)}, ℝ, < ) = ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) |
| 194 | 30, 193 | eqtr2d 2778 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) = (𝑀 lcm 𝑁)) |
| 195 | 194, 45 | eqeltrrd 2842 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 lcm 𝑁) ∈ ℕ) |
| 196 | 195 | nncnd 12282 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 lcm 𝑁) ∈ ℂ) |
| 197 | 92, 196, 63, 53 | divmul3d 12077 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) = (𝑀 lcm 𝑁) ↔ (𝑀 · 𝑁) = ((𝑀 lcm 𝑁) · (𝑀 gcd 𝑁)))) |
| 198 | 194, 197 | mpbid 232 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 · 𝑁) = ((𝑀 lcm 𝑁) · (𝑀 gcd 𝑁))) |
| 199 | 20, 198 | eqtr2d 2778 |
. 2
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 lcm 𝑁) · (𝑀 gcd 𝑁)) = (abs‘(𝑀 · 𝑁))) |
| 200 | | simprl 771 |
. . . 4
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℕ ∧ (𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾))) → 𝐾 ∈ ℕ) |
| 201 | | eleq1 2829 |
. . . . . . . 8
⊢ (𝑛 = 𝐾 → (𝑛 ∈ ℕ ↔ 𝐾 ∈ ℕ)) |
| 202 | | breq2 5147 |
. . . . . . . . 9
⊢ (𝑛 = 𝐾 → (𝑀 ∥ 𝑛 ↔ 𝑀 ∥ 𝐾)) |
| 203 | | breq2 5147 |
. . . . . . . . 9
⊢ (𝑛 = 𝐾 → (𝑁 ∥ 𝑛 ↔ 𝑁 ∥ 𝐾)) |
| 204 | 202, 203 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑛 = 𝐾 → ((𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛) ↔ (𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾))) |
| 205 | 201, 204 | anbi12d 632 |
. . . . . . 7
⊢ (𝑛 = 𝐾 → ((𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛)) ↔ (𝐾 ∈ ℕ ∧ (𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾)))) |
| 206 | 205 | anbi2d 630 |
. . . . . 6
⊢ (𝑛 = 𝐾 → (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) ↔ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℕ ∧ (𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾))))) |
| 207 | | breq2 5147 |
. . . . . 6
⊢ (𝑛 = 𝐾 → ((𝑀 lcm 𝑁) ∥ 𝑛 ↔ (𝑀 lcm 𝑁) ∥ 𝐾)) |
| 208 | 206, 207 | imbi12d 344 |
. . . . 5
⊢ (𝑛 = 𝐾 → ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → (𝑀 lcm 𝑁) ∥ 𝑛) ↔ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℕ ∧ (𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾))) → (𝑀 lcm 𝑁) ∥ 𝐾))) |
| 209 | 194 | breq1d 5153 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ (𝑀 lcm 𝑁) ∥ 𝑛)) |
| 210 | 209 | adantr 480 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ (𝑀 lcm 𝑁) ∥ 𝑛)) |
| 211 | 185, 210 | mpbid 232 |
. . . . 5
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → (𝑀 lcm 𝑁) ∥ 𝑛) |
| 212 | 208, 211 | vtoclg 3554 |
. . . 4
⊢ (𝐾 ∈ ℕ → (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℕ ∧ (𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾))) → (𝑀 lcm 𝑁) ∥ 𝐾)) |
| 213 | 200, 212 | mpcom 38 |
. . 3
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℕ ∧ (𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾))) → (𝑀 lcm 𝑁) ∥ 𝐾) |
| 214 | 213 | ex 412 |
. 2
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐾 ∈ ℕ ∧ (𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾)) → (𝑀 lcm 𝑁) ∥ 𝐾)) |
| 215 | 199, 214 | jca 511 |
1
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 lcm 𝑁) · (𝑀 gcd 𝑁)) = (abs‘(𝑀 · 𝑁)) ∧ ((𝐾 ∈ ℕ ∧ (𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾)) → (𝑀 lcm 𝑁) ∥ 𝐾))) |