Step | Hyp | Ref
| Expression |
1 | | nnmulcl 11878 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 · 𝑁) ∈ ℕ) |
2 | 1 | nnred 11869 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 · 𝑁) ∈ ℝ) |
3 | | nnz 12223 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
4 | 3 | adantr 484 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℤ) |
5 | 4 | zred 12306 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℝ) |
6 | | nnz 12223 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
7 | 6 | adantl 485 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℤ) |
8 | 7 | zred 12306 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℝ) |
9 | | 0red 10860 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 0 ∈
ℝ) |
10 | | nnre 11861 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
11 | | nngt0 11885 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 0 <
𝑀) |
12 | 9, 10, 11 | ltled 11004 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → 0 ≤
𝑀) |
13 | 12 | adantr 484 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 ≤
𝑀) |
14 | | 0red 10860 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 0 ∈
ℝ) |
15 | | nnre 11861 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
16 | | nngt0 11885 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
17 | 14, 15, 16 | ltled 11004 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 0 ≤
𝑁) |
18 | 17 | adantl 485 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 ≤
𝑁) |
19 | 5, 8, 13, 18 | mulge0d 11433 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 ≤
(𝑀 · 𝑁)) |
20 | 2, 19 | absidd 15010 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(abs‘(𝑀 ·
𝑁)) = (𝑀 · 𝑁)) |
21 | 3, 6 | anim12i 616 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ∈ ℤ ∧ 𝑁 ∈
ℤ)) |
22 | | nnne0 11888 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → 𝑀 ≠ 0) |
23 | 22 | neneqd 2946 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → ¬
𝑀 = 0) |
24 | | nnne0 11888 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
25 | 24 | neneqd 2946 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ¬
𝑁 = 0) |
26 | 23, 25 | anim12i 616 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (¬
𝑀 = 0 ∧ ¬ 𝑁 = 0)) |
27 | | ioran 984 |
. . . . . . 7
⊢ (¬
(𝑀 = 0 ∨ 𝑁 = 0) ↔ (¬ 𝑀 = 0 ∧ ¬ 𝑁 = 0)) |
28 | 26, 27 | sylibr 237 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ¬
(𝑀 = 0 ∨ 𝑁 = 0)) |
29 | | lcmn0val 16176 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm 𝑁) = inf({𝑥 ∈ ℕ ∣ (𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥)}, ℝ, < )) |
30 | 21, 28, 29 | syl2anc 587 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 lcm 𝑁) = inf({𝑥 ∈ ℕ ∣ (𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥)}, ℝ, < )) |
31 | | ltso 10937 |
. . . . . . 7
⊢ < Or
ℝ |
32 | 31 | a1i 11 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → < Or
ℝ) |
33 | | gcddvds 16086 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)) |
34 | 33 | simpld 498 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∥ 𝑀) |
35 | | gcdcl 16089 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈
ℕ0) |
36 | 35 | nn0zd 12304 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈ ℤ) |
37 | | dvdsmultr1 15881 |
. . . . . . . . . . . 12
⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 → (𝑀 gcd 𝑁) ∥ (𝑀 · 𝑁))) |
38 | 37 | 3expb 1122 |
. . . . . . . . . . 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 16090 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℕ) |
43 | | nndivdvds 15848 |
. . . . . . . . 9
⊢ (((𝑀 · 𝑁) ∈ ℕ ∧ (𝑀 gcd 𝑁) ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ (𝑀 · 𝑁) ↔ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℕ)) |
44 | 1, 42, 43 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ (𝑀 · 𝑁) ↔ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℕ)) |
45 | 41, 44 | mpbid 235 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℕ) |
46 | 45 | nnred 11869 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℝ) |
47 | | breq2 5071 |
. . . . . . . 8
⊢ (𝑥 = ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) → (𝑀 ∥ 𝑥 ↔ 𝑀 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)))) |
48 | | breq2 5071 |
. . . . . . . 8
⊢ (𝑥 = ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) → (𝑁 ∥ 𝑥 ↔ 𝑁 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)))) |
49 | 47, 48 | anbi12d 634 |
. . . . . . 7
⊢ (𝑥 = ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) → ((𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥) ↔ (𝑀 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∧ 𝑁 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))))) |
50 | 33 | simprd 499 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∥ 𝑁) |
51 | 21, 50 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∥ 𝑁) |
52 | 21, 36 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℤ) |
53 | 42 | nnne0d 11904 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ≠ 0) |
54 | | dvdsval2 15842 |
. . . . . . . . . . . 12
⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ (𝑀 gcd 𝑁) ≠ 0 ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑁 ↔ (𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ)) |
55 | 52, 53, 7, 54 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ 𝑁 ↔ (𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ)) |
56 | 51, 55 | mpbid 235 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ) |
57 | | dvdsmul1 15863 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ (𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ) → 𝑀 ∥ (𝑀 · (𝑁 / (𝑀 gcd 𝑁)))) |
58 | 4, 56, 57 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∥ (𝑀 · (𝑁 / (𝑀 gcd 𝑁)))) |
59 | | nncn 11862 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) |
60 | 59 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℂ) |
61 | | nncn 11862 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
62 | 61 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℂ) |
63 | 42 | nncnd 11870 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℂ) |
64 | 60, 62, 63, 53 | divassd 11667 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) = (𝑀 · (𝑁 / (𝑀 gcd 𝑁)))) |
65 | 58, 64 | breqtrrd 5095 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) |
66 | 21, 34 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∥ 𝑀) |
67 | | dvdsval2 15842 |
. . . . . . . . . . . 12
⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ (𝑀 gcd 𝑁) ≠ 0 ∧ 𝑀 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ↔ (𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ)) |
68 | 52, 53, 4, 67 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ↔ (𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ)) |
69 | 66, 68 | mpbid 235 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ) |
70 | | dvdsmul1 15863 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ (𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ) → 𝑁 ∥ (𝑁 · (𝑀 / (𝑀 gcd 𝑁)))) |
71 | 7, 69, 70 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∥ (𝑁 · (𝑀 / (𝑀 gcd 𝑁)))) |
72 | 60, 62 | mulcomd 10878 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 · 𝑁) = (𝑁 · 𝑀)) |
73 | 72 | oveq1d 7246 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) = ((𝑁 · 𝑀) / (𝑀 gcd 𝑁))) |
74 | 62, 60, 63, 53 | divassd 11667 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 · 𝑀) / (𝑀 gcd 𝑁)) = (𝑁 · (𝑀 / (𝑀 gcd 𝑁)))) |
75 | 73, 74 | eqtrd 2778 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) = (𝑁 · (𝑀 / (𝑀 gcd 𝑁)))) |
76 | 71, 75 | breqtrrd 5095 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) |
77 | 65, 76 | jca 515 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∧ 𝑁 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)))) |
78 | 49, 45, 77 | elrabd 3616 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ {𝑥 ∈ ℕ ∣ (𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥)}) |
79 | 46 | adantr 484 |
. . . . . . 7
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ {𝑥 ∈ ℕ ∣ (𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥)}) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℝ) |
80 | | elrabi 3608 |
. . . . . . . . 9
⊢ (𝑛 ∈ {𝑥 ∈ ℕ ∣ (𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥)} → 𝑛 ∈ ℕ) |
81 | 80 | nnred 11869 |
. . . . . . . 8
⊢ (𝑛 ∈ {𝑥 ∈ ℕ ∣ (𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥)} → 𝑛 ∈ ℝ) |
82 | 81 | adantl 485 |
. . . . . . 7
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ {𝑥 ∈ ℕ ∣ (𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥)}) → 𝑛 ∈ ℝ) |
83 | | breq2 5071 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑛 → (𝑀 ∥ 𝑥 ↔ 𝑀 ∥ 𝑛)) |
84 | | breq2 5071 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑛 → (𝑁 ∥ 𝑥 ↔ 𝑁 ∥ 𝑛)) |
85 | 83, 84 | anbi12d 634 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → ((𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥) ↔ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) |
86 | 85 | elrab 3614 |
. . . . . . . 8
⊢ (𝑛 ∈ {𝑥 ∈ ℕ ∣ (𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥)} ↔ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) |
87 | | bezout 16127 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℤ
(𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) |
88 | 21, 87 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℤ
(𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) |
89 | 88 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) |
90 | | nncn 11862 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
91 | 90 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑛 ∈
ℂ) |
92 | 1 | nncnd 11870 |
. . . . . . . . . . . . . . . . . . . . . 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 11508 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 · 𝑁) ≠ 0) |
100 | 53 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 gcd 𝑁) ≠ 0) |
101 | 91, 93, 94, 99, 100 | divdiv2d 11664 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) = ((𝑛 · (𝑀 gcd 𝑁)) / (𝑀 · 𝑁))) |
102 | 101 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑀 ∈
ℕ ∧ 𝑁 ∈
ℕ) ∧ 𝑛 ∈
ℕ) ∧ (𝑥 ∈
ℤ ∧ 𝑦 ∈
ℤ)) ∧ (𝑀 gcd
𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) = ((𝑛 · (𝑀 gcd 𝑁)) / (𝑀 · 𝑁))) |
103 | | oveq2 7239 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)) → (𝑛 · (𝑀 gcd 𝑁)) = (𝑛 · ((𝑀 · 𝑥) + (𝑁 · 𝑦)))) |
104 | 103 | oveq1d 7246 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)) → ((𝑛 · (𝑀 gcd 𝑁)) / (𝑀 · 𝑁)) = ((𝑛 · ((𝑀 · 𝑥) + (𝑁 · 𝑦))) / (𝑀 · 𝑁))) |
105 | | zcn 12205 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
106 | 105 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑥 ∈
ℂ) |
107 | 95, 106 | mulcld 10877 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 · 𝑥) ∈ ℂ) |
108 | | zcn 12205 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℂ) |
109 | 108 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑦 ∈
ℂ) |
110 | 96, 109 | mulcld 10877 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑁 · 𝑦) ∈ ℂ) |
111 | 91, 107, 110 | adddid 10881 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · ((𝑀 · 𝑥) + (𝑁 · 𝑦))) = ((𝑛 · (𝑀 · 𝑥)) + (𝑛 · (𝑁 · 𝑦)))) |
112 | 111 | oveq1d 7246 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑛 · ((𝑀 · 𝑥) + (𝑁 · 𝑦))) / (𝑀 · 𝑁)) = (((𝑛 · (𝑀 · 𝑥)) + (𝑛 · (𝑁 · 𝑦))) / (𝑀 · 𝑁))) |
113 | 91, 107 | mulcld 10877 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · (𝑀 · 𝑥)) ∈ ℂ) |
114 | 91, 110 | mulcld 10877 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · (𝑁 · 𝑦)) ∈ ℂ) |
115 | 113, 114,
93, 99 | divdird 11670 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) →
(((𝑛 · (𝑀 · 𝑥)) + (𝑛 · (𝑁 · 𝑦))) / (𝑀 · 𝑁)) = (((𝑛 · (𝑀 · 𝑥)) / (𝑀 · 𝑁)) + ((𝑛 · (𝑁 · 𝑦)) / (𝑀 · 𝑁)))) |
116 | 112, 115 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑛 · ((𝑀 · 𝑥) + (𝑁 · 𝑦))) / (𝑀 · 𝑁)) = (((𝑛 · (𝑀 · 𝑥)) / (𝑀 · 𝑁)) + ((𝑛 · (𝑁 · 𝑦)) / (𝑀 · 𝑁)))) |
117 | 104, 116 | sylan9eqr 2801 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑀 ∈
ℕ ∧ 𝑁 ∈
ℕ) ∧ 𝑛 ∈
ℕ) ∧ (𝑥 ∈
ℤ ∧ 𝑦 ∈
ℤ)) ∧ (𝑀 gcd
𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → ((𝑛 · (𝑀 gcd 𝑁)) / (𝑀 · 𝑁)) = (((𝑛 · (𝑀 · 𝑥)) / (𝑀 · 𝑁)) + ((𝑛 · (𝑁 · 𝑦)) / (𝑀 · 𝑁)))) |
118 | 91, 95, 106 | mul12d 11065 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · (𝑀 · 𝑥)) = (𝑀 · (𝑛 · 𝑥))) |
119 | 118 | oveq1d 7246 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑛 · (𝑀 · 𝑥)) / (𝑀 · 𝑁)) = ((𝑀 · (𝑛 · 𝑥)) / (𝑀 · 𝑁))) |
120 | 91, 106 | mulcld 10877 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · 𝑥) ∈ ℂ) |
121 | 120, 96, 95, 98, 97 | divcan5d 11658 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 · (𝑛 · 𝑥)) / (𝑀 · 𝑁)) = ((𝑛 · 𝑥) / 𝑁)) |
122 | 119, 121 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑛 · (𝑀 · 𝑥)) / (𝑀 · 𝑁)) = ((𝑛 · 𝑥) / 𝑁)) |
123 | 91, 96, 109 | mul12d 11065 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · (𝑁 · 𝑦)) = (𝑁 · (𝑛 · 𝑦))) |
124 | 123 | oveq1d 7246 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑛 · (𝑁 · 𝑦)) / (𝑀 · 𝑁)) = ((𝑁 · (𝑛 · 𝑦)) / (𝑀 · 𝑁))) |
125 | 72 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 · 𝑁) = (𝑁 · 𝑀)) |
126 | 125 | oveq2d 7247 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑁 · (𝑛 · 𝑦)) / (𝑀 · 𝑁)) = ((𝑁 · (𝑛 · 𝑦)) / (𝑁 · 𝑀))) |
127 | 91, 109 | mulcld 10877 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · 𝑦) ∈ ℂ) |
128 | 127, 95, 96, 97, 98 | divcan5d 11658 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑁 · (𝑛 · 𝑦)) / (𝑁 · 𝑀)) = ((𝑛 · 𝑦) / 𝑀)) |
129 | 124, 126,
128 | 3eqtrd 2782 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑛 · (𝑁 · 𝑦)) / (𝑀 · 𝑁)) = ((𝑛 · 𝑦) / 𝑀)) |
130 | 122, 129 | oveq12d 7249 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) →
(((𝑛 · (𝑀 · 𝑥)) / (𝑀 · 𝑁)) + ((𝑛 · (𝑁 · 𝑦)) / (𝑀 · 𝑁))) = (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀))) |
131 | 130 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑀 ∈
ℕ ∧ 𝑁 ∈
ℕ) ∧ 𝑛 ∈
ℕ) ∧ (𝑥 ∈
ℤ ∧ 𝑦 ∈
ℤ)) ∧ (𝑀 gcd
𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → (((𝑛 · (𝑀 · 𝑥)) / (𝑀 · 𝑁)) + ((𝑛 · (𝑁 · 𝑦)) / (𝑀 · 𝑁))) = (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀))) |
132 | 102, 117,
131 | 3eqtrd 2782 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑀 ∈
ℕ ∧ 𝑁 ∈
ℕ) ∧ 𝑛 ∈
ℕ) ∧ (𝑥 ∈
ℤ ∧ 𝑦 ∈
ℤ)) ∧ (𝑀 gcd
𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) = (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀))) |
133 | 132 | ex 416 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)) → (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) = (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)))) |
134 | 133 | adantlrr 721 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)) → (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) = (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)))) |
135 | 134 | imp 410 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑀 ∈
ℕ ∧ 𝑁 ∈
ℕ) ∧ (𝑛 ∈
ℕ ∧ (𝑀 ∥
𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) = (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀))) |
136 | 6 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑁 ∈
ℤ) |
137 | | nnz 12223 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
138 | 137 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑛 ∈
ℤ) |
139 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑥 ∈
ℤ) |
140 | | dvdsmultr1 15881 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝑁 ∥ 𝑛 → 𝑁 ∥ (𝑛 · 𝑥))) |
141 | 136, 138,
139, 140 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑁 ∥ 𝑛 → 𝑁 ∥ (𝑛 · 𝑥))) |
142 | 138, 139 | zmulcld 12312 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · 𝑥) ∈ ℤ) |
143 | | dvdsval2 15842 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ (𝑛 · 𝑥) ∈ ℤ) → (𝑁 ∥ (𝑛 · 𝑥) ↔ ((𝑛 · 𝑥) / 𝑁) ∈ ℤ)) |
144 | 136, 98, 142, 143 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑁 ∥ (𝑛 · 𝑥) ↔ ((𝑛 · 𝑥) / 𝑁) ∈ ℤ)) |
145 | 141, 144 | sylibd 242 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑁 ∥ 𝑛 → ((𝑛 · 𝑥) / 𝑁) ∈ ℤ)) |
146 | 145 | adantld 494 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛) → ((𝑛 · 𝑥) / 𝑁) ∈ ℤ)) |
147 | 146 | 3impia 1119 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛)) → ((𝑛 · 𝑥) / 𝑁) ∈ ℤ) |
148 | 3 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑀 ∈
ℤ) |
149 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑦 ∈
ℤ) |
150 | | dvdsmultr1 15881 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑀 ∥ 𝑛 → 𝑀 ∥ (𝑛 · 𝑦))) |
151 | 148, 138,
149, 150 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 ∥ 𝑛 → 𝑀 ∥ (𝑛 · 𝑦))) |
152 | 138, 149 | zmulcld 12312 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · 𝑦) ∈ ℤ) |
153 | | dvdsval2 15842 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝑛 · 𝑦) ∈ ℤ) → (𝑀 ∥ (𝑛 · 𝑦) ↔ ((𝑛 · 𝑦) / 𝑀) ∈ ℤ)) |
154 | 148, 97, 152, 153 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 ∥ (𝑛 · 𝑦) ↔ ((𝑛 · 𝑦) / 𝑀) ∈ ℤ)) |
155 | 151, 154 | sylibd 242 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 ∥ 𝑛 → ((𝑛 · 𝑦) / 𝑀) ∈ ℤ)) |
156 | 155 | adantrd 495 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛) → ((𝑛 · 𝑦) / 𝑀) ∈ ℤ)) |
157 | 156 | 3impia 1119 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛)) → ((𝑛 · 𝑦) / 𝑀) ∈ ℤ) |
158 | 147, 157 | zaddcld 12310 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛)) → (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)) ∈ ℤ) |
159 | 158 | 3expia 1123 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛) → (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)) ∈ ℤ)) |
160 | 159 | an32s 652 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ 𝑛 ∈ ℕ) → ((𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛) → (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)) ∈ ℤ)) |
161 | 160 | impr 458 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)) ∈ ℤ) |
162 | 161 | an32s 652 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)) ∈ ℤ) |
163 | 162 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑀 ∈
ℕ ∧ 𝑁 ∈
ℕ) ∧ (𝑛 ∈
ℕ ∧ (𝑀 ∥
𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)) ∈ ℤ) |
164 | 135, 163 | eqeltrd 2839 |
. . . . . . . . . . . . . 14
⊢
(((((𝑀 ∈
ℕ ∧ 𝑁 ∈
ℕ) ∧ (𝑛 ∈
ℕ ∧ (𝑀 ∥
𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) ∈ ℤ) |
165 | 45 | nnzd 12305 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℤ) |
166 | 165 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℤ) |
167 | 1 | nnne0d 11904 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 · 𝑁) ≠ 0) |
168 | 92, 63, 167, 53 | divne0d 11648 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ≠ 0) |
169 | 168 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ≠ 0) |
170 | 138 | adantlrr 721 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑛 ∈ ℤ) |
171 | | dvdsval2 15842 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℤ ∧ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ≠ 0 ∧ 𝑛 ∈ ℤ) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) ∈ ℤ)) |
172 | 166, 169,
170, 171 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) ∈ ℤ)) |
173 | 172 | adantr 484 |
. . . . . . . . . . . . . 14
⊢
(((((𝑀 ∈
ℕ ∧ 𝑁 ∈
ℕ) ∧ (𝑛 ∈
ℕ ∧ (𝑀 ∥
𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) ∈ ℤ)) |
174 | 164, 173 | mpbird 260 |
. . . . . . . . . . . . 13
⊢
(((((𝑀 ∈
ℕ ∧ 𝑁 ∈
ℕ) ∧ (𝑛 ∈
ℕ ∧ (𝑀 ∥
𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛) |
175 | 174 | ex 416 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛)) |
176 | 175 | reximdvva 3204 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛)) |
177 | 89, 176 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛) |
178 | | 1z 12231 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
179 | | ne0i 4263 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℤ → ℤ ≠ ∅) |
180 | | r19.9rzv 4425 |
. . . . . . . . . . . 12
⊢ (ℤ
≠ ∅ → (((𝑀
· 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ ∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛)) |
181 | 178, 179,
180 | mp2b 10 |
. . . . . . . . . . 11
⊢ (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ ∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛) |
182 | | r19.9rzv 4425 |
. . . . . . . . . . . 12
⊢ (ℤ
≠ ∅ → (∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛)) |
183 | 178, 179,
182 | mp2b 10 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛) |
184 | 181, 183 | bitri 278 |
. . . . . . . . . 10
⊢ (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛) |
185 | 177, 184 | sylibr 237 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛) |
186 | 165 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℤ) |
187 | | simprl 771 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → 𝑛 ∈ ℕ) |
188 | | dvdsle 15895 |
. . . . . . . . . 10
⊢ ((((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℤ ∧ 𝑛 ∈ ℕ) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ≤ 𝑛)) |
189 | 186, 187,
188 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ≤ 𝑛)) |
190 | 185, 189 | mpd 15 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ≤ 𝑛) |
191 | 86, 190 | sylan2b 597 |
. . . . . . 7
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ {𝑥 ∈ ℕ ∣ (𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥)}) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ≤ 𝑛) |
192 | 79, 82, 191 | lensymd 11007 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ {𝑥 ∈ ℕ ∣ (𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥)}) → ¬ 𝑛 < ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) |
193 | 32, 46, 78, 192 | infmin 9134 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
inf({𝑥 ∈ ℕ
∣ (𝑀 ∥ 𝑥 ∧ 𝑁 ∥ 𝑥)}, ℝ, < ) = ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) |
194 | 30, 193 | eqtr2d 2779 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) = (𝑀 lcm 𝑁)) |
195 | 194, 45 | eqeltrrd 2840 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 lcm 𝑁) ∈ ℕ) |
196 | 195 | nncnd 11870 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 lcm 𝑁) ∈ ℂ) |
197 | 92, 196, 63, 53 | divmul3d 11666 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) = (𝑀 lcm 𝑁) ↔ (𝑀 · 𝑁) = ((𝑀 lcm 𝑁) · (𝑀 gcd 𝑁)))) |
198 | 194, 197 | mpbid 235 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 · 𝑁) = ((𝑀 lcm 𝑁) · (𝑀 gcd 𝑁))) |
199 | 20, 198 | eqtr2d 2779 |
. 2
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 lcm 𝑁) · (𝑀 gcd 𝑁)) = (abs‘(𝑀 · 𝑁))) |
200 | | simprl 771 |
. . . 4
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℕ ∧ (𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾))) → 𝐾 ∈ ℕ) |
201 | | eleq1 2826 |
. . . . . . . 8
⊢ (𝑛 = 𝐾 → (𝑛 ∈ ℕ ↔ 𝐾 ∈ ℕ)) |
202 | | breq2 5071 |
. . . . . . . . 9
⊢ (𝑛 = 𝐾 → (𝑀 ∥ 𝑛 ↔ 𝑀 ∥ 𝐾)) |
203 | | breq2 5071 |
. . . . . . . . 9
⊢ (𝑛 = 𝐾 → (𝑁 ∥ 𝑛 ↔ 𝑁 ∥ 𝐾)) |
204 | 202, 203 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑛 = 𝐾 → ((𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛) ↔ (𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾))) |
205 | 201, 204 | anbi12d 634 |
. . . . . . 7
⊢ (𝑛 = 𝐾 → ((𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛)) ↔ (𝐾 ∈ ℕ ∧ (𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾)))) |
206 | 205 | anbi2d 632 |
. . . . . 6
⊢ (𝑛 = 𝐾 → (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) ↔ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℕ ∧ (𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾))))) |
207 | | breq2 5071 |
. . . . . 6
⊢ (𝑛 = 𝐾 → ((𝑀 lcm 𝑁) ∥ 𝑛 ↔ (𝑀 lcm 𝑁) ∥ 𝐾)) |
208 | 206, 207 | imbi12d 348 |
. . . . 5
⊢ (𝑛 = 𝐾 → ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → (𝑀 lcm 𝑁) ∥ 𝑛) ↔ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℕ ∧ (𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾))) → (𝑀 lcm 𝑁) ∥ 𝐾))) |
209 | 194 | breq1d 5077 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ (𝑀 lcm 𝑁) ∥ 𝑛)) |
210 | 209 | adantr 484 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ (𝑀 lcm 𝑁) ∥ 𝑛)) |
211 | 185, 210 | mpbid 235 |
. . . . 5
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛))) → (𝑀 lcm 𝑁) ∥ 𝑛) |
212 | 208, 211 | vtoclg 3493 |
. . . 4
⊢ (𝐾 ∈ ℕ → (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℕ ∧ (𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾))) → (𝑀 lcm 𝑁) ∥ 𝐾)) |
213 | 200, 212 | mpcom 38 |
. . 3
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℕ ∧ (𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾))) → (𝑀 lcm 𝑁) ∥ 𝐾) |
214 | 213 | ex 416 |
. 2
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐾 ∈ ℕ ∧ (𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾)) → (𝑀 lcm 𝑁) ∥ 𝐾)) |
215 | 199, 214 | jca 515 |
1
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 lcm 𝑁) · (𝑀 gcd 𝑁)) = (abs‘(𝑀 · 𝑁)) ∧ ((𝐾 ∈ ℕ ∧ (𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾)) → (𝑀 lcm 𝑁) ∥ 𝐾))) |