Step | Hyp | Ref
| Expression |
1 | | breq1 5028 |
. . . 4
⊢ (𝑘 = (𝑀 + 𝐾) → (𝑘 ∥ (lcm‘(1...𝑁)) ↔ (𝑀 + 𝐾) ∥ (lcm‘(1...𝑁)))) |
2 | | fzssz 12943 |
. . . . . . 7
⊢
(1...𝑁) ⊆
ℤ |
3 | | fzfi 13374 |
. . . . . . 7
⊢
(1...𝑁) ∈
Fin |
4 | 2, 3 | pm3.2i 475 |
. . . . . 6
⊢
((1...𝑁) ⊆
ℤ ∧ (1...𝑁)
∈ Fin) |
5 | 4 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((1...𝑁) ⊆ ℤ ∧ (1...𝑁) ∈ Fin)) |
6 | | dvdslcmf 16012 |
. . . . 5
⊢
(((1...𝑁) ⊆
ℤ ∧ (1...𝑁)
∈ Fin) → ∀𝑘 ∈ (1...𝑁)𝑘 ∥ (lcm‘(1...𝑁))) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)𝑘 ∥ (lcm‘(1...𝑁))) |
8 | | 1zzd 12037 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℤ) |
9 | | lcmineqlem4.2 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
10 | 9 | nnzd 12110 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
11 | | 0zd 12017 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℤ) |
12 | | lcmineqlem4.1 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) |
13 | 12 | nnzd 12110 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℤ) |
14 | 13, 10 | zsubcld 12116 |
. . . . 5
⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℤ) |
15 | 9 | nnred 11674 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℝ) |
16 | 15 | leidd 11229 |
. . . . . 6
⊢ (𝜑 → 𝑀 ≤ 𝑀) |
17 | | fznn 13009 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (1...𝑀) ↔ (𝑀 ∈ ℕ ∧ 𝑀 ≤ 𝑀))) |
18 | 10, 17 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑀 ∈ (1...𝑀) ↔ (𝑀 ∈ ℕ ∧ 𝑀 ≤ 𝑀))) |
19 | 9, 16, 18 | mpbir2and 713 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ (1...𝑀)) |
20 | | lcmineqlem4.4 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ (0...(𝑁 − 𝑀))) |
21 | | 1cnd 10659 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℂ) |
22 | 21 | addid1d 10863 |
. . . . . 6
⊢ (𝜑 → (1 + 0) =
1) |
23 | 22 | eqcomd 2765 |
. . . . 5
⊢ (𝜑 → 1 = (1 +
0)) |
24 | 12 | nncnd 11675 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℂ) |
25 | 9 | nncnd 11675 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℂ) |
26 | 24, 25 | npcand 11024 |
. . . . . 6
⊢ (𝜑 → ((𝑁 − 𝑀) + 𝑀) = 𝑁) |
27 | | eqcom 2766 |
. . . . . . . . 9
⊢ (((𝑁 − 𝑀) + 𝑀) = 𝑁 ↔ 𝑁 = ((𝑁 − 𝑀) + 𝑀)) |
28 | 27 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (((𝑁 − 𝑀) + 𝑀) = 𝑁 ↔ 𝑁 = ((𝑁 − 𝑀) + 𝑀))) |
29 | 24, 25 | jca 516 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ)) |
30 | | subcl 10908 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (𝑁 − 𝑀) ∈ ℂ) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℂ) |
32 | 31, 25 | jca 516 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁 − 𝑀) ∈ ℂ ∧ 𝑀 ∈ ℂ)) |
33 | | addcom 10849 |
. . . . . . . . . 10
⊢ (((𝑁 − 𝑀) ∈ ℂ ∧ 𝑀 ∈ ℂ) → ((𝑁 − 𝑀) + 𝑀) = (𝑀 + (𝑁 − 𝑀))) |
34 | 32, 33 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 − 𝑀) + 𝑀) = (𝑀 + (𝑁 − 𝑀))) |
35 | | eqeq2 2771 |
. . . . . . . . 9
⊢ (((𝑁 − 𝑀) + 𝑀) = (𝑀 + (𝑁 − 𝑀)) → (𝑁 = ((𝑁 − 𝑀) + 𝑀) ↔ 𝑁 = (𝑀 + (𝑁 − 𝑀)))) |
36 | 34, 35 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 = ((𝑁 − 𝑀) + 𝑀) ↔ 𝑁 = (𝑀 + (𝑁 − 𝑀)))) |
37 | 28, 36 | bitrd 282 |
. . . . . . 7
⊢ (𝜑 → (((𝑁 − 𝑀) + 𝑀) = 𝑁 ↔ 𝑁 = (𝑀 + (𝑁 − 𝑀)))) |
38 | 37 | pm5.74i 274 |
. . . . . 6
⊢ ((𝜑 → ((𝑁 − 𝑀) + 𝑀) = 𝑁) ↔ (𝜑 → 𝑁 = (𝑀 + (𝑁 − 𝑀)))) |
39 | 26, 38 | mpbi 233 |
. . . . 5
⊢ (𝜑 → 𝑁 = (𝑀 + (𝑁 − 𝑀))) |
40 | 8, 10, 11, 14, 19, 20, 23, 39 | fzadd2d 39530 |
. . . 4
⊢ (𝜑 → (𝑀 + 𝐾) ∈ (1...𝑁)) |
41 | 1, 7, 40 | rspcdva 3541 |
. . 3
⊢ (𝜑 → (𝑀 + 𝐾) ∥ (lcm‘(1...𝑁))) |
42 | | fz1ssnn 12972 |
. . . . . . 7
⊢
(1...𝑁) ⊆
ℕ |
43 | 42, 3 | pm3.2i 475 |
. . . . . 6
⊢
((1...𝑁) ⊆
ℕ ∧ (1...𝑁)
∈ Fin) |
44 | | lcmfnncl 16010 |
. . . . . 6
⊢
(((1...𝑁) ⊆
ℕ ∧ (1...𝑁)
∈ Fin) → (lcm‘(1...𝑁)) ∈ ℕ) |
45 | 43, 44 | ax-mp 5 |
. . . . 5
⊢
(lcm‘(1...𝑁)) ∈ ℕ |
46 | 45 | a1i 11 |
. . . 4
⊢ (𝜑 →
(lcm‘(1...𝑁))
∈ ℕ) |
47 | | elfznn0 13034 |
. . . . . 6
⊢ (𝐾 ∈ (0...(𝑁 − 𝑀)) → 𝐾 ∈
ℕ0) |
48 | 20, 47 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
49 | | nnnn0addcl 11949 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ ℕ0)
→ (𝑀 + 𝐾) ∈
ℕ) |
50 | 9, 48, 49 | syl2anc 588 |
. . . 4
⊢ (𝜑 → (𝑀 + 𝐾) ∈ ℕ) |
51 | | nndivdvds 15649 |
. . . 4
⊢
(((lcm‘(1...𝑁)) ∈ ℕ ∧ (𝑀 + 𝐾) ∈ ℕ) → ((𝑀 + 𝐾) ∥ (lcm‘(1...𝑁)) ↔
((lcm‘(1...𝑁))
/ (𝑀 + 𝐾)) ∈ ℕ)) |
52 | 46, 50, 51 | syl2anc 588 |
. . 3
⊢ (𝜑 → ((𝑀 + 𝐾) ∥ (lcm‘(1...𝑁)) ↔
((lcm‘(1...𝑁))
/ (𝑀 + 𝐾)) ∈ ℕ)) |
53 | 41, 52 | mpbid 235 |
. 2
⊢ (𝜑 →
((lcm‘(1...𝑁))
/ (𝑀 + 𝐾)) ∈ ℕ) |
54 | 53 | nnzd 12110 |
1
⊢ (𝜑 →
((lcm‘(1...𝑁))
/ (𝑀 + 𝐾)) ∈ ℤ) |