Step | Hyp | Ref
| Expression |
1 | | elfzelz 13256 |
. . . . . . 7
⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℤ) |
2 | 1 | zred 12426 |
. . . . . 6
⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℝ) |
3 | | eluzel2 12587 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝐾) → 𝐾 ∈ ℤ) |
4 | 3 | adantl 482 |
. . . . . . 7
⊢ (((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝐾 ∈ ℤ) |
5 | 4 | zred 12426 |
. . . . . 6
⊢ (((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝐾 ∈ ℝ) |
6 | | lelttric 11082 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (𝑥 ≤ 𝐾 ∨ 𝐾 < 𝑥)) |
7 | 2, 5, 6 | syl2anr 597 |
. . . . 5
⊢ ((((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑥 ≤ 𝐾 ∨ 𝐾 < 𝑥)) |
8 | | elfzuz 13252 |
. . . . . . 7
⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ (ℤ≥‘𝑀)) |
9 | | elfz5 13248 |
. . . . . . 7
⊢ ((𝑥 ∈
(ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → (𝑥 ∈ (𝑀...𝐾) ↔ 𝑥 ≤ 𝐾)) |
10 | 8, 4, 9 | syl2anr 597 |
. . . . . 6
⊢ ((((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑥 ∈ (𝑀...𝐾) ↔ 𝑥 ≤ 𝐾)) |
11 | | simpl 483 |
. . . . . . . . 9
⊢ (((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → (𝐾 + 1) ∈
(ℤ≥‘𝑀)) |
12 | | eluzelz 12592 |
. . . . . . . . 9
⊢ ((𝐾 + 1) ∈
(ℤ≥‘𝑀) → (𝐾 + 1) ∈ ℤ) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
⊢ (((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → (𝐾 + 1) ∈ ℤ) |
14 | | eluz 12596 |
. . . . . . . 8
⊢ (((𝐾 + 1) ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝑥 ∈
(ℤ≥‘(𝐾 + 1)) ↔ (𝐾 + 1) ≤ 𝑥)) |
15 | 13, 1, 14 | syl2an 596 |
. . . . . . 7
⊢ ((((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑥 ∈ (ℤ≥‘(𝐾 + 1)) ↔ (𝐾 + 1) ≤ 𝑥)) |
16 | | elfzuz3 13253 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝑥)) |
17 | 16 | adantl 482 |
. . . . . . . 8
⊢ ((((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑁 ∈ (ℤ≥‘𝑥)) |
18 | | elfzuzb 13250 |
. . . . . . . . 9
⊢ (𝑥 ∈ ((𝐾 + 1)...𝑁) ↔ (𝑥 ∈ (ℤ≥‘(𝐾 + 1)) ∧ 𝑁 ∈ (ℤ≥‘𝑥))) |
19 | 18 | rbaib 539 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑥) → (𝑥 ∈ ((𝐾 + 1)...𝑁) ↔ 𝑥 ∈ (ℤ≥‘(𝐾 + 1)))) |
20 | 17, 19 | syl 17 |
. . . . . . 7
⊢ ((((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑥 ∈ ((𝐾 + 1)...𝑁) ↔ 𝑥 ∈ (ℤ≥‘(𝐾 + 1)))) |
21 | | zltp1le 12370 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝐾 < 𝑥 ↔ (𝐾 + 1) ≤ 𝑥)) |
22 | 4, 1, 21 | syl2an 596 |
. . . . . . 7
⊢ ((((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐾 < 𝑥 ↔ (𝐾 + 1) ≤ 𝑥)) |
23 | 15, 20, 22 | 3bitr4d 311 |
. . . . . 6
⊢ ((((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑥 ∈ ((𝐾 + 1)...𝑁) ↔ 𝐾 < 𝑥)) |
24 | 10, 23 | orbi12d 916 |
. . . . 5
⊢ ((((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝑥 ∈ (𝑀...𝐾) ∨ 𝑥 ∈ ((𝐾 + 1)...𝑁)) ↔ (𝑥 ≤ 𝐾 ∨ 𝐾 < 𝑥))) |
25 | 7, 24 | mpbird 256 |
. . . 4
⊢ ((((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑥 ∈ (𝑀...𝐾) ∨ 𝑥 ∈ ((𝐾 + 1)...𝑁))) |
26 | | elfzuz 13252 |
. . . . . . 7
⊢ (𝑥 ∈ (𝑀...𝐾) → 𝑥 ∈ (ℤ≥‘𝑀)) |
27 | 26 | adantl 482 |
. . . . . 6
⊢ ((((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧ 𝑥 ∈ (𝑀...𝐾)) → 𝑥 ∈ (ℤ≥‘𝑀)) |
28 | | simpr 485 |
. . . . . . 7
⊢ (((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝑁 ∈ (ℤ≥‘𝐾)) |
29 | | elfzuz3 13253 |
. . . . . . 7
⊢ (𝑥 ∈ (𝑀...𝐾) → 𝐾 ∈ (ℤ≥‘𝑥)) |
30 | | uztrn 12600 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑥)) → 𝑁 ∈ (ℤ≥‘𝑥)) |
31 | 28, 29, 30 | syl2an 596 |
. . . . . 6
⊢ ((((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧ 𝑥 ∈ (𝑀...𝐾)) → 𝑁 ∈ (ℤ≥‘𝑥)) |
32 | | elfzuzb 13250 |
. . . . . 6
⊢ (𝑥 ∈ (𝑀...𝑁) ↔ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑥))) |
33 | 27, 31, 32 | sylanbrc 583 |
. . . . 5
⊢ ((((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧ 𝑥 ∈ (𝑀...𝐾)) → 𝑥 ∈ (𝑀...𝑁)) |
34 | | elfzuz 13252 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝐾 + 1)...𝑁) → 𝑥 ∈ (ℤ≥‘(𝐾 + 1))) |
35 | | uztrn 12600 |
. . . . . . 7
⊢ ((𝑥 ∈
(ℤ≥‘(𝐾 + 1)) ∧ (𝐾 + 1) ∈
(ℤ≥‘𝑀)) → 𝑥 ∈ (ℤ≥‘𝑀)) |
36 | 34, 11, 35 | syl2anr 597 |
. . . . . 6
⊢ ((((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧ 𝑥 ∈ ((𝐾 + 1)...𝑁)) → 𝑥 ∈ (ℤ≥‘𝑀)) |
37 | | elfzuz3 13253 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝐾 + 1)...𝑁) → 𝑁 ∈ (ℤ≥‘𝑥)) |
38 | 37 | adantl 482 |
. . . . . 6
⊢ ((((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧ 𝑥 ∈ ((𝐾 + 1)...𝑁)) → 𝑁 ∈ (ℤ≥‘𝑥)) |
39 | 36, 38, 32 | sylanbrc 583 |
. . . . 5
⊢ ((((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧ 𝑥 ∈ ((𝐾 + 1)...𝑁)) → 𝑥 ∈ (𝑀...𝑁)) |
40 | 33, 39 | jaodan 955 |
. . . 4
⊢ ((((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ∧ (𝑥 ∈ (𝑀...𝐾) ∨ 𝑥 ∈ ((𝐾 + 1)...𝑁))) → 𝑥 ∈ (𝑀...𝑁)) |
41 | 25, 40 | impbida 798 |
. . 3
⊢ (((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → (𝑥 ∈ (𝑀...𝑁) ↔ (𝑥 ∈ (𝑀...𝐾) ∨ 𝑥 ∈ ((𝐾 + 1)...𝑁)))) |
42 | | elun 4083 |
. . 3
⊢ (𝑥 ∈ ((𝑀...𝐾) ∪ ((𝐾 + 1)...𝑁)) ↔ (𝑥 ∈ (𝑀...𝐾) ∨ 𝑥 ∈ ((𝐾 + 1)...𝑁))) |
43 | 41, 42 | bitr4di 289 |
. 2
⊢ (((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → (𝑥 ∈ (𝑀...𝑁) ↔ 𝑥 ∈ ((𝑀...𝐾) ∪ ((𝐾 + 1)...𝑁)))) |
44 | 43 | eqrdv 2736 |
1
⊢ (((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → (𝑀...𝑁) = ((𝑀...𝐾) ∪ ((𝐾 + 1)...𝑁))) |