| Step | Hyp | Ref
| Expression |
| 1 | | breq1 5146 |
. . . 4
⊢ (𝑘 = (𝑀 + 𝐾) → (𝑘 ∥ (lcm‘(1...𝑁)) ↔ (𝑀 + 𝐾) ∥ (lcm‘(1...𝑁)))) |
| 2 | | fzssz 13566 |
. . . . . . 7
⊢
(1...𝑁) ⊆
ℤ |
| 3 | | fzfi 14013 |
. . . . . . 7
⊢
(1...𝑁) ∈
Fin |
| 4 | 2, 3 | pm3.2i 470 |
. . . . . 6
⊢
((1...𝑁) ⊆
ℤ ∧ (1...𝑁)
∈ Fin) |
| 5 | 4 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((1...𝑁) ⊆ ℤ ∧ (1...𝑁) ∈ Fin)) |
| 6 | | dvdslcmf 16668 |
. . . . 5
⊢
(((1...𝑁) ⊆
ℤ ∧ (1...𝑁)
∈ Fin) → ∀𝑘 ∈ (1...𝑁)𝑘 ∥ (lcm‘(1...𝑁))) |
| 7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)𝑘 ∥ (lcm‘(1...𝑁))) |
| 8 | | 1zzd 12648 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℤ) |
| 9 | | lcmineqlem4.2 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 10 | 9 | nnzd 12640 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 11 | | 0zd 12625 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℤ) |
| 12 | | lcmineqlem4.1 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 13 | 12 | nnzd 12640 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 14 | 13, 10 | zsubcld 12727 |
. . . . 5
⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℤ) |
| 15 | 9 | nnred 12281 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 16 | 15 | leidd 11829 |
. . . . . 6
⊢ (𝜑 → 𝑀 ≤ 𝑀) |
| 17 | | fznn 13632 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (1...𝑀) ↔ (𝑀 ∈ ℕ ∧ 𝑀 ≤ 𝑀))) |
| 18 | 10, 17 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑀 ∈ (1...𝑀) ↔ (𝑀 ∈ ℕ ∧ 𝑀 ≤ 𝑀))) |
| 19 | 9, 16, 18 | mpbir2and 713 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ (1...𝑀)) |
| 20 | | lcmineqlem4.4 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ (0...(𝑁 − 𝑀))) |
| 21 | | 1cnd 11256 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℂ) |
| 22 | 21 | addridd 11461 |
. . . . . 6
⊢ (𝜑 → (1 + 0) =
1) |
| 23 | 22 | eqcomd 2743 |
. . . . 5
⊢ (𝜑 → 1 = (1 +
0)) |
| 24 | 12 | nncnd 12282 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 25 | 9 | nncnd 12282 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℂ) |
| 26 | 24, 25 | npcand 11624 |
. . . . . 6
⊢ (𝜑 → ((𝑁 − 𝑀) + 𝑀) = 𝑁) |
| 27 | | eqcom 2744 |
. . . . . . . . 9
⊢ (((𝑁 − 𝑀) + 𝑀) = 𝑁 ↔ 𝑁 = ((𝑁 − 𝑀) + 𝑀)) |
| 28 | 27 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (((𝑁 − 𝑀) + 𝑀) = 𝑁 ↔ 𝑁 = ((𝑁 − 𝑀) + 𝑀))) |
| 29 | 24, 25 | jca 511 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ)) |
| 30 | | subcl 11507 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (𝑁 − 𝑀) ∈ ℂ) |
| 31 | 29, 30 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℂ) |
| 32 | 31, 25 | jca 511 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁 − 𝑀) ∈ ℂ ∧ 𝑀 ∈ ℂ)) |
| 33 | | addcom 11447 |
. . . . . . . . . 10
⊢ (((𝑁 − 𝑀) ∈ ℂ ∧ 𝑀 ∈ ℂ) → ((𝑁 − 𝑀) + 𝑀) = (𝑀 + (𝑁 − 𝑀))) |
| 34 | 32, 33 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 − 𝑀) + 𝑀) = (𝑀 + (𝑁 − 𝑀))) |
| 35 | | eqeq2 2749 |
. . . . . . . . 9
⊢ (((𝑁 − 𝑀) + 𝑀) = (𝑀 + (𝑁 − 𝑀)) → (𝑁 = ((𝑁 − 𝑀) + 𝑀) ↔ 𝑁 = (𝑀 + (𝑁 − 𝑀)))) |
| 36 | 34, 35 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 = ((𝑁 − 𝑀) + 𝑀) ↔ 𝑁 = (𝑀 + (𝑁 − 𝑀)))) |
| 37 | 28, 36 | bitrd 279 |
. . . . . . 7
⊢ (𝜑 → (((𝑁 − 𝑀) + 𝑀) = 𝑁 ↔ 𝑁 = (𝑀 + (𝑁 − 𝑀)))) |
| 38 | 37 | pm5.74i 271 |
. . . . . 6
⊢ ((𝜑 → ((𝑁 − 𝑀) + 𝑀) = 𝑁) ↔ (𝜑 → 𝑁 = (𝑀 + (𝑁 − 𝑀)))) |
| 39 | 26, 38 | mpbi 230 |
. . . . 5
⊢ (𝜑 → 𝑁 = (𝑀 + (𝑁 − 𝑀))) |
| 40 | 8, 10, 11, 14, 19, 20, 23, 39 | fzadd2d 41979 |
. . . 4
⊢ (𝜑 → (𝑀 + 𝐾) ∈ (1...𝑁)) |
| 41 | 1, 7, 40 | rspcdva 3623 |
. . 3
⊢ (𝜑 → (𝑀 + 𝐾) ∥ (lcm‘(1...𝑁))) |
| 42 | | fz1ssnn 13595 |
. . . . . . 7
⊢
(1...𝑁) ⊆
ℕ |
| 43 | 42, 3 | pm3.2i 470 |
. . . . . 6
⊢
((1...𝑁) ⊆
ℕ ∧ (1...𝑁)
∈ Fin) |
| 44 | | lcmfnncl 16666 |
. . . . . 6
⊢
(((1...𝑁) ⊆
ℕ ∧ (1...𝑁)
∈ Fin) → (lcm‘(1...𝑁)) ∈ ℕ) |
| 45 | 43, 44 | ax-mp 5 |
. . . . 5
⊢
(lcm‘(1...𝑁)) ∈ ℕ |
| 46 | 45 | a1i 11 |
. . . 4
⊢ (𝜑 →
(lcm‘(1...𝑁))
∈ ℕ) |
| 47 | | elfznn0 13660 |
. . . . . 6
⊢ (𝐾 ∈ (0...(𝑁 − 𝑀)) → 𝐾 ∈
ℕ0) |
| 48 | 20, 47 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
| 49 | | nnnn0addcl 12556 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐾 ∈ ℕ0)
→ (𝑀 + 𝐾) ∈
ℕ) |
| 50 | 9, 48, 49 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝑀 + 𝐾) ∈ ℕ) |
| 51 | | nndivdvds 16299 |
. . . 4
⊢
(((lcm‘(1...𝑁)) ∈ ℕ ∧ (𝑀 + 𝐾) ∈ ℕ) → ((𝑀 + 𝐾) ∥ (lcm‘(1...𝑁)) ↔
((lcm‘(1...𝑁))
/ (𝑀 + 𝐾)) ∈ ℕ)) |
| 52 | 46, 50, 51 | syl2anc 584 |
. . 3
⊢ (𝜑 → ((𝑀 + 𝐾) ∥ (lcm‘(1...𝑁)) ↔
((lcm‘(1...𝑁))
/ (𝑀 + 𝐾)) ∈ ℕ)) |
| 53 | 41, 52 | mpbid 232 |
. 2
⊢ (𝜑 →
((lcm‘(1...𝑁))
/ (𝑀 + 𝐾)) ∈ ℕ) |
| 54 | 53 | nnzd 12640 |
1
⊢ (𝜑 →
((lcm‘(1...𝑁))
/ (𝑀 + 𝐾)) ∈ ℤ) |