Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) |
2 |
|
elfzel1 |
⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑀 ∈ ℤ ) |
3 |
2
|
adantl |
⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ∈ ℤ ) |
4 |
|
elfzel2 |
⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ℤ ) |
5 |
4
|
adantl |
⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑁 ∈ ℤ ) |
6 |
|
simpl |
⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐽 ∈ ℤ ) |
7 |
|
elfzelz |
⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ∈ ℤ ) |
8 |
7
|
adantl |
⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐾 ∈ ℤ ) |
9 |
|
fzrev2 |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐽 − 𝐾 ) ∈ ( ( 𝐽 − 𝑁 ) ... ( 𝐽 − 𝑀 ) ) ) ) |
10 |
3 5 6 8 9
|
syl22anc |
⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐽 − 𝐾 ) ∈ ( ( 𝐽 − 𝑁 ) ... ( 𝐽 − 𝑀 ) ) ) ) |
11 |
1 10
|
mpbid |
⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐽 − 𝐾 ) ∈ ( ( 𝐽 − 𝑁 ) ... ( 𝐽 − 𝑀 ) ) ) |