Step |
Hyp |
Ref |
Expression |
1 |
|
elfzelz |
⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∈ ℤ ) |
2 |
1
|
adantl |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∈ ℤ ) |
3 |
|
nnnn0 |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 ) |
4 |
3
|
faccld |
⊢ ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) ∈ ℕ ) |
5 |
4
|
nnzd |
⊢ ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) ∈ ℤ ) |
6 |
5
|
adantr |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ( ! ‘ 𝑁 ) ∈ ℤ ) |
7 |
|
elfzuz |
⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∈ ( ℤ≥ ‘ 2 ) ) |
8 |
|
eluz2nn |
⊢ ( 𝐼 ∈ ( ℤ≥ ‘ 2 ) → 𝐼 ∈ ℕ ) |
9 |
7 8
|
syl |
⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∈ ℕ ) |
10 |
|
elfzuz3 |
⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐼 ) ) |
11 |
9 10
|
jca |
⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → ( 𝐼 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐼 ) ) ) |
12 |
11
|
adantl |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ( 𝐼 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐼 ) ) ) |
13 |
|
dvdsfac |
⊢ ( ( 𝐼 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐼 ) ) → 𝐼 ∥ ( ! ‘ 𝑁 ) ) |
14 |
12 13
|
syl |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∥ ( ! ‘ 𝑁 ) ) |
15 |
|
iddvds |
⊢ ( 𝐼 ∈ ℤ → 𝐼 ∥ 𝐼 ) |
16 |
1 15
|
syl |
⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∥ 𝐼 ) |
17 |
16
|
adantl |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∥ 𝐼 ) |
18 |
2 6 2 14 17
|
dvds2addd |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∥ ( ( ! ‘ 𝑁 ) + 𝐼 ) ) |