Step |
Hyp |
Ref |
Expression |
1 |
|
zre |
⊢ ( 𝐽 ∈ ℤ → 𝐽 ∈ ℝ ) |
2 |
|
zre |
⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ ) |
3 |
|
zre |
⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ ) |
4 |
|
suble |
⊢ ( ( 𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝐽 − 𝐾 ) ≤ 𝑁 ↔ ( 𝐽 − 𝑁 ) ≤ 𝐾 ) ) |
5 |
1 2 3 4
|
syl3an |
⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐽 − 𝐾 ) ≤ 𝑁 ↔ ( 𝐽 − 𝑁 ) ≤ 𝐾 ) ) |
6 |
5
|
3comr |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝐽 − 𝐾 ) ≤ 𝑁 ↔ ( 𝐽 − 𝑁 ) ≤ 𝐾 ) ) |
7 |
6
|
3expb |
⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( 𝐽 − 𝐾 ) ≤ 𝑁 ↔ ( 𝐽 − 𝑁 ) ≤ 𝐾 ) ) |
8 |
7
|
adantll |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( 𝐽 − 𝐾 ) ≤ 𝑁 ↔ ( 𝐽 − 𝑁 ) ≤ 𝐾 ) ) |
9 |
|
zre |
⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ ) |
10 |
|
lesub |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝑀 ≤ ( 𝐽 − 𝐾 ) ↔ 𝐾 ≤ ( 𝐽 − 𝑀 ) ) ) |
11 |
9 1 2 10
|
syl3an |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ≤ ( 𝐽 − 𝐾 ) ↔ 𝐾 ≤ ( 𝐽 − 𝑀 ) ) ) |
12 |
11
|
3expb |
⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝑀 ≤ ( 𝐽 − 𝐾 ) ↔ 𝐾 ≤ ( 𝐽 − 𝑀 ) ) ) |
13 |
12
|
adantlr |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝑀 ≤ ( 𝐽 − 𝐾 ) ↔ 𝐾 ≤ ( 𝐽 − 𝑀 ) ) ) |
14 |
8 13
|
anbi12d |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( ( 𝐽 − 𝐾 ) ≤ 𝑁 ∧ 𝑀 ≤ ( 𝐽 − 𝐾 ) ) ↔ ( ( 𝐽 − 𝑁 ) ≤ 𝐾 ∧ 𝐾 ≤ ( 𝐽 − 𝑀 ) ) ) ) |
15 |
|
ancom |
⊢ ( ( ( 𝐽 − 𝐾 ) ≤ 𝑁 ∧ 𝑀 ≤ ( 𝐽 − 𝐾 ) ) ↔ ( 𝑀 ≤ ( 𝐽 − 𝐾 ) ∧ ( 𝐽 − 𝐾 ) ≤ 𝑁 ) ) |
16 |
14 15
|
bitr3di |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( ( 𝐽 − 𝑁 ) ≤ 𝐾 ∧ 𝐾 ≤ ( 𝐽 − 𝑀 ) ) ↔ ( 𝑀 ≤ ( 𝐽 − 𝐾 ) ∧ ( 𝐽 − 𝐾 ) ≤ 𝑁 ) ) ) |
17 |
|
simprr |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → 𝐾 ∈ ℤ ) |
18 |
|
zsubcl |
⊢ ( ( 𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐽 − 𝑁 ) ∈ ℤ ) |
19 |
18
|
ancoms |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( 𝐽 − 𝑁 ) ∈ ℤ ) |
20 |
19
|
ad2ant2lr |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐽 − 𝑁 ) ∈ ℤ ) |
21 |
|
zsubcl |
⊢ ( ( 𝐽 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐽 − 𝑀 ) ∈ ℤ ) |
22 |
21
|
ancoms |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( 𝐽 − 𝑀 ) ∈ ℤ ) |
23 |
22
|
ad2ant2r |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐽 − 𝑀 ) ∈ ℤ ) |
24 |
|
elfz |
⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝐽 − 𝑁 ) ∈ ℤ ∧ ( 𝐽 − 𝑀 ) ∈ ℤ ) → ( 𝐾 ∈ ( ( 𝐽 − 𝑁 ) ... ( 𝐽 − 𝑀 ) ) ↔ ( ( 𝐽 − 𝑁 ) ≤ 𝐾 ∧ 𝐾 ≤ ( 𝐽 − 𝑀 ) ) ) ) |
25 |
17 20 23 24
|
syl3anc |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐾 ∈ ( ( 𝐽 − 𝑁 ) ... ( 𝐽 − 𝑀 ) ) ↔ ( ( 𝐽 − 𝑁 ) ≤ 𝐾 ∧ 𝐾 ≤ ( 𝐽 − 𝑀 ) ) ) ) |
26 |
|
zsubcl |
⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐽 − 𝐾 ) ∈ ℤ ) |
27 |
26
|
adantl |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐽 − 𝐾 ) ∈ ℤ ) |
28 |
|
simpll |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → 𝑀 ∈ ℤ ) |
29 |
|
simplr |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → 𝑁 ∈ ℤ ) |
30 |
|
elfz |
⊢ ( ( ( 𝐽 − 𝐾 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐽 − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑀 ≤ ( 𝐽 − 𝐾 ) ∧ ( 𝐽 − 𝐾 ) ≤ 𝑁 ) ) ) |
31 |
27 28 29 30
|
syl3anc |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( 𝐽 − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑀 ≤ ( 𝐽 − 𝐾 ) ∧ ( 𝐽 − 𝐾 ) ≤ 𝑁 ) ) ) |
32 |
16 25 31
|
3bitr4d |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐾 ∈ ( ( 𝐽 − 𝑁 ) ... ( 𝐽 − 𝑀 ) ) ↔ ( 𝐽 − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) ) |