Step |
Hyp |
Ref |
Expression |
1 |
|
elfzelz |
⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑥 ∈ ℤ ) |
2 |
1
|
zred |
⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑥 ∈ ℝ ) |
3 |
|
eluzel2 |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝐾 ∈ ℤ ) |
4 |
3
|
adantl |
⊢ ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐾 ∈ ℤ ) |
5 |
4
|
zred |
⊢ ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐾 ∈ ℝ ) |
6 |
|
lelttric |
⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝑥 ≤ 𝐾 ∨ 𝐾 < 𝑥 ) ) |
7 |
2 5 6
|
syl2anr |
⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑥 ≤ 𝐾 ∨ 𝐾 < 𝑥 ) ) |
8 |
|
elfzuz |
⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
9 |
|
elfz5 |
⊢ ( ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ℤ ) → ( 𝑥 ∈ ( 𝑀 ... 𝐾 ) ↔ 𝑥 ≤ 𝐾 ) ) |
10 |
8 4 9
|
syl2anr |
⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 ... 𝐾 ) ↔ 𝑥 ≤ 𝐾 ) ) |
11 |
|
simpl |
⊢ ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) |
12 |
|
eluzelz |
⊢ ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 + 1 ) ∈ ℤ ) |
13 |
11 12
|
syl |
⊢ ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝐾 + 1 ) ∈ ℤ ) |
14 |
|
eluz |
⊢ ( ( ( 𝐾 + 1 ) ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝑥 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ↔ ( 𝐾 + 1 ) ≤ 𝑥 ) ) |
15 |
13 1 14
|
syl2an |
⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑥 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ↔ ( 𝐾 + 1 ) ≤ 𝑥 ) ) |
16 |
|
elfzuz3 |
⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) ) |
17 |
16
|
adantl |
⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) ) |
18 |
|
elfzuzb |
⊢ ( 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ↔ ( 𝑥 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) ) ) |
19 |
18
|
rbaib |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) → ( 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ↔ 𝑥 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ) ) |
20 |
17 19
|
syl |
⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ↔ 𝑥 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ) ) |
21 |
|
zltp1le |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝐾 < 𝑥 ↔ ( 𝐾 + 1 ) ≤ 𝑥 ) ) |
22 |
4 1 21
|
syl2an |
⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐾 < 𝑥 ↔ ( 𝐾 + 1 ) ≤ 𝑥 ) ) |
23 |
15 20 22
|
3bitr4d |
⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ↔ 𝐾 < 𝑥 ) ) |
24 |
10 23
|
orbi12d |
⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑥 ∈ ( 𝑀 ... 𝐾 ) ∨ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) ↔ ( 𝑥 ≤ 𝐾 ∨ 𝐾 < 𝑥 ) ) ) |
25 |
7 24
|
mpbird |
⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 ... 𝐾 ) ∨ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) ) |
26 |
|
elfzuz |
⊢ ( 𝑥 ∈ ( 𝑀 ... 𝐾 ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
27 |
26
|
adantl |
⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝐾 ) ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
28 |
|
simpr |
⊢ ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) |
29 |
|
elfzuz3 |
⊢ ( 𝑥 ∈ ( 𝑀 ... 𝐾 ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑥 ) ) |
30 |
|
uztrn |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑥 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) ) |
31 |
28 29 30
|
syl2an |
⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝐾 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) ) |
32 |
|
elfzuzb |
⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) ) ) |
33 |
27 31 32
|
sylanbrc |
⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝐾 ) ) → 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) |
34 |
|
elfzuz |
⊢ ( 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) → 𝑥 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ) |
35 |
|
uztrn |
⊢ ( ( 𝑥 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ∧ ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
36 |
34 11 35
|
syl2anr |
⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
37 |
|
elfzuz3 |
⊢ ( 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) ) |
38 |
37
|
adantl |
⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) ) |
39 |
36 38 32
|
sylanbrc |
⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) |
40 |
33 39
|
jaodan |
⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝑀 ... 𝐾 ) ∨ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) ) → 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) |
41 |
25 40
|
impbida |
⊢ ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑥 ∈ ( 𝑀 ... 𝐾 ) ∨ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) ) ) |
42 |
|
elun |
⊢ ( 𝑥 ∈ ( ( 𝑀 ... 𝐾 ) ∪ ( ( 𝐾 + 1 ) ... 𝑁 ) ) ↔ ( 𝑥 ∈ ( 𝑀 ... 𝐾 ) ∨ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) ) |
43 |
41 42
|
bitr4di |
⊢ ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑥 ∈ ( ( 𝑀 ... 𝐾 ) ∪ ( ( 𝐾 + 1 ) ... 𝑁 ) ) ) ) |
44 |
43
|
eqrdv |
⊢ ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... 𝐾 ) ∪ ( ( 𝐾 + 1 ) ... 𝑁 ) ) ) |