Proof of Theorem fzrev
Step | Hyp | Ref
| Expression |
1 | | ancom 461 |
. . 3
⊢ (((𝐽 − 𝐾) ≤ 𝑁 ∧ 𝑀 ≤ (𝐽 − 𝐾)) ↔ (𝑀 ≤ (𝐽 − 𝐾) ∧ (𝐽 − 𝐾) ≤ 𝑁)) |
2 | | zre 11974 |
. . . . . . . 8
⊢ (𝐽 ∈ ℤ → 𝐽 ∈
ℝ) |
3 | | zre 11974 |
. . . . . . . 8
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℝ) |
4 | | zre 11974 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
5 | | suble 11107 |
. . . . . . . 8
⊢ ((𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝐽 − 𝐾) ≤ 𝑁 ↔ (𝐽 − 𝑁) ≤ 𝐾)) |
6 | 2, 3, 4, 5 | syl3an 1152 |
. . . . . . 7
⊢ ((𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐽 − 𝐾) ≤ 𝑁 ↔ (𝐽 − 𝑁) ≤ 𝐾)) |
7 | 6 | 3comr 1117 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝐽 − 𝐾) ≤ 𝑁 ↔ (𝐽 − 𝑁) ≤ 𝐾)) |
8 | 7 | 3expb 1112 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → ((𝐽 − 𝐾) ≤ 𝑁 ↔ (𝐽 − 𝑁) ≤ 𝐾)) |
9 | 8 | adantll 710 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → ((𝐽 − 𝐾) ≤ 𝑁 ↔ (𝐽 − 𝑁) ≤ 𝐾)) |
10 | | zre 11974 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
11 | | lesub 11108 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (𝑀 ≤ (𝐽 − 𝐾) ↔ 𝐾 ≤ (𝐽 − 𝑀))) |
12 | 10, 2, 3, 11 | syl3an 1152 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ≤ (𝐽 − 𝐾) ↔ 𝐾 ≤ (𝐽 − 𝑀))) |
13 | 12 | 3expb 1112 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝑀 ≤ (𝐽 − 𝐾) ↔ 𝐾 ≤ (𝐽 − 𝑀))) |
14 | 13 | adantlr 711 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝑀 ≤ (𝐽 − 𝐾) ↔ 𝐾 ≤ (𝐽 − 𝑀))) |
15 | 9, 14 | anbi12d 630 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) →
(((𝐽 − 𝐾) ≤ 𝑁 ∧ 𝑀 ≤ (𝐽 − 𝐾)) ↔ ((𝐽 − 𝑁) ≤ 𝐾 ∧ 𝐾 ≤ (𝐽 − 𝑀)))) |
16 | 1, 15 | syl5rbbr 287 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) →
(((𝐽 − 𝑁) ≤ 𝐾 ∧ 𝐾 ≤ (𝐽 − 𝑀)) ↔ (𝑀 ≤ (𝐽 − 𝐾) ∧ (𝐽 − 𝐾) ≤ 𝑁))) |
17 | | simprr 769 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → 𝐾 ∈
ℤ) |
18 | | zsubcl 12013 |
. . . . 5
⊢ ((𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐽 − 𝑁) ∈ ℤ) |
19 | 18 | ancoms 459 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ) → (𝐽 − 𝑁) ∈ ℤ) |
20 | 19 | ad2ant2lr 744 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐽 − 𝑁) ∈ ℤ) |
21 | | zsubcl 12013 |
. . . . 5
⊢ ((𝐽 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐽 − 𝑀) ∈ ℤ) |
22 | 21 | ancoms 459 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝐽 ∈ ℤ) → (𝐽 − 𝑀) ∈ ℤ) |
23 | 22 | ad2ant2r 743 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐽 − 𝑀) ∈ ℤ) |
24 | | elfz 12888 |
. . 3
⊢ ((𝐾 ∈ ℤ ∧ (𝐽 − 𝑁) ∈ ℤ ∧ (𝐽 − 𝑀) ∈ ℤ) → (𝐾 ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀)) ↔ ((𝐽 − 𝑁) ≤ 𝐾 ∧ 𝐾 ≤ (𝐽 − 𝑀)))) |
25 | 17, 20, 23, 24 | syl3anc 1363 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐾 ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀)) ↔ ((𝐽 − 𝑁) ≤ 𝐾 ∧ 𝐾 ≤ (𝐽 − 𝑀)))) |
26 | | zsubcl 12013 |
. . . 4
⊢ ((𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐽 − 𝐾) ∈ ℤ) |
27 | 26 | adantl 482 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐽 − 𝐾) ∈ ℤ) |
28 | | simpll 763 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → 𝑀 ∈
ℤ) |
29 | | simplr 765 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → 𝑁 ∈
ℤ) |
30 | | elfz 12888 |
. . 3
⊢ (((𝐽 − 𝐾) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐽 − 𝐾) ∈ (𝑀...𝑁) ↔ (𝑀 ≤ (𝐽 − 𝐾) ∧ (𝐽 − 𝐾) ≤ 𝑁))) |
31 | 27, 28, 29, 30 | syl3anc 1363 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → ((𝐽 − 𝐾) ∈ (𝑀...𝑁) ↔ (𝑀 ≤ (𝐽 − 𝐾) ∧ (𝐽 − 𝐾) ≤ 𝑁))) |
32 | 16, 25, 31 | 3bitr4d 312 |
1
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐾 ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀)) ↔ (𝐽 − 𝐾) ∈ (𝑀...𝑁))) |