Step |
Hyp |
Ref |
Expression |
1 |
|
2nn0 |
|- 2 e. NN0 |
2 |
|
4nn0 |
|- 4 e. NN0 |
3 |
|
2re |
|- 2 e. RR |
4 |
|
4re |
|- 4 e. RR |
5 |
|
2lt4 |
|- 2 < 4 |
6 |
3 4 5
|
ltleii |
|- 2 <_ 4 |
7 |
|
elfz2nn0 |
|- ( 2 e. ( 0 ... 4 ) <-> ( 2 e. NN0 /\ 4 e. NN0 /\ 2 <_ 4 ) ) |
8 |
1 2 6 7
|
mpbir3an |
|- 2 e. ( 0 ... 4 ) |
9 |
|
fzosplit |
|- ( 2 e. ( 0 ... 4 ) -> ( 0 ..^ 4 ) = ( ( 0 ..^ 2 ) u. ( 2 ..^ 4 ) ) ) |
10 |
8 9
|
ax-mp |
|- ( 0 ..^ 4 ) = ( ( 0 ..^ 2 ) u. ( 2 ..^ 4 ) ) |
11 |
|
fzo0to2pr |
|- ( 0 ..^ 2 ) = { 0 , 1 } |
12 |
|
4z |
|- 4 e. ZZ |
13 |
|
fzoval |
|- ( 4 e. ZZ -> ( 2 ..^ 4 ) = ( 2 ... ( 4 - 1 ) ) ) |
14 |
12 13
|
ax-mp |
|- ( 2 ..^ 4 ) = ( 2 ... ( 4 - 1 ) ) |
15 |
|
4m1e3 |
|- ( 4 - 1 ) = 3 |
16 |
|
df-3 |
|- 3 = ( 2 + 1 ) |
17 |
15 16
|
eqtri |
|- ( 4 - 1 ) = ( 2 + 1 ) |
18 |
17
|
oveq2i |
|- ( 2 ... ( 4 - 1 ) ) = ( 2 ... ( 2 + 1 ) ) |
19 |
|
2z |
|- 2 e. ZZ |
20 |
|
fzpr |
|- ( 2 e. ZZ -> ( 2 ... ( 2 + 1 ) ) = { 2 , ( 2 + 1 ) } ) |
21 |
19 20
|
ax-mp |
|- ( 2 ... ( 2 + 1 ) ) = { 2 , ( 2 + 1 ) } |
22 |
18 21
|
eqtri |
|- ( 2 ... ( 4 - 1 ) ) = { 2 , ( 2 + 1 ) } |
23 |
|
2p1e3 |
|- ( 2 + 1 ) = 3 |
24 |
23
|
preq2i |
|- { 2 , ( 2 + 1 ) } = { 2 , 3 } |
25 |
14 22 24
|
3eqtri |
|- ( 2 ..^ 4 ) = { 2 , 3 } |
26 |
11 25
|
uneq12i |
|- ( ( 0 ..^ 2 ) u. ( 2 ..^ 4 ) ) = ( { 0 , 1 } u. { 2 , 3 } ) |
27 |
10 26
|
eqtri |
|- ( 0 ..^ 4 ) = ( { 0 , 1 } u. { 2 , 3 } ) |