Step | Hyp | Ref
| Expression |
1 | | elfzelz 8660 |
. . . . . 6
⊢ (x ∈ (𝑀...𝑁) → x ∈
ℤ) |
2 | | eluzel2 8254 |
. . . . . . 7
⊢ (𝑁 ∈ (ℤ≥‘𝐾) → 𝐾 ∈
ℤ) |
3 | 2 | adantl 262 |
. . . . . 6
⊢ (((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝐾 ∈
ℤ) |
4 | | zlelttric 8066 |
. . . . . 6
⊢
((x ∈ ℤ ∧ 𝐾 ∈ ℤ) → (x ≤ 𝐾 ∨ 𝐾 < x)) |
5 | 1, 3, 4 | syl2anr 274 |
. . . . 5
⊢ ((((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧
x ∈
(𝑀...𝑁)) → (x ≤ 𝐾 ∨ 𝐾 < x)) |
6 | | elfzuz 8656 |
. . . . . . 7
⊢ (x ∈ (𝑀...𝑁) → x ∈
(ℤ≥‘𝑀)) |
7 | | elfz5 8652 |
. . . . . . 7
⊢
((x ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → (x ∈ (𝑀...𝐾) ↔ x ≤ 𝐾)) |
8 | 6, 3, 7 | syl2anr 274 |
. . . . . 6
⊢ ((((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧
x ∈
(𝑀...𝑁)) → (x ∈ (𝑀...𝐾) ↔ x ≤ 𝐾)) |
9 | | simpl 102 |
. . . . . . . . 9
⊢ (((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → (𝐾 + 1) ∈
(ℤ≥‘𝑀)) |
10 | | eluzelz 8258 |
. . . . . . . . 9
⊢ ((𝐾 + 1) ∈ (ℤ≥‘𝑀) → (𝐾 + 1) ∈
ℤ) |
11 | 9, 10 | syl 14 |
. . . . . . . 8
⊢ (((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → (𝐾 + 1) ∈
ℤ) |
12 | | eluz 8262 |
. . . . . . . 8
⊢ (((𝐾 + 1) ∈ ℤ ∧
x ∈
ℤ) → (x ∈ (ℤ≥‘(𝐾 + 1)) ↔ (𝐾 + 1) ≤ x)) |
13 | 11, 1, 12 | syl2an 273 |
. . . . . . 7
⊢ ((((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧
x ∈
(𝑀...𝑁)) → (x ∈
(ℤ≥‘(𝐾 + 1)) ↔ (𝐾 + 1) ≤ x)) |
14 | | elfzuz3 8657 |
. . . . . . . . 9
⊢ (x ∈ (𝑀...𝑁) → 𝑁 ∈
(ℤ≥‘x)) |
15 | 14 | adantl 262 |
. . . . . . . 8
⊢ ((((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧
x ∈
(𝑀...𝑁)) → 𝑁 ∈
(ℤ≥‘x)) |
16 | | elfzuzb 8654 |
. . . . . . . . 9
⊢ (x ∈ ((𝐾 + 1)...𝑁) ↔ (x ∈
(ℤ≥‘(𝐾 + 1)) ∧
𝑁 ∈ (ℤ≥‘x))) |
17 | 16 | rbaib 829 |
. . . . . . . 8
⊢ (𝑁 ∈ (ℤ≥‘x) → (x
∈ ((𝐾 + 1)...𝑁) ↔ x ∈
(ℤ≥‘(𝐾 + 1)))) |
18 | 15, 17 | syl 14 |
. . . . . . 7
⊢ ((((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧
x ∈
(𝑀...𝑁)) → (x ∈ ((𝐾 + 1)...𝑁) ↔ x ∈
(ℤ≥‘(𝐾 + 1)))) |
19 | | zltp1le 8074 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℤ ∧
x ∈
ℤ) → (𝐾 <
x ↔ (𝐾 + 1) ≤ x)) |
20 | 3, 1, 19 | syl2an 273 |
. . . . . . 7
⊢ ((((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧
x ∈
(𝑀...𝑁)) → (𝐾 < x
↔ (𝐾 + 1) ≤
x)) |
21 | 13, 18, 20 | 3bitr4d 209 |
. . . . . 6
⊢ ((((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧
x ∈
(𝑀...𝑁)) → (x ∈ ((𝐾 + 1)...𝑁) ↔ 𝐾 < x)) |
22 | 8, 21 | orbi12d 706 |
. . . . 5
⊢ ((((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧
x ∈
(𝑀...𝑁)) → ((x ∈ (𝑀...𝐾) ∨
x ∈
((𝐾 + 1)...𝑁)) ↔ (x ≤ 𝐾 ∨ 𝐾 < x))) |
23 | 5, 22 | mpbird 156 |
. . . 4
⊢ ((((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧
x ∈
(𝑀...𝑁)) → (x ∈ (𝑀...𝐾) ∨
x ∈
((𝐾 + 1)...𝑁))) |
24 | | elfzuz 8656 |
. . . . . . 7
⊢ (x ∈ (𝑀...𝐾) → x ∈
(ℤ≥‘𝑀)) |
25 | 24 | adantl 262 |
. . . . . 6
⊢ ((((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧
x ∈
(𝑀...𝐾)) → x ∈
(ℤ≥‘𝑀)) |
26 | | simpr 103 |
. . . . . . 7
⊢ (((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝑁 ∈
(ℤ≥‘𝐾)) |
27 | | elfzuz3 8657 |
. . . . . . 7
⊢ (x ∈ (𝑀...𝐾) → 𝐾 ∈
(ℤ≥‘x)) |
28 | | uztrn 8265 |
. . . . . . 7
⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘x)) → 𝑁 ∈
(ℤ≥‘x)) |
29 | 26, 27, 28 | syl2an 273 |
. . . . . 6
⊢ ((((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧
x ∈
(𝑀...𝐾)) → 𝑁 ∈
(ℤ≥‘x)) |
30 | | elfzuzb 8654 |
. . . . . 6
⊢ (x ∈ (𝑀...𝑁) ↔ (x ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘x))) |
31 | 25, 29, 30 | sylanbrc 394 |
. . . . 5
⊢ ((((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧
x ∈
(𝑀...𝐾)) → x ∈ (𝑀...𝑁)) |
32 | | elfzuz 8656 |
. . . . . . 7
⊢ (x ∈ ((𝐾 + 1)...𝑁) → x ∈
(ℤ≥‘(𝐾 + 1))) |
33 | | uztrn 8265 |
. . . . . . 7
⊢
((x ∈ (ℤ≥‘(𝐾 + 1)) ∧
(𝐾 + 1) ∈ (ℤ≥‘𝑀)) → x ∈
(ℤ≥‘𝑀)) |
34 | 32, 9, 33 | syl2anr 274 |
. . . . . 6
⊢ ((((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧
x ∈
((𝐾 + 1)...𝑁)) → x ∈
(ℤ≥‘𝑀)) |
35 | | elfzuz3 8657 |
. . . . . . 7
⊢ (x ∈ ((𝐾 + 1)...𝑁) → 𝑁 ∈
(ℤ≥‘x)) |
36 | 35 | adantl 262 |
. . . . . 6
⊢ ((((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧
x ∈
((𝐾 + 1)...𝑁)) → 𝑁 ∈
(ℤ≥‘x)) |
37 | 34, 36, 30 | sylanbrc 394 |
. . . . 5
⊢ ((((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧
x ∈
((𝐾 + 1)...𝑁)) → x ∈ (𝑀...𝑁)) |
38 | 31, 37 | jaodan 709 |
. . . 4
⊢ ((((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧
(x ∈
(𝑀...𝐾) ∨
x ∈
((𝐾 + 1)...𝑁))) → x ∈ (𝑀...𝑁)) |
39 | 23, 38 | impbida 528 |
. . 3
⊢ (((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → (x ∈ (𝑀...𝑁) ↔ (x ∈ (𝑀...𝐾) ∨
x ∈
((𝐾 + 1)...𝑁)))) |
40 | | elun 3078 |
. . 3
⊢ (x ∈ ((𝑀...𝐾) ∪ ((𝐾 + 1)...𝑁)) ↔ (x ∈ (𝑀...𝐾) ∨
x ∈
((𝐾 + 1)...𝑁))) |
41 | 39, 40 | syl6bbr 187 |
. 2
⊢ (((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → (x ∈ (𝑀...𝑁) ↔ x ∈ ((𝑀...𝐾) ∪ ((𝐾 + 1)...𝑁)))) |
42 | 41 | eqrdv 2035 |
1
⊢ (((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → (𝑀...𝑁) = ((𝑀...𝐾) ∪ ((𝐾 + 1)...𝑁))) |