Step |
Hyp |
Ref |
Expression |
1 |
|
elfzelz |
|- ( x e. ( M ... N ) -> x e. ZZ ) |
2 |
1
|
zred |
|- ( x e. ( M ... N ) -> x e. RR ) |
3 |
|
eluzel2 |
|- ( N e. ( ZZ>= ` K ) -> K e. ZZ ) |
4 |
3
|
adantl |
|- ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) -> K e. ZZ ) |
5 |
4
|
zred |
|- ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) -> K e. RR ) |
6 |
|
lelttric |
|- ( ( x e. RR /\ K e. RR ) -> ( x <_ K \/ K < x ) ) |
7 |
2 5 6
|
syl2anr |
|- ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... N ) ) -> ( x <_ K \/ K < x ) ) |
8 |
|
elfzuz |
|- ( x e. ( M ... N ) -> x e. ( ZZ>= ` M ) ) |
9 |
|
elfz5 |
|- ( ( x e. ( ZZ>= ` M ) /\ K e. ZZ ) -> ( x e. ( M ... K ) <-> x <_ K ) ) |
10 |
8 4 9
|
syl2anr |
|- ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... N ) ) -> ( x e. ( M ... K ) <-> x <_ K ) ) |
11 |
|
simpl |
|- ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) -> ( K + 1 ) e. ( ZZ>= ` M ) ) |
12 |
|
eluzelz |
|- ( ( K + 1 ) e. ( ZZ>= ` M ) -> ( K + 1 ) e. ZZ ) |
13 |
11 12
|
syl |
|- ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) -> ( K + 1 ) e. ZZ ) |
14 |
|
eluz |
|- ( ( ( K + 1 ) e. ZZ /\ x e. ZZ ) -> ( x e. ( ZZ>= ` ( K + 1 ) ) <-> ( K + 1 ) <_ x ) ) |
15 |
13 1 14
|
syl2an |
|- ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... N ) ) -> ( x e. ( ZZ>= ` ( K + 1 ) ) <-> ( K + 1 ) <_ x ) ) |
16 |
|
elfzuz3 |
|- ( x e. ( M ... N ) -> N e. ( ZZ>= ` x ) ) |
17 |
16
|
adantl |
|- ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... N ) ) -> N e. ( ZZ>= ` x ) ) |
18 |
|
elfzuzb |
|- ( x e. ( ( K + 1 ) ... N ) <-> ( x e. ( ZZ>= ` ( K + 1 ) ) /\ N e. ( ZZ>= ` x ) ) ) |
19 |
18
|
rbaib |
|- ( N e. ( ZZ>= ` x ) -> ( x e. ( ( K + 1 ) ... N ) <-> x e. ( ZZ>= ` ( K + 1 ) ) ) ) |
20 |
17 19
|
syl |
|- ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... N ) ) -> ( x e. ( ( K + 1 ) ... N ) <-> x e. ( ZZ>= ` ( K + 1 ) ) ) ) |
21 |
|
zltp1le |
|- ( ( K e. ZZ /\ x e. ZZ ) -> ( K < x <-> ( K + 1 ) <_ x ) ) |
22 |
4 1 21
|
syl2an |
|- ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... N ) ) -> ( K < x <-> ( K + 1 ) <_ x ) ) |
23 |
15 20 22
|
3bitr4d |
|- ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... N ) ) -> ( x e. ( ( K + 1 ) ... N ) <-> K < x ) ) |
24 |
10 23
|
orbi12d |
|- ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... N ) ) -> ( ( x e. ( M ... K ) \/ x e. ( ( K + 1 ) ... N ) ) <-> ( x <_ K \/ K < x ) ) ) |
25 |
7 24
|
mpbird |
|- ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... N ) ) -> ( x e. ( M ... K ) \/ x e. ( ( K + 1 ) ... N ) ) ) |
26 |
|
elfzuz |
|- ( x e. ( M ... K ) -> x e. ( ZZ>= ` M ) ) |
27 |
26
|
adantl |
|- ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... K ) ) -> x e. ( ZZ>= ` M ) ) |
28 |
|
simpr |
|- ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) -> N e. ( ZZ>= ` K ) ) |
29 |
|
elfzuz3 |
|- ( x e. ( M ... K ) -> K e. ( ZZ>= ` x ) ) |
30 |
|
uztrn |
|- ( ( N e. ( ZZ>= ` K ) /\ K e. ( ZZ>= ` x ) ) -> N e. ( ZZ>= ` x ) ) |
31 |
28 29 30
|
syl2an |
|- ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... K ) ) -> N e. ( ZZ>= ` x ) ) |
32 |
|
elfzuzb |
|- ( x e. ( M ... N ) <-> ( x e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` x ) ) ) |
33 |
27 31 32
|
sylanbrc |
|- ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( M ... K ) ) -> x e. ( M ... N ) ) |
34 |
|
elfzuz |
|- ( x e. ( ( K + 1 ) ... N ) -> x e. ( ZZ>= ` ( K + 1 ) ) ) |
35 |
|
uztrn |
|- ( ( x e. ( ZZ>= ` ( K + 1 ) ) /\ ( K + 1 ) e. ( ZZ>= ` M ) ) -> x e. ( ZZ>= ` M ) ) |
36 |
34 11 35
|
syl2anr |
|- ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( ( K + 1 ) ... N ) ) -> x e. ( ZZ>= ` M ) ) |
37 |
|
elfzuz3 |
|- ( x e. ( ( K + 1 ) ... N ) -> N e. ( ZZ>= ` x ) ) |
38 |
37
|
adantl |
|- ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( ( K + 1 ) ... N ) ) -> N e. ( ZZ>= ` x ) ) |
39 |
36 38 32
|
sylanbrc |
|- ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ x e. ( ( K + 1 ) ... N ) ) -> x e. ( M ... N ) ) |
40 |
33 39
|
jaodan |
|- ( ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) /\ ( x e. ( M ... K ) \/ x e. ( ( K + 1 ) ... N ) ) ) -> x e. ( M ... N ) ) |
41 |
25 40
|
impbida |
|- ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) -> ( x e. ( M ... N ) <-> ( x e. ( M ... K ) \/ x e. ( ( K + 1 ) ... N ) ) ) ) |
42 |
|
elun |
|- ( x e. ( ( M ... K ) u. ( ( K + 1 ) ... N ) ) <-> ( x e. ( M ... K ) \/ x e. ( ( K + 1 ) ... N ) ) ) |
43 |
41 42
|
bitr4di |
|- ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) -> ( x e. ( M ... N ) <-> x e. ( ( M ... K ) u. ( ( K + 1 ) ... N ) ) ) ) |
44 |
43
|
eqrdv |
|- ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) -> ( M ... N ) = ( ( M ... K ) u. ( ( K + 1 ) ... N ) ) ) |