Step | Hyp | Ref
| Expression |
1 | | fveq2 6717 |
. . . . 5
⊢ (𝑥 = 𝐾 → (!‘𝑥) = (!‘𝐾)) |
2 | 1 | breq2d 5065 |
. . . 4
⊢ (𝑥 = 𝐾 → (𝐾 ∥ (!‘𝑥) ↔ 𝐾 ∥ (!‘𝐾))) |
3 | 2 | imbi2d 344 |
. . 3
⊢ (𝑥 = 𝐾 → ((𝐾 ∈ ℕ → 𝐾 ∥ (!‘𝑥)) ↔ (𝐾 ∈ ℕ → 𝐾 ∥ (!‘𝐾)))) |
4 | | fveq2 6717 |
. . . . 5
⊢ (𝑥 = 𝑦 → (!‘𝑥) = (!‘𝑦)) |
5 | 4 | breq2d 5065 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝐾 ∥ (!‘𝑥) ↔ 𝐾 ∥ (!‘𝑦))) |
6 | 5 | imbi2d 344 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝐾 ∈ ℕ → 𝐾 ∥ (!‘𝑥)) ↔ (𝐾 ∈ ℕ → 𝐾 ∥ (!‘𝑦)))) |
7 | | fveq2 6717 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (!‘𝑥) = (!‘(𝑦 + 1))) |
8 | 7 | breq2d 5065 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → (𝐾 ∥ (!‘𝑥) ↔ 𝐾 ∥ (!‘(𝑦 + 1)))) |
9 | 8 | imbi2d 344 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → ((𝐾 ∈ ℕ → 𝐾 ∥ (!‘𝑥)) ↔ (𝐾 ∈ ℕ → 𝐾 ∥ (!‘(𝑦 + 1))))) |
10 | | fveq2 6717 |
. . . . 5
⊢ (𝑥 = 𝑁 → (!‘𝑥) = (!‘𝑁)) |
11 | 10 | breq2d 5065 |
. . . 4
⊢ (𝑥 = 𝑁 → (𝐾 ∥ (!‘𝑥) ↔ 𝐾 ∥ (!‘𝑁))) |
12 | 11 | imbi2d 344 |
. . 3
⊢ (𝑥 = 𝑁 → ((𝐾 ∈ ℕ → 𝐾 ∥ (!‘𝑥)) ↔ (𝐾 ∈ ℕ → 𝐾 ∥ (!‘𝑁)))) |
13 | | nnm1nn0 12131 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈
ℕ0) |
14 | 13 | faccld 13850 |
. . . . . 6
⊢ (𝐾 ∈ ℕ →
(!‘(𝐾 − 1))
∈ ℕ) |
15 | 14 | nnzd 12281 |
. . . . 5
⊢ (𝐾 ∈ ℕ →
(!‘(𝐾 − 1))
∈ ℤ) |
16 | | nnz 12199 |
. . . . 5
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℤ) |
17 | | dvdsmul2 15840 |
. . . . 5
⊢
(((!‘(𝐾
− 1)) ∈ ℤ ∧ 𝐾 ∈ ℤ) → 𝐾 ∥ ((!‘(𝐾 − 1)) · 𝐾)) |
18 | 15, 16, 17 | syl2anc 587 |
. . . 4
⊢ (𝐾 ∈ ℕ → 𝐾 ∥ ((!‘(𝐾 − 1)) · 𝐾)) |
19 | | facnn2 13848 |
. . . 4
⊢ (𝐾 ∈ ℕ →
(!‘𝐾) =
((!‘(𝐾 − 1))
· 𝐾)) |
20 | 18, 19 | breqtrrd 5081 |
. . 3
⊢ (𝐾 ∈ ℕ → 𝐾 ∥ (!‘𝐾)) |
21 | 16 | adantl 485 |
. . . . . . 7
⊢ ((𝑦 ∈
(ℤ≥‘𝐾) ∧ 𝐾 ∈ ℕ) → 𝐾 ∈ ℤ) |
22 | | elnnuz 12478 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℕ ↔ 𝐾 ∈
(ℤ≥‘1)) |
23 | | uztrn 12456 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈
(ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘1))
→ 𝑦 ∈
(ℤ≥‘1)) |
24 | 22, 23 | sylan2b 597 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈
(ℤ≥‘𝐾) ∧ 𝐾 ∈ ℕ) → 𝑦 ∈
(ℤ≥‘1)) |
25 | | elnnuz 12478 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ ↔ 𝑦 ∈
(ℤ≥‘1)) |
26 | 24, 25 | sylibr 237 |
. . . . . . . . . 10
⊢ ((𝑦 ∈
(ℤ≥‘𝐾) ∧ 𝐾 ∈ ℕ) → 𝑦 ∈ ℕ) |
27 | 26 | nnnn0d 12150 |
. . . . . . . . 9
⊢ ((𝑦 ∈
(ℤ≥‘𝐾) ∧ 𝐾 ∈ ℕ) → 𝑦 ∈ ℕ0) |
28 | 27 | faccld 13850 |
. . . . . . . 8
⊢ ((𝑦 ∈
(ℤ≥‘𝐾) ∧ 𝐾 ∈ ℕ) → (!‘𝑦) ∈
ℕ) |
29 | 28 | nnzd 12281 |
. . . . . . 7
⊢ ((𝑦 ∈
(ℤ≥‘𝐾) ∧ 𝐾 ∈ ℕ) → (!‘𝑦) ∈
ℤ) |
30 | 26 | nnzd 12281 |
. . . . . . . 8
⊢ ((𝑦 ∈
(ℤ≥‘𝐾) ∧ 𝐾 ∈ ℕ) → 𝑦 ∈ ℤ) |
31 | 30 | peano2zd 12285 |
. . . . . . 7
⊢ ((𝑦 ∈
(ℤ≥‘𝐾) ∧ 𝐾 ∈ ℕ) → (𝑦 + 1) ∈ ℤ) |
32 | | dvdsmultr1 15857 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧
(!‘𝑦) ∈ ℤ
∧ (𝑦 + 1) ∈
ℤ) → (𝐾 ∥
(!‘𝑦) → 𝐾 ∥ ((!‘𝑦) · (𝑦 + 1)))) |
33 | 21, 29, 31, 32 | syl3anc 1373 |
. . . . . 6
⊢ ((𝑦 ∈
(ℤ≥‘𝐾) ∧ 𝐾 ∈ ℕ) → (𝐾 ∥ (!‘𝑦) → 𝐾 ∥ ((!‘𝑦) · (𝑦 + 1)))) |
34 | | facp1 13844 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ0
→ (!‘(𝑦 + 1)) =
((!‘𝑦) ·
(𝑦 + 1))) |
35 | 27, 34 | syl 17 |
. . . . . . 7
⊢ ((𝑦 ∈
(ℤ≥‘𝐾) ∧ 𝐾 ∈ ℕ) → (!‘(𝑦 + 1)) = ((!‘𝑦) · (𝑦 + 1))) |
36 | 35 | breq2d 5065 |
. . . . . 6
⊢ ((𝑦 ∈
(ℤ≥‘𝐾) ∧ 𝐾 ∈ ℕ) → (𝐾 ∥ (!‘(𝑦 + 1)) ↔ 𝐾 ∥ ((!‘𝑦) · (𝑦 + 1)))) |
37 | 33, 36 | sylibrd 262 |
. . . . 5
⊢ ((𝑦 ∈
(ℤ≥‘𝐾) ∧ 𝐾 ∈ ℕ) → (𝐾 ∥ (!‘𝑦) → 𝐾 ∥ (!‘(𝑦 + 1)))) |
38 | 37 | ex 416 |
. . . 4
⊢ (𝑦 ∈
(ℤ≥‘𝐾) → (𝐾 ∈ ℕ → (𝐾 ∥ (!‘𝑦) → 𝐾 ∥ (!‘(𝑦 + 1))))) |
39 | 38 | a2d 29 |
. . 3
⊢ (𝑦 ∈
(ℤ≥‘𝐾) → ((𝐾 ∈ ℕ → 𝐾 ∥ (!‘𝑦)) → (𝐾 ∈ ℕ → 𝐾 ∥ (!‘(𝑦 + 1))))) |
40 | 3, 6, 9, 12, 20, 39 | uzind4i 12506 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘𝐾) → (𝐾 ∈ ℕ → 𝐾 ∥ (!‘𝑁))) |
41 | 40 | impcom 411 |
1
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘𝐾)) → 𝐾 ∥ (!‘𝑁)) |